Yet more image computations for SMV, the symbolic model verifier
Hiromi Hiraishi · Systems and Computers in Japan · 2000
This paper describes a collection of techniques to improve the efficiency of the pre- and postimage computations that are the core of the Symbolic Model Verifier (SMV), which is used for formal logic design verification. The proposed techniques aim mostly at improving the efficiency of the verification of asynchronous processes. The improvements are mainly made by (1) the early elimination of process variables in the postimage computations, (2) the application of the conjunctive partitioning technique to the verification of asynchronous processes, (3) the early substitution of the stable state variables, and (4) the nondeterministic substitution method for the preimage computations. The experimental measurements show that the proposed techniques are very effective and result in a speedup of up to 50 times compared to the original SMV. © 2000 Scripta Technica, Syst Comp Jpn, 31(9): 1–9, 2000