I have written a System Verilog property for the gated clock to make sure that the gated clock is really gated when the clock enable is disabled. Given below is the code and other relevant details. Basic requirement is met during simulation.
But, I’d request to review and provide inputs in case if it can be made more robust.
On the similar lines, I have written a property for reset as well. This is resulting in false assertion failure at reset release; as the disabling of res_en and release of reset happens at the same time in design, where-as throughout expects it to happen after a cycle delay. Need help to get it resolved.
At first glance, it looked to me like you need a first_match() in the antecedent, as you have multiple possible matches, and all threads of the antecedent must be tested and must succeed.
However, after more thoughts, you do NOT want the first_match() in this particular case.
I recommend that you modify your not operator to the bitwise negative operator. Thus,
Rationale: Since your variable are declared as single bits, you should use good coding practices, and use the Binary logical operators instead of the Binary bitwise operators. You are doing logical operations.
Yes, you get the same result in either case, but the notion is different.
On the similar lines, I have written a property for reset as well. This is resulting in false assertion failure at reset release; as the disabling of res_en and release of reset happens at the same time in design, where-as throughout expects it to happen after a cycle delay. Need help to get it resolved.
Reset enable: res_en
Reset signal: reset_n
clock: ref_clk
[list=1]
[*] The goto with 0 does not make sense: [->0] b [->m] is equivalent to ( !b [*0:$] ##1 b)[*m], thus
(~reset_n throughout res_en [->0]) is same as
(~reset_n throughout res_en [0])
[] You probably meant
As the async reset assertion is immediate, the reset_n signal changes directly with reset_en change, where-as the throughout is expecting the old value of reset_n at the time of reset assertion and hence a assertion failure is issued.
So, how do I handle the through-out check here? Please suggest.
In reply to S.P.Rajkumar.V:
I think you need the within operator
property rst_disable_chk;
@(posedge ref_clk)
$fell(reset_en) |-> (reset_n[*1:$] ##1 reset_en) within reset_en [->1];
endproperty
// The sequence containment within specifies a sequence occurring within another sequence.
// Note: (seq1 within seq2) is equivalent to:
((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
Thank you. ‘within’ has perfectly worked in this scenario.
In the test scenario the above sequence has satisfied once and assertion has passed; and then the second time the test scenario stopped at reset release itself, there-by encountering an incomplete assertion issue at the end of simulation. The same issue can occur with all other previous assertions as well (since it all depends on stimulus).
I hope the only solution here is to re-code each assertion sequence above by splitting them into multiple parts (say for ex. one each for reset-assertion, de-assertion, and intermediate checks).
Could you just comment, if there is any other way to go-ahead with the existing code?
In reply to S.P.Rajkumar.V:
If I understand you correctly, your test scenario looks as follows:
let k=5; // an example
let n=2000; // another supposition
// $fell(reset_en) ##[1:n] reset_en ##[1:k] $fell(reset_en) ##[1:$] end_of_simulation
// In that case the assertion ap_reset is fired twice.
// It succeeds at the first firing with the sequence $fell(reset_en) ##[1:n] reset_en ##[1:k]
// However the second firing never completes since there is no reset_n==1.
// That second sequence is $fell(reset_en) ##[1:$] end_of_simulation
ap_reset: assert property(@(posedge ref_clk)
$fell(reset_en) |-> (reset_n[*1:$] ##1 reset_en) within reset_en [->1]);
// So the tool gave you the correct response.
// If you want to test this assertion once, you could put the assertion in an initial statement
initial begin
// Maybe some wait cycles ??
ap_reset: assert property(@(posedge ref_clk)
$fell(reset_en) |-> (reset_n[*1:$] ##1 reset_en) within reset_en [->1]);
end
Yes, the issue encountered is similar and the tools response is also correct.
After enabling the assertions for functional tests (written by other engineers), incomplete issue has occurred. It is expected, as the reset is released initially in all those tests once and then some data processing/manipulation will happen. The complete reset gating/ungating sequence will not be present in those test scenarios.
I’ll make use of initial at the moment for my reset/clock test scenarios.
Thank you very much for clarifying all my queries.
Hi. I have question with your assertion about checking the clock gating.
I’m not so sure if it can catch any errors in clock gating. It’s because g_clk is in-phase with ref_clk, and the checking is done only at the positive edge of ref_clk.
So let’s say that clk_en fell but there’s a bug and g_clk still continues to toggle. Since ref_clk and g_clk are in-phase, and the checking is done in positive edge of ref_clk, then it will never catch g_clk as high. It always samples g_clk as low.
Good point. You could use a clock twice the reference clock, if available. Another option to consider (and try) is to use the neg edge of ref clock in the consequent.
Ben Ben@systemverilog.us
Nice catch. Although my initial post may make an impression that g_clk is derived out of ref_clk, it is not. Both clocks (ref_clk and g_clk) are unrelated, so assertion works fine in this scenario.
After little more analysis, I believe initial assertion would work fine even in the case reported by you (i.e, g_clk being gated version of ref_clk).
Because, ‘throughout’ as the name suggests that, it checks for validity of some condition (!g_clk) as long as other condition (CLK_EN → 1) becomes true; It doesn’t check only at each posedge of ref_clk_i.
Let me know your thoughts on the same.
I’ll try to simulate the scenario suggested by you later, to double check my analysis.
After little more analysis, I believe initial assertion would work fine even in the case reported by you (i.e, g_clk being gated version of ref_clk).
Because, ‘throughout’ as the name suggests that, it checks for validity of some condition (!g_clk) as long as other condition (CLK_EN → 1) becomes true; It doesn’t check only at each posedge of ref_clk_i.
Wrong on the following statement: It doesn’t check only at each posedge of ref_clk_i.
with
@(posedge ref_clk)
($fell(clk_en) ##[2:4] !g_clk) |-> (!g_clk throughout clk_en[->1]);
All variables ARE SAMPLED @(posedge ref_clk)
This would solved the problem though by using a multiclock, specifically,
@(negedge ref_clk) in the consequent.
@(posedge ref_clk)
($fell(clk_en) ##[2:4] !g_clk) |->
@(negedge ref_clk)(!g_clk throughout clk_en[->1]);
BTW, g_clk is sampled in the Preponed region, thus, with clk_en==1’b1, @posedge(ref_clk) the sampled value of g_clk==0 (it has not risen yet).
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
Thank you for correcting my post.
I have experimented little bit and learnt more on ‘throughout’ after your update, with which my misconceptions are gone now. :)
Hi Ben,
Is there a way that a property can be written to make sure that the gated clock is available when clock enable is not disabled and ref_clk is not available with us to be used as an event in the property?
The context behind asking this query is that i want this checker on g_clk to sit inside IP RTL, where IP provides clk_en.
I thought to generate a local clock(using g_clk) and use it in the property but this may add to my simulation time- calculating time-period for local clock continuously.
Is there any other solution possible to my problem?
In reply to ysaini:
Keep in mind that an assertion is a statement that a given property is required to hold.
SVA is just a notation with a set of rules to write assertions. Long before SVA or PSL, verification engineers wrote assertions in Verilog and VHDL, and before that, the verification was visual with scopes (if you’re my age). The point here is that for this case, consider writing just SystemVerilog code. Your solution sounds plausible.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
This assertion will fail for the following scenario, where clocks start toggling ‘n’ cycles before clk_en goes high. How would we add tolerance to this scenario?
In reply to ben@SystemVerilog.us:
This assertion will fail for the following scenario, where clocks start toggling ‘n’ cycles before clk_en goes high. How would we add tolerance to this scenario?
I am not clear as to which assertion you are talking about. This one?
@(posedge ref_clk)
($fell(clk_en) ##[2:4] !g_clk) |->
@(negedge ref_clk)(!g_clk throughout clk_en[->1]);
In any case, you can control the start and behavior on an assertion with supporting logic, like events. Please clarify your requirements.
Ben ben@systemverilog.us
Yes, this is the assertion I’m talking about. My requirement is:
I want to create a tolerance window few cycles AFTER clk_en has a 1->0 transition, as well as a few cycles BEFORE clk_en has a 0->1 transition.
In your example, the ##[2:4] is the tolerance window for few cycles after clk_en has a 1->0 transition($fell). That works perfectly fine.
However, I also want to cover the case where clocks might start ticking few cycles before clk_en goes from 0->1. Your earlier assertion will fail in this case. How do we cover that case?
If I want to create a tolerance window before and after 0-1> and 1->0 transition of clk_en, how do we go about that? The before and after is for each of the 2 transitions. So basically 4 windows: before 0->1, after 0->1, before 1->0, and after 1->0.
In reply to imajeeth:
You can use the $past function. Let me explain this concept in a more generic sense; I’ll let you work out your specific issues. You may have to write multiple assertions.
// Requirements: if(b) then "a" occurred 1 to 3 cycles ago
generate for (genvar i=1; i<=3; i++)
begin
ap_ab: cover property(@(posedge clk) b |-> $past(a, i));
end
endgenerate
From my SVA Handbook 4th Edition, 2016 4.2.1.1.2 $past
The $past function provides the sampled value that an expression held in a previous nth cycle. The syntax of the function is: $past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
expression1 represents the expression being sought.
The three optional arguments define the following:
expression1 and expression2 can be any expression allowed in assertions.
number_of_ticks specifies the number of clock ticks in the past. number_of_ticks must be one or greater, and must be static (i.e., known at elaboration time). If number_of_ticks is not specified, then it defaults to 1. If the specified clock tick in the past is before the start of simulation, the returned value from the $past function is a value of X.
expression2 is used as a gating expression for the clocking event. The value returned for $past is expression1 sampled number_of_ticks gated cycles ago. In other words, for:
$past(data, 3, load_enable, @(posedge clk)) the returned value is the sampled value of data in the 3rd prior cycle in which load_enable was true. This is demonstrated in Figure 4.1.1.1-2 /ch4/4.2/past.sv
clocking_event specifies the clocking event for sampling expression. A clock tick is based on clocking_event.
Examples: :
regload |=> reg_data==$past(data); // value of load_data at the previous cycle
regload |-> ##2 reg_data==$past(data, 2); // value of load_data at 2 cycles ago
regload |-> ##2 reg_data==$past(data, 2, 1, @(posedge clk)); // value of load_data at 2 cycles ago
regload |-> ##2 reg_data==$past(data, 3, load_enable, @ (posedge clk) );
// value of data when it was sampled 3 gated cycles ago with load_enable as the gate.