SV Assertion

SystemVerilog
1

How do I write a property for the following:-
When signal aa toggles from 0 to 1, signal bb should become 1’b0 after 5 ns and should remain 1’b0 till signal aa = 1.
Note that signal aa is an asynchronous input.

Thanks!

2

In reply to new_to_uvm:
Try something like the following:
Keep in mind that task t_aabb() is forked at every @(posedge aa), thus, the 2n posedge of aa will triggered it again.

with a guard for a single trigger of the task

(1) - EDA Playground // code below

fork    // bb==0 
    begin @(posedge bb) bb_err: assert(0) else err3=1; end // occurs before aa==1
    begin @(posedge aa) bb_ok: assert(! bb) else err4=1; end // bb should be 0 
  join_any 


// When signal aa toggles from 0 to 1, signal bb should become 1'b0 after 5 ns 
// and should remain 1'b0 till signal aa = 1.
module m; 
  timeunit 100ps;  timeprecision 100ps;    
  bit aa, bb, guard; 
  int err1, err2, err3, err4, done;

  task automatic t_aabb();
    realtime t; 
    t=$realtime;
    fork  // bb==1 at entry 
    @(negedge bb) bb_early_ns: assert($realtime-t <50.1
                                      && $realtime-t >= 40.9) else err1=1; 
    #50.5 bb5ns: assert(bb==0) else err2=1;        
  join_any 
  fork    // bb==0 
    begin @(posedge bb) bb_err: assert(0) else err3=1; end // occurs before aa==1
    begin @(posedge aa) bb_ok: assert(! bb) else err4=1; end // bb should be 0 
  join_any  
   done=done+1; // end of the task   
  endtask: t_aabb

  always @(posedge aa) if(!guard) fork t_aabb(); join_none 

  initial begin 
    $dumpfile("dump.vcd"); $dumpvars;
    repeat(1) begin 
     aa=0; bb=1; #20 aa=1; #10 aa=0; guard=1; #40 bb=0; #80 aa=1;
     #100  aa=0; bb=1; #20 aa=1; #10 aa=0; #70 bb=0; #80 aa=1;
     #20 $finish;
    end
  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

3

In reply to ben@SystemVerilog.us:

I solved this assertion using the same approached I explained in my paper
Understanding the SVA Engine Using the Fork-Join Model Verification Horizons - July 2020 | Verification Academy Using a model, the paper addresses important concepts about attempts and threads. Emphasizes the total independence of attempts.

I strongly recommend reading this paper to understand the model behind SVA.