Assertions for Data Integrity Checks

The Importance of Data Integrity

What do we mean by "data integrity"? In the context of hardware verification, it typically covers a few key properties:

• Data is not lost: A transaction that enters a block must eventually exit.
• Data is not corrupted: The data that exits a block is identical to what entered.
• Data is not reordered (unless allowed): For a protocol like a FIFO, transactions must exit in the same order they entered.
• Data is stable: Control or data signals remain constant during specific operational phases.

To see why this is so critical, let's consider a common design block like a FIFO.

These potential bugs—lost, overwritten, or reordered data—are exactly what data integrity assertions are designed to catch. Let's build the SVA patterns to do just that.

1. Checking Data Stability with $stable

The simplest form of data integrity is stability. You often need to verify that once a transaction starts, its associated control signals, address, or data payload remain constant until the transaction completes.

The SVA system function $stable() is the perfect tool for this. It evaluates to true if its argument has the same value as it did in the previous clock cycle. It's essentially a shorthand for (signal == $past(signal)).

Let's look at a typical bus protocol with a SETUP phase and an ACCESS phase. The rule is that during the ACCESS phase, the bus signals must remain stable.

The property for this check would look something like this:

// Antecedent: The start of the ACCESS phase
sequence s_access_start;
  !pready ##1 pready; 
endsequence

// Consequent: During the ACCESS phase, signals must be stable
property p_access_stability;
  @(posedge pclk)
  s_access_start |=> $stable(paddr) && 
                      $stable(pwdata) && 
                      $stable(psel) && 
                      $stable(pwrite);
endproperty

a_access_stability: assert property (p_access_stability);

This is a clean and declarative way to specify data stability. When an interviewer asks you to verify configuration registers or bus signals during a transfer, $stable() should be your first thought.

2. Verifying No-Corruption in Pipelines

Now for a more complex scenario: data corruption. How do you verify that the data that comes out of a multi-stage pipeline is the same data that went in, especially when multiple transactions can be active at once?

This requires a powerful SVA feature: local variables. A local variable declared within a property is created for each evaluation attempt of that property. This allows us to "tag" a transaction when it starts and use that tag to check for the correct data when it finishes.

Let's apply this to a real-world, pipelined protocol.

The core pattern you just studied is a cornerstone of advanced SVA and a frequent topic in FV interviews. Let's break it down:

1. Tag the Transaction: When a request (REQ) occurs, capture its unique identifier (the value of the request counter req_count) into a local variable.

   (REQ, local_req_id = req_count)
   

2. Specify the Consequent: Imply (|=>) that at some point in the future, a grant (GRA) must occur where the grant counter (gra_count) matches the captured ID.

   |=> ... ##1 (GRA && gra_count == local_req_id)
   

3. Refine with Negative Constraints: As the article shows, you must also specify what should not happen. During the delay between the request and its corresponding grant, no other grant with this ID should appear. This prevents false passes.

   (!GRA || gra_count != local_req_id)[*1:$]
   

This (antecedent, capture_data) |=> (delay_with_constraints) ##1 (consequent && check_data) pattern is incredibly versatile for verifying any pipelined data transfer, from CPU instruction pipelines to network-on-chip packets.

3. Advanced Integrity Checks with Reference Models

What if data isn't just flowing through a pipeline, but is being stored and retrieved from a memory-like structure (a register file, a cache, a reorder buffer)? The time between write and read can be variable and data can be accessed out of order.

For these scenarios, relying solely on local variables within a single property can become difficult. A more scalable approach, fundamental to both formal and simulation-based verification, is to use a reference model. This is auxiliary verification logic that mimics the behavior of the DUT.

In SystemVerilog, an associative array is an excellent tool for building a simple reference model for data storage.

The technique here is a bridge between formal properties and simulation scoreboards:

1. Model the Storage: Create an associative array to act as a "shadow memory".
   int mem_aarray[int]; // Key is address, value is data
