Parameterized SVA for Reusable Verification IP

1. The Foundation: Parameterizing Properties and Modules

The simplest way to make a property reusable is by using arguments. However, the real power comes from packaging these properties inside a parameterized container, like a module.

Let's revisit the robust CDC checker from our previous lesson and make it reusable.

Original Concept (Specific):
A checker for a specific 32-bit bus with a 4-cycle latency.

New Goal (Generic):
A checker for a bus of any WIDTH with any LATENCY.

We can achieve this by wrapping our property in a module that accepts parameters.

// A reusable, parameterized CDC checker module
module cdc_checker #(
  parameter WIDTH   = 32,
  parameter LATENCY = 4
) (
  input                      clk_a,
  input                      clk_b,
  input        [WIDTH-1:0]   data_in,
  input        [WIDTH-1:0]   sync_data_out
);

  // Property to check data integrity across the clock domain
  property p_cdc_data_integrity;
    logic [WIDTH-1:0] temp_data;
    
    @(posedge clk_a)
      // 1. On source clock, detect a change and store the value
      ($changed(data_in), temp_data = data_in) |->
    @(posedge clk_b)
      // 2. Immediately switch to destination clock



      ##[LATENCY] (sync_data_out === temp_data);
      // NOTE: We've simplified the ##[0:1] from last lesson for clarity here,
      // but in a real scenario, you might parameterize that as well.
  endproperty

  a_cdc_check: assert property (p_cdc_data_integrity);

endmodule

This cdc_checker module is now a piece of Verification IP (VIP). You can instantiate it for a 16-bit bus with 2-cycle latency, or an 8-bit bus with 5-cycle latency, just by changing the parameters. But how do we attach this VIP to our design without modifying the design's source code?

2. Attaching Reusable VIP: The bind Construct

The SystemVerilog bind construct is the standard, non-intrusive way to instantiate a module (like our checker) inside another target module or instance in the design hierarchy. This allows you to keep your verification code completely separate from the design code (RTL), which is excellent practice.

After watching the video, let's apply this to our cdc_checker. Imagine our Design Under Test (DUT) is a module named DataCrosser which contains the CDC logic.

// In a separate verification file (e.g., tb_top.sv)
module tb_top;

  // ... DUT instantiation and other testbench components ...

  // Bind our parameterized checker to ALL instances of the DataCrosser module
  bind DataCrosser cdc_checker #(
    .WIDTH   (16),   // Override parameters for this specific bind
    .LATENCY (3)
  ) u_cdc_checker_16b (
    .clk_a         (clk_a),           // Connect checker ports to signals
    .clk_b         (clk_b),           // inside the DataCrosser module
    .data_in       (src_domain_data),
    .sync_data_out (dest_domain_data)
  );

endmodule

With that single bind statement, you've attached your reusable assertion module to every instance of DataCrosser in your design, with the parameters set to a width of 16 and latency of 3. This is incredibly efficient.

3. A Better Container: The checker Construct

While modules work, SystemVerilog introduced the checker construct specifically for packaging assertions. It offers several advantages over using a plain module.

The key takeaways from the paper are that checkers are superior to modules for VIP because they:

• Can infer clock and reset from their context.
• Have more flexible argument types (e.g., can accept sequences/properties as inputs).
• Are more efficient and have cleaner, race-free semantics.
• Have a more concise instantiation syntax.

Here is what a parameterized FIFO check might look like inside a checker:

checker fifo_props #(parameter DEPTH = 16) (
  input logic       clk, rst_n,
  input logic       push, pop,
  input logic       full, empty,
  output logic      overflow_err, underflow_err
);

  default clocking @(posedge clk); endclocking
  default disable iff (!rst_n);

  a_overflow:  assert property (full && push)
    overflow_err = 1'b1; else overflow_err = 1'b0;
    
  a_underflow: assert property (empty && pop)
    underflow_err = 1'b1; else underflow_err = 1'b0;

endchecker

This self-contained, parameterized checker can be bound to any FIFO in your design, providing a clean, reusable verification component.

4. Advanced Scalability for Formal: Symbolic Variables

So far, our parameterization works well for simulation. For formal, however, proving a design with WIDTH=32 does not automatically prove it for WIDTH=64. You would need to run separate formal sessions for each parameter set.

A more powerful technique for formal verification is using symbolic variables. A symbolic variable is a signal whose value is chosen by the formal tool at the beginning of a proof trace but remains constant for the duration of that trace. The tool then implicitly proves the property for all legal values of that symbolic variable.

This is a form of parameterization where the "parameter" is an index or value explored by the tool itself.

Let's apply this concept. Imagine an arbiter with 8 request inputs (req[7:0]) and 8 grant outputs (gnt[7:0]). Instead of writing 8 separate properties, we can write one, using a symbolic variable to represent the request index.

The Symbolic Variable Approach:

1. Declare a free variable: This variable, idx, will be controlled by the formal tool.

   wire [2:0] idx; // Formal tool will drive this
   

