aman-goel / avr Goto Github PK

View Code? Open in Web Editor NEW

73.0 4.0 20.0 931.36 MB

Reads a state transition system and performs property checking

License: GNU General Public License v3.0

Python 0.49% Shell 0.19% Verilog 32.00% SystemVerilog 1.68% Makefile 0.09% C++ 65.52% C 0.03% Dockerfile 0.01%

model-checking formal-verification verilog ic3 pdr

avr's People

Stargazers

Watchers

Forkers

madebymars zzephaniahh psychedel fanhy2114 jankcorn will62794 log-when mgudemann fengwz17 dh73 nianzelee zengyingchao mrwater98 adamzsofi balp-jbt gipsyh cyanokobalamyne xdddduo

avr's Issues

Add Dockerfile/Docker compose

Hi,

It was not clear from the readme, what distributions avr works on, but I saw dependencies are installed with apt.

I am not sure how active this tool/repository is, but I propose the addition of a really simple dockerfile to make the tool easier to try locally. I attached the dockerfile and docker-compose I used, usage is the following:

(have docker and docker-compose set up on your machine)
docker-compose up -d
docker exec -it avr-docker-avr-1 bash
run ./build.sh manually, as it is interactive
use the examples in this repository or put any input files into the input_files directory besides the docker files, it will be available under /app/input_files
use avr

It is a simple container that could be improved in many ways, but it works. Maybe it will be useful for somebody else as well.

docker-compose.yml.txt
Dockerfile.txt
(remove .txt extension from both files)

Assertion failed when using Boolector as backend solver

Version: dbc3371
Environment: Ubuntu 22.04 (Linux kernel 6.5.0-17-generic)
Command line: /avr.py --bmc --bin ./build/bin-boolector --timeout 900 --memout 15000 counter_v.btor2.txt
- AVR was compiled with Boolector, and binaries are put under ./build/bin-boolector/
- Input file counter_v.btor2.txt attached
Result

Copyright (c) 2016 - Present  Aman Goel and Karem Sakallah, University of Michigan
	(output dir: output/work_test)
	(frontend: btor2)
	(property: all (1 assertions))
	(problem size: 4 bits)
	(abstraction: sa+uf)
reach: reach_bt.cpp:1178: virtual void _bt::bt_API::assert_distinct_constants(): Assertion `0' failed.

Compile Error

passes/sat/freduce.cc:457:55: error: ‘numeric_limits’ is not a member of ‘std’

g++ (Ubuntu 13.2.0-4ubuntu3) 13.2.0

Error in Python3.12

Traceback (most recent call last):
  File "/root/avr/./avr.py", line 18, in <module>
    from distutils import spawn
ModuleNotFoundError: No module named 'distutils'

Assertion failure for some btor models

for example for

https://github.com/makaimann/btor-benchmarks/blob/master/data-integrity/unsafe/btor2/arbitrated_top_n2_w16_d64_e0.btor2

I get

Copyright (c) 2016 - Present  Aman Goel and Karem Sakallah, University of Michigan            
        (output dir: output/work_test)                                                        
        (frontend: btor2)                                                                     
        (property: all (1 assertions))                                                        
        (problem size: 2131 bits)                                                             
        (abstraction: sa+uf)                                                                  
   0    : 0     : 0 s: 0    0s                                                                
   11   : 1     : 0 7 s: 7    0s                                                                                                                                                            
   2254 : 2     : 0 12 276 s: 288    102s                                                     
   2263 : 3     : 0 13 158 128 s: 299    103s                  reach: reach_coi.cpp:1163: bool reach::Reach::allowed_relation(Inst*, Inst*, OpInst::OpType): Assertion `opt != OpInst::Eq' f
ailed.                                         
   2263 : 3     : 0 13 159 128 s: 300    103s                                                 
      Result        Time        Mem.       #Refs                                              
                     sec          MB                                                          
       f_err      103.24         534        2263

The same error appears for other models from this benchmark, too.

Assertion failed when using MathSAT as backend solver

Version: dbc3371
Environment: Ubuntu 22.04 (Linux kernel 6.5.0-17-generic)
Command line: ./avr.py --bmc --bin ./build/bin-mathsat5 --timeout 900 --memout 15000 counter_v.btor2.txt
- AVR was compiled with MathSAT, and binaries are put under ./build/bin-mathsat5/
- Input file counter_v.btor2.txt attached
Result

