SynAbs: model reduction tool for Verilog verification

Current model checking tools suffer from the state space explosion problem due to the large number of generated states. In general, approaches like compositional verification and model reduction are used to tackle this problem. In this paper, we present a model reduction tool, called SynAbs, for Verilog verification. The reduction algorithms implemented are based on syntactic analysis and are applied prior to model checking. We have tested the efficiency of the algorithms using small examples. We have achieved reduction in both space and time requirements.