Report Number: CS-TR-88-1210
Institution: Stanford University, Department of Computer Science
Title: String-Functional Semantics for Formal Verification of Synchronous Circuits
Author: Bronstein, Alexandre
Author: Talcott, Carolyn L.
Date: June 1988
Abstract: 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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/88/1210/CS-TR-88-1210.pdf