Named & Parameterized Properties

Properties as reusable units

Named sequences and properties accept formal arguments, making them templates rather than one-off checks. Arguments default to untyped — substituted syntactically at elaboration, so an actual can be a signal, an expression, a constant, even a clocking event. You can also type arguments explicitly, and two special types unlock composition: a sequence formal accepts any sequence actual, and a property formal accepts a property — letting you write combinators like "this obligation, but gated and reset-aware". Untyped + defaults covers 90% of practical libraries.

// The workhorse template every team writes:
property req_gets_grant(req, gnt, int min = 1, int max = 4);
  $rose(req) |-> ##[min:max] gnt;
endproperty

// Instantiations across unrelated interfaces:
a_cpu:  assert property (@(posedge clk)  disable iff (!rst_n)
          req_gets_grant(cpu_req,  cpu_gnt));            // defaults 1..4
a_dma:  assert property (@(posedge clk)  disable iff (!rst_n)
          req_gets_grant(dma_req,  dma_gnt, 2, 16));
a_dbg:  assert property (@(posedge dbg_clk) disable iff (!dbg_rst_n)
          req_gets_grant(dbg_req,  dbg_gnt, 1, 64));

Sequence and property arguments

Typed sequence/property formals turn properties into combinators. A classic pair: a window-checker that takes the triggering sequence as an argument, and a wrapper that adds standard reset/enable plumbing around any property your team writes.

// sequence argument: 'trigger' can be ANY sequence
property after_trigger_resp(sequence trigger, resp, int max);
  trigger |-> ##[1:max] resp;
endproperty
a_b2b: assert property (@(posedge clk)
  after_trigger_resp(wr_start ##1 wr_beat [->4], wr_resp, 8));

// property argument: a reusable gating combinator
property gated(property p, en);
  if (en) p;                  // obligation only when enabled
endproperty

// untyped event argument: clock passed in by the caller
property req_gets_grant_clk(clkev, req, gnt, int max = 4);
  @clkev $rose(req) |-> ##[1:max] gnt;
endproperty
a_clk: assert property (req_gets_grant_clk(posedge phy_clk,
                                           phy_req, phy_gnt, 6));

ARGUMENT KINDS — what can be passed

  untyped (default)  signal, expression, constant, clocking event
                     → textual substitution at elaboration
  int / typed        elaboration-time constants for ranges [min:max]
  sequence           any sequence actual → temporal triggers as args
  property           any property actual → combinators / wrappers

  NOT passable: runtime-variable repetition counts —
  ##[min:max] bounds must elaborate to constants.

Local clock vs argument clock

A property can carry its own clock or inherit one. Resolution order at the assertion site: an explicit @(...) inside the property wins; otherwise the clock at the assert statement applies; otherwise an enclosing default clocking block. Library guidance: keep reusable properties CLOCKLESS (and reset-less) and bind clock + disable iff at each assertion site — a property hard-wired to @(posedge clk) cannot be reused on dbg_clk, and a hidden internal clock that differs from the caller's expectation is a notorious source of checks that sample the wrong domain while appearing healthy.

// LIBRARY STYLE — clockless, resetless template:
property handshake(req, gnt, int max);
  $rose(req) |-> ##[1:max] gnt;     // no @, no disable iff
endproperty

// Caller binds environment-specific clock and reset:
a_core: assert property (@(posedge core_clk) disable iff (!core_rst_n)
           handshake(c_req, c_gnt, 4));
a_phy:  assert property (@(posedge phy_clk)  disable iff (!phy_rst_n)
           handshake(p_req, p_gnt, 12));

// ANTI-PATTERN — clock buried in the library property:
property handshake_bad(req, gnt);
  @(posedge clk) $rose(req) |-> ##[1:4] gnt;  // which clk? whose?
endproperty  // silently samples the module-scope clk it elaborated in

Interview angle and review

Interview angle

• "Design a reusable req/gnt property." — they want req_gets_grant(req, gnt, min, max) with $rose, ranged consequent, defaults, and clock/reset bound at the assert site, not inside.

• "What can a property argument be?" — untyped (signals/expressions/clock events), typed constants for ranges, and sequence/property formals for composition; ranges must be elaboration-time constants.

• "How is the clock resolved for a clockless property?" — assert-site clock, else default clocking; explicit internal @ overrides everything.

• "Why keep disable iff out of library properties?" — reset polarity/name differs per environment; bake it in and the library is unusable or, worse, silently wrong.

Key takeaways

• Untyped formals are elaboration-time substitution — signals, expressions, constants, even clock events all pass through.

• sequence/property typed formals enable combinators: triggers, gates, and wrappers as arguments.

• Delay/repetition bounds must be elaboration-time constants — no runtime-variable windows.

• Library discipline: clockless, resetless properties; bind @clock and disable iff at each assertion site.

Common pitfalls

• Hard-wiring @(posedge clk) inside a library property — it silently samples whatever clk was in elaboration scope.

• Trying to pass a runtime variable as a ##[min:max] bound — bounds must be constants; restructure or generate.

• Duplicating the same handshake assertion 12 times with edits instead of parameterizing — divergence bugs during maintenance.

• Forgetting default argument values exist — call sites stuffed with boilerplate constants that drift apart.

• Embedding disable iff (!rst_n) in shared properties used across reset domains — wrong reset gating in half the instances.