Sciweavers

Share
ISVLSI
2007
IEEE

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

10 years 9 months ago
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.
Ulrich Kühne, Daniel Große, Rolf Drechs
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where ISVLSI
Authors Ulrich Kühne, Daniel Große, Rolf Drechsler
Comments (0)
books