414
A. Goel and K. Sakallah
2 Motivation
Consider a predicate p := (a + b < 1) defined over two 32-bit variables a and
b. An equivalent propositional-level representation of p will involve a bit-blasted
expression involving 64 Boolean variables and several hundred clauses. As a
consequence, bit-level model checking algorithms do not scale as variable bit
widths increase and suffer from the so-called state-space explosion problem [26].
AVR derives its motivation from the fact that the word-level representation
of a problem contains useful high-level information that can be exploited for
better scalability. Building on our previous work [33,34], AVR uses this insight
to infer an implicit syntax-guided abstraction using terms built from objects
present in the word-level syntactic description of the problem (like a, b, 1, +,
<). The approach can be further combined with data abstraction using uninterpreted functions [20,11] to simplify reasoning for the underlying query solver.
This, coupled with efficient SMT solving, allows for an effective word-level model
checking algorithm that can scale better than bit-level engines for a variety of
verification problems. Moreover, the underlying induction-based verification procedure has the unique strength of producing word-level proof certificates that
are useful in a variety of applications [32,37,45,44].
3 System Architecture
9HULORJ
YLD
YLD0DWK6DW
%725
YLD%WRU7RROV
3UHSURFHVVRU
VLPSOHRSWLPL]DWLRQV
SURSHUW\GLUHFWHGVSOLWWLQJ
%RROHFWRU
%9$UUD\V
0DWK6$7
8)%9/,$$UUD\V
LQWHUSRODWLRQ
=
8)%9/,$
IXWXUHH[WHQVLRQV
3URRI
5DFH
0XOWL
(QJLQH
:UDSSHU
)URQWHQGV
6076ROYHU
%DFNHQGV
8WLOLWLHV 8WLOLWLHV
VPWVWDWVGRW
&HUWLILFDWH &HUWLILFDWH
SURRIVPWFH[ZLWQHVV
8VHU,QSXW 8VHU ,QSXW
YYPWEWRU
$95&RUH
,&6$
LQFUHPHQWDOUHILQHPHQW
LQFUHPHQWDOFDFKLQJ
H[WUDFWFRQFDWKDQGOHU
)HDWXUHV
H[WUDFWFRQFDWKDQGOHU
GDWDDEVWUDFWLRQ
LQWHUSRODWLRQ
ERXQGHGPRGHOFKHFNLQJ
$GGRQV
ERXQGHGPRGHOFKHFNLQJ
FHUWLILFDWHSULQWHU
GRWYLVXDOL]HU
8WLOLWLHV
UHH[WHQVLRQV
TXDQWLILHUIUHH
Fig. 1: Verification flow with AVR
UF: uninterpreted functions, BV: bit-vectors, LIA: linear integer arithmetic
Fig. 1 shows the architecture and verification flow of AVR.
Frontends in AVR extract the model checking problem from inputs in different
formats using openly-available tools.
– Verilog + SystemVerilog Assertions [9] (using Yosys [55])
– VMT [8]
(using MathSAT 5 [24])
– BTOR2 [51]
(using Btor2Tools [3])
A. Goel and K. Sakallah
2 Motivation
Consider a predicate p := (a + b < 1) defined over two 32-bit variables a and
b. An equivalent propositional-level representation of p will involve a bit-blasted
expression involving 64 Boolean variables and several hundred clauses. As a
consequence, bit-level model checking algorithms do not scale as variable bit
widths increase and suffer from the so-called state-space explosion problem [26].
AVR derives its motivation from the fact that the word-level representation
of a problem contains useful high-level information that can be exploited for
better scalability. Building on our previous work [33,34], AVR uses this insight
to infer an implicit syntax-guided abstraction using terms built from objects
present in the word-level syntactic description of the problem (like a, b, 1, +,
<). The approach can be further combined with data abstraction using uninterpreted functions [20,11] to simplify reasoning for the underlying query solver.
This, coupled with efficient SMT solving, allows for an effective word-level model
checking algorithm that can scale better than bit-level engines for a variety of
verification problems. Moreover, the underlying induction-based verification procedure has the unique strength of producing word-level proof certificates that
are useful in a variety of applications [32,37,45,44].
3 System Architecture
9HULORJ
YLD
YLD0DWK6DW
%725
YLD%WRU7RROV
3UHSURFHVVRU
VLPSOHRSWLPL]DWLRQV
SURSHUW\GLUHFWHGVSOLWWLQJ
%RROHFWRU
%9$UUD\V
0DWK6$7
8)%9/,$$UUD\V
LQWHUSRODWLRQ
=
8)%9/,$
IXWXUHH[WHQVLRQV
3URRI
5DFH
0XOWL
(QJLQH
:UDSSHU
)URQWHQGV
6076ROYHU
%DFNHQGV
8WLOLWLHV 8WLOLWLHV
VPWVWDWVGRW
&HUWLILFDWH &HUWLILFDWH
SURRIVPWFH[ZLWQHVV
8VHU,QSXW 8VHU ,QSXW
YYPWEWRU
$95&RUH
,&6$
LQFUHPHQWDOUHILQHPHQW
LQFUHPHQWDOFDFKLQJ
H[WUDFWFRQFDWKDQGOHU
)HDWXUHV
H[WUDFWFRQFDWKDQGOHU
GDWDDEVWUDFWLRQ
LQWHUSRODWLRQ
ERXQGHGPRGHOFKHFNLQJ
$GGRQV
ERXQGHGPRGHOFKHFNLQJ
FHUWLILFDWHSULQWHU
GRWYLVXDOL]HU
8WLOLWLHV
UHH[WHQVLRQV
TXDQWLILHUIUHH
Fig. 1: Verification flow with AVR
UF: uninterpreted functions, BV: bit-vectors, LIA: linear integer arithmetic
Fig. 1 shows the architecture and verification flow of AVR.
Frontends in AVR extract the model checking problem from inputs in different
formats using openly-available tools.
– Verilog + SystemVerilog Assertions [9] (using Yosys [55])
– VMT [8]
(using MathSAT 5 [24])
– BTOR2 [51]
(using Btor2Tools [3])