2. Constrain its value and make it stable: We tell the tool that idx can be any legal index, but it must not change during the proof trace. This makes it symbolic.

   // Assume idx is stable for the whole trace
   assume property (@(posedge clk) $stable(idx));
   
   // Assume idx is within the valid range (this might be implicit by its width)
   assume property (idx < 8); 
   

3. Write the parameterized property: Now, write the property using idx.

   property p_grant_follows_req;
     $rose(req[idx]) |=> s_eventually $rose(gnt[idx]);
   endproperty
   
   a_arbiter_liveness: assert property (p_grant_follows_req);
   

By proving a_arbiter_liveness once, the formal tool has effectively proven that for any chosen requester i from 0 to 7, if req[i] is asserted, gnt[i] will eventually follow. This is vastly more powerful and scalable than manual parameterization for formal proofs.

The "Elegant" testbench shown in Example 7 of the paper is the ultimate expression of this: it uses multiple symbolic variables (i, j, k) to select an input, bridge, and output channel, allowing a single scoreboard to verify all 256 possible paths through a complex design in one go.

Conclusion

Today we elevated your SVA skills from writing bespoke properties to engineering reusable, scalable Verification IP. This is a critical step toward senior-level competency and a frequent topic in tough interviews.

Key Takeaways:

• Parameterize with parameter: Use parameter in module or checker wrappers to create configurable properties (e.g., for bus widths, latencies).
• Package for Reuse: Encapsulate parameterized properties in modules or, preferably, the modern checker construct.
• Attach Non-Intrusively with bind: Use the bind statement to apply your verification IP to DUT modules without modifying their source code.
• Scale Formal Proofs with Symbolic Variables: For truly scalable formal verification, use symbolic variables (free variables + $stable assumption) to let the tool explore an entire indexed or parameterized space in a single proof.

In our next module, "Applying SVA: Common Protocol Patterns," we will start putting these powerful techniques into practice. The very first lesson will focus on using local variables to track state, a fundamental building block for the complex handshake, FIFO, and arbiter checkers we will be building.

🧠 Interview & Practice Drill

This section will test your ability to apply these professional-grade techniques.

🎤 Interview Drill Section

1. Rapid Fire Theory:

   • An engineer wants to check a property on 100 instances of a module ALU. What is the most efficient way to apply the assertion without modifying the ALU's code?
   • What are two key advantages of using the checker construct over a module for packaging assertions?
   • Explain the concept of a "symbolic variable" in a formal context. How is it different from a regular parameter?
   • You are asked to verify a parameterized FIFO. For the formal proof, what is the main limitation of using a Verilog parameter for the FIFO depth? How would a symbolic variable approach be superior?

2. Resume Deep Dive Question:

   • "Your resume mentions a 'Formal Property Verification of In-House Parity Module' project with 'parameterized checkers'. This is a perfect example. Can you walk me through exactly how you implemented this?
     • Did you use a parameterized module or a checker? Why?
     • Show me the pseudo-code for the container and the parameter for the data width.
     • How did you apply this checker to the Parity Module DUT? Did you use bind?
     • For the formal proof, how did you ensure your verification was complete for all possible data widths supported by the design? Did you use multiple runs, or a more advanced technique like symbolic variables?"

3. Whiteboard Problem:

   • You need to verify a memory controller. The requirement is: "After a read request (rd_req) is issued, the read data valid (rd_vld) must not assert for at least MIN_LATENCY cycles, but must assert no later than MAX_LATENCY cycles."
   • Write a reusable checker named latency_check that takes MIN_LATENCY and MAX_LATENCY as parameters.
   • The checker should take clk, rst_n, rd_req, and rd_vld as inputs.
   • The property should check that rd_vld is low for MIN_LATENCY cycles after rd_req, and then becomes high at some point in the following MAX_LATENCY - MIN_LATENCY cycles.

🧩 Coding Exercises

1. Parameterized Stability Checker:

   • Write a module named stability_checker with a parameter STABLE_CYCLES.
   • It should take clk, rst_n, and a generic data_bus as inputs. The width of data_bus should also be a parameter, WIDTH.
   • Inside, write a property p_is_stable that asserts that if the data_bus is not stable (i.e., $stable(data_bus) is false), it must become stable and remain stable for at least STABLE_CYCLES.
   • Write a bind statement to attach this checker to a module named DataGenerator, connecting the checker's inputs to signals core_clk, core_rst_n, and gen_data[63:0]. Set STABLE_CYCLES to 5 for this binding.

2. Symbolic Variable for Data Integrity:

   • You are verifying a 128-bit data bus (data_bus[127:0]) that passes through a pipeline.
   • Write a formal verification snippet that uses a symbolic variable bit_idx (from 0 to 127) to verify data integrity for any single bit of the bus.
   • The property should state: "The value of data_bus[bit_idx] at the input of the pipeline is the same as the value of data_bus_out[bit_idx] 4 cycles later."
   • Include the declaration of bit_idx and the necessary assume properties to make it a symbolic variable.