Netlist validation using Yosys

Question

I'd like to ask if I can validate my design in yosys. I re-synthesized my netlist, used yosys to get the execution (topological order).

Now I want to check the validation of this design by inserting some inputs to the netlist and check the output.

For example, I used s27 bench mark for my model, I want to make sure the output of my design matches the output of s27 bench mark. I went through yosys manual and I was not able to know what command do that. Also, I used other tools such as Veriwell. But I really prefer using yosys.

CliffordVienna · Accepted Answer · 2016-01-26T14:19:40.513

If simulating the post-synthesis netlist with a given test bench is all you want to do, then you should just use a simulator for that. (However, I would strongly recommend Icarus Verilog over Veriwell.)

You can of course use formal methods to prove equivalence of two circuits in Yosys, but this is much more complicated and requires a certain amount of experience when attempted with a larger designs.

The following shell script demonstrates two different elementary methods of formal equivalence checking of post-synthesis netlists with yosys:

# download fiedler-cooley.v
if [ ! -f fiedler-cooley.v ]; then
    wget https://raw.githubusercontent.com/cliffordwolf/yosys/master/tests/simple/fiedler-cooley.v
fi

# synthesis for ice40
yosys -p 'synth_ice40 -top up3down5 -blif up3down5.blif' fiedler-cooley.v

# formal verification with equiv_*
yosys -l check1.log -p '
    # gold design
    read_verilog fiedler-cooley.v
    prep -top up3down5
    splitnets -ports;;
    design -stash gold

    # gate design
    read_blif up3down5.blif
    techmap -autoproc -map +/ice40/cells_sim.v
    prep -top up3down5
    design -stash gate

    # prove equivalence
    design -copy-from gold -as gold up3down5
    design -copy-from gate -as gate up3down5
    equiv_make gold gate equiv
    hierarchy -top equiv
    equiv_simple
    equiv_status -assert
'

# formal verification with BMC and temproral induction (yosys "sat" command")
yosys -l check2.log -p '
    # gold design
    read_verilog fiedler-cooley.v
    prep -top up3down5
    splitnets -ports;;
    design -stash gold

    # gate design
    read_blif up3down5.blif
    techmap -autoproc -map +/ice40/cells_sim.v
    prep -top up3down5
    design -stash gate

    # prove equivalence
    design -copy-from gold -as gold up3down5
    design -copy-from gate -as gate up3down5
    miter -equiv -flatten gold gate miter
    hierarchy -top miter
    sat -verify -tempinduct -prove trigger 0 -seq 1 -set-at 1 in_up,in_down 0
'

# formal verification with BMC+tempinduct using undef modeling
yosys -l check3.log -p '
        # gold design
        read_verilog fiedler-cooley.v
        prep -top up3down5
        splitnets -ports;;
        design -stash gold

        # gate design
        read_blif up3down5.blif
        techmap -autoproc -map +/ice40/cells_sim.v
        prep -top up3down5
        design -stash gate

        # prove equivalence
        design -copy-from gold -as gold up3down5
        design -copy-from gate -as gate up3down5
        miter -equiv -flatten -ignore_gold_x gold gate miter
        hierarchy -top miter
        sat -verify -tempinduct -prove trigger 0 -set-init-undef -set-def-inputs
'

Each method of formal equivalence checking has its pros and cons.

For example, the first method above needs to be able to match a sufficient number of internal wires by name in order to successfully verify equivalence. But it is capable of breaking large circuits down into smaller ones and thus performs well even with larger designs.

The second method does not need to match any internal wires by name, but needs a reset condition for the circuit (the -seq 1 -set-at 1 in_up,in_down 0 part) and only works on circuits that "leak" all internal state to its outputs within a small number of cycles regardless of the sequence of input signals.

The third method is a variation on the second method that uses modeling of undef states to avoid the requirement for a reset condition, but produces a more complex SAT model and thus might be less efficient computationally.

That all being said, you should never rely on one tool to check the output itself has produced. E.g. if there is a bug in the Yosys Verilog front-end, then this will effect synthesis and verification likewise and the problem is never detected. So if you use Yosys to verify Yosys' output then you should only do that in addition to a verification scheme that uses an independent code-base. For example Icarus Verilog or Verilator would be two simulators that do not share any code with Yosys (or each other afaict). Also: In general, formal verification does not substitute for simulation. (Especially not formal equivalence checking: How do you know that the model you check equivalence with is correct in the first place?)

Netlist validation using Yosys

1 Answers1