I am writing a property of below specification:
“my_seq to my_seq delay should not be less than my_timing.”
NOTE: I have to use the variable t because the timing needs to be calculated from other variables in my actual design.
I tried not when writing the property.
property my_prop;
int t;
@(negedge clk) disable iff (!rstn)
my_seq |-> not (##0 (1, t = my_timing - 1)
##1 (1, t = t - 1)[*0:$]
##1 my_seq ##0 (t > 0));
endproperty
It looks okay. I get assertion errors only when the design does not meet above specification.
But I’m concerned if this kind of property can become too heavy.
That is, once the property is enabled, it might not finish until the end of the simulation. (Am I wrong about this?)
Is there a better solution to write this specification?
+) Below is the initial trial but I guess it’s written in wrong syntax.
I got compile error with below.
property my_prop;
int t;
@(negedge clk) disable iff (!rstn)
my_seq |-> ##0 (1, t = my_timing - 1)
##1 (not (my_seq), t = t - 1)[*0:$]
##1 (t <= 0);
endproperty
The “not” operator is a property operator and is not a sequence operator.
Thus, the following is incorrect.
##1 (not (my_seq), t = t - 1)[*0:$]
If the consequent has a infinite delay range it can never fail; it can succeed
a |-> ##[1:$] b; // same as
a |-> ##1 b or ##2 b or ##3 b or ... ##n b; // can never fail
//
a |-> ##1 (1, t = t - 1)[*0:$] ##1 c; // is same as
a |-> ##1 c or ((1, t = t - 1)[*1] ##1 c) or ((1, t = t - 1)[*2] ##1 c) or ..
// Thus, can never fail
//
a |-> ##1 (b, t = t - 1)[*0:$] ##1 c; // is same as
a |-> ##1 c or ((b, t = t - 1)[*1] ##1 c) or ((b, t = t - 1)[*2] ##1 c) or ..
// This CAN fail because a sequence of " b==1 ##1 b==0" fails the b[*2], and would also fail the b[*3] and etc.
The use of not of a sequence can be confusing. Why not making it a positive type of requirement. Thus instead of [list]
“my_seq to my_seq delay should not be less than my_timing.”, use
“my_seq to my_seq delay should be >= than my_timing.”
[*] You need the **first_match()**operator to get a failure.
[/list]
Below is code, link to the test file, and the simulation results.
int my_timing= 4;
sequence my_seq;
( a ##1 b);
endsequence
// "my_seq to my_seq delay should not be less than my_timing."
// "my_seq to my_seq delay should be >= than my_timing."
property my_prop;
int t, count=0;
@(negedge clk) disable iff (!rstn)
(my_seq, t = my_timing -1 ) |-> // ** Don't need the "-1", was a copy/paste mistake
##1 first_match((1, count=count+1'b1)[*0:$] ##1 my_seq) ##0 (count >= t);
endproperty
ap_my_prop: assert property(my_prop);
By modifying “should not be < than” to “should be >= than”, isn’t it more likely to become an incomplete assertion at the end of the simulation?
How should I interpret incomplete assertions in this case? Can I just say it PASSED?
An assertion can be in one of the following states:
vacuous
pass or success
fail
in execution;
Incomplete if the simulation ends and the assertion has not succeeded or failed.
An incomplete assertion will be identified as FAIL if the sequence is marked as strong.
Assertions are written to express requirements. I don’t see a difference in expressing that a delay should not be less than or equal to5 cycles and delay should be greater or equal to 5 cycles. Where is the INCOMPLETION? An assertion is incomplete if you have not provided enough cycles in the simulation to complete.
[*] Is is possible to write a property sticking to “should not be < than”? This is just to solve the incompleteness issue, IF needed.
i.e., “when my_seq is issued, my_seq cannot be issued within my_timing.”
From my SVA Handbook Guideline: Qualify as strong properties that are sequences and have range delays or consecutive repetition operators (e.g., [*, [->, [= ) and are consequents in an assertion. This is important when it is necessary to qualify an assertion as a failure if the consequent never terminates at the end of simulation. Example:
Assertions are written to express requirements. I don’t see a difference in expressing that a delay should not be less than or equal to5 cycles and delay should be greater or equal to 5 cycles. Where is the INCOMPLETION? An assertion is incomplete if you have not provided enough cycles in the simulation to complete.
If you see the property written as “should be >= than”, it won’t finish until first_match(~) is found.
In the following cases, the property would not become completed because there are no more my_seq following.****
my_seq is issued only once during the simulation.
10 consecutive my_seq issued. (Focus on the last my_seq issued.)
Since above two scenarios are not out of the specification, I shouldn’t put strong in the property to get errors on incompletion.
But in the case the property is written as “should not be < than”, the property will be completed my_timing cycles after the point it is enabled.
I am starting to think that getting incomplete assertions would not matter much.
I just thought it can be written more efficiently.
Please correct me if I am thinking it the wrong way.
In reply to Jung Ik Moon:
Your not property would not work either.
If you know that there will be no more than n my_seq, like no more than 10, then you can count the number of valid my_seq and use that count as an antecedent to the rest of the property. Below is the key aspect of this solution:
int my_timing= 4, count_seq;
function void inc_count();
count_seq=count_seq+1'b1;
endfunction : inc_count
// no more my_seq following.
property my_prop_nomore;
int t, count=0;
@(negedge clk) disable iff (!rstn)
count_seq <=10 |-> // If >10, then vacuity thereafter
(my_seq, t = my_timing, inc_count() ) |->
##1 first_match((1, count=count+1'b1)[*0:$] ##1
(my_seq, inc_count())) ##0 (count >= t);
endproperty
ap_my_prop_nomore: assert property(my_prop_nomore);
Complete code
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
bit clk, a, b, rstn=1'b1;
int my_timing= 4, count_seq;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
function void inc_count();
count_seq=count_seq+1'b1;
endfunction : inc_count
sequence my_seq;
( a ##1 b);
endsequence
// "my_seq to my_seq delay should not be less than my_timing."
// "my_seq to my_seq delay should be >= than my_timing."
property my_prop;
int t, count=0;
@(negedge clk) disable iff (!rstn)
(my_seq, t = my_timing - 1) |->
##1 first_match((1, count=count+1'b1)[*0:$] ##1 my_seq) ##0 (count >= t);
endproperty
ap_my_prop: assert property(my_prop);
// no more my_seq following.
property my_prop_nomore;
int t, count=0;
@(negedge clk) disable iff (!rstn)
count_seq <=10 |->
(my_seq, t = my_timing, inc_count() ) |->
##1 first_match((1, count=count+1'b1)[*0:$] ##1
(my_seq, inc_count())) ##0 (count >= t);
endproperty
ap_my_prop_nomore: assert property(my_prop_nomore);
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(a, b) with
{ a dist {1'b1:=1, 1'b0:=3};
b dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
end
$stop;
end
endmodule
In reply to Jung Ik Moon:
If you have a signal that can be used as a trigger to identify an upcoming end of the simulation, you can use that with an assertion control or part of the disabling condition (like in a default disable) to stop the checking of assertions. From my book: .
The $assertcontrol provides finer granularity in how and which types of assertions are controlled. The syntax is repeated below:
$assertcontrol ( control_type [ , [ assertion_type ] [ , [ directive_type ]
[ , [ levels ] [ , list_of_scopes_or_assertions ] ] ] ] ) ;
let OFF = 4; // assertion control type
// Assertion directives
let ASSERT = 1; // directive_type for assertion control tasks
let COVER = 2; // directive_type for assertion control tasks
let ASSUME = 4; // directive_type for assertion control tasks
let ALL_DIRECTIVES = (ASSERT|COVER|ASSUME); // (i.e., 7)
let ALL_ASSERTS = (CONCURRENT|S_IMMEDIATE|D_IMMEDIATE|EXPECT); // (i.e., 31)
/* The OFF control stops the checking of all specified assertions until a subsequent
$assertcontrol with a control_type of 3 (On). No new attempts will be started. Attempts that are already executing for the assertions, and their pass or fail statements, are not affected. Any queued or pending assertions are not flushed and may still mature. No new instances of assertions are queued. The assertions are re-enabled with a subsequent $assertcontrol with a control_type of 3 (On).
This control_type value does not affect expect statements. For example,*/
$assertcontrol(OFF); // using default values of all other arguments
$assertcontrol(LOCK, ALL_ASSERTS, ALL_DIRECTIVES, 0, ap_x1); // lock any changes to ap_x1
