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

In reply to Jadoon:

OK, I worked out the AsFrom assertion and the tb for it.
The png result is at http://systemverilog.us/ccsl.png
The code is at http://systemverilog.us/ccsl.sv
I used constrained-randomization with count as the vehicle to define the types of constraints.
Using constrained-randomization is a fast way of achieving a variety of test vectors.
BTW, I added an error on count 16 to demonstrate the failure.


module ccsl;
  bit a, o, clk, clk1, rst;
  int count; 
  // Initially, o must be 0
  ap_o0: assert property(@(posedge clk) 
  		$rose(rst) |-> o==0); 
  		                             
  // AsFrom: Initially O is 0, A comes at any time. On Kth arrival of A sampled on clk, 
  // O should be there, and afterwards O is exactly same as A.
  // Let k==5
  ap_AsFrom: assert property(@(posedge clk)  		                            
      (($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1] |-> 
                                                    o==1'b1 ##1 a ~^ o[*1000]); 
 
 initial forever #5 clk=!clk;
 
 initial begin 
 	@(negedge clk) rst <= 1'b1;
 	@(negedge clk) rst <= 1'b0;
 end
  
  always @(posedge clk) 
     begin 
     	if (count <4) begin 
     	   if(a ) count<=count+1'b1; // increment before update of "a" 
     	   if(!randomize(rst, a, o) with 
       		{ rst dist {1'b1:=1, 1'b0:=999}; // can comment this line 
       		  a   dist {1'b1:=25, 1'b0:=75};
       		  o   dist {1'b1:=10, 1'b0:=70}; 
       		  0==1'b0;}) $display("error");    	   
           end
        
        else if (count == 4) begin 
        	if(!randomize(rst, a, o) with 
       		{ rst dist {1'b1:=1, 1'b0:=999};
       		  a   dist {1'b1:=30, 1'b0:=70};
       		  o   dist {1'b1:=10, 1'b0:=10};
       		  o==a; }) $display("error"); 
        	if(a) count<=count+1'b1;
            end 
            
        else if (count >= 5 && count <16 ) begin 
        	count<=count+1'b1;
        	if(!randomize(rst, a, o) with 
       		{ rst dist {1'b1:=1, 1'b0:=999};
       		  //a   dist {1'b1:=30, 1'b0:=30};
       		  //o   dist {1'b1:=10, 1'b0:=10};
       		  o==a; }) $display("error");             
            end 
        else if (count==16) begin 
        	count<=count+1'b1;
            if(!randomize(rst, a, o) with 
       		{ rst dist {1'b1:=1, 1'b0:=99};
       		  a   dist {1'b1:=30, 1'b0:=30};
       		  o   dist {1'b1:=10, 1'b0:=10};
       		  a!=o; }) $display("error");           
         end 
         else  begin 
        	count<=count+1'b1;
        	if(!randomize(rst, a, o) with 
       		{ rst dist {1'b1:=1, 1'b0:=999};
       		  a   dist {1'b1:=30, 1'b0:=30};
       		  o   dist {1'b1:=10, 1'b0:=10};
       		  o==a; }) $display("error");  
        	end 
     end 
endmodule 

Ben SystemVerilog.us