BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-88-1210
       ENTRY:: April 24, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: String-Functional Semantics for Formal Verification of
               Synchronous Circuits
        TYPE:: Technical Report
      AUTHOR:: Bronstein, Alexandre
      AUTHOR:: Talcott, Carolyn L.
        DATE:: June 1988
       PAGES:: 64
    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.
       NOTES:: [Adminitrivia V1/Prg/19950424]
         END:: STAN//CS-TR-88-1210