Counting number of events on clock a, while clock o is forbidden

SystemVerilog
, ,
16

In reply to ben@SystemVerilog.us:

I believe that there are issues with the requirements.
// Contradiction: O will be 1 once in its life time and after that will die away.
// O can’t be 1 while A is 0, any occurrence of O other than the one specified above is a violation
Is o ==1 once and only once?


// Initially, o must be 0
  ap_o0: assert property(@(posedge clk) 
  		$rose(rst) |-> o==0); 
  		                             
  ap_p0: assert property(@(posedge clk)  		                            
      ($rose(rst) ##1 a[->5]) intersect !o[*] |=> o==1'b1 ##0 a ~^ o[*1000]); 
 // Contradiction:  O will be 1 once in its life time and after that will die away.
  // O can't be 1 while A is 0, any occurrence of O other than the one specified above is a violation

Ben SystemVerilog.us