Property checking based on hierarchical integer

This article describes a high level model of digital circuits for application of formal verification properties at this level. In our method, a behavioral state machine is represented by a multiplexer based structure of linear integer equations, and RT level properties are directly applied. It reduces the need for large BDD data structures and uses far less memory. Furthermore, there is no need to separate the data and control sections in circuits. We used a canonical form of linear TED as stated in M. Ciesielski et al. (2002). This paper compares our results with those of the VIS verification tool which is a BDD based program. Also run it on gate level designs.