Symbolic model checking

Note

While it is possible to perform model checking directly in Yosys, it is highly recommended to use SBY or EQY for formal hardware verification.

Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or has not) a given property.

One application is Formal Equivalence Checking: Proving that two circuits are identical. For example this is a very useful feature when debugging custom passes in Yosys.

Other applications include checking if a module conforms to interface standards.

The sat command in Yosys can be used to perform Symbolic Model Checking.

Checking techmap

Let’s take a look at an example included in the Yosys code base under docs/source/code_examples/synth_flow:

Listing 86 techmap_01_map.v
module \$add (A, B, Y);

parameter A_SIGNED = 0;
parameter B_SIGNED = 0;
parameter A_WIDTH = 1;
parameter B_WIDTH = 1;
parameter Y_WIDTH = 1;

input [A_WIDTH-1:0] A;
input [B_WIDTH-1:0] B;
output [Y_WIDTH-1:0] Y;

generate
  if ((A_WIDTH == 32) && (B_WIDTH == 32))
    begin
      wire [16:0] S1 = A[15:0] + B[15:0];
      wire [15:0] S2 = A[31:16] + B[31:16] + S1[16];
      assign Y = {S2[15:0], S1[15:0]};
    end
  else
    wire _TECHMAP_FAIL_ = 1;
endgenerate

endmodule
Listing 87 techmap_01.v
module test(input [31:0]  a, b,
            output [31:0] y);
assign y = a + b;
endmodule
Listing 88 techmap_01.ys
read_verilog techmap_01.v
hierarchy -check -top test
techmap -map techmap_01_map.v;;

To see if it is correct we can use the following code:

# read test design
read_verilog techmap_01.v
hierarchy -top test

# create two version of the design: test_orig and test_mapped
copy test test_orig
rename test test_mapped

# apply the techmap only to test_mapped
techmap -map techmap_01_map.v test_mapped

# create a miter circuit to test equivalence
miter -equiv -make_assert -make_outputs test_orig test_mapped miter
flatten miter

# run equivalence check
sat -verify -prove-asserts -show-inputs -show-outputs miter

Result:

Solving problem with 945 variables and 2505 clauses..
SAT proof finished - no model found: SUCCESS!

AXI4 Stream Master

The code used in this section is included in the Yosys code base under docs/source/code_examples/axis.

The following AXI4 Stream Master has a bug. But the bug is not exposed if the slave keeps tready asserted all the time. (Something a test bench might do.)

Symbolic Model Checking can be used to expose the bug and find a sequence of values for tready that yield the incorrect behavior.

Listing 89 axis_master.v
module axis_master(aclk, aresetn, tvalid, tready, tdata);
    input aclk, aresetn, tready;
    output reg tvalid;
    output reg [7:0] tdata;

    reg [31:0] state;
    always @(posedge aclk) begin
        if (!aresetn) begin
	    state <= 314159265;
	    tvalid <= 0;
	    tdata <= 'bx;
	end else begin
	    if (tvalid && tready)
	    	tvalid <= 0;
	    if (!tvalid || !tready) begin
	    //             ^- should not be inverted!
                state = state ^ state << 13;
                state = state ^ state >> 7;
                state = state ^ state << 17;
		if (state[9:8] == 0) begin
		    tvalid <= 1;
		    tdata <= state;
		end
	    end
	end
    end
endmodule
Listing 90 axis_test.v
module axis_test(aclk, tready);
    input aclk, tready;
    wire aresetn, tvalid;
    wire [7:0] tdata;

    integer counter = 0;
    reg aresetn = 0;

    axis_master uut (aclk, aresetn, tvalid, tready, tdata);

    always @(posedge aclk) begin
    	if (aresetn && tready && tvalid) begin
	    if (counter == 0) assert(tdata ==  19);
	    if (counter == 1) assert(tdata ==  99);
	    if (counter == 2) assert(tdata ==   1);
	    if (counter == 3) assert(tdata == 244);
	    if (counter == 4) assert(tdata == 133);
	    if (counter == 5) assert(tdata == 209);
	    if (counter == 6) assert(tdata == 241);
	    if (counter == 7) assert(tdata == 137);
	    if (counter == 8) assert(tdata == 176);
	    if (counter == 9) assert(tdata ==   6);
	    counter <= counter + 1;
	end
	aresetn <= 1;
    end
endmodule
Listing 91 test.ys
read_verilog -sv axis_master.v axis_test.v
hierarchy -top axis_test

proc; flatten;;
sat -seq 50 -prove-asserts

Result with unmodified axis_master.v:

Solving problem with 159344 variables and 442126 clauses..
SAT proof finished - model found: FAIL!

Result with fixed axis_master.v:

Solving problem with 159144 variables and 441626 clauses..
SAT proof finished - no model found: SUCCESS!

Witness framework and per-property tracking

When using AIGER-based formal verification flows (such as the abc engine in SBY), Yosys provides infrastructure for tracking individual formal properties through the verification pipeline.

The rename -witness pass assigns public names to all cells that participate in the witness framework:

These public names allow downstream tools to refer to individual properties by their hierarchical path rather than by anonymous internal identifiers.

The write_aiger -ywmap option generates a map file for conversion to and from Yosys witness traces, and also allows for mapping AIGER bad-state properties and invariant constraints back to individual formal properties by name. This enables features like per-property pass/fail reporting (e.g. abc pdr with --keep-going mode).

The write_smt2 backend similarly uses the public witness names when emitting SMT2 comments. Cells whose hdlname attribute contains the _witness_ marker are treated as having private names for comment purposes, keeping solver output clean.