Model Checker Front-end System Design And Implementation

The principal validation methods for complex systems are simulation, emulation and testing. These methods usually involve providing certain inputs and observing the corresponding outputs. These methods can be an efficient way to find many errors. However, for many complex designs, checking all of possible interaction and potential pitfalls using simulation and testing techniques is rarely possible.A very attractive and increasingly appealing alternative to simulation and testing is the approach of model checking which is discussed in this paper. The model checking is an approach of formal verification, ensuring the correctness of the design. The model checking problem is described as follows. Given a Kripke structure M={S, R, L} that represents a concurrent system and a temporal formula f expressing some desired specification, find the set of all states in S that satisfy f:{s∈S| M, s|=f}.The model checker cannot directly verify the design which should be changed into the finite state machine. To solve this problem, in this paper, the front-end of the model checker has been analyzed. Two programs have been designed for extracting finite state machine from Verilog HDL. Each of these programs plays a role of compiler: VL2BLIF and BLIF2FSM. VL2BLIF compiles Verilog HDL to BLIF-MV, while BLIF2FSM compiles BLIF-MV to finite state machine represented by binary decision diagrams.The main results are as follows:1. The syntax and semantics of Verilog HDL are analyzed by Lex&yacc.2. The state transition relations and the statements in Verilog programs are studied in detail, and the updating for reg variables are also discussed.3. Both state transition relation and relations between multiple-variables in BLIF-MV are investigated.4. The finite state machine in BLIF-MV is represented by binary decision diagrams which are analyzed so that the memory of Boolean functions can be reduced.