Reads a state transition system and performs property checking
(also known as Averroes v2.0)
Copyright (c) 2016 - Present Aman Goel ([email protected]) and Karem Sakallah ([email protected]) , University of Michigan
Reads a state transition system and performs property checking using equality abstraction
src/
./build.sh
from the avr folder to install all dependencies and compile the source code with default options. AVR binaries are generated in the folder build/bin/
python3 avr.py -o <output-path> -n <test-name> <path>/<file>.btor2
(check the output in <output-path>/work_<test-name>)
Example: python3 avr.py -o foo -n bar examples/btor2/counter.btor2
(check the output in foo/work_bar)
Use AVR Proof Race to automatically run multiple configurations in parallel
python3 avr_pr.py -o <output-path> -n <test-name> <path>/<file>.btor2
(check the output in <output-path>/pr_<test-name>)
Example: python3 avr_pr.py -o foo -n bar examples/btor2/counter.btor2
(check the output in foo/pr_bar)
AVR creates a directory <output-path>
/pr_<test-name>
which contains results, statistics and logs relating to the run
<output-path>
└── pr_<test-name>
├── <test-name>.btor2 [BTOR2 input file]
├── result.pr [result: h for safe, v for unsafe, f_* for timeout / memout / error]
├── cex.witness [witness in BTOR2 format (if property is proved unsafe)]
├── inv.txt [inductive invariant proof (if property is proved safe)]
├── <test-name>.results [statistics file]
├── design.smt2 [input design in VMT format]
├── inv.smt2 [inductive invariant proof in VMT format (if property is proved safe)]
└── work_w<i>/ [worker <i> log directory]
As a quick summary relating to the run, AVR produces certain key information as output.
For example, running python3 avr_pr.py examples/btor2/counter.btor2
produces the following output:
@ 0s (starting avr proof race)
@ 0s (output dir: output/pr_test)
@ 0s (max 5 workers)
@ 0s (started worker 0 with pid 13366)
@ 0s (started worker 1 with pid 13368)
@ 0s (started worker 2 with pid 13370)
@ 0s (spawned 3 workers)
@ 0s (total 3 workers using 37 MB)
@ 0s (worker 0 finished with result safe) python3 avr.py
@ 0s (worker 0 output)
(output dir: output/pr_test/work_w0)
(frontend: btor2)
(property: all (1 assertions))
(4 / 4 flops initialized)
(abstraction: sa+uf)
1 : 0 : 0 s: 0 0s
2 : 1 : 0 0 s: 0 0s
2 : 1 : 0 0 s: 0 0s
Result Time Mem. #Refs
sec MB
h 0.01 15 2
@ 0s (stopping all workers)
@ 0s (proof race finished with answer safe in 0.19 seconds)
@ 0s (copied results from worker 0 in output/pr_test)
":" separated numbers indicate the following:
<# of refinements learnt> : <max frame> : <# of added clauses in each frame> s: <total # of clauses learnt>
Result can be mapped as follows:
h -> Property holds (safe) [inv.txt contains the inductive invariant proof]
v -> Property violated (unsafe) [cex.witness contains the counterexample]
f_* -> Time or memory limit exceeded / error
Copyright (c) 2016 - Present Aman Goel and Karem Sakallah, University of Michigan. All rights reserved.
AVR is provided as is, without any warranty. Any usage of AVR needs to comply with the usage terms as detailed in the file LICENSE.
BACKEND_*
flag in src/reach/reach_backend.h
to change solver backends for different kinds of SMT queries.BACKEND_*
flags in src/reach/reach_backend.h
(rename build/bin/
folder every time), and customize proof race workers in workers.txt
(by changing --bin <binary-path>
) to run proof race with different SMT solver configurations.<test-name>.results
. Here is an incomplete and somewhat outdated description on these statistics: link to spreadsheet../build.sh
to install Yosys
<output-path>
(default: output) and <test-name>
(default: test) can be customized using command-line options -o
and -n
in avr_pr.py
).property
is a reserved keyword.<prop-name>
in the avr.py
. The option tries finding a signal named *<prop-name>
in the design as property and discards all other assertions (if a match is found).We would be glad to hear from you and help you in the case you are having a difficulty in using AVR Please report bugs and share your usage experience via email ([email protected]) or on github (https://github.com/aman-goel/avr)