Digital Circuits as Moore Machines

TL;DR

This work addresses how to specify real-time, compositional behavior of digital circuits without hardware-description languages by modeling circuits as Moore machines driven by input event sequences. It develops a formal framework using $\epsilon$, $w$, and the $\mathit{held}$ function to track input durations, alongside a fixed propagation delay $n$ to define gate behavior, demonstrated on a bus, NAND gate, and an SR latch built from NAND gates. A key contribution is the constructive proof that cross-coupled NANDs yield an SR latch with latency bound $3n+3$, and the use of concurrent-state-machine composition to model circuit interconnections. The approach enables refined timing analysis (e.g., via hysteresis and stability predicates) and offers a language-free, automata-theoretic perspective on timing, correctness, and composability of digital designs.

Abstract

This paper illustrates a technique for specifying the timing, logical operation, and compositional circuit design of digital circuits in terms of ordinary state machines with output (Moore machines). The method is illustrated here with specifications of gates, latches, and other simple circuits and via the construction of devices starting with a SR latch built from gates. The method is based on "classical" automata and recursive functions on strings (sequential functions).