search

hdl / conda-eda

Conda recipes for FPGA EDA tools for simulation, synthesis, place and route and bitstream generation.
https://anaconda.org/LiteX-Hub
Apache License 2.0
94 stars 27 forks source link

add symbi-yosys package with yices-smt2 #252

Open alanvgreen opened 2 years ago

alanvgreen commented 2 years ago

Part 3 of the zero2asic course uses symbi-yosys (sby) with the yices engine.

Usng I was able to install sby with conda install -c litex-hub symbiyosys, but then got this failure:

$ sby -f timer.sby 
SBY  2:44:03 [timer] Removing directory 'timer'.
SBY  2:44:03 [timer] Copy 'timer.v' to 'timer/src/timer.v'.
SBY  2:44:03 [timer] engine_0: smtbmc
SBY  2:44:03 [timer] base: starting process "cd timer/src; yosys -ql ../model/design.log ../model/design.ys"
SBY  2:44:03 [timer] base: finished (returncode=0)
SBY  2:44:03 [timer] smt2: starting process "cd timer/model; yosys -ql design_smt2.log design_smt2.ys"
SBY  2:44:03 [timer] smt2: finished (returncode=0)
SBY  2:44:03 [timer] engine_0: starting process "cd timer; yosys-smtbmc --presat --unroll -c --noprogress -t 20  --append 0 --dump-vcd engine_0/trace%.vcd --dump-vlogtb engine_0/trace%_tb.v --dump-smtc engine_0/trace%.smtc model/design_smt2.smt2"
SBY  2:44:04 [timer] engine_0: ##   0:00:00  Solver: yices
SBY  2:44:04 [timer] engine_0: ##   0:00:00  SMT Solver 'yices-smt2' not found in path.
SBY  2:44:04 [timer] engine_0: finished (returncode=1)
SBY  2:44:04 [timer] ERROR: engine_0: Engine terminated without status.
SBY  2:44:04 [timer] DONE (ERROR, rc=16)

timer.sby contains:

[options]
mode cover

[engines]
smtbmc

[script]
read -formal timer.v
prep -top timer

[files]
timer.v
proppy commented 2 years ago

According to https://symbiyosys.readthedocs.io/en/latest/reference.html#engines-section, symbiyosys support a wide variety of engines / solvers selection.

It looks that z3 is a supported option and I could find a packaged version here (albeit outdated, current upstream version is 4.11): https://anaconda.org/asmeurer/z3.

Does it work if you change the solver according to the symbiflow docs?

proppy commented 2 years ago

Also see https://github.com/hdl/conda-eda/blob/master/.github/workflows/Build.yml#L297 it seems that the build are currently disabled because of #70

proppy commented 2 years ago

Actually looking at the recipe a little bit closer, it seems that z3 https://github.com/hdl/conda-eda/blob/master/formal/symbiyosys/build.sh#L52 and boolector https://github.com/hdl/conda-eda/blob/master/formal/symbiyosys/build.sh#L25 are the two solvers included in the build.

proppy commented 2 years ago

@alanvgreen what happens if you switch the configuration to:

[options]
mode cover

[engines]
smtbmc z3

[script]
read -formal timer.v
prep -top timer

[files]
timer.v
alanvgreen commented 2 years ago

Setting [engines] to smtbmc z3 worked for a simple example: Symbiyosys completes without errors and produces correct output.