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 ALU vs Reference Model (with a bug)

SystemVerilog Formal Verification

An 8-bit ALU whose set-less-than compares unsigned. One assertion against a reference model finds it.

Open in IDE
design.sv
// SVA form: always_comb a_model: assert (y == model);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module alu8 (input [2:0] op, input [7:0] a, input [7:0] b, output reg [7:0] y);
  // ops: 0 add, 1 sub, 2 and, 3 or, 4 xor, 5 shift left by b[2:0], 6 set-less-than (signed), 7 pass b
  always @(*)
    case (op)
      3'd0: y = a + b;
      3'd1: y = a - b;
      3'd2: y = a & b;
      3'd3: y = a | b;
      3'd4: y = a ^ b;
      3'd5: y = a << b[2:0];
      3'd6: y = (a < b) ? 8'd1 : 8'd0;      // bug: compares unsigned, the spec says signed
      default: y = b;
    endcase

`ifdef FORMAL
  // reference model, written independently of the RTL
  reg [7:0] model;
  always @(*) begin
    case (op)
      3'd0: model = a + b;
      3'd1: model = a + ~b + 8'd1;                       // two's complement subtraction
      3'd2: model = ~(~a | ~b);                          // De Morgan
      3'd3: model = ~(~a & ~b);
      3'd4: model = (a | b) & ~(a & b);
      3'd5: model = a * (8'd1 << b[2:0]);                // shift as multiplication
      3'd6: model = ($signed(a) < $signed(b)) ? 8'd1 : 8'd0;
      default: model = b;
    endcase
  end
  always @(*) assert (y == model);
`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.