Abstract

Microelectronics systems become more and more complex, making the detection of errors extremely difficult. Model checking, as a formal hardware verification technique, can potentially catch subtle hardware design errors. It is used to automatically verify temporal properties on finite state systems. However, model checking tools suffer from the state explosion problem; when the number of states representing the program under verification grows exponentially. state explosion problem. The main idea of model reduction is to suppress the techniques that involve both approaches can greatly reduce the design under techniques in which, variables not influencing the property's variables are removed and the values domains of state variables in the system model are values according to their dependency to the property to be verified. After the above procedures are done, the state space of the reduced program is smaller than that of the original one, while the correctness of the properties are preserved. We have developed a tool called SynAbs which accepts a subset of the Verilog hardware description language and universally quantified computation tree logic (CTL) temporal properties, and generates a reduced Verilog code which can be fed into a CTL model checker. We have successfully applied our tool on the verification of a number of simple Verilog programs.