"within" in SVA

SystemVerilog
,
1

sequence s32a;
@(posedge clk) ((!a && ! b) ##1 (c [->3]) ##1 (a &&b));
endsequence

sequence s32b;
@(posedge clk) $fell(start) ##[5:10] $rose(start);
endsequence

sequence s32;
@(posedge clk) s32a within s32b;
endsequence

property p32;
@(posedge clk) $fell(start) |-> s32;
endproperty

a32 : assert property (p32);

The waveform is
10 CLK #0 :: clk=1 start=1 a=1 b=1 c=0
20 CLK #1 :: clk=1 start=1 a=1 b=1 c=0
30 CLK #2 :: clk=1 start=0 a=1 b=1 c=0
40 CLK #3 :: clk=1 start=0 a=0 b=0 c=0
50 CLK #4 :: clk=1 start=0 a=0 b=0 c=1
60 CLK #5 :: clk=1 start=0 a=0 b=0 c=0
70 CLK #6 :: clk=1 start=0 a=0 b=0 c=1
80 CLK #7 :: clk=1 start=1 a=0 b=0 c=0
90 CLK #8 :: clk=1 start=1 a=0 b=0 c=1
100 CLK #9 :: clk=1 start=1 a=1 b=1 c=0
110 CLK #10:: clk=1 start=1 a=1 b=1 c=0

“s32a within s32b” is disobeyed. But why there is no assertion error occur?

The reason described in the book is “a ‘go to’ repetition operator is used to check for signal ‘c’, it acts as a blocking sequence”.

Can experts give me some explanations, why?

Thanks.

2

“s32a within s32b” is disobeyed. But why there is no assertion error occur?
The reason described in the book is “a ‘go to’ repetition operator is used to check for signal ‘c’, it acts as a blocking sequence”.

The term “blocking sequence” is not in SV1800. However, the following equivalents can be defined

(seq1 within seq2) is equivalent to: 
((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
and 
c[->3] is equivalent to:
!c[*0:$] ##1 c ##1 !c[*0:$] ##1 c ##1 !c[*0:$] ##1 c

Your assertion a32 should have failed. If it did not, check with your tool vendor.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • SystemVerilog Assertions Handbook, 2005 ISBN 0-9705394-7-9
  • 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