Assertion Question

SystemVerilog
, , ,
6

In reply to MICRO_91:

Comments about the replies:

Requirement :
Sig1 will be high for a few numbers of clock cycles. // Number of clocks are unknown
sig2 can only be high for one clock cycle while sig1 is high.
sig2 toggles do not care if sig1 is not high.


property 
@(posedge clk)
$rose(sig1) |-> sig2[->1] ##1 !sig2[*1:$] intersect sig1[*1:$];
endproperty

I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))?
rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];
when the sequence sig2 ##1 !sig2occurs, the consequent is satisfied.
However, it fails to check if sig2 occurs again for one or more cycles when sig1 remains high for more cycles.
How about something like:
Edit code - EDA Playground // code
EPWave Waveform Viewer // wave

  
    module my_module;
      bit clk, sig1, sig2; 
      int pass, fail; 
      initial forever #1 clk = !clk;
      ap_sig1_2: assert property( @(posedge clk)
          $rose(sig1) |-> (sig1 && sig2)[=1] intersect 
          ##1 !(sig1)[->1]) pass=pass+1; else fail=fail+1;
      initial begin
         $dumpfile("dump.vcd"); $dumpvars; 
         #2 @(posedge clk) sig1 <= 1; 
         repeat(2) @(posedge clk); 
         sig2 <=1; @(posedge clk) sig2 <= 0;
         repeat(2) @(posedge clk); 
         sig1 <= 0; 
         #4 $finish;
      end
    endmodule

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog