Help with assertion inside always@(*) combinational block alongside with for loop

SystemVerilog
,
1

Anyone familiar with formally verification of

always @(*)

as in doing

assert()

for

always @(*)

along side with

for

loop

1012×1084 126 KB

2

In reply to feiphung:

What is your question?

3

In reply to dave_59:

How to do assert(logic) inside a ‘for’ loop inside always@(*) block ?

I suppose it is easier to do assert() without ‘for’ loop OR inside always@(posedge clk) block

4

In reply to feiphung:
I don’t see the issue here.


module m;
  `include "uvm_macros.svh"
     import uvm_pkg::*;
bit clk; 
bit[3:0] a=4, b=5, c; 
initial forever #10 clk=!clk;  
  
always_comb begin
    for (int i=0; i<=3; i++) begin
      assert(a[i] > b[i]) else $display("i a[i] b[i]", i, a[i], b[i]);        
      ap_ab: assert property(@ (posedge clk) a[i] |=> b[i]);  
    end    
end
        initial begin 
         repeat(20) begin 
             @(posedge clk);   
             if (!randomize(a, b)  with 
             { a dist {1'b1:=1, 1'b0:=1};
               b dist {1'b1:=1, 1'b0:=2};  
         }) `uvm_error("MYERR", "This is a randomize error");
         end 
         $finish; 
        end  
endmodule 
...
# KERNEL: i a[i] b[i]          100
# KERNEL: i a[i] b[i]          200
# KERNEL: i a[i] b[i]          300
# KERNEL: i a[i] b[i]          000
# KERNEL: i a[i] b[i]          100
# KERNEL: i a[i] b[i]          200
# KERNEL: i a[i] b[i]          300
# ASSERT: Error: ASRT_0005 testbench.sv(10): Assertion "ap_ab" FAILED at time: 50ns (3 clk), scope: m, start-time: 30ns (2 clk)
# ASSERT: Error: ASRT_0005 testbench.sv(10): Assertion "ap_ab" FAILED at time: 70ns (4 clk), scope: m, start-time: 50ns (3 clk)

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers:
5

In reply to ben@SystemVerilog.us:

I am new to UVM.

I do not know what your uvm code is trying to achieve.
Could you write a few lines of comments on the UVM code itself ?

6

In reply to feiphung:
pm the above example i only used the UVM messenging with severity levels’ there is a lot lot more to uvm. The Universal Verification Methodology (UVM) Class Reference addresses verification complexity and interoperability within companies and throughout the electronics industry for both novice and advanced teams while also providing consistency. UVM has claimed wide acceptance in the verification methodology of advanced designs. For the reporting of messages, UVM provides several macros that resemble the SystemVerilog severity levels, but provide more options and consistency with the UVM verification environment.
Ben

7

In reply to ben@SystemVerilog.us:

What are the two assert() inside always_comb block trying to achieve ?

8

In reply to feiphung:
you need to study the types of assertions.
Once the always_comb is triggered becuase of a change in any of the signals inside that construct, the
assert(a[i] > b[i]) else $display(“i a[i] b[i]”, i, a[i], b[i]);
is an immediate asn and checks he conditions described on the asn.

Also, the concurrent asd is triggered and at then next posedge of clk, the sampled variables are checked. In this case, if a[i] is true, then at the nect clk cycle b[i] must be true.
ap_ab: assert property(@ (posedge clk) a[i] |=> b[i]);
There is a lot more to assertions, and you need to study the SystemVerilog assertions described in 1800’17 chapter 16. Of course, my SVA book expands on SVA with lots of examples and text using knowledge got thru experience of 4 authors and providing examples of issues addressed by users on this forum.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home.html
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
9

In reply to ben@SystemVerilog.us:

I am quite confused with your UVM example.
Maybe let me rephrase my question to a simple test case below:

What assert(logic) could be used for the following always @(*) block ?

module test_assert
(
	input clk,
	output done
);


// a list of 8 integers
localparam MAX_VALUE = 10;
localparam NUM_OF_ITEMS = 8;
reg [$clog2(MAX_VALUE)-1:0] number_list [NUM_OF_ITEMS-1:0];

generate

	genvar list_index;
	for(list_index=0; list_index<NUM_OF_ITEMS; list_index=list_index+1)
	begin: assign_number_to_list
	
		always @(posedge clk) 
			number_list[list_index] <= list_index;  // a list that contains {1,2,3,4,5,6,7,8}
	end
		
endgenerate


// we have 2,4,6 as even integer
// we have 1,3,5,7 as odd integer
reg [$clog2(NUM_OF_ITEMS)-1:0] num_of_evens_minus_num_of_odds;
integer index;

always @(*)
begin
	num_of_evens_minus_num_of_odds <= 0;

	for(index=0; index<NUM_OF_ITEMS; index=index+1)
	begin: computation_logic
	
		if((number_list[index] % 2) == 0)  // even integer
			num_of_evens_minus_num_of_odds <= num_of_evens_minus_num_of_odds + 1;
			
		else num_of_evens_minus_num_of_odds <= num_of_evens_minus_num_of_odds - 1;
	end
end

always @(posedge clk) done <= 1;  // the always @(*) will finish in 1 clock cycle

endmodule
10

In reply to feiphung:

No one can write an assertion without knowing the requirement it needs to verify. If you tell us that, we might be able to show you the code to implement it. If you show us an assertion we might be able to tell you what requirement it was written to verify. So far I’ve seen neither.

Also, the `uvm_error in Ben’s example was a distraction. This of using $display or $error instead. That is all it is doing.