AssertionError in sby tests

[saahm]

I tried running the tests in the tests directory.
I called make test

...
SBY 11:09:12 [cover] engine_0: [btor>mc] bad state property 1 at bound k = 6 UNSATISFIABLE
SBY 11:09:12 [cover] engine_0: [btor>mc] found 1 reachable and 0 unreachable bad state properties at bound k = 6
SBY 11:09:12 [cover] engine_0_0: *** 'btorsim' error: invalid command line option '--vcd' (try '-h')
SBY 11:09:12 [cover] engine_0_0: finished (returncode=1)
Traceback (most recent call last):
  File "../sbysrc/sby.py", line 469, in <module>
    task_retcode = run_task(task)
  File "../sbysrc/sby.py", line 442, in run_task
    task.run(setupmode)
  File "/home/sallar/tools/SymbiYosys/sbysrc/sby_core.py", line 712, in run
    self.taskloop()
  File "/home/sallar/tools/SymbiYosys/sbysrc/sby_core.py", line 281, in taskloop
    proc.poll()
  File "/home/sallar/tools/SymbiYosys/sbysrc/sby_core.py", line 192, in poll
    self.handle_exit(self.p.returncode)
  File "/home/sallar/tools/SymbiYosys/sbysrc/sby_core.py", line 116, in handle_exit
    self.exit_callback(retcode)
  File "/home/sallar/tools/SymbiYosys/sbysrc/sby_engine_btor.py", line 113, in exit_callback2
    assert retcode == 0
AssertionError
make: *** [Makefile:12: test_cover] Fehler 1

It shows that sby tries calling btorsim with the argument --vcd which is not present in btorsim

usage: btorsim [ <option> ... ] [ <btor> [ <witness> ] ]

where <option> is one of the following

  -h        print this command line option summary
  -c        check only <witness> and do not print trace
  -v        increase verbosity level (multiple times if necessary)
  -r <n>    generate <n> random transitions (default 20)
  -s <s>    random seed (default '0')

  -b <n>    fake simulation to satisfy bad state property 'b<n>'
  -j <n>    fake simulation to satisfy justice property 'j<n>'

  --states  print all states

and '<btor>' is sequential model in 'BTOR' format
and '<witness>' a trace in 'BTOR' witness format.

The simulator either checks a given witness (checking mode) or
randomly generates inputs (random mode). If no BTOR model path is
specified then it is read from '<stdin>'.  The simulator only uses
checking mode if both the BTOR model and a witness file are specified.

I've installed sby according to the readthedocs page
How can I get the tests running correctly?

[nakengelhardt]

Please update btorsim, the --vcd argument was added in hwmcc/btor2tools#10.

[saahm]

Thanks for your reply. I updated btorsim but i got an issue with abc_bmc3 now instead.

SymbiYosys/tests$ make test
python3 make/collect_tests.py
cd regression && python3 /home/sallar/tools/SymbiYosys/sbysrc/sby.py -f aim_vs_smt2_nonzero_start_offset.sby abc_bmc3
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] Removing directory '/home/sallar/tools/SymbiYosys/tests/regression/aim_vs_smt2_nonzero_start_offset_abc_bmc3'.
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] Writing 'aim_vs_smt2_nonzero_start_offset_abc_bmc3/src/test.sv'.
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] engine_0: abc bmc3
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] base: starting process "cd aim_vs_smt2_nonzero_start_offset_abc_bmc3/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] base: ERROR: No such command: write_jny (type 'help' for a command overview)
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] base: finished (returncode=1)
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] base: task failed. ERROR.
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 10:14:27 [aim_vs_smt2_nonzero_start_offset_abc_bmc3] DONE (ERROR, rc=16)
SBY 10:14:27 The following tasks failed: ['abc_bmc3']
make: *** [make/rules/test/regression/aim_vs_smt2_nonzero_start_offset.sby.mk:3: regression/aim_vs_smt2_nonzero_start_offset_abc_bmc3] Fehler 16

I made sure to also update my sby before trying that.
So i updated boolector as well as sby.

Do I also have to update other tools (since it mentions abc_bmc I would guess something like yosys?)

[mmicko]

@saahm looks like you have latest sby, but not latest yosys. write_jny is added in previous release

[saahm]

@saahm looks like you have latest sby, but not latest yosys. write_jny is added in previous release

Thanks, that seemed to help here for that.
But it only revealed that btorsim still seems to lack that parameter for me.
I checked out the latest version of boolector from Jan 25 and built it according to the readmes. (Including copying the built binaries into my bin directories)

Did I miss something again? According to the pullrequest linked by nakengelhardt it has been merged, so I'm confused why its not appearing?

[mmicko]

Well boolector itself in scripts download old version https://github.com/Boolector/boolector/blob/master/contrib/setup-btor2tools.sh we package in TabbyCad and use always the latest ( so one from https://github.com/Boolector/btor2tools/ )
So I recommend compile btorsim from master as separate project, and install btorsim over one from boolector.

[nakengelhardt]

Ah, I see what is happening. The contrib setup script for btor2tools in boolector is pinned to a fairly old revision, 1df768d, so you need to manually update btor2tools to a newer revision. I will update the documentation for sby.

[saahm]

Ahh, I will do that an update you here once I did it. Thanks so far.

[nakengelhardt]

Updated docs: https://symbiyosys.readthedocs.io/en/latest/install.html#boolector

[saahm]

Updated docs: https://symbiyosys.readthedocs.io/en/latest/install.html#boolector

its missing cd btor2tools ;)

[saahm]

Updated docs: https://symbiyosys.readthedocs.io/en/latest/install.html#boolector

its missing cd btor2tools ;)

and the sudo infront of the make install -- as it will copy into non-user directories.

That aside it works not, and progresses to give me a new error:

SBY 11:53:49 [demo_btormc] engine_0: [btor>mc] found 1 reachable and 0 unreachable bad state properties at bound k = 8
SBY 11:53:49 [demo_btormc] engine_0: [btor>mc] deleting model checker: 1 inputs, 3 states, 1 bad, 0 constraints
SBY 11:53:49 [demo_btormc] engine_0: finished (returncode=0)
SBY 11:53:49 [demo_btormc] engine_0_0: btorsim: error while loading shared libraries: libbtor2parser.so: cannot open shared object file: No such file or directory
SBY 11:53:49 [demo_btormc] engine_0_0: finished (returncode=127)
SBY 11:53:49 [demo_btormc] engine_0_0: COMMAND NOT FOUND. ERROR.
SBY 11:53:49 [demo_btormc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 11:53:49 [demo_btormc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 11:53:49 [demo_btormc] DONE (ERROR, rc=16)
SBY 11:53:49 The following tasks failed: ['btormc']
make: *** [make/rules/test/unsorted/demo.sby.mk:3: unsorted/demo_btormc] Fehler 16

[nakengelhardt]

Can you try if building btorsim with cmake . -DBUILD_SHARED_LIBS=OFF fixes this?

[saahm]

Can you try if building btorsim with cmake . -DBUILD_SHARED_LIBS=OFF fixes this?

That fixed it, tho I noticed when the tests were running that one test required "xmlschema" as python dependency.
pip install xmlschema is missing somewhere on the way too.

With that everything is running finely :) Thank you! If there is nothing further to be added this can be closed

[nakengelhardt]

@jix with the changes in #163, can we now also check for installed packages? Or is this something we should rather check in the junit validation script itself?