Copyright (c) 2016 - Present  Aman Goel and Karem Sakallah, University of Michigan
	(output dir: output/work_test)
	(frontend: btor2)
	(property: all (1 assertions))
	(problem size: 4 bits)
	(abstraction: sa+uf)
  0s	(bmc: safe till step 0)
	(bmc: abstract mode disabled at step 1)
  0s	(bmc: safe till step 5)
  0s	(bmc: safe till step 10)
reach: reach_m5.cpp:1315: virtual int _m5::m5_API::s_check(long int, bool): Assertion `!MSAT_ERROR_MODEL(*m_model)' failed.

g++: error: ......No such file or directory

There is a bug here showing No such file or directory

Two small btor2 files that seem trigger bugs

We have verified the syntactic correctness of these cases with btro2tools/catbtor.
We use the following command to run AVR:

python3 avr.py -n tmp -o tmp ${BTOR2_FILE}

Case 1

1 sort bitvec 4
2 constd 1 -7
3 const 1 0110
4 state 1 bv2_4
5 sub 1 3 4
6 sort bitvec 5
7 constd 6 -11
8 slice 1 7 4 1
9 rol 1 5 8
10 const 1 0000
11 consth 1 0
12 ror 1 10 11
13 state 1 bv0_4
14 init 1 13 12
15 sort bitvec 1
16 const 15 0
17 rol 1 4 11
18 ite 1 16 4 17
19 nor 1 18 4
20 next 1 13 19
21 state 1 bv1_4
22 init 1 21 9
23 input 1 input1_4
24 neg 1 23
25 sort bitvec 3
26 input 25
27 sext 1 26 1
28 srem 1 24 27
29 next 1 21 28
30 init 1 4 2
31 input 1 input0_4
32 next 1 4 31
33 ror 1 13 21
34 and 1 33 33
35 and 1 13 21
36 sdiv 1 35 31
37 slte 15 34 36
38 bad 37

corresponding error message:

avr_word_netlist.cpp:912: static Inst* OpInst::create(OpInst::OpType, InstL, int, bool, Inst*, SORT): Assertion ‘0’ failed.

Case 2

1 sort bitvec 7
2 sort bitvec 4
3 const 2 1010
4 constd 2 -8
5 inc 2 4
6 ror 2 3 5
7 uext 1 6 3
8 state 1 bv2_7
9 neg 1 8
10 sort bitvec 6
11 zero 10
12 sext 1 11 1
13 state 1 bv0_7
14 sll 1 12 13
15 init 1 13 9
16 state 1 bv1_7
17 dec 1 16
18 consth 1 01
19 smod 1 13 18
20 srl 1 17 19
21 neg 1 20
22 next 1 13 21
23 init 1 16 14
24 and 1 8 13
25 next 1 16 24
26 init 1 8 7
27 sort bitvec 8
28 input 2 input1_4
29 sext 27 28 4
30 slice 1 29 6 0
31 next 1 8 30
32 sort bitvec 1
33 const 32 1
34 neg 32 33
35 sra 1 13 13
36 add 1 13 13
37 ult 32 35 36
38 neq 32 34 37
39 bad 38

corresponding error message:

reach: reach_y2.cpp:7367: void _y2::y2_API::inst2yices(Inst*, bool): Assertion ‘0’ failed.

Could you please help to confirm if these are bugs of AVR, or we didn't build AVR properly? (or some reasons else~~

Wrong path for libbtor2parser.a in reach's Makefile

Line 40 of ./src/reach/Makefile should be

BT_LIB += $(BT_DIR)/deps/btor2tools/build/lib/libbtor2parser.a

instead of

BT_LIB += $(BT_DIR)/deps/btor2tools/build/libbtor2parser.a

aman-goel / avr Goto Github PK

avr's People

Stargazers

Watchers

Forkers

avr's Issues

Add Dockerfile/Docker compose

Assertion failed when using Boolector as backend solver

Compile Error

Error in Python3.12

Assertion failure for some btor models

Assertion failed when using MathSAT as backend solver

g++: error: ......No such file or directory

Two small btor2 files that seem trigger bugs

Case 1

Case 2

Wrong path for libbtor2parser.a in reach's Makefile

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent