Execution of action block in Abort properties (reject_on / accept_on)

[LFT]

Hi Forum,

I am writing SVA for an intention for

valid once asserted should remain high till ready is asserted

As an additional requirement I want that valid should remain asserted b/w clocking events as well

I modeled it using reject_on

For +define+M1 I observe that 1 tool shows the failure asynchronously at T:40 units

i.e as soon as valid is low

whereas 2 tools execute the fail action block at the next nearest clocking event at T:45 units

I understand that we don’t discuss tool related issues but my intention here is to understand the working as per LRM

I went through the LRM section 16.12.14 Abort properties but I don’t see LRM elaborating on this

If the boolean_expression inreject_on(boolean_expr) / accept_on(boolean_expr)

is true asynchronously, then should the action block execute at the same time step or should it execute at the nearest clocking event ?

Thanks in advance

[user49]

Based on the behavior defined in the IEEE 1800 LRM sections you provided and the standard scheduling semantics of SystemVerilog, here is the answer:

The action block should execute at the same time step in which the asynchronous condition becomes true. It does not wait for the nearest clocking event.

Detailed Explanation

1. Immediate Evaluation

The LRM excerpt states: “accept_on and reject_on are evaluated at the granularity of the simulation time step… [they] represent asynchronous resets.”

This means the simulator monitors the expression_or_dist continuously (similar to a sensitivity list on a combinational block). The moment the condition becomes true—even if it is in the middle of a clock cycle—the property evaluation concludes immediately.

• If it is reject_on(cond), the assertion fails immediately at that specific time stamp.

• If it is accept_on(cond), the assertion succeeds (passes) immediately at that specific time stamp.

2. Execution in the Reactive Region

While the “check” happens immediately, SystemVerilog schedules the execution of the Action Block (the pass or fail statement) in the Reactive Region of that same time step.

This ensures that the action block executes after all design code (Active region) and program code (Observed region) for that specific nanosecond have settled, but before the time advances to the next step.

Example Scenario

Imagine a clock period of 10ns (edges at 0, 10, 20…).

Code snippet

// Assertion with asynchronous reject
assert property (@(posedge clk) req |-> reject_on(reset) ack);

1. Time 10ns: req is sampled high. The assertion starts checking for ack.

2. Time 15ns: reset (the abort condition) goes high asynchronously.

   • Because reject_on is asynchronous, the assertion fails instantly at 15ns.

   • The else block (action block) executes at 15ns (in the Reactive region).

3. Time 20ns: The next clock edge arrives. (The assertion is already dead; nothing happens here regarding that specific evaluation).

Comparison Summary

Operator	When is Condition Checked?	When does Action Block Execute?
reject_on	Asynchronously (any time step)	Same time step the condition became true.
sync_reject_on	Synchronously (only at clock edge)	At the nearest clocking event (when the clock ticks).

Would you like an example code snippet demonstrating how to test this specific timing behavior?

[LFT]

Thanks Ben for the detailed explanation

@user49

Would you like an example code snippet demonstrating how to test this specific timing behavior?

(1) Thanks but I am clear on this ( have tested it locally with examples )

(2) In your example scenario I believe there is a typo

Either there should be a non-overlapping implication or go-to operator for ack ( ack[→1] ).

Without either each attempt would end at the same clock it started

(3)

@user49

The LRM excerpt states: “accept_on and reject_on are evaluated at the granularity of the simulation time step… [they] represent asynchronous resets.”

This means the simulator monitors the expression_or_dist continuously (similar to a sensitivity list on a combinational block). The moment the condition becomes true—even if it is in the middle of a clock cycle—the property evaluation concludes immediately.

• If it is reject_on(cond), the assertion fails immediately at that specific time stamp.

• If it is accept_on(cond), the assertion succeeds (passes) immediately at that specific time stamp.

I revisited LRM for execution of action block

(a) LRM Section 16.12.14 mentions

If during the evaluation, the abort condition becomes true, then the overall evaluation of the
property results in false

(b) LRM Section 16.14.1 Assert statement mentions

When the property for the assert statement is evaluated to be false, the fail statements of the action_block are executed.

Hence for reject_on via (a) and (b) the fail action block should execute (in reactive region) at the same time step that the boolean_expression is sampled true i.e time 40 units

(4) Final 3 questions from my side

(a) Last line of LRM Section 16.12.14 mentions

Abort conditions shall not contain any reference to local variables and the sequence methods triggered and matched.

[Q1] I am trying to understand the logical reason behind this restriction

Abort condition is evaluated using sampled value

I am aware that local variables are assigned on match of a sequence in the observed region

As per LRM Section 16.10 Local variables

The sampled value of a local variable is defined as the current value

So local variables do have a sampled value, then why does the restriction exist ?

[Q2] Similarly why is there a restriction on using sequence methods triggered and matched in abort condition ?

Section 16.5.1 of the LRM says

The default sampled value of the triggered event method (see 15.5.3) and the sequence methods triggered and matched is false (1’b0) .

(b) LRM Section 16.12.14 mentions

The semantics of reject_on(expression_or_dist) property_expr is the same as
not(accept_on( expression_or_dist) not( property_expr)) .

[Q3] I am clear on why is there a 2nd not operator associated with property_expr ?