As we had discussed ealrier concurrent assertion work on clock edges, so the sequence also. There are two ways clocks can be specified for a sequence to work.

• implied clock : In this clock is specified in property and sequence just uses that clock.
• explicit clock : In this clock is specified inside the sequence block and sequence uses this clock.

Till now we have seen implied clock, below example shows the explicit clock.

  1 //+++++++++++++++++++++++++++++++++++++++++++++++++
  2 //   DUT With assertions
  3 //+++++++++++++++++++++++++++++++++++++++++++++++++
  4 module clock_assertion(
  5   input wire clk,req,reset, 
  6   output reg gnt);
  7 //=================================================
  8 // Sequence Layer
  9 // Here clock is specified inside the sequence
 10 //=================================================
 11 sequence req_gnt_seq;
 12   @ (posedge clk) 
 13   (~req & gnt)  ##1  (~req & ~gnt);
 14 endsequence
 15 //=================================================
 16 // Property Specification Layer
 17 // Still requires clock for the property
 18 //=================================================
 19 property req_gnt_prop;
 20   @ (posedge clk) 
 21     disable iff (reset)
 22       req |=> req_gnt_seq;
 23 endproperty
 24 //=================================================
 25 // Assertion Directive Layer
 26 //=================================================
 27 req_gnt_assert : assert property (req_gnt_prop)
 28                  else
 29                  $display("@%0dns Assertion Failed", $time);
 30 //=================================================
 31 // Actual DUT RTL
 32 //=================================================
 33 always @ (posedge clk)
 34   gnt <= req;
 35 
 36 endmodule
 37 
 38 //+++++++++++++++++++++++++++++++++++++++++++++++
 39 //   Testbench Code
 40 //+++++++++++++++++++++++++++++++++++++++++++++++
 41 module concurrent_assertion_tb();
 42 
 43 reg clk = 0;
 44 reg reset, req = 0;
 45 wire gnt;
 46 
 47 always  #3  clk ++;
 48 
 49 initial begin
 50   reset <= 1;
 51    #20  reset <= 0;
 52   // Make the assertion pass
 53    #100  @ (posedge clk) req  <= 1;
 54   @ (posedge clk) req <= 0;
 55   // Make the assertion fail
 56    #100  @ (posedge clk) req  <= 1;
 57   repeat (2) @ (posedge clk);
 58   req <= 0;
 59    #10  $finish;
 60 end
 61 
 62 clock_assertion dut (clk,req,reset,gnt);
 63 
 64 endmodule

 "clock_sequence.sv", 27: dut.req_gnt_assert: 
   started at 237s failed at 243s
         Offending '((~req) & gnt)'
 @243ns Assertion Failed

Copyright © 1998-2014

Deepak Kumar Tala - All rights reserved

Do you have any Comment? mail me at:deepak@asic-world.com