Creating Assertions

Step 3: Code SVA Assertions (con't)

Full check of address write through data transfer and write response*

[Full-size Image]

The full SVA sequence (created by Zazz) is pretty intimidating:

property AW_W_B_completion;
int wcount;
int wid;
@(posedge ACLK)
 (AWVALID & AWREADY)  |-> (1'b1, wcount=AWLEN+1) ##0 (1'b1, wid=AWID) ##0
(
   ( (  (WVALID & WREADY & (WID==wid)) [->1] ) ##0 (1'b1, wcount=wcount-1) ) [*1:16]
)
 ##0  (WLAST & (wcount==0))  ##0
(
    (##[0:bresp_timeout] (1'b1)) intersect
   ( (BVALID & BREADY & (BID==wid)) [->1] )
);
endproperty