Symbolic Values and Data Independence

Many designs repeat the same logic for many channels, lanes, entries or addresses. Writing the same property eight times is tedious, and checking eight copies makes the run larger. A symbolic value lets you write the property once, for one index that the tool chooses freely. Because the tool can pick any index, one property covers all of them. This article applies the idea to an 8-channel interrupt controller and finds a bug that only affects one channel.

8 min read | Intermediate

What You'll Learn

• Use a symbolic index to check every channel of a design with one property
• Explain why a freely chosen constant covers all values
• Recognize data independence and use it to shrink data widths
• Find a cross-channel bug in an interrupt controller

Symbolic Constants

A symbolic constant is a value that the tool chooses at the start of a run and keeps for the whole run. You have already used two: the tracked value magic in the data integrity article, and the tracked address ta in the register file article. The same trick works for any index.

The reasoning is always the same. The property must hold for every value of the constant. If it fails for any value, the tool can choose that value and show the failure. So one property with a symbolic index is as strong as one property per index.

In the lab, symbolic constants are declared with (* anyconst *). In SVA flows, they are undriven inputs with an assumption that keeps them stable, assume property (@(posedge clk) $stable(ch));.

The Design: an Interrupt Controller

Eight peripherals signal interrupts with a one-cycle pulse on irq[i]. The controller sets pending[i], and the processor clears it with an acknowledge carrying the channel number:

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);
  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
endmodule

The bug is planted in one channel: acknowledging channel 4 also clears channel 5, as a copy-and-paste error in a hand-written decoder would. A lost interrupt is one of the worst bugs a system can have, and a test that never has channels 4 and 5 pending together will not see it.

One Property for Eight Channels

`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

The run fails at step 4, with the tool's choice ch = 5. Interrupts arrive on channels 4 and 5 together in step 1 (irq = 0011_0000), both are pending in step 2, the processor acknowledges channel 4 in step 2, and in step 3 both pending bits are gone. Channel 5's interrupt was lost.

Data Independence

Many blocks only move data around without looking at it: FIFOs, buffers, crossbars, register files. Their control never depends on the data values. For such blocks, a check with a tracked value does not need wide data: whether the data is 1 bit or 64 bits, the control behaves the same, and the tracked value catches loss, duplication and reordering as long as it can be told apart from other words.

That is why the FIFO checks in this tutorial use 8-bit data, and why the shrinking the problem article can cut the width further. Be careful with blocks that do look at the data, such as a packet parser or an ECC unit: there, the data width is part of the behavior.

Running It in ChipVerify Lab

The example below is the buggy controller with the symbolic-channel properties. It fails at step 4 with ch = 5.

Common Mistakes