Open lighteningfingers opened 5 years ago
Do you know which version of suprove you are using? It seems to work with the one I have installed:
SBY 14:39:49 [MCVE] Removing direcory 'MCVE'.
SBY 14:39:49 [MCVE] Copy 'MCVE.sv' to 'MCVE/src/MCVE.sv'.
SBY 14:39:49 [MCVE] engine_0: aiger suprove
SBY 14:39:49 [MCVE] nomem: starting process "cd MCVE/src; yosys -ql ../model/design_nomem.log ../model/design_nomem.ys"
SBY 14:39:50 [MCVE] nomem: finished (returncode=0)
SBY 14:39:50 [MCVE] aig: starting process "cd MCVE/model; yosys -ql design_aiger.log design_aiger.ys"
SBY 14:39:50 [MCVE] aig: finished (returncode=0)
SBY 14:39:50 [MCVE] engine_0: starting process "cd MCVE; suprove model/design_aiger.aig"
SBY 14:39:50 [MCVE] engine_0: finished (returncode=0)
SBY 14:39:50 [MCVE] engine_0: Status returned by engine: FAIL
SBY 14:39:50 [MCVE] base: starting process "cd MCVE/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:39:50 [MCVE] base: finished (returncode=0)
SBY 14:39:50 [MCVE] smt2: starting process "cd MCVE/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 14:39:50 [MCVE] smt2: finished (returncode=0)
SBY 14:39:50 [MCVE] engine_0: starting process "cd MCVE; yosys-smtbmc -s yices --noprogress --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc --aig model/design_aiger.aim:engine_0/trace.aiw model/design_smt2.smt2"
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Solver: yices
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Skipping step 0 (and assuming pass)..
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Skipping step 1 (and assuming pass)..
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Skipping step 2 (and assuming pass)..
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Checking assertions in step 3..
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 BMC failed!
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Assert failed in MCVE: MCVE.sv:37
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Writing trace to VCD file: engine_0/trace.vcd
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Writing trace to constraints file: engine_0/trace.smtc
SBY 14:39:50 [MCVE] engine_0: ## 0:00:00 Status: FAILED (!)
SBY 14:39:50 [MCVE] engine_0: finished (returncode=1)
SBY 14:39:50 [MCVE] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:39:50 [MCVE] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:39:50 [MCVE] summary: engine_0 (aiger suprove) returned FAIL
SBY 14:39:50 [MCVE] summary: counterexample trace: MCVE/engine_0/trace.vcd
SBY 14:39:50 [MCVE] DONE (FAIL, rc=2)
And looking closer at the output you posted:
SBY 12:13:58 [MCVE] engine_0: finished (returncode=127)
Return code 127 usually means command not found. Are you sure you have suprove installed properly? Can you run suprove on aiger files on the command line?
ok, so I can run super_prove from the command line but not suprove
incidentally I get a similar but different result when trying to use avy:
SBY 14:21:21 [assert_seq_proof] engine_0: starting process "cd assert_seq_proof; avy --cex - model/design_aiger.aig"
SBY 14:21:21 [assert_seq_proof] engine_0: finished (returncode=139)
running on the command line I get:
[sprigg@krypton assert_seq_proof]$ avy --cex - model/design_aiger.aig
Warning: The last 7 outputs are interpreted as constraints.
Segmentation fault
ok, so I can run super_prove from the command line but not suprove
Did you create a suprove
wrapper, as described in https://symbiyosys.readthedocs.io/en/latest/quickstart.html#super-prove?
This is what I see when running avy
:
SBY 16:06:01 [MCVE] Removing direcory 'MCVE'.
SBY 16:06:01 [MCVE] Copy 'MCVE.sv' to 'MCVE/src/MCVE.sv'.
SBY 16:06:01 [MCVE] engine_0: aiger avy
SBY 16:06:01 [MCVE] nomem: starting process "cd MCVE/src; yosys -ql ../model/design_nomem.log ../model/design_nomem.ys"
SBY 16:06:01 [MCVE] nomem: finished (returncode=0)
SBY 16:06:01 [MCVE] aig: starting process "cd MCVE/model; yosys -ql design_aiger.log design_aiger.ys"
SBY 16:06:01 [MCVE] aig: finished (returncode=0)
SBY 16:06:01 [MCVE] engine_0: starting process "cd MCVE; avy --cex - model/design_aiger.aig"
SBY 16:06:01 [MCVE] engine_0: finished (returncode=1)
SBY 16:06:01 [MCVE] engine_0: Status returned by engine: FAIL
SBY 16:06:01 [MCVE] base: starting process "cd MCVE/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 16:06:01 [MCVE] base: finished (returncode=0)
SBY 16:06:01 [MCVE] smt2: starting process "cd MCVE/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 16:06:01 [MCVE] smt2: finished (returncode=0)
SBY 16:06:01 [MCVE] engine_0: starting process "cd MCVE; yosys-smtbmc -s yices --noprogress --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc --aig model/design_aiger.aim:engine_0/trace.aiw model/design_smt2.smt2"
SBY 16:06:01 [MCVE] engine_0: ## 0:00:00 Solver: yices
SBY 16:06:01 [MCVE] engine_0: ## 0:00:00 Skipping step 0 (and assuming pass)..
SBY 16:06:01 [MCVE] engine_0: ## 0:00:00 Checking assertions in step 1..
SBY 16:06:01 [MCVE] engine_0: ## 0:00:00 Status: PASSED
SBY 16:06:01 [MCVE] engine_0: finished (returncode=0)
Traceback (most recent call last):
File "/usr/local/bin/sby", line 388, in <module>
retcode |= run_job(t)
File "/usr/local/bin/sby", line 346, in run_job
job.run(setupmode)
File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 634, in run
self.taskloop()
File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 251, in taskloop
task.poll()
File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 170, in poll
self.handle_exit(self.p.returncode)
File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 108, in handle_exit
self.exit_callback(retcode)
File "/usr/local/bin/../share/yosys/python3/sby_engine_aiger.py", line 129, in exit_callback2
assert task2_status == "FAIL"
AssertionError
Meaning avy
produced a model but then yosys-smtbmc using yices was not able to verify that model. Strange.
$ avy --cex - MCVE/model/design_aiger.aig
Warning: The last 6 outputs are interpreted as constraints.
1
b0
00000000000
0000000000000000
0000000000000000
.
That looks like an issue in avy, For one, that witness is too short. Here is the witness from abc pdr
:
cat MCVE/engine_0/trace.aiw
000000000000
0000000000000000
1010000000001000
1000000000001000
1010000000001001# DONE
And here is the witness from suprove
:
$ cat MCVE/engine_0/trace.aiw
1
b0
00000000000
0000000000000001
1110000000000000
1100000000000000
1110000000000000
.
Both 4 cycles deep, both not completely zeros. I guess there's a bug in avy
here. However, that does not seem to be the issue you are fighting. That one I can't reproduce it seems.
ok thanks, so a type-o in our suprove wrapper, now sorted.
The avy, I just get a segmentation fault when run manually:
[sprigg@krypton symbyosys]$ cd assert_seq_proof; avy --cex - model/design_aiger.aig
Warning: The last 7 outputs are interpreted as constraints.
Segmentation fault
The avy, I just get a segmentation fault when run manually:
Funny. I'm using git master of avy, built earlier today.
However, I now ran it in valgrind and there are errors. So it really looks like there is an avy issue here. I'll investigate further..
Steps to reproduce the issue
using the files from the enclosed zip MCVE.zip
from the command line run "sby -f MCVE.sby"
Note: as configured this elementary example contains a purposeful fail condition (line 37 should contain an addition rather than AND operator).
Expected behavior
When the config file is reconfigured to use the "abc pdr" engine the following response is seen:
Actual behavior
what is seen with the suprove engine: