In reply to ben@SystemVerilog.us:
thank u it was great help ,now the code is working
replacing || with && and current_time and clk_period should have same data type. :)
In reply to ben@SystemVerilog.us:
thank u it was great help ,now the code is working
replacing || with && and current_time and clk_period should have same data type. :)
In reply to raghav kumar:
I have a question. I’m still learning SVA, and I have not seen the following syntax used in the above example.
Could you tell me what the antecedent part ( (('1,current_time=$realtime) ) means? Thank you.
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));
In reply to jaecho@broadcom:
Could you tell me what the antecedent part ( (('1,current_time=$realtime) ) means?
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));
The ('1,current_time=$realtime) is called a sequence_match_item
sequence_expr ::= // one of the possibilities is
( sequence_expr {, sequence_match_item }) [ sequence_abbrev ]
sequence_match_item ::=
operator_assignment
| inc_or_dec_expression
| subroutine_call
sequence_abbrev ::= consecutive_repetition
consecutive_repetition ::=
[* const_or_range_expression ]
| [*]
| [+]
In this case, ('1,current_time=$realtime) the '1 is a sequence expression, which means that at every attempt, it will succeed. sequence_match_item are typically used in things like
property p; // if wr, data -> mem, check data is properly written after 4 cycles
int v_data, v_addr; // this is a slow memory, or it goes through other paths.
(wr, v_data=data, v_addr=addr) |-> ##4 mem[v_addr]==mem_data;
endproperty
Ben Cohen SystemVerilog.us
In reply to ben@SystemVerilog.us:
Thank you for your answer. I could not look for this in LRM, since I did not know what this is called (sequenc_match_item). I do see it now.
BTW, I have your book (SystemVerilog Assertions Handbook) and just getting started with it.
In reply to jaecho@broadcom:
BTW, I have your book (SystemVerilog Assertions Handbook) and just getting started with it.
I hope you find the book useful for your projects. Make sure you understand in chapter 1 the section on attempts and threads. Also make sure you understand the needs for the first_match operator. Understanding those concepts can save lots of time. The dictionary of examples is also very useful as it reinforces the uses of the various constructs.
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
I am new to system verilog assertions , i have read in the LRM that real data type is not allowed to be passed to property but in the above example of clock
checker it is being passed .
can you help me on this
In reply to SAKET@ KUMAR:
You CAN use real in expressions that result in a Boolean. For example
property preal;
real v;
(a, v=3.14) |=> v> 4.0;
endproperty
ap_real: assert property(@(posedge clk) preal );
You cannot use real in clock delays or repeat time.
// ILLEGAL
a ##1.2 b
In reply to SAKET@ KUMAR:
How can we check whether Ton and Toff of the clock are as desired (using SVA)?
In reply to perumallatarun:
See vhttps://verificationacademy.com/forums/systemverilog/checking-clock-using-sva
In reply to ben@SystemVerilog.us:
Hi All,
When I run the above code in VCS I am getting the following error please let me know any switches in the command line to be used. Or if this should be run using specific version of vcs(I am using version 2013 of vcs).
Error-[SVA-ITRHS] Invalid type in local variable assign
clock_generate_assert.sv, 6
clock_assert, “$realtime”
Expressions involving real, realtime, string, event and dynamic
SystemVerilog types including virtual interface references are not allowed
in local variable assignments in properties and sequences.
Regards,
Rajesh.B
In reply to rajeshsois:
This forum is not for tool issues. You will need to contact your vendor directly for support.
In reply to rajeshsois:
In reply to ben@SystemVerilog.us:
When I run the above code in VCS I am getting the following error please let me know any switches in the command line to be used. Or if this should be run using specific version of vcs(I am using version 2013 of vcs).
Error-[SVA-ITRHS] Invalid type in local variable assign
clock_generate_assert.sv, 6
clock_assert, "$realtime"
Expressions involving real, realtime, string, event and dynamic
SystemVerilog types including virtual interface references are not allowed
in local variable assignments in properties and sequences.
As mentioned, this forum does not address tools. However, it DOES address language issues. Referring to 1800: 16.6 Boolean expressions
/* Assertions that perform checks based on time values should capture these values in the same context. It is not recommended to capture time outside of the assertion. Time should be captured within the assertion using local variables. The following example illustrates how a problem may arise when capturing time in different contexts. In property p1, a time value, t, is captured in a procedural context based on the current value of count. Within the assertion, a comparison is made between the time value t and the time value returned by $realtime in the assertion context based on the sampled value of count. In both contexts,
$realtime returns the current time value. As a result, the comparison between values of time captured in the different contexts yields an inconsistent result. The inconsistency results in the computation for p1 checking the amount of time that elapses between 8 periods of clk instead of the intended 7. In property p2, both time values are captured within the assertion context. This strategy yields a consistent result. */
bit count[2:0];
realtime t;
initial count = 0;
always @(posedge clk) begin
if (count == 0) t = $realtime; //capture t in a procedural context
count++;
end
property p1;
@(posedge clk)
count == 7 |-> $realtime – t < 50.5;
endproperty
property p2;
realtime l_t;
@(posedge clk)
(count == 0, l_t = $realtime) ##1 (count == 7)[->1] |->
$realtime – l_t < 50.5;
endproperty
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
Hi I know this is an old thread, but I’m quite interested in the OP’s assertion code as I’m trying to write clock assertions as well. I have two questions:
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));
What is the '1 at the beginning of the statement for? What does it achieve?
Thanks!
In reply to silverace99:
Hi I know this is an old thread, but I’m quite interested in the OP’s assertion code as I’m trying to write clock assertions as well. I have two questions:
(('1,current_time=$realtime) |=>(clk_period==$realtime-current_time));
What is the '1 at the beginning of the statement for? What does it achieve?
The 1’b1 (a more typical application here) makes the antecedent true, and thus variable in the sequence match item is updated. You can replace the 1’b1 with a variable (e.g., k), but if that variable evaluates to zero, the property is vacuous.
- Let’s say I want to pull out the value of $realtime-current_time into an error message if this property catches a failure. Is there a way I can pull out the value of a variable inside a property? If not, what are my options?
Two solutions: Edit code - EDA Playground
module M;
bit clk;
realtime t1, clk_period=20.0;
initial forever #11 clk=!clk;
property p2;
realtime current_time;
@(posedge clk)
('1,current_time=$realtime) |=>
(clk_period==$realtime-current_time);
endproperty
ap2: assert property(p2) else
begin
$display ("error"); // local variable is not accessible here ******!!!
end
function automatic bit check_period(realtime now_time);
if ($realtime-now_time != clk_period) begin
t1=$realtime-now_time; // <<<<module variable update here
return 0;
end
else return 1'b1;
endfunction : check_period
property p3;
realtime current_time;
bit pass;
@(posedge clk)
('1,current_time=$realtime) |=>
(1, pass=check_period(current_time));
endproperty
ap3: assert property(p3);
endmodule
Another option is to use tasks and do whatever you want. See my recently published paper
Abstract: Understanding the engine behind SVA provides not only a better appreciation and limitations of SVA, but in some situations provide features that cannot be simply implemented with the current definition of SVA. This paper first explains, by example, how a relatively simple assertion example can be written without SVA with the use of SystemVerilog tasks; this provides the basis for understanding the concepts of multithreading and exit of threads upon a condition, such as an error in the assertion. The paper then provides examples that uses computational variables within threads; those variables can cause, in some cases, errors in SVA. The strictly emulation model with tasks solves this issue.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
In reply to ben@SystemVerilog.us:
I see. so by pulling all the variables into a function, you’ve moved the variable scope up to a level an error message can access. Very cool. Thanks Ben!
In reply to silverace99:
Should be
(1, pass=check_period(current_time))##0 pass;
This makes the assertion pass or fail.
In reply to raghav kumar:
Hi, can you tell me that why '1 is used in ('1,current_time=$realtime)?
Also whats the difference if we write 1 instead of '1 or if we write any other number 2,3 etc.
In reply to akashsoni29:
Actually, it should be 1’b1 as that is the standard definition of “true”.
Of course, any number other than zero would work.
I had a typo when I wrote '1,apologies.
Better stick to a standard.
Ben