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 5f6b36e91f 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.