Formal verification cells

Note

Some front-ends may not support the generic $check cell, in such cases calling chformal -lower will convert each $check cell into it’s equivalent. See chformal for more.

yosys> help $allconst

Properties:

is_evaluable

Simulation model (verilog)

Listing 214 simlib.v

module \$allconst (Y);

    parameter WIDTH = 0;

    output [WIDTH-1:0] Y;

    assign Y = 'bx;

endmodule

yosys> help $allseq

Properties:

is_evaluable

Simulation model (verilog)

Listing 215 simlib.v

module \$allseq (Y);

    parameter WIDTH = 0;

    output [WIDTH-1:0] Y;

    assign Y = 'bx;

endmodule

yosys> help $anyconst

Properties:

is_evaluable

Simulation model (verilog)

Listing 216 simlib.v

module \$anyconst (Y);

    parameter WIDTH = 0;

    output [WIDTH-1:0] Y;

    assign Y = 'bx;

endmodule

yosys> help $anyinit

Simulation model (verilog)

Listing 217 simlib.v

module \$anyinit (D, Q);

    parameter WIDTH = 0;

    input [WIDTH-1:0] D;
    output reg [WIDTH-1:0] Q;

    initial Q <= 'bx;

    always @(`SIMLIB_GLOBAL_CLOCK) begin
        Q <= D;
    end

endmodule

yosys> help $anyseq

Properties:

is_evaluable

Simulation model (verilog)

Listing 218 simlib.v

module \$anyseq (Y);

    parameter WIDTH = 0;

    output [WIDTH-1:0] Y;

    assign Y = 'bx;

endmodule

yosys> help $assert

Properties:

is_evaluable

Simulation model (verilog)

Listing 219 simlib.v

module \$assert (A, EN);

    input A, EN;

    `ifndef SIMLIB_NOCHECKS
    always @* begin
        if (A !== 1'b1 && EN === 1'b1) begin
            $display("Assertion %m failed!");
            $stop;
        end
    end
    `endif

endmodule

yosys> help $assume

Properties:

is_evaluable

Simulation model (verilog)

Listing 220 simlib.v

module \$assume (A, EN);

    input A, EN;

    `ifndef SIMLIB_NOCHECKS
    always @* begin
        if (A !== 1'b1 && EN === 1'b1) begin
            $display("Assumption %m failed!");
            $stop;
        end
    end
    `endif

endmodule

yosys> help $cover

Properties:

is_evaluable

Simulation model (verilog)

Listing 221 simlib.v

module \$cover (A, EN);

    input A, EN;

endmodule

yosys> help $equiv

Properties:

is_evaluable

Simulation model (verilog)

Listing 222 simlib.v

module \$equiv (A, B, Y);

    input A, B;
    output Y;

    assign Y = (A !== 1'bx && A !== B) ? 1'bx : A;

    `ifndef SIMLIB_NOCHECKS
    always @* begin
        if (A !== 1'bx && A !== B) begin
            $display("Equivalence failed!");
            $stop;
        end
    end
    `endif

endmodule

yosys> help $fair

Properties:

is_evaluable

Simulation model (verilog)

Listing 223 simlib.v

module \$fair (A, EN);

    input A, EN;

endmodule

yosys> help $ff

Simulation model (verilog)

Listing 224 simlib.v

module \$ff (D, Q);

    parameter WIDTH = 0;

    input [WIDTH-1:0] D;
    output reg [WIDTH-1:0] Q;

    always @(`SIMLIB_GLOBAL_CLOCK) begin
        Q <= D;
    end

endmodule

yosys> help $initstate

Properties:

is_evaluable

Simulation model (verilog)

Listing 225 simlib.v

module \$initstate (Y);

    output reg Y = 1;
    reg [3:0] cnt = 1;
    reg trig = 0;

    initial trig <= 1;

    always @(cnt, trig) begin
        Y <= |cnt;
        cnt <= cnt + |cnt;
    end

endmodule

yosys> help $live

Properties:

is_evaluable

Simulation model (verilog)

Listing 226 simlib.v

module \$live (A, EN);

    input A, EN;

endmodule

Formal support cells

yosys> help $future_ff

Simulation model (verilog)

Listing 227 simlib.v

module \$future_ff (A, Y);

    parameter WIDTH = 0;

    input [WIDTH-1:0] A;
    output [WIDTH-1:0] Y;

    assign Y = A;

endmodule

yosys> help $get_tag

Simulation model (verilog)

Listing 228 simlib.v

module \$get_tag (A, Y);

    parameter TAG = "";
    parameter WIDTH = 0;

    input [WIDTH-1:0] A;
    output [WIDTH-1:0] Y;

    assign Y = A;

endmodule

yosys> help $original_tag

Simulation model (verilog)

Listing 229 simlib.v

module \$original_tag (A, Y);

    parameter TAG = "";
    parameter WIDTH = 0;

    input [WIDTH-1:0] A;
    output [WIDTH-1:0] Y;

    assign Y = A;

endmodule

yosys> help $overwrite_tag

Simulation model (verilog)

Listing 230 simlib.v

module \$overwrite_tag (A, SET, CLR);

    parameter TAG = "";
    parameter WIDTH = 0;

    input [WIDTH-1:0] A;
    input [WIDTH-1:0] SET;
    input [WIDTH-1:0] CLR;

endmodule

yosys> help $set_tag

Simulation model (verilog)

Listing 231 simlib.v

module \$set_tag (A, SET, CLR, Y);

    parameter TAG = "";
    parameter WIDTH = 0;

    input [WIDTH-1:0] A;
    input [WIDTH-1:0] SET;
    input [WIDTH-1:0] CLR;
    output [WIDTH-1:0] Y;

    assign Y = A;

endmodule