SVA介紹----重複運算符

重複運算符

• • 連續重複運算符
  • • 1. 信号的連續重複
    • 2. 序列的連續重複
    • 3. 帶延遲視窗的序列的連續重複
    • 4. 連續重複和可能運算符
  • 跟随運算符
  • 非連續重複運算符

• 如果給定信号“start”在任何時鐘上升沿，出現上升沿；然後，時鐘下個周期起，a信号連續持續三個周期的高電平；然後，下個時鐘周期，信号”stop“為高；利用此前的方法，我們可以這樣寫：

//備援的代碼寫法
sequence test;
	@(posedge clk) $rose(a) |->	##1 a ##1 a ##1 a ##1 stop;
endsequence
           

• 為了解決這種備援的寫法，SVA提供了三種不同的運算符：
  • 連續重複： 使用者可以指定信号或序列，在指定數量的周期内都連續的比對；
    • consecutive repetition
    • 要求必須在連續的時鐘周期比對；
    • 文法：signal or sequence [*n]
  • 跟随重複： 使用者可以指定信号或序列，比對達到指定次數，但是不要求連續；
    • go to repetition
    • 不要求在連續時鐘比對，要求最後一次比對在整個比對結束之前；
    • 文法：signal or sequence [->]
  • 非連續重複：
    • non-consecutive repetition
    • 不要求在連續時鐘比對，不要求最後一次比對在整個比對結束之前；
    • signal or sequence [=>]

連續重複運算符

1. 信号的連續重複

//信号的連續重複
sequence p21;
	@(posedge clk) $rose(a) |->	##2 (a[*3]) ##2 stop ##1 !stop;
	//整個序列檢查時長為 2+3+2+1 = 8
endsequence
           

2. 序列的連續重複

//序列a ##2 b 重複三次；
property p22;
	@(posedge clk) $rose(a) |->	##2 ((a ##2 b)[*3]) ##2 stop ##1 !stop;
	//整個序列檢查時長為 2+3*2+2+1 = 11
endproperty
           

3. 帶延遲視窗的序列的連續重複

//序列a ##[1:4] b 重複三次；
property p23;
	@(posedge clk) $rose(a) |->	##2 ((a ##[1:4] b)[*3]) ##2 stop ##1 !stop;
endproperty
//((a ##[1:4] b)[*3])可以擴充為：
//((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b)) ##1
//((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b)) ##1
//((a ##1 b) or (a ##2 b) or (a ##3 b) or (a ##4 b))
           

4. 連續重複和可能運算符

//序列a[*1:5]表示信号a從某個時刻，連續重複1～5次；
property p24a;
	@(posedge clk) $rose(a) |->	##2 (a[*1:5]) ##1 stop ##1 !stop;
endproperty
//(a[*1:5])可以擴充為：
// a or
// (a ##1 a) or 
// (a ##1 a ##1 a) or 
// (a ##1 a ##1 a ##1 a) or
// (a ##1 a ##1 a ##1 a ##1 a)
           

//序列a[*1:5]表示信号a從某個時刻，連續重複1～n次，直至stop信号為高；
property p24b;
	@(posedge clk) $rose(a) |->	##2 (a[*1:$]) ##1 stop ##1 !stop;
endproperty
//(a[*1:$])可以擴充為：
// a or
// (a ##1 a) or 
// (a ##1 a ##1 a) or 
// (a ##1 a ##1 a ##1 a) or
// (a ##1 a ##1 a ##1 a ##1 a)
// ......
           

跟随運算符

//屬性檢查start上升沿後，兩個時鐘周期後，a連續或間斷的出現三次，然後下個周期，stop信号為高；
//在stop有效的前一個周期，信号a必須比對；
property p25;
	@(posedge clk) $rose(a) |->	##2 (a[->3]) ##1 stop ##1 !stop;
endproperty
a25: assert property(p25);
           

非連續重複運算符

//屬性檢查start上升沿後，兩個時鐘周期後，a連續或間斷的出現三次，然後下個周期，stop信号為高；
//在stop有效的前一個周期，信号a不要求必須比對；
property p26;
	@(posedge clk) $rose(a) |->	##2 (a[=3]) ##1 stop ##1 !stop;
endproperty
a25: assert property(p25);
           

屬性p25/p26做同樣的檢查，唯一的差別是p26使用的是非連續重複元算，而不是跟随運算符，是以在信号"stop"有效的前一個時鐘周期，信号“a”不需要一定有效比對。