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 Bug Hunt: five designs

SystemVerilog Formal Verification

Five small designs, each with one bug. Select a top module, write one property in its FORMAL block, and find the bug.

Open in IDE
Related tutorial:
gray.sv
module gray_cnt (input clk, input rst, input en, output [3:0] gray);
  // 4-bit counter with a Gray-coded output: consecutive values differ in exactly one bit
  reg [3:0] bin;
  always @(posedge clk)
    if (rst)     bin <= 4'd0;
    else if (en) bin <= bin + 4'd1;
  assign gray = bin ^ (bin << 1);                 // bug: should be bin ^ (bin >> 1)
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // write your property here
`endif
endmodule
parity.sv
module par_reg (input clk, input rst, input [7:0] d, output reg [7:0] q, output reg p);
  // registers a byte together with its even parity bit
  always @(posedge clk)
    if (rst) begin q <= 8'd0; p <= 1'b0; end
    else     begin q <= d;    p <= ^d[6:0]; end      // bug: bit 7 is missing from the parity
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // write your property here
`endif
endmodule
edge.sv
module rise_det (input clk, input rst, input in, output rise);
  // one-cycle pulse on every rising edge of in
  reg in_d;
  always @(posedge clk) in_d <= rst ? 1'b0 : in;
  assign rise = in ^ in_d;                         // bug: also pulses on falling edges
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // write your property here
`endif
endmodule
updown.sv
module ud_cnt (input clk, input rst, input up, input dn, output reg [3:0] q);
  // up/down counter that saturates at 0 and at 15
  always @(posedge clk)
    if (rst)                    q <= 4'd0;
    else if (up && !dn && q != 4'd15) q <= q + 4'd1;
    else if (dn && !up)               q <= q - 4'd1;   // bug: no check for 0
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // write your property here
`endif
endmodule
oneshot.sv
module one_shot (input clk, input rst, input trig, output reg pulse);
  // a single one-cycle pulse for each rising edge of trig, even if trig stays high
  reg trig_d;
  always @(posedge clk)
    if (rst) begin trig_d <= 1'b0; pulse <= 1'b0; end
    else begin
      trig_d <= trig;
      pulse  <= trig;                               // bug: should be trig && !trig_d
    end
`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // write your property here
`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.