Using Synchronized Transitions for Simulation and Timing Verification

Synchronized Transitions is a formal notation for hardware specification, verification, and simulation. This paper describes the use of Synchronized Transistions in the design of a chip for high bandwidth interprocessor communication. The chip uses a hybrid of synchronous and self-timed circuit techniques; a proof is presented that all timing requirements are satisfied. The Synchronized Transistions notation is presented, and it is shown how programs can be translated into logic predicates, providing a basis for formal verification. The use of Synchronized Transistions in the simulation of the chip is described, and the design choices of using both simulation and formal proofs are discussed.

Keywords: Formal hardware verification, invariants, real-time systems, self-timed circuits, simulation, timing verification.