I don't understand these sentences about concurrent assertion and simulation event

SystemVerilog
, , ,
1

I am reading 16.9.3 Sampled value functions of Sequence operations in IEEE 1800-2017 Standard for SystemVerilog.

I don’t understand the sentences below. These are on page 395.


logic a, b, clk;
// ...
al_bad: assert property (@clk a == b)
  else $error("Different values: a = %b, b = %b", a, b);
a2_ok: assert property (@clk a == b)
  else $error("Different values: a = %b, b = %b",
    $sampled(a), $sampled(b));

If in some clock tick the sampled value of a is 0 and of b is 1, but their current values in the Reactive region of this tick are 0, then assertion a1_bad will report Different values: a = 0, b = 0. This is because action blocks are evaluated in the Reactive region (see 16.14.1). Assertion a2_ok reports the intended message Different values: a = 0, b = 1 because the values of a and b in its action block are evaluated in the same context as in the assertion.

I read “4. Scheduling semantics” to understand this sentence. “a == b” of a1_bad is sampled at PREPONED events region, is evaluated at OBSERVED events region. And the fail action block is executed at REACTIVE events region. If so, the difference between a and b would have already been evaluated in the OBSERVED events region. Why are the results of a1_bad and a2_ok different? The REACTIVE events region is later than OBSERVED events region.

2

In reply to jh_veryveri:

“a==b” is not sampled in the preponed region, only the variables a and b (the operands) are sampled. The expression “$sampled(a) == $sampled(b)” is what gets evaluated in the observed region.

If you have

assert property (@clk p_expression) else $error(a_expression)

All of the operands inside p_expression implicitly use their sampled values. But in the action block a_expression uses their current values in the reactive region. You must explicitly use $sampled(a) to get the preponed value of a in the expression.

3

In reply to dave_59:

Thanks to your reply.

I misunderstand sampling values in the preponed region. Thanks to you, I could understand.

In the example above, in the preponed region, a has a value of 0, b is 1, and in the reactive region, the values of a and b are 0. $sample returns the values of preponed region. The action block of assertion is executed in the reactive region. So the action block of a1_bad reports “a = 0, b = 0” and the action block of a2_ok reports “a = 0, b = 1”.

Please confirm that my understanding is correct.

thank you.

4

In reply to jh_veryveri:

In this case the sampled value is the same asthe preponed value. (all referencing the same clk). The p_expression and the a_expression have completely independent evaluation semantics; they don’t even have to refer to the same variables. You just need to know that all of the operands in the p_expression implicitly use the sampled values. The a_expression uses the values of its operands when the action block executes in the reactive region.