In reply to Jadoon:
Several comments:
Syntax
// $rose(rst) ##1 ((a[=5]) intersect (!o[*])) |=> ((a ~^ o)[*0:1000]);
// TOO MANY parentheses, modified it to:
($rose(rst) ##1 a[=5]) intersect !o[*] |=> (a ~^ o)[*0:1000]
*-------------------------------------
// You seem to INSIST on using in this case the a[=5] instead of the a[->5].
// b[=2] is equivalent to: // From my book, page 37
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]
b[->2] is equivalent to: // From my book, page 35
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
//Thus, looking at the antecedent, using 2 for simplicity
($rose(rst) ##1 a[=2]) intersect !o[*]) // is same as
($rose(rst) ##1 !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]) intersect !o[*])
// The last !b[*0:$] creates a problem because all matches of antecedent must be
// executed for an assertion to succeed. See 2.5.1 first_match operator for an explanation.
// THUS, the assertion can never succeed; it can fail or be vacuous.
If you insist on using the [=5], then use the first_match operator
first_match($rose(rst) ##1 a[=5]) intersect !o[*] |=> (a ~^ o)[*0:1000]
// But, by using the goto -> operator, you don't need a first_match.
($rose(rst) ##1 a[->2]) intersect !o[*]) // is same as
($rose(rst) ##1 !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b) intersect !o[*])
Requirements
- I have two variables A and O that are related to each other.
- Each clock cycle of clk, the values of A,O are sampled.
- Initially, the O must be 0 else it would be a violation.
[Ben] That should be a separate assertion
*----------------------------------------------- - There is no restriction on A, that when it can come.
- When we see the high value on A for the nth time (say 5th time), then that’s the moment when O should also be 1.
- The sampled value of A can possibly be 1 for five consecutive cycles of clk or it can come literally after a gap of 1000s of cycles of clk.
- O will be 1 once in its life time and after that will die away.
- O can’t be 1 while A is 0, any occurrence of O other than the one specified above is a violation.
[Ben] I believe that what you lastly wrote seems to be what you need. Below is code that I tested.
module ccsl;
bit a, o, clk, rst;
// Initially, o must be 0
ap_o0: assert property(@(posedge clk)
$rose(rst) |-> o==0);
ap_p0: assert property(@(posedge clk)
($rose(rst) ##1 a[->5]) intersect !o[*] |=> a ~^ o[*0:1000]);
initial forever #5 clk=!clk;
initial begin
@(posedge clk) rst <= 1'b1;
@(posedge clk) rst <= 1'b0;
end
always @(posedge clk)
begin
if (!randomize(rst, a, o) with
{ rst dist {1'b1:=1, 1'b0:=99};
a dist {1'b1:=40, 1'b0:=60};
o dist {1'b1:=10, 1'b0:=70}; }) $display("error");
end
endmodule
A few lessons that you may have learned from this exercise:
- Making requirements clear is necessary.
- Assertions help in clarifying the requirement becuase it forces you to explain.
- Write many small assertions
- If confusing, write the requirements, step-by-step in English
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