Assertion to ensure a signal comes up only few number of times in 100 clocks

SystemVerilog
,
1

I am a beginner with assertions. I was trying to write an assertion to ensure a signal comes up only a fixed number of times. For example 5 times in 100 clock cycles. When I wrote down the assertion, I found one more thing which I am not able to understand:

  property p (bit ck1, bit ck2);
    @(posedge ck2) (ck2==1); 
  endproperty

This property always evaluates to FAIL when asserted even though we wait for posedge on the same signal.

So my question is 2 fold:

  1. How do I write the assertion to ensure a signal comes up only n times in 100 clock cycles. For example n = 5.
  2. Why does the property above always evaluate to fail when asserted? - Is it possible to clock on the same signal and assert a property on the same signal?

Thanks.

2

In reply to sphen:
The reason your assertion always fails is that the Boolean expression (ck2==1) uses the sampled value of ck2, which is the value it has at the beginning of the of the time slot when @(posedge cl2) happens. So that will always be 0 (or X).

You need to be more specific about your condition, but I’ll assume you meant to say you want to check when signal is true n time in any overlapping 100 clock cycles. The most efficient way to do that would be to create 100 bit shift register with a 1 set each time your signal is true and assert that the count of ones is 5.

bit [1:100] count5;

always @(posedge ck) count5 = {count5,signal==1};

property
@(posedge ck2) enable |-> $countones(count5) == 5;
endproperty

You’ll need to enable the assertion after the first 100 clock cycles.

If the 100 clocks cycles is not overlapping, you can do something similar, but you’ll need to be more specific about how the period starts.

3

In reply to dave_59:

Hi Dave, I was studying this problem too, and thought that that Nonconsecutive operator would be a robust way to check that the signal in question was asserted 5 times;

Nonconsecutive Repetition

Nonconsecutive repetition specifies finitely many iterative matches of the operand Boolean expression, with a delay of one or more clock ticks from one match of the operand to the next successive match and no match of the operand strictly in between. The overall repetition sequence matches at or after the last iterative match of the operand, but before any later match of the operand.

sequence Write_4;
@(negedge clk) (!WR & RD) [=4]
endsequence

The Write_4 sequence describes 4 not necessarily consecutive writes to memory.

4

In reply to ljgiordano:
The repetition operators have two problems with the requirement here.
There are no cycle bounds for the overall operation. You would have to create a counter to count the number of cycles. And the repetition operators are good for matching “at least N” repetitions - you need a little more to catch the extra occurrences.

Doable - but not for an assertions beginner.

5

In reply to dave_59:
I see 3 possible solutions, using 20 instead of 100:

  1. At every clock, in any 20 clock cycles, there should be 5 "a"s, after the 1st 20 cycles

initial begin
repeat(20) @(posedge clk);
go <= 1'b1;
end
ap_go20: assert property(go |-> $countones(a20) == 5);
  1. At every clock, in any 20 clock cycles, there should be 5 "a"s, starting from the first clock
property p5in20;
int v20=20, vcount=0 ;
((v20 > 0, v20=v20-1'b1)  [*0:$] ##1 v20==0) intersect
((a[->1], vcount=vcount+1'b1) [*0:$] ##1 vcount==5);
endproperty
ap5in20: assert property(p5in20);
  1. At every clock, in any 20 clock cycles following an “a”, there should be 5 "a"s, starting from the first clock
property p5in20_aftera;
int v20=20, vcount=0 ;
(a, v20=v20-1'b1, vcount=vcount+1'b1) |=>
((v20 > 0, v20=v20-1'b1)  [*0:$] ##1 v20==0) intersect
((a[->1], vcount=vcount+1'b1) [*0:$] ##1 vcount==5);
endproperty
ap5in20_aftera: assert property(p5in20_aftera);

Testbench code for above assertions:


import uvm_pkg::*; `include "uvm_macros.svh" 
module top; 
	bit clk, a, go;  
	bit[19:0] a20; 
	wire[19:0] count1s; 
	assign count1s = $countones(a20);
	always @(posedge clk) a20 = {a, a20};
	
	default clocking @(posedge clk); endclocking
	initial forever #10 clk=!clk;  
	initial begin 
		repeat(20) @(posedge clk);   
		go <= 1'b1; 
	end
	
	ap_go20: assert property(go |-> $countones(a20) == 5);  
		
	property p5in20; 
		int v20=20, vcount=0 ; 
			((v20 > 0, v20=v20-1'b1)  [*0:$] ##1 v20==0) intersect 
			((a[->1], vcount=vcount+1'b1) [*0:$] ##1 vcount==5); 
		endproperty 
	ap5in20: assert property(p5in20);  
	
	property p5in20_aftera; 
		int v20=20, vcount=0 ; 
		(a, v20=v20-1'b1, vcount=vcount+1'b1) |=> 
			((v20 > 0, v20=v20-1'b1)  [*0:$] ##1 v20==0) intersect 
			((a[->1], vcount=vcount+1'b1) [*0:$] ##1 vcount==5); 
	endproperty 
	ap5in20_aftera: assert property(p5in20_aftera);  	
			               

	initial begin 
		repeat(200) begin 
			@(posedge clk);   
			if (!randomize(a)  with 
					{ a dist {1'b1:=1, 1'b0:=7};
					}) `uvm_error("MYERR", "This is a randomize error")
					end 
					$finish; 
		end 
endmodule

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

  • SVA 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