Ready-to-run snippets

Code Examples

Ready-to-run Verilog, SystemVerilog, and UVM examples. Click any to open it live in the IDE.

← All examples

FV X-Propagation: two copies (with a bug)

SystemVerilog Formal Verification

Two copies of a pipeline with independent start values: after reset their outputs must agree. Also a decoder with an unreachable branch (top dec_dead).

Open in IDE
Related tutorial:
dut.sv
module valid_pipe (input clk, input rst, input in_valid, input [7:0] in_data,
                   output out_valid, output [7:0] out_data);
  // two-stage pipeline; the valid bits travel with the data
  reg       v1, v2;
  reg [7:0] d1, d2;
  always @(posedge clk) begin
    if (rst) v1 <= 1'b0;                       // bug: v2 is not reset
    else     v1 <= in_valid;
    v2 <= v1;
    d1 <= in_data;
    d2 <= d1;
  end
  assign out_valid = v2;
  assign out_data  = d2;

endmodule
two.sv
module xprop_two (input clk, input rst, input in_valid, input [7:0] in_data);
  // two copies of the same design, same inputs; registers without a reset start at independent free values
  wire v_a, v_b; wire [7:0] d_a, d_b;
  valid_pipe u_a (.clk(clk), .rst(rst), .in_valid(in_valid), .in_data(in_data), .out_valid(v_a), .out_data(d_a));
  valid_pipe u_b (.clk(clk), .rst(rst), .in_valid(in_valid), .in_data(in_data), .out_valid(v_b), .out_data(d_b));
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // after reset, the start values must not matter: valid outputs agree, and so does valid data
  always @(*) if (!init && !rst) assert (v_a == v_b);
  always @(*) if (!init && !rst && v_a && v_b) assert (d_a == d_b);
`endif
endmodule
dec.sv
// Second example: set Top Module to dec_dead.
module dec_dead (input clk, input rst, input [1:0] op, input [7:0] x, output reg [7:0] y);
  always @(posedge clk)
    if (rst) y <= 8'd0;
    else case (op)
      2'd0: y <= x;
      2'd1: y <= x + 8'd1;
      2'd2: y <= x << 1;
      2'd3: y <= 8'hFF;                       // reserved opcode: upstream never sends it
    endcase

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // environment: opcode 3 is reserved and never sent
  always @(*) assume (op != 2'd3);
  // reachability of each branch, meant to fail when reachable
  always @(*) if (!init && !rst) assert (op != 2'd2);   // branch 2
  always @(*) if (!init && !rst) assert (op != 2'd3);   // branch 3
`endif
endmodule
Admin mode — edit and delete controls are visible on each row. Use the IDE to add new snippets via File → Save as Snippet.