How to check a signal is going high once using assertion

Hi,
Could you please let me know how to write a signal is going high once using system verilog assertion. could you please let me know the following code is correct.


module one;
 int a ,b,clk; 
  initial
    forever
      #5 clk=~clk;
  initial begin
   #1000ns $finish; 
  end
  initial begin
    #5 a=1;
    
  end
 property rstcheck(logic a);
   firstmatch( ##[1:$] $rose(a));

  endproperty
  
  first:assert property ( @( posedge clk)rstcheck(a));
                   
initial begin 
   
end 
    endmodule     
    



In reply to ben@SystemVerilog.us:

Thanks ben for the clarificaions.

In reply to ben@SystemVerilog.us:

initial ap_a_once_ever: assert property(@ (posedge clk)
         $rose(a) [->1]  |=> strong(a[*1:$])  );

How to modify this one to make sure this assertion fails when a gets de-asserted at some point in the simulation?

In reply to nimitz_class:
OOPS! I made a mistake. Should be


 let max= int'(1.0E30); 
    initial ap_a_once_ever: assert property(@ (posedge clk)
         $rose(a) [->1]  |=> strong(a[*max]));

testbench


module top;
    timeunit 1ns;  timeprecision 100ps; 
    bit clk, a, b=1, c=1, reset_n;
    default clocking @(posedge clk);
    endclocking
    initial forever #10 clk = !clk;
    initial begin 
        #100 @(posedge clk) a <=1'b1; 
        // #1000 a <= 1'b0; 
    end 
    let max= int'(1.0E30); 
    initial ap_a_once_ever: assert property(@ (posedge clk)
         $rose(a) [->1]  |=> strong(a[*max]));
      // will fail if a==0 or at end of sim  
    
    initial begin
        #2000; 
      $finish;
    end
  endmodule
  
   
  
  
  

In reply to ben@SystemVerilog.us:

In reply to nimitz_class:
OOPS! I made a mistake. Should be


let max= int'(1.0E30); 
initial ap_a_once_ever: assert property(@ (posedge clk)
$rose(a) [->1]  |=> strong(a[*max]));

testbench


module top;
timeunit 1ns;  timeprecision 100ps; 
bit clk, a, b=1, c=1, reset_n;
default clocking @(posedge clk);
endclocking
initial forever #10 clk = !clk;
initial begin 
#100 @(posedge clk) a <=1'b1; 
// #1000 a <= 1'b0; 
end 
let max= int'(1.0E30); 
initial ap_a_once_ever: assert property(@ (posedge clk)
$rose(a) [->1]  |=> strong(a[*max]));
// will fail if a==0 or at end of sim  
initial begin
#2000; 
$finish;
end
endmodule

I tried this and it works when a gets de-asserted, but it also fails initially when a is zero for some time. So, in my simulation a is zero from the start of the simulation and gets asserted after a point. So, I want this assertion to capture the bug - i.e. whenever a falls after it goes high.

In reply to ben@SystemVerilog.us:

Also, this consumes too much memory. Need a better way to do this.

In reply to nimitz_class:
http://systemverilog.us/vf/quicktest.sv


initial ap_a_once_ever: assert property(@ (posedge clk)
         $rose(a) [->1]  |=> strong(a[*300000]));

FOr faster simulation


bit a_rose, a_fell; 
    task automatic t_a; 
        @($rose(a, @(posedge clk))) begin 
         a_rose=1'b1; 
            // fork
                @($fell(a, @(posedge clk))) begin 
                    `uvm_error("MYERR", "a fell ");
                a_fell=1'b1; 
                end
            //join  
            end
    endtask

    initial t_a(); 
    final begin 
        $display("%t at final", $realtime );
        if(a_rose && a_fell) $display("%t a_rose and  fell", $realtime );
    end

FOr some reason the final message is not displayed. I’ll let you debug that