A New High Level Model Based on Integer Equations to Check CTL Properties in VHDL Environment

Abstract:- This paper describes the use of integer equations for high level modeling of digital circuits for rule-based formal verification at this level. BDD operations are not applicable to a large datapath because of large CPU time and memory usage. In our method, a behavioral state machine is represented by a list of integer equations, and RT level properties are directly applied to this representation. Furthermore, this method is applied to circuits without having to separate their data and control sections. For this implementation, we use a canonical form of integer equations, which simplifies equations instead of solving them. This paper compares our results with those of the VIS verification tool that is a BDD based program