Widths, Signedness and Initial State

On this page

Part 3 of 10, lesson 4 of 19Property Development and ConstraintsAll levels

Why it matters

Two properties can look identical and differ in one width. A 200 + 100 sum wraps to 44 in eight bits, so a check written in eight bits agrees with the design and proves nothing. A comparison made on an unsigned view reads -5 as 251, so a negative input is not below the bound. A counter that leans on an initial value passes where the flow honours it and fails where it does not. Job of this lesson: three bug-and-fix pairs, each run.

The core idea

The property computes in the mathematics of the specification, not in the truncated arithmetic of the implementation: widen the expected sum by one bit, declare signedness as the specification does, and start from a reset you assume, not from an initial value you hope is honoured. Context decides width in Verilog: (a + b) > 8'd255 is evaluated in eight bits and is never true. Check reset values in the cycle after a reset edge, never behind a reset disable.

Trap	What passes wrongly	Fix
Narrow expression	8-bit sum compared in 8 bits: wrap agrees with wrap	Expect `{1'b0, a} + {1'b0, b}` in 9 bits
Unsigned view of a signed value	-5 reads as 251, above the bound	Declare the input signed in the property
Initial value instead of reset	Passes where an initial value is honoured	Reset every control register, assume the reset at step 0

Worked example 1: the overflow flag

A registered adder sets ovf when the true sum exceeds 255. The faulty one computes the flag in eight bits. The 9-bit specification proves on the good design and fails on the faulty one at step 3 (depth 4; depth 3 passes). The narrow specification, which copies the wrap, passes on the faulty design and fails on the good one:

wsum.sv

// formal: prove 4 expect pass slang top wsum
`define FORMAL
// wsum: registered 8-bit adder with an overflow flag. BUG=1 computes the flag in 8 bits, so it never sets.
// NARROW=1 swaps the specification for one written in the design's own 8-bit arithmetic.
module wsum #(parameter BUG = 0, parameter NARROW = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  output reg  [7:0] s,
  output reg        ovf
);
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; ovf <= 1'b0; end
    else begin
      s   <= a + b;
      ovf <= (BUG == 1) ? ((a + b) > 8'd255) : (({1'b0, a} + {1'b0, b}) > 9'd255);
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [7:0] pa, pb;
  always @(posedge clk) begin pa <= a; pb <= b; end
  wire [8:0] wide = {1'b0, pa} + {1'b0, pb};          // the specification's sum: 9 bits, no wrap
  generate if (NARROW) begin : g_narrow
    // the same flag, specified in 8-bit arithmetic: it copies the design's own wrap
    always @(posedge clk) if (!init && !$past(rst)) a_ovf_narrow: assert (ovf == ((pa + pb) > 8'd255));
  end else begin : g_wide
    always @(posedge clk) if (!init && !$past(rst)) begin
      a_ovf: assert (ovf == (wide > 9'd255));
      a_sum: assert (s == wide[7:0]);
    end
  end endgenerate
  always @(posedge clk) if (!init && !$past(rst)) c_ovf: cover (ovf);
`endif
endmodule

wsum.sv

// formal: bmc 4 expect fail slang top wsum define BUG=1
`define FORMAL
// wsum: registered 8-bit adder with an overflow flag. BUG=1 computes the flag in 8 bits, so it never sets.
// NARROW=1 swaps the specification for one written in the design's own 8-bit arithmetic.
module wsum #(parameter BUG = 0, parameter NARROW = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  output reg  [7:0] s,
  output reg        ovf
);
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; ovf <= 1'b0; end
    else begin
      s   <= a + b;
      ovf <= (BUG == 1) ? ((a + b) > 8'd255) : (({1'b0, a} + {1'b0, b}) > 9'd255);
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [7:0] pa, pb;
  always @(posedge clk) begin pa <= a; pb <= b; end
  wire [8:0] wide = {1'b0, pa} + {1'b0, pb};          // the specification's sum: 9 bits, no wrap
  generate if (NARROW) begin : g_narrow
    // the same flag, specified in 8-bit arithmetic: it copies the design's own wrap
    always @(posedge clk) if (!init && !$past(rst)) a_ovf_narrow: assert (ovf == ((pa + pb) > 8'd255));
  end else begin : g_wide
    always @(posedge clk) if (!init && !$past(rst)) begin
      a_ovf: assert (ovf == (wide > 9'd255));
      a_sum: assert (s == wide[7:0]);
    end
  end endgenerate
  always @(posedge clk) if (!init && !$past(rst)) c_ovf: cover (ovf);
`endif
endmodule

