High-level symbolic simulation using integer equations

The Taylor expansion diagram (TED) has been recently introduced as a compact and canonical representation for arithmetic functions with finite Taylor series. It can represent Boolean logic interacting with arithmetic functions canonically. One of the main disadvantages of TED is that relations must be bit expanded to be represented in TED. This paper represents a method for high-level symbolic simulation and property checking based on integer equations. Functionality of design is represented in conditional TED (CTED), which is our enhancement of TED to represent relations without bit expansion. This way, a more compact structure is achieved for high-level designs, containing control path statements like if and case. The symbolic simulator is used for high-level property checking. Properties are in the form of assertions, and support integer equality and inequalities as well as Boolean equations. We have implemented our symbolic simulator for Verilog. It contains the CTED package with all necessary operations.