Improving the Quality of Bounded Model Checking by Means of Coverage Estimation

Formal verification has become an important step in circuit and system design. A prominent technique is Bounded Model Checking (BMC) which is widely used in industry. In BMC it is checked if certain properties hold for the design. But even if all properties could be successfully verified, it is difficult to determine if the properties cover the entire functional behavior of the circuit. Recently, a new approach for estimating coverage in BMC has been presented that can easily be integrated in existing BMC tools. In this paper we give experimental results on the application of the technique to the block-level verification of a RISC CPU. The experiments show that the costs for coverage estimation are comparable to the verification costs. Furthermore it is demonstrated how the technique can be applied to achieve full coverage on a higher level. As an example, we investigate the instruction set verification of a RISC CPU.