wsum.sv

// formal: prove 6 expect pass slang top wsum define BUG=1 define NARROW=1
`define FORMAL
// wsum: registered 8-bit adder with an overflow flag. BUG=1 computes the flag in 8 bits, so it never sets.
// NARROW=1 swaps the specification for one written in the design's own 8-bit arithmetic.
module wsum #(parameter BUG = 0, parameter NARROW = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  output reg  [7:0] s,
  output reg        ovf
);
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; ovf <= 1'b0; end
    else begin
      s   <= a + b;
      ovf <= (BUG == 1) ? ((a + b) > 8'd255) : (({1'b0, a} + {1'b0, b}) > 9'd255);
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [7:0] pa, pb;
  always @(posedge clk) begin pa <= a; pb <= b; end
  wire [8:0] wide = {1'b0, pa} + {1'b0, pb};          // the specification's sum: 9 bits, no wrap
  generate if (NARROW) begin : g_narrow
    // the same flag, specified in 8-bit arithmetic: it copies the design's own wrap
    always @(posedge clk) if (!init && !$past(rst)) a_ovf_narrow: assert (ovf == ((pa + pb) > 8'd255));
  end else begin : g_wide
    always @(posedge clk) if (!init && !$past(rst)) begin
      a_ovf: assert (ovf == (wide > 9'd255));
      a_sum: assert (s == wide[7:0]);
    end
  end endgenerate
  always @(posedge clk) if (!init && !$past(rst)) c_ovf: cover (ovf);
`endif
endmodule

wsum.sv

// formal: bmc 6 expect fail slang top wsum define NARROW=1
`define FORMAL
// wsum: registered 8-bit adder with an overflow flag. BUG=1 computes the flag in 8 bits, so it never sets.
// NARROW=1 swaps the specification for one written in the design's own 8-bit arithmetic.
module wsum #(parameter BUG = 0, parameter NARROW = 0) (
  input  wire       clk,
  input  wire       rst,
  input  wire [7:0] a,
  input  wire [7:0] b,
  output reg  [7:0] s,
  output reg        ovf
);
  always @(posedge clk) begin
    if (rst) begin s <= 8'd0; ovf <= 1'b0; end
    else begin
      s   <= a + b;
      ovf <= (BUG == 1) ? ((a + b) > 8'd255) : (({1'b0, a} + {1'b0, b}) > 9'd255);
    end
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg [7:0] pa, pb;
  always @(posedge clk) begin pa <= a; pb <= b; end
  wire [8:0] wide = {1'b0, pa} + {1'b0, pb};          // the specification's sum: 9 bits, no wrap
  generate if (NARROW) begin : g_narrow
    // the same flag, specified in 8-bit arithmetic: it copies the design's own wrap
    always @(posedge clk) if (!init && !$past(rst)) a_ovf_narrow: assert (ovf == ((pa + pb) > 8'd255));
  end else begin : g_wide
    always @(posedge clk) if (!init && !$past(rst)) begin
      a_ovf: assert (ovf == (wide > 9'd255));
      a_sum: assert (s == wide[7:0]);
    end
  end endgenerate
  always @(posedge clk) if (!init && !$past(rst)) c_ovf: cover (ovf);
`endif
endmodule

The third run is the false pass: the faulty flag proves against a specification written in the same eight bits. The fourth shows that specification cannot be right: it fails on the good adder.

Worked example 2: signedness

A flag marks a signed input below 10. The faulty version compares an unsigned view, so every negative input reads as at least 128. The signed specification fails on it at step 3; a specification written with the same unsigned view proves it.

lowflag.sv

// formal: prove 4 expect pass slang top lowflag
`define FORMAL
// lowflag: flags a signed 8-bit input that is below 10. BUG=1 compares it as unsigned, so negative inputs read as large.
// UNSIGNED=1 swaps the specification for one written with an unsigned view of the input.
module lowflag #(parameter BUG = 0, parameter UNSIGNED = 0) (
  input  wire              clk,
  input  wire              rst,
  input  wire signed [7:0] x,
  output reg               low
);
  always @(posedge clk) begin
    if (rst) low <= 1'b0;
    else     low <= (BUG == 1) ? ($unsigned(x) < 8'd10) : (x < 8'sd10);
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg signed [7:0] px;
  always @(posedge clk) px <= x;
  generate if (UNSIGNED) begin : g_u
    always @(posedge clk) if (!init && !$past(rst)) a_low_unsigned: assert (low == ($unsigned(px) < 8'd10));
  end else begin : g_s
    always @(posedge clk) if (!init && !$past(rst)) a_low: assert (low == (px < 8'sd10));
  end endgenerate
  always @(posedge clk) if (!init && !$past(rst)) c_neg: cover (low && px[7]);
`endif
endmodule

