摘要: A new functional semantics is proposed for synchronous circuits, as a basis for reasoning formally about that class of hardware systems. Technically, we define an extensional semantics with monotonic length-preserving functions on... 展开 A new functional semantics is proposed for synchronous circuits, as a basis for reasoning formally about that class of hardware systems. Technically, we define an extensional semantics with monotonic length-preserving functions on finite strings, and an intensional semantics based on functionals on those functions. As support for the semantics we prove the equivalence of the extensional semantics with a simple operational semantics, as well as a characterization of circuits which obey the every loop is clocked design rule. Also, we develop the foundations in complete detail both to increase confidence in the theory, and as a prerequisite to its future mechanization. (rrh) 收起