Data Integrity Properties

Control properties check that signals behave: counts stay in range, handshakes are held. Data integrity properties check what the design is for: every word that goes in comes out, unchanged, in the right order. They are harder to write, because a FIFO or a pipeline can hold many words at once. This article shows the standard formal technique for them, the tracked value, also called the magic value, and uses it to find a FIFO bug that every count-based check misses.

11 min read | Intermediate

What You'll Learn

• Explain why data integrity needs more than control properties
• Check a fixed-latency pipeline with $past(data, N)
• Follow one freely chosen value through a FIFO with the tracked value technique
• Find a write-pointer bug that leaves the count of a FIFO correct

The Simple Case: Fixed Latency

When a block always takes the same number of cycles, data integrity is one line. A pipeline with two register stages must output what it received two cycles earlier:

a_pipe: assert property (@(posedge clk) disable iff (rst) ##2 dout == $past(din, 2));

With a valid signal, the rule only applies to valid words: out_valid |-> dout == $past(din, 2). In the lab form this is if (...) assert (dout == $past(din, 2)); with the usual reset guards for two cycles of history.

Many blocks are not that simple. A FIFO holds a word for as long as the reader is busy, so the delay between input and output depends on the traffic. $past with a fixed number of cycles cannot describe that.

The Idea of the Tracked Value

A simulation scoreboard keeps a copy of every word in a queue and compares each output with the oldest copy. A formal tool cannot keep an unbounded queue, and it does not need to. It is enough to follow a single word, as long as the tool may choose which word.

• Declare a value magic that the tool chooses freely at the start and that never changes.
• When magic is pushed for the first time, record how many words are in front of it.
• On every pop, lower that number by 1.
• When the number is 0 and a pop happens, the word that comes out must be magic.

Because the tool chooses magic and the inputs freely, it effectively tries every data value in every position. If any word could be lost, overwritten, duplicated or reordered, there is a choice of magic and inputs that shows it. One small counter replaces a full scoreboard.

The Design: a 4-Entry FIFO

The FIFO stores up to 4 bytes in a small memory, with a write pointer, a read pointer and a count. A push writes at wptr, a pop reads at rptr:

module fifo4 (input clk, input rst,
              input push, input [7:0] din, input pop,
              output [7:0] dout, output full, output empty);
  reg [7:0] mem [0:3];
  reg [1:0] wptr, rptr;
  reg [2:0] count;
  assign full  = (count == 3'd4);
  assign empty = (count == 3'd0);
  assign dout  = mem[rptr];
  wire do_push = push && !full;
  wire do_pop  = pop && !empty;
  always @(posedge clk)
    if (rst) begin
      wptr <= 2'd0; rptr <= 2'd0; count <= 3'd0;
    end else begin
      if (do_push) mem[wptr] <= din;
      if (do_push && !do_pop) wptr <= wptr + 2'd1;   // bug: should be if (do_push)
      if (do_pop)  rptr <= rptr + 2'd1;
      count <= count + do_push - do_pop;
    end
endmodule

The designer treated a push and a pop in the same cycle as "nothing changes", which is true for the count but not for the pointers. When both happen, the word is written but the write pointer does not move, so the next push overwrites it.

The Tracked Value in SVA

The tracking logic is ordinary RTL. Only the final check is an assertion. In SVA flows, magic is often an undriven signal that the tool may set freely, with an assumption that keeps it constant:

m_magic: assume property (@(posedge clk) $stable(magic));
a_order: assert property (@(posedge clk) disable iff (rst)
                          tracking && ahead == 3'd0 && do_pop |-> dout == magic);

Here tracking is 1 while magic is inside the FIFO and ahead is the number of words in front of it, both computed by the helper logic below.

Running It in ChipVerify Lab

Yosys has a direct way to declare a value that the tool chooses once and keeps: the attribute (* anyconst *). The whole check:

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(posedge clk) if (!init) assert (count <= 3'd4);

  // tracked value: one word, chosen freely by the tool, followed through the FIFO
  (* anyconst *) reg [7:0] magic;
  reg       tracking = 1'b0;   // magic is inside the FIFO
  reg       done     = 1'b0;   // magic has already been through once
  reg [2:0] ahead;             // number of words in front of magic
  always @(posedge clk)
    if (rst) begin
      tracking <= 1'b0; done <= 1'b0;
    end else if (!tracking && !done && do_push && din == magic) begin
      tracking <= 1'b1;
      ahead    <= count - do_pop;
    end else if (tracking && do_pop) begin
      if (ahead == 3'd0) begin tracking <= 1'b0; done <= 1'b1; end
      else               ahead <= ahead - 3'd1;
    end
  // when magic reaches the head of the FIFO and is popped, the output is magic
  always @(posedge clk) if (!init && !rst && tracking && ahead == 3'd0 && do_pop) assert (dout == magic);
`endif

Two details matter. When magic is pushed in the same cycle as a pop, one of the words in front leaves at once, so ahead starts at count - do_pop. And only the first push of magic is tracked. If the same value is pushed again later, the first copy still comes out first, so the check stays correct.

The run fails at step 5. The tool chose magic = 255:

In step 1, 127 is pushed into slot 0. In step 2, 255 is pushed while 127 is popped: 255 goes into slot 1, but the write pointer stays at 1. In step 3, the next push writes 0 into slot 1, overwriting 255. In step 4, 255 should come out, but dout is 0. The word was lost.

The count assertion passes on this trace, and it passes on the buggy FIFO at any depth: the count is updated correctly, only the data is wrong. Remove the tracked value and the run is a clean PASS. With the fix, if (do_push) wptr <= wptr + 2'd1;, the full check passes.

Common Mistakes