lowflag.sv

// formal: bmc 4 expect fail slang top lowflag define BUG=1
`define FORMAL
// lowflag: flags a signed 8-bit input that is below 10. BUG=1 compares it as unsigned, so negative inputs read as large.
// UNSIGNED=1 swaps the specification for one written with an unsigned view of the input.
module lowflag #(parameter BUG = 0, parameter UNSIGNED = 0) (
  input  wire              clk,
  input  wire              rst,
  input  wire signed [7:0] x,
  output reg               low
);
  always @(posedge clk) begin
    if (rst) low <= 1'b0;
    else     low <= (BUG == 1) ? ($unsigned(x) < 8'd10) : (x < 8'sd10);
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg signed [7:0] px;
  always @(posedge clk) px <= x;
  generate if (UNSIGNED) begin : g_u
    always @(posedge clk) if (!init && !$past(rst)) a_low_unsigned: assert (low == ($unsigned(px) < 8'd10));
  end else begin : g_s
    always @(posedge clk) if (!init && !$past(rst)) a_low: assert (low == (px < 8'sd10));
  end endgenerate
  always @(posedge clk) if (!init && !$past(rst)) c_neg: cover (low && px[7]);
`endif
endmodule

lowflag.sv

// formal: prove 6 expect pass slang top lowflag define BUG=1 define UNSIGNED=1
`define FORMAL
// lowflag: flags a signed 8-bit input that is below 10. BUG=1 compares it as unsigned, so negative inputs read as large.
// UNSIGNED=1 swaps the specification for one written with an unsigned view of the input.
module lowflag #(parameter BUG = 0, parameter UNSIGNED = 0) (
  input  wire              clk,
  input  wire              rst,
  input  wire signed [7:0] x,
  output reg               low
);
  always @(posedge clk) begin
    if (rst) low <= 1'b0;
    else     low <= (BUG == 1) ? ($unsigned(x) < 8'd10) : (x < 8'sd10);
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  reg signed [7:0] px;
  always @(posedge clk) px <= x;
  generate if (UNSIGNED) begin : g_u
    always @(posedge clk) if (!init && !$past(rst)) a_low_unsigned: assert (low == ($unsigned(px) < 8'd10));
  end else begin : g_s
    always @(posedge clk) if (!init && !$past(rst)) a_low: assert (low == (px < 8'sd10));
  end endgenerate
  always @(posedge clk) if (!init && !$past(rst)) c_neg: cover (low && px[7]);
`endif
endmodule

Worked example 3: initial state

A 0 to 9 counter with no reset leans on a declared initial value. In this flow the initial value is honoured, so the range property proves; remove the initial value, as a flow that ignores it would, and the start state is arbitrary: the property fails at step 1. The fix is the reset the harness assumes. Only the harness register init relies on an initial value, by design.

decade.sv

// formal: prove 4 expect pass slang top decade define INITV=1 define RST=0
`define FORMAL
// decade: a 0..9 counter. INITV=1 gives it a declared initial value and no reset (it leans on the initial value);
// RST=1 gives it a synchronous reset. With both off the start value is arbitrary.
module decade #(parameter INITV = 0, parameter RST = 1) (
  input  wire clk,
  input  wire rst,
  input  wire en
);
  reg [3:0] cnt;
  generate if (INITV) begin : g_i
    initial cnt = 4'd0;
  end endgenerate
  always @(posedge clk) begin
    if (RST && rst) cnt <= 4'd0;
    else if (en) cnt <= (cnt == 4'd9) ? 4'd0 : cnt + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_range: assert (cnt <= 4'd9);
`endif
endmodule

decade.sv