2. Update the Model: In your verification environment, whenever a write occurs in the DUT, update the associative array with the same data.
   if (write) mem_aarray[addr] = wdata;
3. Assert on Read: Write a property that, upon a read from the DUT, asserts that the data returned (rddata) matches the data stored in your reference model at that address.
   property p_read_after_write; (read && mem_aarray.exists(addr)) |=> rddata == mem_aarray[addr]; endproperty

This approach elegantly handles variable latency and out-of-order access, making it extremely powerful. Understanding it shows an interviewer you can think about verification architecture, not just SVA syntax.

Conclusion

Today we explored three powerful patterns for verifying data integrity, progressing from simple stability checks to complex, multi-transaction verification. These patterns are the bread and butter of verifying control and datapath logic.

Key Takeaways:

• Data Stability: Use $stable(signal) to assert that a signal does not change during a specific phase. This is perfect for configuration registers and bus protocols.
• Pipelined No-Corruption: Use local variables to "tag" transactions as they enter a pipeline and check that the correct data emerges at the end. This is the go-to pattern for request-grant or valid-ready protocols with overlapping transactions.
• Storage No-Corruption: For memory-like structures, use a reference model (e.g., an associative array) to shadow the DUT's state. Assert that the DUT's output matches the reference model's expected output.

In our next lesson, we will shift focus to liveness properties. We'll learn how to write assertions that guarantee something good eventually happens, such as a request eventually getting a grant, and we'll explore the critical difference between strong and weak properties.

🧠 Interview & Practice Drill

Time to solidify these concepts.

🎤 Interview Drill Section

1. Rapid Fire Theory:

   • What is the difference between $stable(sig) and sig == $past(sig)? (Trick question: they are functionally very similar, but $stable is more declarative).
   • You need to verify a 4-entry FIFO. You write a property with a local variable to check that data pushed in is the same as data popped out. What is a key limitation of this approach if the FIFO depth was 1024 entries?
   • An interviewer asks, "How would you verify data integrity on a bus that can return read data out of order?" Which of the three patterns we discussed is most suitable here? Why?

2. Resume Deep Dive Question:

   • "Looking at your Multi-Client Arbiter project, you verified that requests were granted. How did you verify that the grant was for the correct requesting client? If two clients requested in consecutive cycles, how did your properties distinguish which grant belonged to which request? Walk me through the SVA you would write."

3. Whiteboard Problem:

   • A memory-mapped register REG at address 16'hA004 is writable. The specification says that after a write to this address, a status_done bit should be asserted by the DUT within 1 to 5 clock cycles. The data bus is 32 bits wide.
   • Task: Write a single, robust SVA property to verify that:
     1. When a write occurs to address 16'hA004...
     2. ...the status_done bit goes high within 1 to 5 cycles.
     3. ...the value written to the register is the same value that was on the wdata bus during the write cycle. You will need a way to read back the register value, assume a signal reg_internal_value gives you access to it for verification.

🧩 Coding Exercises

Assume a default clock @(posedge clk).

1. Configuration Stability: A module has a 32-bit configuration register CFG. It is loaded once after reset. A signal cfg_load_done goes high for one cycle when the load is complete. Write an assertion to ensure that after cfg_load_done has occurred, the CFG register never changes its value for the rest of the simulation.

2. Request-Data-Acknowledge: A simple protocol works as follows:

   • A client asserts req.
   • The server asserts ack exactly 2 cycles later.
   • In the cycle that ack is asserted, the server must present the correct data on the rdata bus. The data should be req_id + 10. req_id is an 8-bit bus asserted along with req.
   • Write a property to verify that the rdata is correct when ack is asserted.

3. Write-Read Consistency: You are verifying a simple RAM block.

   • Signals: write_en, read_en, addr (8-bit), wdata (32-bit), rdata (32-bit).
   • For simplicity, a read to an address will always happen at least 4 cycles after a write to the same address. There are no other writes to that same address in between.
   • Write an assertion that verifies if you write data D to address A, a subsequent read from address A returns the same data D.