search

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
401 stars 74 forks source link

SymbiYosys fails with an internal exception instead of generating counter example when using abc #27

Closed tmeissner closed 5 years ago

tmeissner commented 5 years ago

During the last weeks I had an error when using abc pdr with SymbiYosys with various designs. When there is an SVA assertion which should fail, SymbiYosys itself fails with an internal assertion which results in a Python exception. If I correct the SVA, which fails, then SymbiYosys runs correctly.

I've created a simplified test design which you can find here: https://git.goodcleanfun.de/tmeissner/bug_reports/src/branch/master/SymbiYosys_27

Running it with make results in an error like this:

SBY 13:51:42 [symbiyosys_flag_check] smt2: finished (returncode=0)
SBY 13:51:42 [symbiyosys_flag_check] engine_0: starting process "cd symbiyosys_flag_check; 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 --aig-noheader model/design_smt2.smt2"
SBY 13:51:42 [symbiyosys_flag_check] engine_0: ##   0:00:00  Solver: yices
SBY 13:51:42 [symbiyosys_flag_check] engine_0: Traceback (most recent call last):
SBY 13:51:42 [symbiyosys_flag_check] engine_0: File "/opt/symbiotic/symbiotic-20190103A/bin/../libexec/yosys-smtbmc", line 515, in <module>
SBY 13:51:42 [symbiyosys_flag_check] engine_0: width = smt.net_width(topmod, path)
SBY 13:51:42 [symbiyosys_flag_check] engine_0: File "/opt/symbiotic/symbiotic-20190103A/libexec/../share/yosys/python3/smtio.py", line 829, in net_width
SBY 13:51:42 [symbiyosys_flag_check] engine_0: assert net_path[-1] in self.modinfo[mod].wsize
SBY 13:51:42 [symbiyosys_flag_check] engine_0: AssertionError
SBY 13:51:42 [symbiyosys_flag_check] engine_0: finished (returncode=1)
Traceback (most recent call last):
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/sby", line 310, in <module>
    retcode |= run_job(t)
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/sby", line 274, in run_job
    job.run()
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_core.py", line 564, in run
    self.taskloop()
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_core.py", line 195, in taskloop
    task.poll()
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_core.py", line 116, in poll
    self.handle_exit(self.p.returncode)
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_core.py", line 71, in handle_exit
    self.exit_callback(retcode)
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_engine_abc.py", line 109, in exit_callback2
    assert task2_status is not None
AssertionError

The same error occurs when doing a bounded model check with abc bmc3. The smtbmc engine is not effected.

cliffordwolf commented 5 years ago

Thanks for reporting this! Fixed in https://github.com/YosysHQ/yosys/commit/e112d2fbf5a31f00ef19e6d05f28fecc1e9c56b9.