sva_properties.txt

Write Assertions for the following descriptions.
1. There could be maximum 2 requests ( req ) within 10 cycles: 
 assert_1: assert property (@(posedge clk) 
 (req[->3] within `TRUE[*10] ) );
2. There should be minimum 2 requests ( req ) within 10 cycles
 sequence s2;
 @ (posedge clk) (req[*2:$] within `TRUE[*10] ) );
 endsequence
 assert_2: assert property ( s2);
3. After 3 requests ( req ), grant ( gnt ) should assert within 3 cycles
property p_req_gnt; 
 @(posedge clk) req[->3] |-> ##[1:3] gnt);
 endproperty 
 assert_3: assert property (p_req_gnt); 
4. No new request ( req ) until grant ( gnt ) occurs
 sequence s4;
 @ (posedge clk) req |=> !req throughout gnt[->];
 endsequence
 assert_4: assert property (s4);
 
5. " hitcnt " can be asserted only when "index[270] is 1 and index[269] is zero and “ index_w ” is one
 sequence s5;
 hitcnt |-> ((index[270]) && (!index[269]) && (index_w));
 endsequence
 assert_5: assert property (@(posedge clk) s5);
6. when "req_32" is asserted for only one cycle, it should not generate another " req " until " strb " is 
asserted or 10 cycles later
 sequence s6;
 $rose(req_32) |-> ##1 ((!req_32) [*10]) or (!req_32 throughout strb[->])));
 endsequence
 assert_6: assert property (@(posedge clk) s6);
7. when design is out of reset, all outputs o1, o2, o3 must be valid (cannot be X or Z) 
 at rising edge of clock ( clk )
assert_6: assert property (@(posedge clk) disable iff (rst) !$isunknown({o1, o2, o3}) );
8. After bus enable ( be_n ) is activated (active low), address ( addr ) is help until the transaction 
terminates (! fail_n or ! abort_n ) // all signals are active low
 
 sequence s8;
 $fell(be_n) |-> $stable( addr) throughout ((! fail_n || ! abort_n) [->1]) ;
 endsequence
 assert_8: assert property (@(posedge clk) s8);
 
 
9. For write transfers, the bus should hold the data stable throughout the extended cycles (wait 
states).
When " st == 2'b11" or " st == 2'b10", indicates wait states.
wire wait_states = (state == 2’b11) || (state == 2’b10); 
assert property ( @(posedge clk) (write_transfer) && (wait_states) |-> $stable(data) ;
 
 
10. For every "start" pulse, there should be corresponding "end" pulse.
start1 |-> ##1 (!start1 throughout end[->1]) 
end1 |-> ##1 (!end1 throughout start1[->1]) 
$fell(rstn)|-> (!end1 throughout start1[->1])
logic [15:0] pend_start_cnt,pend_start_cnt_r;
assign pend_start_cnt=rst?16’b0: ( pend_start_cnt==0) && start2 ? 16’b1: ( pend_start_cnt_r) && 
start2 && !end2 ? pend_start_cnt_r + 1’b1: ( |pend_start_cnt_r) && start2 && !end2 ? 
pend_start_cnt_r -1’b1: pend_start_cnt_r;
no_end2_before_start2: assert property(pend_start_cnt_r==0) |-> !end1
no_pend_start_cnt_oflow: assert property(pend_start_cnt_r==MAX) && !end2 |-> !start2