Lesson 7.4 · Formal Apps for Everyday Problems

Reusable protocol checkers

Interface protocols — valid/ready streams, request/acknowledge, credit-based links, standard on-chip buses — appear on many blocks. Writing their rules once, as a reusable checker, pays off in three ways:

When verifying the block that drives the interface, the rules are assertions.
When verifying the block that receives it, the same rules become assumptions about its inputs.
In simulation, all rules are checked as assertions everywhere.

Because the same rule text is asserted on one side and assumed on the other, the assumption is backed by a proof — the assume-guarantee idea you will meet again in Chapter 10.

vr_checker.sv

// vr_checker.sv — valid/ready stream rules, usable from either side
//   SRC_IS_DUT = 1 : the design under test drives valid/data  -> source rules asserted
//   SRC_IS_DUT = 0 : the design under test drives ready        -> source rules assumed
module vr_checker #(
  parameter int W          = 8,
  parameter bit SRC_IS_DUT = 1'b1,
  parameter int MAX_STALL  = 8      // sink must accept within this many cycles
) (
  input logic         clk,
  input logic         rst,
  input logic         valid,
  input logic         ready,
  input logic [W-1:0] data
);
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  // Source-side rules
  property p_valid_held;  valid && !ready |=> valid;            endproperty
  property p_data_stable; valid && !ready |=> $stable(data);    endproperty
  // Sink-side rule
  property p_no_long_stall; valid |-> ##[0:MAX_STALL-1] ready;  endproperty

  if (SRC_IS_DUT) begin : g_dut_is_source
    a_valid_held:    assert property (p_valid_held);
    a_data_stable:   assert property (p_data_stable);
    m_no_long_stall: assume property (p_no_long_stall);
  end else begin : g_dut_is_sink
    m_valid_held:    assume property (p_valid_held);
    m_data_stable:   assume property (p_data_stable);
    a_no_long_stall: assert property (p_no_long_stall);
  end

  c_stall_then_accept: cover property (valid && !ready ##1 valid && ready);
  c_back_to_back:      cover property (valid && ready ##1 valid && ready);
endmodule

instantiating the checker

// Using the checker in a pipeline stage's formal wrapper: DUT is the sink on its input, the source on its output
vr_checker #(.W(8), .SRC_IS_DUT(1'b0)) u_in_chk  (.clk, .rst, .valid(in_valid),  .ready(in_ready),  .data(in_data));
vr_checker #(.W(8), .SRC_IS_DUT(1'b1)) u_out_chk (.clk, .rst, .valid(out_valid), .ready(out_ready), .data(out_data));