Synthesis engine based on equivalence checking
Yongjiang Lu · Journal of Circuits and Systems · 2007
This paper describes a synthesis engine based on equivalence checking. It synthesizes RTL description into netlist. Because equivalence checking is designed to check the correctness of automatic synthesis from RTL to netlist, correctness is also the key point, which is concerned in this paper. At the same time, a series ways of keeping the similarity of circuits are proposed, which can improve the efficiency of checking engine. Finally experimental results on FORMALITY, a formal verification tool of SYNOPSYS, prove the efficiency of this system.