Verilog Transformation for an RTL SAT Solver in Formal Verification

This paper presents a new method automatically translating the Verilog model to an RTL circuit model which can be used in a state-of-the-art finite-domain satisfiability solver EHSAT to check the verified properties. Different methods are used in the transformations of different data types and expressions of Verilog model. Effective backfilling technology is applied in the processes of if...else and case blocks. Experimental results show that this method can make the transformation effective.