📋 Declaring Named Properties

A property defines a temporal behaviour of the design. It is purely a declaration — on its own it produces no result. It must be used in an assert, assume, or cover statement to have effect.

// Minimal: property with an inline clock and a sequence body
property rule1;
  @(posedge clk) a |-> b ##1 c ##1 d;
endproperty

// With arguments (like a parameterised sequence)
property abc(a, b, c);
  disable iff (a==2) not @(clk) (b ##1 c);
endproperty
// Instantiate with actual args:
env_prop: assert property (abc(rst, in1, in2)) pass_stat else fail_stat;

// With local variables — same syntax as sequences
property e;
  int x;
  (valid_in, (x = pipe_in)) |-> ##5 (pipe_out1 == (x+1));
endproperty

// Where properties can be declared:
// module, interface, program, clocking block, package, compilation-unit scope

📋 Seven Property Kinds

📋 Property Operator Precedence

⛔ disable iff — Asynchronous Reset

disable iff (expr) attaches an asynchronous reset expression to a property. If the reset expression becomes true at any point during a property evaluation, that evaluation is considered to have vacuously passed — not failed. This correctly models hardware where assertions don’t apply during reset.

property rule2;
  @(clkev) disable iff (foo) a |-> not(b ##1 c ##1 d);
endproperty
// While foo is true: all evaluation attempts vacuously pass
// When foo becomes false: evaluation resumes normally

// Practical usage: suppress assertion during reset
// If reset_n is 0 (active-low reset), don't check the property
property req_ack;
  disable iff (!reset_n)
  @(posedge clk) req |-> ##[1:4] ack;
endproperty

→ Implication — |-> and |=>

Implication conditionally evaluates the consequent property only when the antecedent sequence matches. Both forms evaluate vacuously to true when the antecedent does not match.

seq |-> prop

// If seq matches at tick N,
// prop is evaluated starting
// at tick N (the SAME tick as
// the end of seq's match).

seq |=> prop
// Equivalent to:
// seq ##1 'true |-> prop
//
// If seq matches at tick N,
// prop is evaluated starting
// at tick N+1 (one tick after
// the end of seq's match).

Rules for |-> implication

• The antecedent can produce zero, one, or more matches from a given start point.
• If the antecedent produces no match → the implication vacuously passes (returns true).
• For each match of the antecedent, the consequent is separately evaluated starting at the match endpoint.
• The overall implication passes if and only if the consequent passes for every match of the antecedent.

📋 Implication Examples

// Basic: when data_phase is true, irdy and (trdy or stop) must also be true
property data_end;
  @(posedge mclk)
  data_phase |-> ((irdy==0) && ($fell(trdy) || $fell(stop)));
endproperty

// Sequence antecedent: a ##1 b ##1 c must complete, THEN d ##1 e must complete
(a ##1 b ##1 c) |-> (d ##1 e)

// After data_end_exp: frame must rise within 2 ticks, irdy must rise 1 tick later
property data_end_rule1;
  @(posedge mclk)
  'data_end_exp |-> ##[1:2] $rose(frame) ##1 $rose(irdy);
endproperty

// Complex antecedent with nested implication
property p16;
  (write_en & data_valid) ##0
  (write_en && (retire_address[0:4]==addr)) [*2] |->
  ##[3:8] write_en && !data_valid && (write_address[0:4]==addr);
endproperty

// Equivalent nested form:
property p16_nested;
  (write_en & data_valid) |->
  (write_en && (retire_address[0:4]==addr)) [*2] |->
  ##[3:8] write_en && !data_valid && (write_address[0:4]==addr);
endproperty

📋 Property Examples — All Forms

// rule3: if a holds twice in a row, EITHER c appears within 3 ticks OR (d |=> e)
property rule3;
  @(posedge clk) a[*2] |-> ((##[1:3] c) or (d |=> e));
endproperty

// rule4: if a holds twice, BOTH c appears within 3 ticks AND (d |=> e)
property rule4;
  @(posedge clk) a[*2] |-> ((##[1:3] c) and (d |=> e));
endproperty

// rule5: after a then first(b or c), if b won then check d |-> e, else check f
property rule5;
  @(posedge clk)
  a ##1 (b || c)[->1] |->
  if (b)
    (##1 d |-> e)
  else
    f;
endproperty

// rule6: reusable named property — ##1 x |-> y
property rule6(x, y);
  ##1 x |-> y;
endproperty
// rule5a: same as rule5 but using rule6 as a property instance
property rule5a;
  @(posedge clk)
  a ##1 (b || c)[->1] |->
  if (b) rule6(d, e)
  else   f;
endproperty

🔁 Recursive Properties

A property can reference itself. This enables expressing “always”-style liveness properties and complex protocol patterns like retries and out-of-order completions.

// prop_always(p): p must hold at every cycle forever
property prop_always(p);
  p and (1'b1 |=> prop_always(p));
endproperty

// prop_weak_until(p,q): p must hold every cycle until q holds (q not required)
property prop_weak_until(p, q);
  q or (p and (1'b1 |=> prop_weak_until(p, q)));
endproperty

// Trigger recursion from a starting condition
property p1(s, p);
  s |=> prop_always(p);   // after s fires, p must hold forever
endproperty

// Mutually recursive: phase alternation
property check_phase1;
  s1 |-> (phase1_prop and (1'b1 |=> check_phase2));
endproperty
property check_phase2;
  s2 |-> (phase2_prop and (1'b1 |=> check_phase1));
endproperty

Three restrictions on recursive properties

1. No negation: not cannot be applied to any expression that instantiates a recursive property.
2. No disable iff: recursive property declarations cannot use disable iff (consistent with the no-nesting rule for disable iff).
3. Positive time advance: every recursive instantiation must occur after a positive advance in time. Using |-> (overlapping) for the recursive call would be stuck in time — |=> (non-overlapping, +1 tick) is required.

⏱ Multi-Clock Sequences

A sequence can span multiple clock domains by concatenating singly-clocked subsequences with ##1. The ##1 synchronises between the ending tick of the first clock and the nearest strictly subsequent tick of the second clock.

// sig0 checked at posedge clk0; then sync to next posedge clk1; sig1 checked there
@(posedge clk0) sig0 ##1 @(posedge clk1) sig1

// If clk0 == clk1: equivalent to the singly-clocked form
// @(posedge clk0) sig0 ##1 sig1

// Multi-clock sequence using named single-clock sequences
sequence s1; @(posedge clk1) a ##1 b; endsequence
sequence s2; @(posedge clk2) c ##1 d; endsequence
sequence mult_s;
  @(posedge clk) a ##1 @(posedge clk1) s1 ##1 @(posedge clk2) s2;
endsequence

⏱ Multi-Clock Properties

Properties can be freely composed across clocks using not, and, or, and |=>. The overlapped implication |-> and if...else require the same clock at the boundary.

// |=> synchronises between two different clocks
@(posedge clk0) s0 |=> @(posedge clk1) s1
// s0 clocked by clk0; after each match, advance to next posedge clk1; check s1 there

// |=> can synchronise to MULTIPLE consequent clocks
@(posedge clk0) s0 |=> (@(posedge clk1) s1) and (@(posedge clk2) s2)

// |-> requires the SAME clock at both ends
// LEGAL: antecedent ends at clk0; consequent starts at clk0
@(posedge clk0) s0 |-> @(posedge clk0) s1 ##1 @(posedge clk2) s2

// ILLEGAL: |-> with different clocks on antecedent and consequent start
// @(posedge clk0) s0 |-> @(posedge clk1) s1  // ERROR if clk0 ≠ clk1

// if...else: condition and BOTH branch starts must be on the same clock
// LEGAL:
@(posedge clk0) if (b) @(posedge clk0) s1
// ILLEGAL:
// @(posedge clk0) if (b) @(posedge clk0) s1 else @(posedge clk1) s2  // ERROR if clk0≠clk1

📌 Clock Flow

Clock flow lets a clocking event scope extend naturally left-to-right through linear operators, eliminating the need to repeat the same clock event at each sub-expression.

// Full form — clock c stated explicitly everywhere it applies
@(c) x |=> @(c) y ##1 @(d) z

// Simplified via clock flow — c flows across |=> into y
@(c) x |=> y ##1 @(d) z

// Clock flow with |->: reinforces that clock cannot change across it
@(c) x |-> y ##1 @(d) z    // y is implicitly clocked at c (clock flows across |->)

// Clock flow with if...else
@(c) if (b) w ##1 @(d) x else y ##1 @(d) z
// b, w, y are implicitly at clock c; x and z are at clock d

// Adjointness: concatenation and implication are interchangeable
@(c) x ##1 y |=> @(d) z   ≡   @(c) x |=> y |=> @(d) z
@(c) x ##0 y |=> @(d) z   ≡   @(c) x |-> y |=> @(d) z

// Juxtaposed clocks: second overrides first
@(d) @(c) x   ≡   @(c) x   (d nullified)

// Clock flow does NOT escape from parentheses
@(c) w ##1 (x ##1 @(d) y) |=> z
// w, x, z are at c; y is at d; d does NOT flow out of parentheses

📋 matched — Cross-Clock Endpoint Detection

When the source and destination sequences are on different clocks, use .matched instead of .ended. matched stores the match result until the next tick of the destination clock.

// e1 evaluated on clk; e2 uses e1.matched at sysclk ticks
sequence e1(a, b, c);
  @(posedge clk) $rose(a) ##1 b ##1 c;
endsequence

sequence e2;
  @(posedge sysclk)
  reset ##1 inst ##1
  e1(ready, proc1, proc2).matched [->1] ##1 branch_back;
endsequence
// .matched: stores whether e1 reached its endpoint, tested at the next sysclk tick
// .ended would be illegal here because e1 and e2 are on different clocks

✅ assert / assume / cover

A property is inert until used in one of three verification statements. Each serves a different purpose.

// assert: checking — fails if property does not hold
a1: assert property (req_ack)
  $display("OK");
else
  $error("req_ack violated at t=%0t", $time);

// assume: environment constraint
// — for formal: treated as hypothesis, not verified
// — for simulation: must hold; checked and reported like assert, but no action block
assume_ack1: assume property (pr1);

// assume with distribution for random simulation biasing (dist → inside for assert/cover)
a1: assume property @(posedge clk) req dist {0:=40, 1:=60};
// 40% chance req=0, 60% req=1 in random simulation

// cover: functional coverage monitoring
// — reports attempts, successes, failures, vacuous successes
c1: cover property (seq3);          // counts every match
c2: cover property (req_ack) count++;  // pass action on each success

📋 Embedding Assertions in Procedural Code

Concurrent assertions can appear inside always or initial blocks. The block’s event control can infer the clock automatically, and the surrounding if/case context can infer the enabling condition.

// Clock inference: posedge mclk inferred from the always block's event control
property r1; q != d; endproperty
always @(posedge mclk) begin
  q <= d1;
  r1_p: assert property (r1);  // clock inferred: posedge mclk
end

// Enabling condition from if: equivalent to a |-> (q != d)
always @(posedge mclk) begin
  if (a) begin
    q <= d1;
    r3_p: assert property (@(posedge mclk) q != d);  // infers: a |-> (q!=d)
  end
end

// Enabling from case: equivalent to (a==1) |-> (q != d)
always @(posedge mclk) begin
  case (a)
    1: begin
         q <= d1;
         r4p: assert property (@(posedge mclk) q != d);  // infers: (a==1) |-> (q!=d)
       end
  endcase
end

Clock inference rules

• The inferred clock must be the first term of the event control as an edge specifier (posedge expr or negedge expr).
• Variables in the edge expression must not be used anywhere in the always/initial block.
• If a clock is explicitly specified in the property, it must be identical to the inferred clock.

Enabling condition inference restrictions

• No preceding statement with a timing control before the assertion.
• No preceding task call containing a timing control.
• The assertion cannot be inside a loop statement.

⏱ Clock Resolution

A concurrent assertion must resolve to exactly one clock. The clock is determined in this priority order:

1. Explicitly specified clock on the property or assert statement.
2. Inferred clock from the procedural block’s event control.
3. Default clocking block, if declared in scope.

An assertion that resolves to no clock is a compile error.

// Five ways to specify the clock for an assertion:

// 1. Via a named sequence that has a clock
sequence s2; @(posedge clk) a ##2 b; endsequence
assert property (not s2);

// 2. Via the property declaration itself
property p3; @(posedge clk) not (a ##2 b); endproperty
assert property (p3);

// 3. Via inferred clock from always block
always @(posedge clk) assert property (not (a ##2 b));

// 4. Via clocking block
clocking master_clk @(posedge clk);
  property p3; not (a ##2 b); endproperty
endclocking
assert property (master_clk.p3);

// 5. Via default clocking
default clocking master_clk;  // as defined above
property p4; (a ##2 b); endproperty
assert property (p4);  // clock from default clocking

🔗 Binding Properties to Scopes or Instances

The bind directive attaches a module, interface, or program containing assertions to a target module or instance — without modifying the target’s source code. The bound entity runs as if its code were written inside the target.

// Bind a program with properties to every instance of module cpu
bind cpu fpu_props fpu_rules_1(a, b, c);
// cpu      = target module
// fpu_props  = program/module/interface containing properties
// fpu_rules_1 = instance name of fpu_props inside cpu
// (a, b, c) get bound to signals a, b, c in every cpu instance

// Bind to a specific instance only (not every instance)
bind cpu1 fpu_props fpu_rules_1(a, b, c);
// cpu1 = specific hierarchical instance path

// Bind an interface containing an assertion
interface range(input clk, enable, input int minval, expr);
  property crange_en;
    @(posedge clk) enable |-> (minval <= expr);
  endproperty
  range_chk: assert property (crange_en);
endinterface

bind cr_unit range r1(c_clk, c_en, v_low, (in1&&in2));
// Every cr_unit instance now contains interface instance r1

▶ The expect Statement

expect is a procedural blocking statement that waits for a property to succeed or fail. Unlike assert property (which fires on every clock tick), expect fires exactly once per execution, starts on the next clocking event, and blocks the calling process until the property resolves.

program tst;
  initial begin
    #200ms;
    // Block until a ##1 b ##1 c matches starting at next posedge clk after 200ms
    expect( @(posedge clk) a ##1 b ##1 c ) else $error("expect failed");
    ABC: continue_test();  // reached only if sequence matched
  end
endprogram

// In a task: wait up to 10 cycles for data to equal a specific value
integer data;
task automatic wait_for(integer value, output bit success);
  expect( @(posedge clk) ##[1:10] data == value ) success = 1;
  else                                               success = 0;
endtask

initial begin
  bit ok;
  wait_for(23, ok);  // wait up to 10 cycles for data==23
  if (!ok) $error("Timed out waiting for 23");
end

📋 Quick Reference

Property operators at a glance

Multi-clock rules

• Only ##1 between differently-clocked subsequences — not ##0, ##N>1, or any other operator.
• |=> can cross clock boundaries freely.
• |-> requires the same clock on both ends.
• if...else condition and both branch starts must be on the same clock.
• Clock flow extends a clock left-to-right; does not escape parentheses.
• Juxtaposed clocks: second overrides first.
• Use .ended for same-clock endpoint detection; .matched for cross-clock.

Verification statement summary

• assert property — checker; fails trigger action block; default severity $error.
• assume property — constraint; for formal: hypothesis; for sim: verified but no action block.
• cover property — coverage; reports attempts/matches/vacuity; pass statement on each success.
• expect — procedural blocking wait for a single property evaluation.