// formal: bmc 4 expect fail slang top decade define INITV=0 define RST=0
`define FORMAL
// decade: a 0..9 counter. INITV=1 gives it a declared initial value and no reset (it leans on the initial value);
// RST=1 gives it a synchronous reset. With both off the start value is arbitrary.
module decade #(parameter INITV = 0, parameter RST = 1) (
  input  wire clk,
  input  wire rst,
  input  wire en
);
  reg [3:0] cnt;
  generate if (INITV) begin : g_i
    initial cnt = 4'd0;
  end endgenerate
  always @(posedge clk) begin
    if (RST && rst) cnt <= 4'd0;
    else if (en) cnt <= (cnt == 4'd9) ? 4'd0 : cnt + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_range: assert (cnt <= 4'd9);
`endif
endmodule

decade.sv

// formal: prove 4 expect pass slang top decade define INITV=0 define RST=1
`define FORMAL
// decade: a 0..9 counter. INITV=1 gives it a declared initial value and no reset (it leans on the initial value);
// RST=1 gives it a synchronous reset. With both off the start value is arbitrary.
module decade #(parameter INITV = 0, parameter RST = 1) (
  input  wire clk,
  input  wire rst,
  input  wire en
);
  reg [3:0] cnt;
  generate if (INITV) begin : g_i
    initial cnt = 4'd0;
  end endgenerate
  always @(posedge clk) begin
    if (RST && rst) cnt <= 4'd0;
    else if (en) cnt <= (cnt == 4'd9) ? 4'd0 : cnt + 4'd1;
  end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (!init) a_range: assert (cnt <= 4'd9);
`endif
endmodule

example.py

# Exhaustive over every pair of eight-bit operands: where does a specification differ from the design flag?
def flag(a, b, bits):                        # sum compared with 255 in a given width
    return ((a + b) & ((1 << bits) - 1)) > 255

def disagreements(design_bits, spec_bits):
    return sum(flag(a, b, design_bits) != flag(a, b, spec_bits) for a in range(256) for b in range(256))

assert (200 + 100) & 0xFF == 44 and 200 + 100 == 300       # the example in the text
assert disagreements(9, 9) == 0                            # a correct 9-bit flag against the 9-bit specification: no fault visible
assert disagreements(8, 9) == 32640                        # the faulty flag disagrees on every pair that overflows
assert disagreements(8, 8) == 0                            # the narrow specification copies the wrap: the fault is invisible to it
assert disagreements(9, 8) == 32640                        # and it fails the good adder, which is why the fourth run fails
signed_low = lambda x: x < 10
unsigned_low = lambda x: (x & 0xFF) < 10
assert sum(signed_low(x) != unsigned_low(x) for x in range(-128, 128)) == 128   # every negative input is misread
# the check can fail: a specification one bit narrower than the sum hides a fault the wider one finds
try:
    assert disagreements(8, 8) > 0
    raise SystemExit("FAIL: the narrow specification was expected to be blind")
except AssertionError:
    pass
print("PASS: the 8-bit specification is blind on all 32640 overflowing pairs; the 9-bit one sees every one")

What a reviewer looks for

Every expectation that can overflow is written one bit wider than the design; signedness is declared, not inherited.
No property depends on an initial value; reset values are checked in the cycle after reset, with the previous-reset guard.
Each trap above has a run that fails: a width, a sign and an initial-state fault.

Verify and debug

Drive each input to all ones, all zeros and the most negative value; extremes are where a narrow property first lies. If a transition property fails only in the first two cycles, its history guard reads the reset cycle as normal history.

Check yourself The narrow specification proves the faulty adder. What does that tell you about the proof?

It proves the design agrees with itself. The expectation was computed in the design's own truncated arithmetic, so it could not disagree. The good adder failing the same specification is the tell.

Navigate

Why it matters

The core idea

Worked example 1: the overflow flag

Worked example 2: signedness

Worked example 3: initial state

What a reviewer looks for

Verify and debug

Related topics

Widths, Signedness and Initial State

Why it matters

The core idea

Worked example 1: the overflow flag

Worked example 2: signedness

Worked example 3: initial state

What a reviewer looks for

Verify and debug

Related topics

Why it matters

The core idea

Worked example 1: the overflow flag

Worked example 2: signedness

Worked example 3: initial state

What a reviewer looks for

Verify and debug

Related topics

Up next

Why it matters

The core idea

Worked example 1: the overflow flag

Worked example 2: signedness

Worked example 3: initial state

What a reviewer looks for

Verify and debug

Related topics

Up next