Modular Synthesis and Verification of Timed Circuits Using Automatic Abstraction
Abstract
In order to increase performance, circuit designers are beginning to use more aggressive timed circuit designs instead of traditional synchronous static logic designs. Recent design examples have shown that signi cant performance gains are achieved when these aggressive circuit styles are used. Correct operation of these aggressive circuit styles is critically dependent on timing, and in industry they are typically designed by hand. To synthesize and verify timed circuits, the reachable state space of the circuit under the timing constraints needs to be explored. However, complete state space exploration is an exponential problem. State space explosion limits timed circuit designs to small sizes.
Type
