Automatic Verification of Timed Circuits

This paper presents a new formalism and a new algorithm for verifying timed circuits. The formalism, called orbital nets, allows hierarchical verification based on abehavioralsemantics of timed tracetheory. We present improvements to a geometric timing algorithm that take advantage of concurrency by using partial orders to reduce the time and space requirements of verification. This algorithm has been fully automated and incorporated into a design system for timed circuits, and experimental results demonstrate that this verification algorithm is practical for realistic examples.

• Type: Conference
• Year: 1994
• Where: CAV
• Authors: Tomas Rokicki, Chris J. Myers
• Keywords: Algorithm, CAV 1994, Geometric Timing Algorithm, Hardware, Verification Algorithm