Systemverilog 筆記 - Assertions

create Boolean expression -> create sequence expression ->  create property(concurrent) -> assert property

uprange sign $ overlapped implication |-> non-overlapped implication |=> consecutive repetition [*n] go-to repetition [->] non-consecutive repetition [=min_times:max_times] $rose 回傳true,如果LSB轉換到1 $fell  回傳true,如果LSB轉換到0 $stable 回傳true如果沒有轉換準位 $past 是針對前一個clock來取樣,但是傳回值是在現在的clock

##1  經過一個clock cycle delay

a ##2 b  a 的兩個周期以後出現b才會trigger

a ##[1:$]  b  a active 後的任一周期 b active 才會trigger

(a ##2 b) |-> c  a active後兩個周期b active ,同時c也active

(a ##2 b) |=> c  a active後兩個周期b active ,一個週期後c active

(a ##1 b) [*2]  a active後一個周期b active , 這樣的情況要重複兩次

a ##1 (b[*4])  a active後一個周期b要連續active 四個周期

(a ##1 b) [*1  2] = (a ##1 b) or (a ##1 b) ##1 (a ##1 b)  a active後一個周期b要active 一個周期, 這種情形重複一次或是兩次

(a[*1:2] ##1 b)  a active一或是二個周期, 一周期後,b active

a |=> b[=2]  a active 後的下一個周期b 要至少active 兩次(不用連續)

a ##2 b [=3:4] ##1 c  a active 兩個周期之後, b 經過最少三次最多四次active, 一個周期後c active

a |=> b[->2]  a active 後的下一個周期b 要active 兩次(不用連續)

a |=> (b[->2] ##2 c)  a active 後的下一個周期b 要active 兩次(不用連續), 兩周期後c active

(a ##2 b) and (c ##3 d)  and 檢查這兩個序列是否都合格,這兩個序列必須要有相同的起始點, 如果第一個序列比對成功,會等待第二個序列成功, 最後成功時間為第二序列時間

(a ##2 b) or (c ##3 d)  or 檢查這兩個序列是否其中一個合格,這兩個序列必須要有相同的起始點, 時間為最先成功的時間

<anteceent> throughout <consequent> concequent 在 antecedent為active時,必須比對成功,否則會回傳false

(!en) throughout ##2 (reg ##[0:4] gnt) 在en為0的時候, 兩個周期之後 reg 必須為1,且在最小0周期最大四周期的時候 gnt為1

(a ##[2:4] b) intersect (c ##[3:4] d) intersect與and 相似, 不同的是其要求兩個序列比須有相同的比對成功長度, 上面第一個如果2T 3T 4T 比對成功,第二個3T 4T 成功,這樣只會傳回3T 4T

first_match(a ##[2:4] b) first_match(c ##1 d) 如果比對成功處均在同一個地方結束,則濾出第一個比對成功的地方, 如果序列是在不同的地方結束,則其為讓每一個比對成功處為true