Hi
I want to check if a signal is low for minimum 32 clock cycles.
Please help.
In reply to pRoSpEr:
I have written the following assertion:
property poreset_clock_check;
int v_t;
@(posedge clk) (fell(PORESET_B),v_t=0) |-> (1, v_t=v_t+1)[*0:] ##0 $rose(PORESET_B) |-> (v_t >= 32);
endproperty
Do comment on its correctness.
property poreset_clock_check; // Poorly written assertion!!!
int v_t;
@(posedge clk) ($fell(PORESET_B),v_t=0) |->
(1, v_t=v_t+1)[*0:$] ##0 $rose(PORESET_B) |-> (v_t >= 32);
endproperty
ap_poreset_clock_check: assert property(poreset_clock_check);
There are several things wrong with the above assertion:
[list=1]
[*] (1, v_t=v_t+1)[*0:$] ##0 $rose(PORESET_B) includes an empty match.
Note: a[0] is an empty match, and
empty ##0 seq is a no match. The point is that this aspect of the property adds no meaning to the specification, and should be avoided.
Note that (empty ##1 seq) is same as (seq)
[] You cannot have a $fell(PORESET_B) and a rose(PORESET_B) in the same cycle, thus why use the |->? It is a confusing specification, and is meaningless.
**Avoid meaningless terms in an assertion**
[*] v is of type int, and adding a 1 to an int, though OK. However, if v were a vector (e.g., bit[4:0]) adding an integer 1 can lead to errors. I, general I prefer to use 1'b1.
See http://systemverilog.us/int_arith.pdf for an explanation of the error.
[*] The property of the form (x[*0:] ##1 z |-> w) must check ALL terms of the antecedent for it to succeed. Thus, you would need a first_match
Below is code that reflects the needed corrections.
import uvm_pkg::*;
`include "uvm_macros.svh"
module min;
bit clk, PORESET_B;
initial forever #5 clk=!clk;
property poreset_clock_check;
int v_t;
@(posedge clk) ($fell(PORESET_B),v_t=0) |=>
first_match( (1, v_t=v_t+1'b1)[*1:$] ##0 $rose(PORESET_B)) |-> (v_t >= 32);
endproperty
ap_poreset_clock_check: assert property(poreset_clock_check);
always @(posedge clk)
if (!randomize(PORESET_B) with {PORESET_B dist {1'b1:=5, 1'b0:=95};})
`uvm_error("MYERR", "This is a randomize error");
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
In reply to ben@SystemVerilog.us:
Hi Ben,
I agree with points 2 and 3, which were not thought over by me while coding the assertion.
W.r.t point 1 : If I am using |=> operator, then what if the PORESET_B falls on the next sampling event. There seems no need to change [*0:] to [*1:].
W.r.t point 4 : If $rose(PORESET_B) is true, then it will check (v_t >=32) in the same clock. What is the need of first_match as the consequent is calculated on each sampling event?
Please clarify.
In reply to pRoSpEr:
W.r.t point 1 : If I am using |=> operator, then what if the PORESET_B falls on the next sampling event. There seems no need to change [*0:] to [*1:].
A property represents the requirements; thus, though it would work, it adds meaningless info. My point: Avoid meaningless terms in an assertion. From The Presenter's Fieldbook: A Practical Guide - Robert J. Garmston, Co-developer of Cognitive Coaching and Adaptive Schools; emeritus professor, California State University, Sacramento - Google Books
“Too many notes”
W.r.t point 4 : If $rose(PORESET_B) is true, then it will check (v_t >=32) in the same clock. What is the need of first_match as the consequent is calculated on each sampling event?
( (1, v_t=v_t+1'b1)[*0:$] ##0 $rose(PORESET_B)) |-> (v_t >= 32);
// IS SAME as
( (1, v_t=v_t+1'b1)[*0] ##0 $rose(PORESET_B) or // This is a NO match, meaningless
(1, v_t=v_t+1'b1)[*1:$] ##0 $rose(PORESET_B) or
(1, v_t=v_t+1'b1)[*2:$] ##0 $rose(PORESET_B) or
...
(1, v_t=v_t+1'b1)[*n:$] ##0 $rose(PORESET_B) |-> (v_t >= 32);
// For a success, ALL, really ALL terms of the antecedent must be tested for this property to succeed. If any antecedent is a no match, the property for that match is vacuously true. However, since this property can fail on another antecedent match, all terms of this infinite antecedent must be tested. That is why you need the first_match.
Ben Cohen
In reply to ben@SystemVerilog.us:
Hi Ben,
( (1, v_t=v_t+1’b1)[*0:$] ##0 $rose(PORESET_B)) |-> (v_t >= 32);
// IS SAME as
( (1, v_t=v_t+1’b1)[*0] ##0 rose(PORESET_B) or // This is a NO match, meaningless (1, v_t=v_t+1'b1)[*1:] ##0 rose(PORESET_B) or (1, v_t=v_t+1'b1)[*2:] ##0 rose(PORESET_B) or ... (1, v_t=v_t+1'b1)[*n:] ##0 $rose(PORESET_B) |-> (v_t >= 32);
// For a success, ALL, really ALL terms of the antecedent must be tested for this property to succeed. If any antecedent is a no match, the property for that match is vacuously true. However, since this property can fail on another antecedent match, all terms of this infinite antecedent must be tested. That is why you need the first_match.
It seems that the assertion will work as the antecedent will be true, however it is not written accurately.
In reply to pRoSpEr:
It seems that the assertion will work as the antecedent will be true, however it is not written accurately.
That assertion can never succeed, but can fail.
For a success, as I explained, all terms of the antecedent must be tested, but you have an infinite number of terms You need the first_match!
Ben
In reply to pRoSpEr:
Why not simply use?
a_min_32_clk_low : assert property (@(posedge clk)
!a |-> !a[*32]);
Maybe the requirement is little more?
Regards
Srini
http://www.verifworks.com
In reply to Srini @ CVCblr.com:
a_min_32_clk_low : assert property (@(posedge clk)
!a |-> !a[*32]);
That will work, except that the antecedent needs to be something other than !a since at every clock cycle you’ll have a new attempt with the same requirement (at every clock edge “a” must be repeated 32 more times.
Ben Cohen
In reply to ben@SystemVerilog.us:
Good point. How about
a_min_32_clk_low : assert property (@(posedge clk)
##1 $fell(a) |-> !a[*32]);
OP has to confirm whether this will satisfy his need.
In reply to Srini @ CVCblr.com:
Should work.
In reply to Srini @ CVCblr.com:
In reply to ben@SystemVerilog.us:
Good point. How about
a_min_32_clk_low : assert property (@(posedge clk)
##1 $fell(a) |-> !a[*32]);
OP has to confirm whether this will satisfy his need.
Srini
http://www.verifworks.com
Hi,
could you please let me know why ##1 is needed in this assertion.