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 Saturating Adder (with a bug)

SystemVerilog Formal Verification

An 8-bit saturating adder that misses some overflows. An immediate and a clocked assertion find it in the first step.

Open in IDE
design.sv
// SVA form of the properties (used by commercial formal tools):
//   always_comb a_sat_imm: assert (y >= a && y >= b);
//   a_sat: assert property (@(posedge clk) y >= a && y >= b);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module sat_add (input clk, input [7:0] a, input [7:0] b,
                output [7:0] y, output reg [7:0] q);
  // saturating add: a + b, or 255 if the sum does not fit in 8 bits
  assign y = (a[7] & b[7]) ? 8'd255 : a + b;   // bug: misses overflows like 200 + 100
  always @(posedge clk) q <= y;

`ifdef FORMAL
  // immediate assertion on the combinational output
  always @(*) assert (y >= a && y >= b);
  // the same rule, checked only at the clock edge (the lab form of a concurrent assertion)
  always @(posedge clk) assert (y >= a && y >= b);
`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.