SymbiYosysのドキュメントを読む (4. SymbiYosysの作業環境をDockerfileにまとめる)

https://github.com/msyksphinz-self/symbiyosys-docker-env に、SymbiYosysを含めた試行環境を置いておくことにした。

github.com

以下は、SymbiYosys（SBY）およびその依存ツール（Yosys、yosys-smtbmc、Boolectorなど）をインストールした検証用Dockerfileの例である。

FROM ubuntu:24.04
# Necessary for tzdata

ENV DEBIAN_FRONTEND=noninteractive

ARG TZ_ARG=UTC
ENV TZ=${TZ_ARG}

ARG RISCV_ARG=/riscv/
ENV RISCV=${RISCV_ARG}

# Add i386 support for support for Pin
RUN apt autoclean
RUN dpkg --add-architecture i386

RUN apt update
RUN apt install -y build-essential clang bison flex \
    libreadline-dev gawk tcl-dev libffi-dev git \
    graphviz xdot pkg-config python3 python3-pip python3-venv zlib1g-dev \
    curl cmake autoconf gperf \
    libgmp-dev && \
    rm -rf /var/lib/apt/lists/*

# Make venv environment
RUN python3 -m venv /opt/venv \
 && . /opt/venv/bin/activate \
 && pip install --upgrade pip \
 && pip install flask requests

# Update path for venv
ENV PATH="/opt/venv/bin:${PATH}"

RUN python3 -m pip install click

# Install YosysHQ
RUN git clone https://github.com/YosysHQ/yosys --recurse-submodules && \
                cd yosys && \
                make -j$(nproc) && \
        make install

# Install SBY
RUN git clone https://github.com/YosysHQ/sby && \
        cd sby && \
        make install

# Install Bootlector
RUN git clone https://github.com/boolector/boolector && \
        cd boolector && \
        ./contrib/setup-btor2tools.sh && \
        ./contrib/setup-lingeling.sh && \
        ./configure.sh && \
        make -C build -j$(nproc) && \
        cp build/bin/boolector /usr/local/bin/ && \
    cp build/bin/btor* /usr/local/bin/ && \
        cp deps/btor2tools/build/bin/btorsim /usr/local/bin/

# Yices2
RUN git clone https://github.com/SRI-CSL/yices2.git yices2 && \
        cd yices2 && \
        autoconf && \
        ./configure && \
        make -j$(nproc) && \
        make install

サンプル通りにSymbiYosysを動作させると、今度はうまくいった。

cd sby/docs/examples/fifo/
sby -f fifo.sby nofullskip

SBY 16:00:44 [fifo_nofullskip] Removing directory '/home/kimura/work/formal/sby/docs/examples/fifo/fifo_nofullskip'.
SBY 16:00:44 [fifo_nofullskip] Copy '/home/kimura/work/formal/sby/docs/examples/fifo/fifo.sv' to '/home/kimura/work/formal/sby/docs/examples/fifo/fifo_nofullskip/src/fifo.sv'.
SBY 16:00:44 [fifo_nofullskip] engine_0: smtbmc boolector
SBY 16:00:44 [fifo_nofullskip] base: starting process "cd fifo_nofullskip/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 16:00:44 [fifo_nofullskip] base: finished (returncode=0)
SBY 16:00:44 [fifo_nofullskip] prep: starting process "cd fifo_nofullskip/model; yosys -ql design_prep.log design_prep.ys"
SBY 16:00:44 [fifo_nofullskip] prep: finished (returncode=0)
SBY 16:00:44 [fifo_nofullskip] smt2: starting process "cd fifo_nofullskip/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 16:00:44 [fifo_nofullskip] smt2: finished (returncode=0)
SBY 16:00:44 [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 16:00:44 [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 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Solver: boolector
SBY 16:00:44 [fifo_nofullskip] engine_0.induction: ##   0:00:00  Solver: boolector
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Checking assumptions in step 0..
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Checking assertions in step 0..
SBY 16:00:44 [fifo_nofullskip] engine_0.induction: ##   0:00:00  Trying induction in step 20..
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Checking assumptions in step 1..
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Checking assertions in step 1..
SBY 16:00:44 [fifo_nofullskip] engine_0.induction: ##   0:00:00  Trying induction in step 19..
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Checking assumptions in step 2..
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Checking assertions in step 2..
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  BMC failed!
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Assert failed in fifo: a_count_diff
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Writing trace to VCD file: engine_0/trace.vcd
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 16:00:44 [fifo_nofullskip] engine_0.induction: ##   0:00:00  Trying induction in step 18..
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Writing trace to constraints file: engine_0/trace.smtc
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Writing trace to Yosys witness file: engine_0/trace.yw
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: ##   0:00:00  Status: failed
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: finished (returncode=1)
SBY 16:00:44 [fifo_nofullskip] engine_0.basecase: Status returned by engine for basecase: FAIL
SBY 16:00:44 [fifo_nofullskip] engine_0.induction: terminating process
SBY 16:00:44 [fifo_nofullskip] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 16:00:44 [fifo_nofullskip] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 16:00:44 [fifo_nofullskip] summary: engine_0 (smtbmc boolector) returned FAIL for basecase
SBY 16:00:44 [fifo_nofullskip] summary: counterexample trace [basecase]: fifo_nofullskip/engine_0/trace.vcd
SBY 16:00:44 [fifo_nofullskip] summary:   failed assertion fifo.a_count_diff at fifo.sv:106.13-107.71 in step 2
SBY 16:00:44 [fifo_nofullskip] DONE (FAIL, rc=2)
SBY 16:00:44 The following tasks failed: ['nofullskip']

波形を観測すると、うまくいっているように見える。

fifo.sby の nofullskip には define が定義してあるので、これによってハードウェアの一部に不具合が挿入されている：

[script]
nofullskip: read -define NO_FULL_SKIP=1

`ifndef NO_FULL_SKIP
    // write while full => overwrite oldest data, move read pointer
    assign rskip = wen && !ren && data_count >= MAX_DATA;
    // read while empty => read invalid data, keep write pointer in sync
    assign wskip = ren && !wen && data_count == 0;
`else
    assign rskip = 0;
    assign wskip = 0;
`endif // NO_FULL_SKIP

rskipとwskipが実装されていないので： - 書き込み時にdata_count >= MAX_DATA (つまりFIFOがFulllの状態)をスキップしない。 - 読み込み時にdata_count == 0 (つまりFIFOがEmptyの状態)をスキップしない。

ので、異常な動作を防ぐことができない。これが、そのまま再現の波形に現れている。