Need Help to Write a SV Assertion

SystemVerilog
1

Need help to write an assertion to make sure a signal is high for exactly 6 cycles in every 10 cycle window. Signal can be high for any 6 cycles in the 10 cycle window.

Thanks in Advance!

2

In reply to nachiketag:

property signal_stable;
@(posecdge clk) ##[1:10] |-> ##[1:6] ( $stable(x) || $rose(x) ) ;
endproperty

ap_signal_stable: assert property signal_stable;

please correct me if i am wrong .

3

In reply to manikanta710214:

In reply to nachiketag:

property signal_stable;
@(posedge clk) ##[1:10] 1 |-> ##[1:6] ( $stable(x) || $rose(x) ) ;
endproperty
ap_signal_stable: assert property(signal_stable);
// please correct me if i am wrong .

Above is incorrect because the antecedent with be true at every clocking event because
##[1:10] |-> does not compile. I used (##[1:10]1’b1). All that does is fire at every clocking event multiple threads. also, the consequent does not state that signal x has to be true for 6 cycles.

Consider the following approach that I tested, along with error injection. Basically, I have

$rose(a) |=> a[*5] ##1 !a[*4] ##1 $rose(a));

That states that at a rose(a), a is high for 5 more cycles,
and thena is low for 4 more cycles;
this is then followed by another rose(a).
If the framing is available in an external signal, then you can use the within operator; but the requirements need to be clearly defined.
BTW, my testbench below follows the rules that I recommend and explain in my SVA 4th Edition book.


import uvm_pkg::*; `include "uvm_macros.svh" 
module hi6; 
	bit clk, a, env10=1'b1; 
	bit[3:0] d1, d2; 
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;   
	// Need help to write an assertion to make sure a signal
	// is high for exactly 6 cycles in every 10 cycle window. 
	// Signal can be high for any 6 cycles in the 10 cycle window.
	
    ap_hi6: assert property(
    		$rose(a) |=> a[*5] ##1 !a[*4] ##1 $rose(a)); 

    property signal_stable; // ***** Incorrect *** DO NOT USE 
      @(posedge clk) ##[1:10] 1 |-> ##[1:6] ( $stable(a) || $rose(a) ) ;
    endproperty
    ap_signal_stable: assert property(signal_stable);

 initial begin
     repeat(200) begin :r200
       @(posedge clk);   
       a <= 1'b1; 
       repeat(6+d1) @(posedge clk); 
       if (!randomize(d1, d2)  with 
           {d1 dist {4'b0000 :=4, 4'b0001:=1}; // error for hi being 6
            d2 dist {4'b0100 :=3, 4'b0011:=1}; // error for lo being 4 
           }) `uvm_error("MYERR", "This is a randomize error")
       repeat(d2) begin : rd2
         a <= 1'b0; 
         @(posedge clk);
       end  : rd2
     end :r200
     $finish;
 end
endmodule  : hi6

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
4

If the repeat is nonconsecutive, consider the following

$rose(a) |-> a[->6] intersect  1[*10];
// This says that for every rose(a), there are 6 "a"s in 10 cycles.
// Not sure if this is what you want. 
// Assertion needs to be tested to see if it meets your requirements.

Ben@systemverilog.us

5

Thanks Ben! This is exactly what I wanted.

6

In reply to nachiketag:

Thanks Ben! This is exactly what I wanted.

It is interesting how difficult it is to express requirements in English. I had issues in fully understanding what you meant by

Need help to write an assertion to make sure a signal is high for exactly 6 cycles in every 10 cycle window. Signal can be high for any 6 cycles in the 10 cycle window.

My issues with this were:

  1. When is the start of that 10 cycle window?
  2. Is there an envelope signal that identifies that 10 cycle window?

The assertion ($rose(a) |-> a[->6] intersect 1[*10];) clearly identifies the intent.
An English description of the requirements should have then been something like.

Following any rising edge of signal “a”, that signal must be high, consecutively or non-consecutively, exactly six times in the next ten cycles. The start of that ten cycle count is the rise of signal “a”.

BTW, I do not fault you for writing an ambiguous set of requirements; it is not easy. In fact, the things I dreaded the most in my career as an engineer were proposals and requirement documents. FWIW, what has really helped me in the process was teaching and writing books; my first book was in 1995.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us

  • SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
  • Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
  • Component Design by Example ", 2001 ISBN 0-9705394-0-1
  • VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
  • VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115