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.