Digitale Schaltkreise können mit Hilfe logischer Formeln beschrieben werden, wobei man der Einfachheit halber annehmen kann, dass sich der Zustand eines Schaltkreises vollständig durch boolesche Variablen beschreiben lässt. Das bedeutet, dass alle für den Schaltkreis relevanten Elemente entweder durch Variablen mit den Werten null oder eins beschrieben werden können.
Bei synchron arbeitenden Schaltkreisen werden die Ausgabewerte aller Register innerhalb des Schaltkreises sowie die Belegungen der primären Eingänge des Schaltkreises betrachtet.
Bei asynchron arbeitenden Schaltkreisen müssen normalerweise die Belegungen aller Leitungen innerhalb des Schaltkreises betrachtet und modelliert werden.
Der Zustand des Schaltkreises kann eindeutig beschrieben werden, wenn die Belegung der Variablen bekannt ist. Diese Beschreibung kann mit Hilfe eines booleschen Ausdrucks (Logik erster Ordnung) erfolgen, der alle zum System gehörigen Variablen enthält und in dem beschriebenen Zustand wahr ist.