Identifying a Subset of System Verilog Assertions for Efficient Bounded Model Checking

Integrating design and verification becomes more and more important due to the increasing complexity of today´s circuits and systems. SystemVerilog is a description language that embeds verification goals with the help of SystemVerilog assertions (SVAs). Often SVAs are used in simulation-based verification. But in the past first applications in formal verification have been considered, too. In this paper we present an approach to prove SVAs by induction based bounded model checking (BMC). Since checking SVAs is computationally very complex, we define a subset which is sufficient for many practical purposes. For each restriction a rationale is given.The creation of the BMC instance for this subset is explained in detail. Case studies show the application of our approach.