時序電路講究建立時間、保持時間需要留有裕量。這也說明了，在電路中信號的順序以及之間的時序關系十分重要

如果激勵的輸入輸出不滿足設計的要求，那么測試的結果也是不可靠的。同樣，如果設計內部不滿足要求，輸入輸出的關系也不正確。為了檢驗這之間的關系，便引入了assertion.

由參考資料可知幾點，非時序邏輯時，assertion的形式如下：

ASSERTION_TEST:
 assert (condition)
 else
  $error("check failed");

而對于時序邏輯的assertion，形式如下:

ASSERTION_TEST:
 assert
  property(
  @(posedge clk) disable iff (rst)
   condition
  )
  else
   $error("check failed");

或

property ASSERTION_TEST:
  @(posedge clk) disable iff (rst)
   condition
  )
endproperty

ASSERTION_ACTION: assert property (ASSERTION_TEST)

其它的一些系統函數，操作符作用如下，可以進參考資料查看：

那么，接下來我們就做個小測試，使用req ack的握手過程作為檢測過程。

信號的時序圖要求如上圖，握手過程為：

1. req信號拉高，此時ack信號還是低電平
2. 在req信號拉高后，ack信號拉高
3. req端檢測到ack拉高，拉低req信號
4. ack端的處理結束，檢測到req信號拉低，ack信號拉低

那么，我們簡單寫一個ack應答的模塊，內容如下：

module req2ack(
  input  clk ,
  input  rst ,

  input  en  ,
  input  req ,
  output reg ack 
);

reg [7:0] req_arr;

always @ (posedge clk or posedge rst)
begin
 if (rst)
  req_arr <= 'd0;
 else if (en)
  req_arr <= {req_arr[5:0], {2{req}}};
end

always @ (posedge clk or posedge rst)
begin
 if (rst) 
  ack <= 1'b1;
 else if (en)
  ack <= req_arr[7] ; 
end

endmodule

req經過8個時鐘周期和使能信號的延遲后，ack做出應答。

tb簡單寫為：

module tb;

reg clk ;
reg rst ;
reg en  ;
reg req ;
wire ack;

initial begin
 clk = 0;
 rst = 1;
 en  = 0;
 req = 0;
 #100
 rst = 0;
 en  = 1;
 #100
 req = 1;
 wait(ack);
 req = 0;
 #50
 req = 1;
 #20
 req = 0;
 #50
 $finish;
end

initial begin
 $fsdbDumpfile("tb.fsdb");
 $fsdbDumpvars;
 $fsdbDumpSVA;
end

always #10 clk = ~clk;

req2ack req_inst(
  .clk(clk) ,
  .rst(rst) ,
  .en (en ) ,
  .req(req) ,
  .ack(ack) 
);

`ifdef ASSERTION_ENABLE
 `include "tb_assertion.v"
`endif

endmodule

提供20ns的周期時鐘，使能信號；以及兩次req信號拉高的模擬激勵。

assertion定義在tb_assertion.v文件中，在仿真時定義ASSERTION_ENABLE的宏，可以調用assertion檢查。

tb_assertion.v定義為：

check_req_ack_rise:
    assert property(
 @(posedge clk) disable iff (rst)
  $rose(req) |- > ##1 (req & ~ack)[*0:$] ##1 (req & ack)
 )
 else
   $error("req to ack rising edge is fail");

check_req_ack_fall:
    assert property(
 @(posedge clk) disable iff (rst)
  $rose(ack) |- > (req & ack)[*0:$] ##1 (~req & ack)[*0:$] ##1 (~req & ~ack)
 )
 else
  $error("req to ack falling edge is fail");

第一塊內容，檢查req-ack握手過程的1，2兩步；第二塊內容，檢查req-ack握手過程的3，4步。

$rose(req)的意思是由上文或參考資料可知，等到req信號的上升沿有效；

|->操作符表示，LHS(左側表達式)條件滿足，則在同一時刻去檢查RHS的表達式；

##1 代表延時1個時鐘周期；

(req & ~ ack)[*0:$] 代表此時req信號為高，ack信號為低的情況滿足0或多個時鐘周期；周期不確定

第一塊內容的意思是，等到req信號上升沿，過一個時鐘周期檢查req拉高，ack為低的情況是否滿足，這個過程可能持續多個周期，不確定；然后就是ack信號拉高。檢查結束

第二塊內容的意思是，等到ack信號上升沿，檢查req和ack的信號是否都拉高，這個過程可能持續多個周期，不確定；然后req信號拉低，ack保持，也會持續多個周期，最后ack信號也拉低。

最后，在運行vcs時，需要加入“+fsdb+sva_success -assert”

測試結果：

那么，我們對激勵稍作修改下：

initial begin
 clk = 0;
 rst = 1;
 en  = 0;
 req = 0;
 #100
 rst = 0;
 en  = 1;
 #100
 req = 1;
 wait(ack);
 #20
 req = 0;
 wait(~ack);
 #50
 $finish;
end

Assertion的結果：

這只是作為一個小例子，而且寫的過于匆忙，我相信應該是有更好的assertion寫法，所以權當是一次記錄的草稿內容。