380
M. Mann and C. Barrett
5 Experimental Results
We developed a prototype flow for proving the POR and RIS conditions and
applying the necessary constraints. We use the IC3/PDR implementation in
ABC [11], pdr, to prove condition (6) (which implies condition (2)). This requires
manually writing a Verilog property for each atomic instruction.
4 We implemented the ProveRIS algorithm in our SMT-based model checker, CoSA [26],
configured with boolector [29] on the smtcomp19 branch, using CaDiCaL [4] as
the underlying SAT solver.
5 We check the commuting diagram for condition (3)
in CoSA as well. It tries the trivial guard true by default, and allows the user
to provide additional candidate guards if necessary. The set up for proofs in
CoSA is automated based on user-provided annotations for the actions and enable conditions. We show our best results which used an encoding leveraging the
SMT theory of arrays to represent memories for proving conditions, and a pure
bitvector encoding for bounded model checking.
Our flow applies the following steps: i) read in a system description in Verilog
using Yosys [38] and generate AIGER [7] for ABC (or BTOR2 [29] for other
tools); ii) check condition (6) for each atomic instruction; iii) run the ProveRIS
algorithm, and if it returns true, add constraints to rule out all but atomic
instructions; and iv) check POR condition (3) for each pair of atomic instructions
and add constraints for each passing pair of instructions with the associated
guard. Each step depends on the previous step passing successfully. In each of
our experiments described below, we successfully completed every step of this
flow, though in some cases guards were required in step (iv). For POR and RIS
runtimes, we always include the time to check the conditions. We tried running
with POR alone, but it resulted in negligible improvements in runtime and thus
we omit these results. This demonstrates the importance of RIS. We ran all
experiments on a 3.5GHz Intel Xeon CPU with 16GB of RAM.
5.1 Motivating Example
First, we return to our motivating example. We compare the time to reach
the bug using the SAT-based ABC [11] engines pdr and bmc, and SMT-based
bounded model checking using btormc [29] and CoSA. We ran the SMT-based
model checkers both with and without the SMT theory of arrays for the encoding
of the memory. Both btormc and CoSA without the array encoding were able to
reach the bug in 1230s and 1437s, respectively, but all other approaches timed
out at two hours. In particular, pdr times out at 2 hours on the property, but can
4 This could be automated based on user-tagged actions and user-provided enable
conditions.
5 GitHub Commit Hashes for Tools:
Boolector/Btormc: 1989080261235f33e344cbd095e70a337c45bd16
CoSA: ff3c8cee1f0834c03167b2a8ecdd1223031312b3
PySMT: 09dc303185812149550110123ad266326beb1179
Yosys: a4b59de5d48a89ba5e1b46eb44877a91ceb6fa44
ABC: 5776ad07e7247993976bffed4802a5737c456782
M. Mann and C. Barrett
5 Experimental Results
We developed a prototype flow for proving the POR and RIS conditions and
applying the necessary constraints. We use the IC3/PDR implementation in
ABC [11], pdr, to prove condition (6) (which implies condition (2)). This requires
manually writing a Verilog property for each atomic instruction.
4 We implemented the ProveRIS algorithm in our SMT-based model checker, CoSA [26],
configured with boolector [29] on the smtcomp19 branch, using CaDiCaL [4] as
the underlying SAT solver.
5 We check the commuting diagram for condition (3)
in CoSA as well. It tries the trivial guard true by default, and allows the user
to provide additional candidate guards if necessary. The set up for proofs in
CoSA is automated based on user-provided annotations for the actions and enable conditions. We show our best results which used an encoding leveraging the
SMT theory of arrays to represent memories for proving conditions, and a pure
bitvector encoding for bounded model checking.
Our flow applies the following steps: i) read in a system description in Verilog
using Yosys [38] and generate AIGER [7] for ABC (or BTOR2 [29] for other
tools); ii) check condition (6) for each atomic instruction; iii) run the ProveRIS
algorithm, and if it returns true, add constraints to rule out all but atomic
instructions; and iv) check POR condition (3) for each pair of atomic instructions
and add constraints for each passing pair of instructions with the associated
guard. Each step depends on the previous step passing successfully. In each of
our experiments described below, we successfully completed every step of this
flow, though in some cases guards were required in step (iv). For POR and RIS
runtimes, we always include the time to check the conditions. We tried running
with POR alone, but it resulted in negligible improvements in runtime and thus
we omit these results. This demonstrates the importance of RIS. We ran all
experiments on a 3.5GHz Intel Xeon CPU with 16GB of RAM.
5.1 Motivating Example
First, we return to our motivating example. We compare the time to reach
the bug using the SAT-based ABC [11] engines pdr and bmc, and SMT-based
bounded model checking using btormc [29] and CoSA. We ran the SMT-based
model checkers both with and without the SMT theory of arrays for the encoding
of the memory. Both btormc and CoSA without the array encoding were able to
reach the bug in 1230s and 1437s, respectively, but all other approaches timed
out at two hours. In particular, pdr times out at 2 hours on the property, but can
4 This could be automated based on user-tagged actions and user-provided enable
conditions.
5 GitHub Commit Hashes for Tools:
Boolector/Btormc: 1989080261235f33e344cbd095e70a337c45bd16
CoSA: ff3c8cee1f0834c03167b2a8ecdd1223031312b3
PySMT: 09dc303185812149550110123ad266326beb1179
Yosys: a4b59de5d48a89ba5e1b46eb44877a91ceb6fa44
ABC: 5776ad07e7247993976bffed4802a5737c456782