test_async{,buffered} of FIFOFormalCase PREUNSAT

[rroohhh]

Running the testsuite using

• yosys 53c0a6b780
  (this is almost, but not completly the current upstream, however there do not seem to be any relevant new commits that could affect this)
• sby 74f33880bd42
• amaranth 5f6b36e
  Fails with the following two failures:

======================================================================
FAIL: test_async (tests.test_lib_fifo.FIFOFormalCase)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "/tmp/guix-build-python-amaranth-0.3+g5f6b36e91.drv-0/source/tests/test_lib_fifo.py", line 283, in test_async
    self.check_async_fifo(AsyncFIFO(width=8, depth=4))
  File "/tmp/guix-build-python-amaranth-0.3+g5f6b36e91.drv-0/source/tests/test_lib_fifo.py", line 278, in check_async_fifo
    self.assertFormal(FIFOContractSpec(fifo, r_domain="read", w_domain="write",
  File "/tmp/guix-build-python-amaranth-0.3+g5f6b36e91.drv-0/source/tests/utils.py", line 82, in assertFormal
    self.fail("Formal verification failed:\n" + stdout)
AssertionError: Formal verification failed:
SBY 14:41:11 [spec_lib_fifo_async] Removing directory '/tmp/guix-build-python-amaranth-0.3+g5f6b36e91.drv-0/source/tests/spec_lib_fifo_async'.
SBY 14:41:11 [spec_lib_fifo_async] Writing 'spec_lib_fifo_async/src/top.il'.
SBY 14:41:11 [spec_lib_fifo_async] engine_0: smtbmc
SBY 14:41:11 [spec_lib_fifo_async] base: starting process "cd spec_lib_fifo_async/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:41:11 [spec_lib_fifo_async] base: finished (returncode=0)
SBY 14:41:11 [spec_lib_fifo_async] prep: starting process "cd spec_lib_fifo_async/model; yosys -ql design_prep.log design_prep.ys"
SBY 14:41:11 [spec_lib_fifo_async] prep: finished (returncode=0)
SBY 14:41:11 [spec_lib_fifo_async] smt2: starting process "cd spec_lib_fifo_async/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 14:41:11 [spec_lib_fifo_async] smt2: finished (returncode=0)
SBY 14:41:11 [spec_lib_fifo_async] engine_0: starting process "cd spec_lib_fifo_async; yosys-smtbmc --presat --unroll --noprogress -t 17  --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_tb.v --dump-smtc en
gine_0/trace.smtc model/design_smt2.smt2"
SBY 14:41:11 [spec_lib_fifo_async] engine_0: ##   0:00:00  Solver: yices
SBY 14:41:11 [spec_lib_fifo_async] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 14:41:11 [spec_lib_fifo_async] engine_0: ##   0:00:00  Assumptions are unsatisfiable!
SBY 14:41:11 [spec_lib_fifo_async] engine_0: ##   0:00:00  Status: PREUNSAT
SBY 14:41:11 [spec_lib_fifo_async] engine_0: finished (returncode=1)
SBY 14:41:11 [spec_lib_fifo_async] engine_0: Status returned by engine: ERROR
SBY 14:41:11 [spec_lib_fifo_async] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:41:11 [spec_lib_fifo_async] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:41:11 [spec_lib_fifo_async] summary: engine_0 (smtbmc) returned ERROR
SBY 14:41:11 [spec_lib_fifo_async] summary: engine_0 did not produce any traces
SBY 14:41:11 [spec_lib_fifo_async] DONE (ERROR, rc=16)

======================================================================
FAIL: test_async_buffered (tests.test_lib_fifo.FIFOFormalCase)
----------------------------------------------------------------------
Traceback (most recent call last):
  File "/tmp/guix-build-python-amaranth-0.3+g5f6b36e91.drv-0/source/tests/test_lib_fifo.py", line 286, in test_async_buffered
    self.check_async_fifo(AsyncFIFOBuffered(width=8, depth=4))
  File "/tmp/guix-build-python-amaranth-0.3+g5f6b36e91.drv-0/source/tests/test_lib_fifo.py", line 278, in check_async_fifo
    self.assertFormal(FIFOContractSpec(fifo, r_domain="read", w_domain="write",
  File "/tmp/guix-build-python-amaranth-0.3+g5f6b36e91.drv-0/source/tests/utils.py", line 82, in assertFormal
    self.fail("Formal verification failed:\n" + stdout)
AssertionError: Formal verification failed:
SBY 14:41:12 [spec_lib_fifo_async_buffered] Removing directory '/tmp/guix-build-python-amaranth-0.3+g5f6b36e91.drv-0/source/tests/spec_lib_fifo_async_buffered'.
SBY 14:41:12 [spec_lib_fifo_async_buffered] Writing 'spec_lib_fifo_async_buffered/src/top.il'.
SBY 14:41:12 [spec_lib_fifo_async_buffered] engine_0: smtbmc
SBY 14:41:12 [spec_lib_fifo_async_buffered] base: starting process "cd spec_lib_fifo_async_buffered/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:41:12 [spec_lib_fifo_async_buffered] base: finished (returncode=0)
SBY 14:41:12 [spec_lib_fifo_async_buffered] prep: starting process "cd spec_lib_fifo_async_buffered/model; yosys -ql design_prep.log design_prep.ys"
SBY 14:41:12 [spec_lib_fifo_async_buffered] prep: finished (returncode=0)
SBY 14:41:12 [spec_lib_fifo_async_buffered] smt2: starting process "cd spec_lib_fifo_async_buffered/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 14:41:12 [spec_lib_fifo_async_buffered] smt2: finished (returncode=0)
SBY 14:41:12 [spec_lib_fifo_async_buffered] engine_0: starting process "cd spec_lib_fifo_async_buffered; yosys-smtbmc --presat --unroll --noprogress -t 21  --append 0 --dump-vcd engine_0/trace.vcd --dump-yw engine_0/trace.yw --dump-vlogtb engine_0/trace_t
b.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY 14:41:12 [spec_lib_fifo_async_buffered] engine_0: ##   0:00:00  Solver: yices
SBY 14:41:12 [spec_lib_fifo_async_buffered] engine_0: ##   0:00:00  Checking assumptions in step 0..
SBY 14:41:12 [spec_lib_fifo_async_buffered] engine_0: ##   0:00:00  Assumptions are unsatisfiable!
SBY 14:41:12 [spec_lib_fifo_async_buffered] engine_0: ##   0:00:00  Status: PREUNSAT
SBY 14:41:12 [spec_lib_fifo_async_buffered] engine_0: finished (returncode=1)
SBY 14:41:12 [spec_lib_fifo_async_buffered] engine_0: Status returned by engine: ERROR
SBY 14:41:12 [spec_lib_fifo_async_buffered] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:41:12 [spec_lib_fifo_async_buffered] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:41:12 [spec_lib_fifo_async_buffered] summary: engine_0 (smtbmc) returned ERROR
SBY 14:41:12 [spec_lib_fifo_async_buffered] summary: engine_0 did not produce any traces
SBY 14:41:12 [spec_lib_fifo_async_buffered] DONE (ERROR, rc=16)

The following contain the respective working directories
spec_lib_fifo_async_buffered.zip
spec_lib_fifo_async.zip

[whitequark]

Could you bisect, please?

[rroohhh]

I'm on vacation for a week, after that yes.

[whitequark]

Thanks!

[lethalbit]

We ran into this in Torii a while ago, the trivial "fix" is to enable multiclock support.

The behaviour changed after sby commit 6398938e which added support for clock signals in hierarchical designs.