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 Interrupt Controller: symbolic channel (with a bug)

SystemVerilog Formal Verification

One property for a channel the tool chooses covers all eight channels and finds the one that loses interrupts.

Open in IDE
design.sv
// SVA flows: ch is an undriven input with  assume property (@(posedge clk) $stable(ch));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module irq8 (input clk, input rst, input [7:0] irq, input ack_en, input [2:0] ack_id,
             output reg [7:0] pending, output any);
  // 8-channel interrupt controller: a pulse on irq[i] sets pending[i]; an ack for channel i clears it
  assign any = |pending;
  integer i;
  always @(posedge clk)
    if (rst) pending <= 8'd0;
    else
      for (i = 0; i < 8; i = i + 1)
        if (irq[i])                                         pending[i] <= 1'b1;
        else if (ack_en && (ack_id == i || (i == 5 && ack_id == 3'd4)))
                                                            pending[i] <= 1'b0;   // bug: an ack for 4 also clears 5

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // one symbolic channel instead of eight copies of every property
  (* anyconst *) reg [2:0] ch;
  // a pending interrupt stays pending until its own ack
  always @(posedge clk)
    if (!init && !$past(rst) && $past(pending[ch]) && !($past(ack_en) && $past(ack_id) == ch))
      assert (pending[ch]);
  // an irq always sets its pending bit
  always @(posedge clk) if (!init && !$past(rst) && $past(irq[ch])) assert (pending[ch]);
`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.