Hello Moderators,
I am still a newbie to SV assertions and am trying to understand how it functions.
Having spent time looking at articles,blogs on the same I went ahead and tried the following code
I have some doubts on the working of the code
Although all 3 blocks have a delay of 10ns via #10ns or @(posedge clk), I observe that in both I2 and I3, the concurrent assertion is evaluated at time 10ns whereas the $display at the end of I1 executes at time 30ns
(1) Both #10ns in I2 and @(posedge clk) in I3 unblock at time 10ns and evaluate both p1 & p2 at time 10ns ( 1st posedge )
However the @(posedge clk) in I1 unblocks at time 30ns (2nd posedge) although delay of #10ns unblocked at 10ns, why is it so ?
(2) Why do p1 & p2 recognize the posedge of clk at 10ns whereas @(posedge clk) in I1 doesn’t ? How does the event control @(posedge clk) in I1 differ from clocking event @(posedge clk) used in p1 and p2 ?
(3) Does p1 & p2 use the sampled value of clk at time 10 units ( which is X ) ?
Is it same as writing :: assert property(@(poesdge clk) $sampled(clk) ) ?
Questions (1) and (2) are really the same issue. You have a race condition between the first two initial blocks. These blocks are running concurrently.
initial begin // forever unrolled
#10 clk = !clk;
#10 clk = !clk;
#10 clk = !clk;
...
end
and
initial begin:I1
#10 @(posedge clk);
$display("I1 done at time:%0t",$time);
end
If the first initial block resumes after the #10 before the second initial block resumes, you miss the first posedge of clk. If the order is reversed, the @(posedge clk)` catches for first posedge.
For question (3), The properties p1 and p2 look at sampled value of clk which are always 0 if you are also using clk as the cycle event.
Final two questions from my side.
(a) Unlike I1 why is there is no race condition for the 2 concurrent assertions ?
Is there a subtle difference b/w the @(posedge clk) in concurrent assertions p1 & p2 and a procedural event control like @(posedge clk) in I1 ?
As concurrent assertions are evaluated in observed region, the expression i.e clk is evaluated in observed region using the sampled value of clk
(b) By observed region although the clock transition has passed,
how does @(posedge clk) unblock in p1 & p2 ?
Is it similar to a procedural event control @(posedge clk) which unblocks in active region ?
Concurrent assertions are not procedural statements and do not block procedural processes/threads.
Concurrent assertions are declarative constructs that are scheduled, sampled, and evaluated in the same manner, regardless of whether they are declared within or outside a procedural process. The only difference lies in the context of a procedural process. When a concurrent assertion is declared within a procedural process, it doesn’t initiate an assertion thread until the process reaches the point in the code where the assertion is evaluated.n is declared. Outside, it initiates an assertion thread every clock cycle.
Thanks Dave. Adding following quote from Section 16.14.6 of LRM
Unlike an immediate assertion, a procedural concurrent assertion is not immediately evaluated when reached in procedural code.
Instead, the assertion and the current values of all constant and automatic expressions appearing in its assertion arguments (see 16.14.6.1)
are placed in a procedural assertion queue associated with the currently executing process.
Each of the entries in this queue is said to be a pending procedural assertion instance.
At T: 10ns, both p1 & p2 are placed in procedural assertion queue associated with their respective process i.e initial blocks I2 & I3 respectively.
LRM further states ::
In the Observed region of each simulation time step, each pending procedural assertion instance that is currently present in a procedural assertion queue shall mature, which means it is confirmed for execution.
When a pending procedural assertion instance matures, if the current time step is one that corresponds to that assertion instance’s leading clocking event, an evaluation attempt of the assertion begins immediately within the Observed region.
In the observed region of time 10ns both p1 & p2 are evaluated since the current time step corresponds to their leading clocking event (even though the clocking event has passed by then)
As a result, there is no race condition with procedural concurrent assertions
Hi Dave,
I was trying a variation of the above code ( edaplayground )
The negedge of clk occurs at 3ns , 9ns , 12ns , …
1st execution of always block starts at 3ns and ends at 9ns ( 1st negedge at 3ns + DELAY (6ns) )
(Q1)(a) Should the negedge of clk at 9ns result in 2nd execution of always block ?
always@(negedge clk) begin:I1
<procedural_statements>
end
// Is equivalent to
initial begin:I1
@(negedge clk);
<procedural_statements>
@(negedge clk);
<procedural_statements>
@(negedge clk);
<procedural_statements>
@(negedge clk);
<procedural_statements>
.......
end
As per my understanding the event control @(negedge clk) would unblock only if @(negedge clk) executes first & remains blocked before clock inversion occurs via always.
(Q1)(b) In this case does there exist a possible race condition at 9ns between event control @(negedge clk) & clk assignment via always #3 clk = !clk ?
(Q2) As per LRM what should be the ideal output foredaplayground?
My confusion stems from observing different output across tools.
Across the 4 EDA tools, 1 throws a compilation error, 2 don’t trigger fail action block whereas 1 tool executes fail action block at T:12ns & 18ns
Due to multi-clocked property expression, I expected fail action block to execute at 12ns & 18ns.
What would be the ideal output ?