Hi All ,
I am trying the following two codes which has multiple clocked property in the consequent as well as call to sequence method .matched :: edaplayground1
Due to multiple clocks in consequent i.e |=> @( posedge clk ) my expectation is the sequence ’ aRb ’ must end at T:22 units i.e Subsequent posedge of clk after Antecedent is True .
However the output varies across tools . Some show as assertion pass at T:22 while others show FAIL at T:22 or T:18 units .
**
Any suggestions on how the consequent is evaluated ?
As sequence method ’ .matched ’ works on Source and Destination clock ,
what’s the destination clock source in this case ? Is it @( posedge clk ) due to multiple clocked property ?**
My expectation is due to Multi-clocked Consequent ( |=> @( posedge clk1 ) ) , after antecedent is True at T:30 at subsequent clock tick of clk1 i.e at T:34 as ’ aRb.matched ’ is still True the assertion should PASS at T:34 .
However only 1 tool agrees with me while the others give assertion Failure .
Would like to hear your thoughts on the following :
Using the above table for multiclocked property =>
(1) For eda1 : aRb(a,b).matched would be evaluated at T:22 units at the nearest posedge of clk after Antecedent is True .
For the assertion to PASS sequence ' arb ' should have completed at posedge of clk at T:18 .
Since sequence ' aRb ' completes at T:22 units the assertion FAILS .
( Had we used .triggered instead of .matched the assertion PASSes at T:22 units. )
Using .matched if we were to change the stimulus to :
initial begin
a = 1 ;
#13 ; a = 0 ; // Sampled at posedge of clk1 at T : 14
#03 ; c = 1 ; // Antecedent is True at T : 18 .
b = 1 ; // Sampled at posedge of clk at T : 18 . Sequence ' aRb ' Ends at T:18
#12 ; $finish();
end
The **assertion PASSes at T:22 units on 2 of the 4 tools .**
**Generally .matched is used when there are 2 separate clocks , the LRM doesn't describe a scenario on the behavior when .matched is used with single clock .
Maybe that's why tools have different outputs based on their implementation .**
(2) For eda2 : .matched is used with 2 separate clocks ( source clock ’ clk2 ’ and destination clock ’ clk1 ’ ) which is as per LRM .
aRb(a,b).matched would be evaluated at T:34 units at the subsequent posedge of clk1 after Antecedent is True .
For the assertion to PASS sequence ' arb ' should have completed at previous posedge of clk2 at T:30 .
**Since sequence ’ aRb ’ does indeed complete at T:30 units I expected the assertion to PASS at T:34 .
In reply to Have_A_Doubt:
I edited your code by removing blank lines and unneeded spaces to make the code more compact.
I also added variables err1 and edp1 and incremented those variables on error and endpoint.
This displays key points more easily in the waveforms.
In this forum, we don’t talk about vendors. Thus, I’ll stick to 1800.
Question: What is the expected behavior in multiclocking when the sampling clock of the endpoint uses the same clock as the sequence that generates that endpoint. Should results be the same when .triggered vs .matched were used. Summary of code:
//Endpoint of sequence aRB clocked at clk
sequence aRb( aFell, bRose ); @( posedge clk ) $fell( aFell ) ##1 $rose( bRose);
// Leading clocking event of assertion ist clk1, clocking the antecedent
@( posedge clk1 ) $rose( c )
// |=> is followed by a clock change to sequence aRB clock and tested aRB’s endpoint
@( posedge clk1 ) $rose( c ) |=> @( posedge clk ) aRb(a,b).matched;
// @( posedge clk1 ) $rose( c ) |=> @( posedge clk ) aRb(a,b).triggered;
CONCLUSIONS
it is my opinion that in that model you should expect the same results in using .matched vs .triggered.
I am in conversation with my 1800 committee members to get their reactions.
Again, I can’t talk about tools or tool comparisons here, per forum regulations.
I am disappointed that I see different results with different tools.
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
(1) Behavior of .matched using a single clock is currently undefined as per LRM currently . Maybe for future versions of the LRM this would be addressed as well .
Would like to hear 1800 committee member's opinion on the same .
(2) For edalink2 the assertion should pass at T:34 units i.e at the subsequent posedge of clk1 , after the antecedent is True .
In reply to Have_A_Doubt:
It is not true that (1) the behavior of .matched using a single clock is currently undefined as per LRM currently1800 says: The triggered status of the sequence is set in the Observed region and persists through the remainder of the time step.
The matched status of the sequence is set in the Observed region and persists until the Observed region following the arrival of the first clock tick of the destination sequence after the match.
[Ben]Thus, the matched is set in the same region as the triggered.
Also, the matched persists beyond the time step where the triggered ends until the Observed region following the arrival of the first clock tick of the destination sequence after the match. THUS: It is reasonable to say that in a singly clocked model the simulation results of a .matched should be the same as a .triggered because in a singly clocked model, the arrival of the first clock tick of the destination sequence after the match is zero.
Would like to hear 1800 committee member’s opinion on the same.
I was a member of the 1800’2017 committee or SVA and I am currently in conversation with members of that committee. I’ll get back to you on how 1800 should behave as soon as I hear back from them. Yes, there is a new revision of 1800 that includes mostly clarifications. I was invited to participate in that effort and will push on that point.
The bottom line question is:
In a singly clocked model, should the results of a
seq.matched be the same as seq.triggered ? Summary and conclusions
It is my opinion that in a singly clock model the .triggered should yield the same results as the .matched. This is because in both cases the triggered status of the sequence is set in the Observed region and persists through the remainder of the time step.
Rational: 1800: 16.13.6 Sequence methods
The value of method triggered evaluates to true (1’b1) if the operand sequence has reached its end point at that particular point in time and false (1’b0) otherwise. The triggered status of the sequence is set in the Observed region and persists through the remainder of the time step.
The method matched is used to detect the end point of one sequence (the source sequence) referenced in a multiclocked sequence (the destination sequence). [Ben] For example:
sequence s; @posedge sysclk) a; endsequence
assert property(@posedge clk) 1 |-> @(posedge clk) s.matched);
// * The endpoint of s is the source sequence, which occurs at posedge sysclk
// * s.matched is the destination sequence, which occurs at posedge clk
1800: It can only be used in sequence expressions. Unlike triggered, matched provides synchronization between two clocks by storing the result of the source sequence until the arrival of the first clock tick of the destination sequence after the match. The matched status of the sequence is set in the Observed region and persists until the Observed region following the arrival of the first clock tick of the destination sequence after the match.
[Ben] comparing the definitions side by side:
The triggered status of the sequence is set in the Observed region and persists through the remainder of the time step.
The matched status of the sequence is set in the Observed region and persists until
the Observed region following the arrival of the first clock tick of the destination sequence after the match.
Thus, in a singly clocked system, I can say that the Observed region following the arrival of the first clock tick of the destination sequence after the match occurs in the same time step as source sequence,
THEREFORE, in a singly clocked model, I should see the same results in using .matched or .triggered.
The simulator versions on edaplayground are old. However, your observation on edaplayground about different results should be reviewed by vendors.
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Ben ,
The matched status of the sequence is set in the Observed region and persists until the Observed region following thearrival of the first clock tick of the destination sequence after the match.
So even if we have a single clock for source and destination , shouldn’t that mean that .matched returns true at next destination clock instead of same clock ?
For edalink2 even though sequence aRb ends at T:30 and both posedges of clk1 and clk2 overlap at T:30 ,
the assertion passes at Next posedge of clk1 i.e T:34 .
Similarly I feel even if the source and destination clock are same , .matched should be True at Next clock after it actually ends .
In reply to Have_A_Doubt:
You are absolutely correct and I made a mistake, so did one vendor :) )
The end point occurs when the source sequence has a match on its clock (i.e., there is no next there). However, for .matched this endpoint is memorized till the following tick of the target clock where .matched is used.
Thus, .matched is different than .triggered
Also, the LRM says The matched status of the sequence is set in the Observed region and persists until the Observed region following the arrival of the first clock tick of the destination sequence after the match.
My apologies for my error. Your posting is doing a good thing:
It brought up a good issue that vendor(s) need to fix. (we don’t discuss vendors here.
It makes for a good paper that I am planning on writing.
Ben
