Scalable and scalably-verifiable sequential synthesis

This paper describes an efficient implementation of an effective sequential synthesis operation that uses induction to detect and merge sequentially-equivalent nodes. State-encoding, scan chains, and test vectors are essentially preserved. Moreover, the sequential synthesis results are guaranteed to be sequentially verifiable against the original circuits. Verification can use an independent inductive prover similar to that used for synthesis, with guaranteed completeness and with experimental runtimes close to that of synthesis. Experiments with this form of sequential synthesis show surprising effectiveness; when applied to the largest academic benchmarks, an average reduction in both registers and area of more than 30% is obtained; on a set of 50 industrial benchmarks ranging in size from 100 to 20K registers an average reduction of 32% in registers and 15% in area is obtained while preserving delay. The geometric means for the runtimes for synthesis and sequential verification on ...

• Type: Conference
• Year: 2008
• Where: ICCAD
• Authors: Alan Mishchenko, Michael L. Case, Robert K. Brayton, Stephen Jang
• Keywords: Average Reduction, Effective Sequential Synthesis, Hardware, ICCAD 2008, Sequential Verification