Apparent problem in induction verifier

[davidboles]

Version

Yosys 0.28+4 (git sha1 7efc50367, x86_64-apple-darwin20.2-clang 10.0.0-4ubuntu1 -fPIC -Os)

On which OS did this happen?

macOS

Reproduction Steps

With the two files reqwalker.v and reqwalker.sby, the command:

sby -f reqwalker.sby prf

passes if there is an assignment to an unconnected wire but not if that assignment is commented out. This behavior doesn't occur in the December 2, 2020 commercial version of SymbiYosys + Yosys.

The line to have commented out or not is 71 of reqwalker.v

reqwalker.v.txt
reqwalker.sby.txt

Expected Behavior

The verifier shouldn't flag an error when the disconnected assignment isn't present. Looking at the trace file, the tool is making a transition on the variable o_led that is not possible from the design (AFAICT). The output from the run is attached.

pass_output.txt

Actual Behavior

An error is flagged. The output from the run is attached.

fail_output.txt
trace_induct.vcd.txt

[nakengelhardt]

This issue still does not reproduce when using the verific frontend (from the commercial version), but it does reproduce when replacing read with read_verilog.

[jix]

It turns out the issue is that the open source verilog frontend turns the case statement into a ROM (unless there is other logic in the same case statement, even when that logic doesn't end up driving anything). There is no specific handling of ROMs (compared to memories that can be written) when using smtbmc's k-induction mode, so they're treated as memories that are initialized and just happen to receive no writes. Since the induction step of k-induction has to ignore any initialization data, it assumes an unconstrained memory here and is free to make up ROM contents at the start of the induction step.

While I'd like to eventually improve ROM handling for the smt backend and smtbmc, a workaround that works now is to either a) prevent yosys from inferring ROMs in the first place. This can be done using this script, which splits out the hierarchy and proc steps from prep so we can pass -norom to `proc:

read -formal reqwalker.v
hierarchy -top reqwalker
proc -norom
prep

Alternatively it's possible to turn any ROMs into logic at the end of the script using:

read -formal reqwalker.v
prep -top reqwalker
memory_map -rom-only

Both of these variants pass with the open source verilog frontend. These steps are not done by default as they can interact badly with designs that do use partially uninitialized ROMs where the solver is supposed to solve for an initial state. See YosysHQ/yosys#3378 for some prior discussion on this (I'm closing this, as the underlying issue is already tracked there).

[davidboles]

Thanks very much for the explanation - the workarounds get me going again.