Assertion to check pulse 2 inside pulse 1

HI 

Need to write a assertion :: 
1)Pulse 1 should be high for 10~100 clock cycles.
2)Pulse 2 Should be high within Pulse 1 for 1 clock cycle.Pulse 2 should occur only one time.

Please help on this.

Thanks

In reply to syed taahir ahmed:
Restating your requirements:

  1. Following the rise of “a”, “a” should be stable for 10 to 100 cycles.
  2. “a” represents an envelope in which a single pulse “b” should occur once.

  initial 
    ap_b_in_a: assert property(@ (posedge clk) 
       $rose(a)[->1] |-> a[*10:100]  intersect b[->1] ##1 b==0[*1:$]);  
     

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Thanks Ben!!

In reply to ben@SystemVerilog.us:

Hi Ben,

Seems like the property not able to fail for the occurrence of pulse 2 twice in pulse 1, i replicated the scenario in Eda playground ,please have a look.

link:: Edit code - EDA Playground

Thanks

In reply to syed taahir ahmed:
The assertion reflects the requirements:
ref files : http://systemverilog.us/vf/pulses2c.sv
http://systemverilog.us/vf/pulses2c.png


// master_prop states that pulse1 extends between 10 and 100 cycles, and within that region,
// you have ONE occurrence of pulse2=1 and then pulse2==1 possibly being repeated 1 to $.
 pulse1[*10:100]  intersect( pulse2[->1] ##1 pulse2==0[*1:$])
// That property is ian intersection, thus, with pulse1==1 at all cycles within that range, 
// once pulse2==1 and then pulse2=0, THAT intersection is complete and the assertion succeeds. 
// All we asked here is that plse2 occurs within  pulse1[*10:100] but not within pulse1[*100]

   property master_prop;
        @ (posedge clk)
        disable iff (reset)
        $rose(pulse1)[->1] |-> pulse1[*10:100]  intersect( pulse2[->1] ##1 pulse2==0[*1:$]);    
    endproperty
//---------
// Now, what you may be looking for is that pulse1 holds (true) for 100 cycels 
// and within that period pulse2 is a single pulse. 
    property master_prop2;
        @ (posedge clk)
        disable iff (reset)
        $rose(pulse1)[->1] |-> pulse1[*100]  intersect( pulse2[->1] ##1 pulse2==0[*1000]);    
    endproperty
//--------
// However, if you still want pulse1 to be the range 10:100, you could add another assertion
// that once pulse1 occurrs, there should s single pulse2 until pulse1 falls. 
ap_continue: assert property(@ (posedge clk) $rose(pulse1)[->1] |-> 
     $fell(pulse1)[->1]  intersect(pulse2[->1] ##1 pulse2==0[*1:$]));  
 

Assertions can be tricky! That is why you need to test the complex ones and really understand the meaning behind the syntax.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy

In reply to ben@SystemVerilog.us:

Thanks Ben for detailed reply, I’ll get this one executed.

How about this?


property p1;
$rose(Pulse1) |-> Pulse2[=1] within Pulse1[*10:100];
endproperty

In reply to devil47:
First off, let me correct some errors in my response:

  • The following in INCORRECT
    rose(pulse1)[->1] |-> pulse1[*10:100] intersect( pulse2[->1] ##1 pulse2==0[*1:]); // BAD
    rose(pulse1) |-> pulse1[*10:100] intersect( pulse2[->1] ##1 pulse2==0[*0:]); // OK
    $rose(pulse1) |-> pulse1[*10:100] intersect( pulse2[=1] ); // OK
  • Comments
    $rose(pulse1)[->1] should be written as rose(pulse1) becuse the goto operator is meaningless here. b[->1] is equivalent to !b[*0:] ##1 b, thus causing unnecessary attempts.
  • b[=m] is equivalent to ( b [->m] ##1 !b [*0:$]

On your comments:

 
// You suggest 
$rose(Pulse1) |-> Pulse2[=1] within Pulse1[*10:100];

// Note: 
seq1 within seq2) is equivalent to: ((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )

// Thus, your suggestion is equivalent to 
$rose(Pulse1) |-> (1[*0:$] ##1 Pulse2[=1] ##1 1[*0:$]) intersect Pulse1[*10:100];

// That is also equivalent to 
  $rose(a) |-> 
      a[*1:4]  intersect( b[->1] ##1 b==0[*0:1000]) );    


``` verilog

// Always tests your assertions 
// The following model demonstrates that all 3 assertions are equivalent in simulation 
module top; 
   timeunit 1ns/100ps;
   `include "uvm_macros.svh"
    import uvm_pkg::*;
    bit clk, a, b;  
    default clocking @(posedge clk); 
    endclocking
    initial forever #10 clk=!clk;  
    initial begin
      $timeformat(-9, 1, "ns", 8);
      $display("%t", $realtime);
   end 
    ap_within: assert property(@ (posedge clk)  $rose(a) |->
        b[=1] within a[*1:4]);  

    ap_ab_eqv: assert property(@ (posedge clk)  $rose(a) |-> 
    (1[*0:$] ##1 b[=1] ##1 1[*0:$]) intersect a[*1:4]);

    ap_ab1: assert property(@ (posedge clk) 
      $rose(a) |-> 
      a[*1:4]  intersect( b[->1] ##1 b==0[*0:1000]) );  

    
    initial begin 
      repeat(200) begin 
        @(posedge clk);   ##1; 
        if (!randomize(a, b)  with 
        { a dist {1'b1:=5, 1'b0:=1};
          b dist {1'b1:=1, 1'b0:=3};      
      })  `uvm_fatal("RAND", "This is a randomize error") 
     end 
     $stop; 
   end 
endmodule     

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy