Datapaths Against a Reference Model

For control logic, properties describe rules: one grant at a time, no overflow. For a datapath such as an ALU, the rule is the whole function: the output must equal the correct result for every input. The standard formal technique is a reference model, a second description of the function written differently from the RTL, and a single assertion that the two agree. This article checks an 8-bit ALU against a model and finds a signed comparison that was implemented as unsigned.

8 min read | Intermediate

What You'll Learn

• Check a datapath against a reference model with one assertion
• Write a reference model that does not copy the RTL
• Find a signed-versus-unsigned comparison bug
• Know when a reference model check is practical and when the width makes it too slow

The Reference Model Check

The same inputs drive the design and the model, and an assertion compares the outputs:

The model is formal-only code, so it can be written for clarity rather than speed or area. Its value comes from being different from the RTL: if it repeats the RTL expression, it repeats its bugs, as the writing good properties article warned. Good models use a different formulation: subtraction as adding the two's complement, AND through De Morgan's law, a shift as a multiplication by a power of two, comparisons with explicit $signed.

The Design: an 8-Bit ALU

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
endmodule

The specification says set-less-than compares signed numbers, as a processor needs for if (x < 0). In Verilog, a < b on unsigned vectors compares them unsigned.

The Model and the Check

`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

In SVA the check is one line, assert property (@(posedge clk) y == model);, or an immediate assertion in always_comb for a purely combinational block. The run fails in step 0 with op = 6, a = 60 and b = 240. As unsigned numbers, 60 is less than 240, so the ALU outputs 1. As signed numbers, 240 is -16, and 60 is not less than -16, so the model outputs 0.

The Fix and the Run Time

The fix is 3'd6: y = ($signed(a) < $signed(b)) ? 8'd1 : 8'd0;. With it the check passes, in under a second on the lab engine. This works well because the ALU is combinational and 8 bits wide: the solver handles adders, logic and shifts of this size easily, and even the multiplication in the model is by a power of two.

A full multiplier or divider, or a 64-bit datapath, is a different story. As the performance article measured, a multiplier comparison stops finishing at about 10 bits. For wide arithmetic, check a narrow version of the datapath against the model, and check the full width by simulation or by equivalence against a trusted implementation.

Running It in ChipVerify Lab

The example below is the buggy ALU with the reference model. Since the block is combinational, any depth finds the bug in step 0.

Common Mistakes