| Abstract |
|
Retiming combined with combinational optimization is a power-ful sequential synthesis method. However, this methodology has not found wide application because formal sequential verification is not practical and current simulation methodology requires the cor-respondence of latches disallowing any movement of latches. We present a practical verification technique which permits such se-quential synthesis for a class of circuits. In particular, we require certain constraints to be met on the feedback paths of the latches involved in the retiming process. For a general circuit, we can sat-isfy these constraints by fixing the location of some latches, e.g., by making them observable. We show that equivalence checking after performing repeated retiming and synthesis on this class of circuit reduces to a combinational verification problem. We also demonstrate that our methodology covers a large class of circuits by applying it to a set of benchmarks and industrial designs.
|
 Additional Information
|
Citation:
Rajeev K. Ranjan, Vigyan Singhal, Fabio Somenzi, Robert K. Brayton,
"Using Combinational Verification for Sequential Circuits,"
date,
p. 138,
Design, Automation and Test in Europe (DATE '99),
1999
|
