TY - GEN
T1 - Improving the quality of bounded model checking by means of coverage estimation
AU - Kühne, Ulrich
AU - Große, Daniel
AU - Drechsler, Rolf
PY - 2007/11/28
Y1 - 2007/11/28
N2 - 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.
AB - 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.
U2 - 10.1109/ISVLSI.2007.57
DO - 10.1109/ISVLSI.2007.57
M3 - Conference contribution
AN - SCOPUS:36348988347
SN - 0769528961
SN - 9780769528960
T3 - Proceedings - IEEE Computer Society Annual Symposium on VLSI: Emerging VLSI Technologies and Architectures
SP - 165
EP - 170
BT - Proceedings - IEEE Computer Society Annual Symposium on VLSI
T2 - IEEE Computer Society Annual Symposium on VLSI: Emerging VLSI Technologies and Architectures, ISVLSI'07
Y2 - 9 March 2007 through 11 March 2007
ER -