SymbiYosysのドキュメントを読むために、まずはリポジトリ内のドキュメントを読んでみることにする。
SymbiYosysでFIFOサンプルを検証しようとした際の実行ログを以下に示す。
なんか思っているのと違うなあ。VCDファイルも生成されていない。
sby -f fifo.sby nofullskip
SBY 1:18:07 [fifo_nofullskip] Removing directory '/home/msyksphinz/work/formal/sby/docs/examples/fifo/fifo_nofullskip'. SBY 1:18:07 [fifo_nofullskip] Copy '/home/msyksphinz/work/formal/sby/docs/examples/fifo/fifo.sv' to '/home/msyksphinz/work/formal/sby/docs/examples/fifo/fifo_nofullskip/src/fifo.sv'. SBY 1:18:07 [fifo_nofullskip] engine_0: smtbmc boolector SBY 1:18:07 [fifo_nofullskip] base: starting process "cd fifo_nofullskip/src; yosys -ql ../model/design.log ../model/design.ys" SBY 1:18:07 [fifo_nofullskip] base: finished (returncode=0) SBY 1:18:07 [fifo_nofullskip] prep: starting process "cd fifo_nofullskip/model; yosys -ql design_prep.log design_prep.ys" SBY 1:18:07 [fifo_nofullskip] prep: finished (returncode=0) SBY 1:18:07 [fifo_nofullskip] smt2: starting process "cd fifo_nofullskip/model; yosys -ql design_smt2.log design_smt2.ys" SBY 1:18:07 [fifo_nofullskip] smt2: finished (returncode=0) SBY 1:18:07 [fifo_nofullskip] engine_0.basecase: starting process "cd fifo_nofullskip; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20 --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2" SBY 1:18:07 [fifo_nofullskip] engine_0.induction: starting process "cd fifo_nofullskip; yosys-smtbmc -s boolector --presat --unroll -i --noprogress -t 20 --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-yw engine_0/trace_induct.yw --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2" SBY 1:18:07 [fifo_nofullskip] engine_0.induction: ## 0:00:00 Solver: boolector SBY 1:18:07 [fifo_nofullskip] engine_0.basecase: ## 0:00:00 Solver: boolector SBY 1:18:07 [fifo_nofullskip] engine_0.induction: ## 0:00:00 SMT Solver 'boolector' not found in path. SBY 1:18:07 [fifo_nofullskip] engine_0.basecase: ## 0:00:00 SMT Solver 'boolector' not found in path. SBY 1:18:07 [fifo_nofullskip] engine_0.induction: finished (returncode=1) SBY 1:18:07 [fifo_nofullskip] ERROR: engine_0: Engine terminated without status. SBY 1:18:07 [fifo_nofullskip] engine_0.basecase: terminating process SBY 1:18:07 [fifo_nofullskip] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0) SBY 1:18:07 [fifo_nofullskip] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0) SBY 1:18:07 [fifo_nofullskip] summary: engine_0 (smtbmc boolector) did not return a status SBY 1:18:07 [fifo_nofullskip] summary: engine_0 did not produce any traces SBY 1:18:07 [fifo_nofullskip] DONE (ERROR, rc=16) SBY 1:18:07 The following tasks failed: ['nofullskip']
良く読んでみると、Solverとしてのboolectorが入っていない、ということなのかなあ。
Ubuntuでboolectorをインストールしてみる：
sudo apt update sudo apt install boolector
再度実行してみると、以下のようになった。これもやはり動いていない気がする。
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: starting process "cd fifo_nofullskip; yosys-smtbmc -s boolector --presat --unroll --noprogress -t 20 --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 1:47:45 [fifo_nofullskip] engine_0.induction: starting process "cd fifo_nofullskip; yosys-smtbmc -s boolector --presat --unroll -i --noprogress -t 20 --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-yw engine_0/trace_induct.yw --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: ## 0:00:00 Solver: boolector
SBY 1:47:45 [fifo_nofullskip] engine_0.induction: ## 0:00:00 Solver: boolector
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: Traceback (most recent call last):
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: File "/usr/local/bin/yosys-smtbmc", line 1958, in <module>
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: smt_assert_design_assumes(step)
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: File "/usr/local/bin/yosys-smtbmc", line 1602, in smt_assert_design_assumes
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: File "/usr/local/bin/yosys-smtbmc", line 1650, in smt_assert_consequent
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: smt.write("(assert %s)" % expr)
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 498, in write
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: stmt = self.unparse(self.unroll_stmt(s))
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: ^^^^^^^^^^^^^^^^^^^
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 319, in unroll_stmt
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: recursion_helper(self._unroll_stmt_into, stmt, result)
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 88, in recursion_helper
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: request = next(top)
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: ^^^^^^^^^
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 330, in _unroll_stmt_into
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: yield from self._unroll_stmt_into(s, new_stmt, depth - 1)
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 364, in _unroll_stmt_into
SBY 1:47:45 [fifo_nofullskip] engine_0.basecase: yield from self._unroll_stmt_into(decl, tmp, depth - 1)
