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

Simulation model (verilog)

Listing 228 simlib.v

module \$allconst (Y);

    parameter WIDTH = 0;

    output [WIDTH-1:0] Y;

    assign Y = 'bx;

endmodule

yosys> help $allseq

Simulation model (verilog)

Listing 229 simlib.v

module \$allseq (Y);

    parameter WIDTH = 0;

    output [WIDTH-1:0] Y;

    assign Y = 'bx;

endmodule

yosys> help $anyconst

Simulation model (verilog)

Listing 230 simlib.v

module \$anyconst (Y);

    parameter WIDTH = 0;

    output [WIDTH-1:0] Y;

    assign Y = 'bx;

endmodule

yosys> help $anyinit

Simulation model (verilog)

Listing 231 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

Simulation model (verilog)

Listing 232 simlib.v

module \$anyseq (Y);

    parameter WIDTH = 0;

    output [WIDTH-1:0] Y;

    assign Y = 'bx;

endmodule

yosys> help $assert

Simulation model (verilog)

Listing 233 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

Simulation model (verilog)

Listing 234 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

Simulation model (verilog)

Listing 235 simlib.v

module \$cover (A, EN);

    input A, EN;

endmodule

yosys> help $equiv

Simulation model (verilog)

Listing 236 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

Simulation model (verilog)

Listing 237 simlib.v

module \$fair (A, EN);

    input A, EN;

endmodule

yosys> help $ff

Simulation model (verilog)

Listing 238 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

Simulation model (verilog)

Listing 239 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

Simulation model (verilog)

Listing 240 simlib.v

module \$live (A, EN);

    input A, EN;

endmodule

Formal support cells

yosys> help $future_ff

Simulation model (verilog)

Listing 241 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 242 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 243 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 244 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 245 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