Scalable and scalably-verifiable sequential synthesis

This paper describes an efficient implementation of sequential synthesis 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 sequentially verifiable using an independent inductive prover similar to that used for synthesis, with guaranteed completeness. Experiments with this sequential synthesis show effectiveness. When applied to a set of 20 industrial benchmarks ranging up to 26 K registers and up to 53 K 6 -LUTs, average reductions in register and area are 12.9% and 13.1% respectively while delay is reduced by 1.4%. When applied to the largest academic benchmarks, an average reduction in both registers and area is more than 30%. The associated sequential verification is also scalable and runs about 2times slower than synthesis. The implementation is available in the synthesis and verification system ABC.