Can we detect SVA in DUT under UVM?

UVM
1

Hi, I want to know that if I add some SVA in the DUT block and doesn’t change the function of design. Can I detect these SVA inside DUT block in UVM environment?

2

[quote]I want to know that if I add some SVA in the DUT block and doesn’t change the function of design. Can I detect these SVA inside DUT block in UVM environment?[quote]
Yes, this is because the assertions are elaborated at elaboration time (i.e., like modules), not run-time. Assertion statements are illegal in classes. However, see
https://verificationacademy.com/forums/uvm/sva-uvm-class-based-environment-new-paper
I published the following paper in the Feb 2013 edition of the Verification Horizons:
SVA in a UVM Class-based Environment.(page 24)

http://s3.mentor.com/fv/verification-horizons-publication-february-2013.pdf

This article provides an in-depth view of how to apply SystemVerilog assertions (SVA)
to simplify some of the tasks usually done by scoreboards in UVM and also to improve coverage sampling in your testbench. Links to code examples are provided.

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

  • SystemVerilog Assertions Handbook, 3rd Edition, 2013
  • A Pragmatic Approach to VMM Adoption
  • Using PSL/SUGAR … 2nd Edition
  • Real Chip Design and Verification
  • Cmpt Design by Example
  • VHDL books
3

In reply to ben@SystemVerilog.us:

Can u provide me some code example? Now I use a sv file to write assertions about one block and bind them together. Can it be detected in top level UVM?

4

In reply to leapoo:

Now I use a sv file to write assertions about one block and bind them together. Can it be detected in top level UVM?

Assertions and UVM have NO correlation whatsoever. Assertions written in a module or a checker and bound to a DUT will be detected when the DUT is executed, regardless of the environment (i.e., UVM or non-UVM). When you bind a module to another module (e.g., DUT), you are basically instancing the bounded module into the DUT.

As of today’s 1800 LRM, concurrent assertions are illegal in classes. I am trying to change that at the next 1800 revision, maybe in 3 years.

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

  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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
5

In reply to ben@SystemVerilog.us:

Hi, what you sent to me is blocked by my company email system. What’s the format of your package? Can you send me a copy to my private email address yl3059@columbia.edu

Thanks

6

In reply to leapoo:

Then in the UVM assertion report, I could check all the assertions written in the one of the agent interface. As the following command in my Makefile.

vsim top +UVM_TESTNAME=“$(TEST)” -do “coverage save 1.ucdb -onexit;run -all” -c -l 1.log -coverage -assertdebug -voptargs=+acc
vcover report -file assertion_report_detail.txt -assert -verbose 1.ucdb

And the report will show the assertion pass or fail status.
What I did next is to check the internal DUT block signals. For example, to check one AHB protocol module in the TOP DUT. Then I write a SVA_Checker for this module and bind them together. Then what I want to do is check the assertion in this SVA_checker and let the results appear in report. That’s the point I don’t know how to produce these assertions’ report in my UVM environment.

How can I do it?

7

Then what I want to do is check the assertion in this SVA_checker and let the results appear in report. That’s the point I don’t know how to produce these assertions’ report in my UVM environment.

Assertion reports usually appear in a window supplied by the tool. However, you can redirect action block reports in accordance to the UVM methodology. I describe this in my SVA book; the link below provides those pages:
http://systemverilog.us/sva_uvm_reports.pdf
Essentially, you do this:

import uvm_pkg::*; `include "uvm_macros.svh"
module uvm_sva_ex; // File c/uvm_sva_ex.sv
  bit clk, a, b, c, req, ack;
  parameter CLK_HPERIOD = 10;
  string tID="UART ";
  initial begin : clk_gen forever #CLK_HPERIOD clk <= !clk; end : clk_gen
  default clocking def_cb @ (posedge clk); endclocking : def_cb
  ap_LOW: assert property(a) else
     `uvm_info(tID,$sformatf("%m : error in a %b", a), UVM_LOW); // Line 9
  ap_MEDIUM: assert property(a) else
     `uvm_info(tID,$sformatf("%m : error in a %b", a), UVM_MEDIUM); // Line 11
...
// And the simulation run shows: 
# UVM_INFO uvm_sva_ex.sv(13) @ 10: reporter [UART ] uvm_sva_ex.ap_HIGH : error in a 0
# UVM_ERROR uvm_sva_ex.sv(17) @ 10: reporter [UART ] uvm_sva_ex.ap_test2 : error in a 0
# UVM_INFO uvm_sva_ex.sv(11) @ 10: reporter [UART ] uvm_sva_ex.ap_MEDIUM : error in

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

  • A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
  • SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
  • 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
8

In reply to ben@SystemVerilog.us:

Hi, Ben

I have checked what you provided. It’s not match with my problem. We could see that your assertion is still in the “UVM environment”. What I mean “UVM environment” is all UVM components except DUT.

What I want to check is the assertions existing in DUT. For example, my DUT file has DMA_top.v and DMA_ahb.v. I write assertions about DMA_ahb.v in SVA_checker.sv file and bind them together. How can I check this SVA_checker.sv in DUT under UVM and generate results in report file.

9

In reply to leapoo:

The assertions you write to be bound into the DUT may still generate UVM reports in their actions blocks.

10

In reply to dave_59:

How to check them? Do I need to add command in Makefile?

11

In reply to leapoo:

What is it you want to check? The SVA checker is already doing the checking for you. The UVM report summary will report which assertions failed. You can use all the UVM report mechanisms to filter and catch these messages.

12

In reply to dave_59:

Really appreciate for your patience. I’m gonna post my code up. Please help me to find the problem

SVA_checker

import uvm_pkg::*;
`include "uvm_macros.svh"

module trans_SVA_checker (
    //AHB Master I/F
    hclk_i, 
    hreset_i,
    hgrant_i,
    hwrite_o,
    hwdata_o,
    hsize_o,
    haddr_o,
    htrans_o,
    hburst_o,
    hbusreq_o,
    hprot_o,
    hlock_o,
    //AHB Slave I/F
    hready_i,
    hresp_i,
    hrdata_i,
///////////////////
    sync_rst_i,
    dma_ori_addr_i,
    dma_des_addr_i,
    start_i,
    dma_size_i,
    endian_sel_i,
    rd_instr_en_i,
    rd_wr_en_i,
    wr_only_en_i,
    incr_burst_i,
    dir_acs_dat_i,
    dft_glb_gt_se,
    tm_i,

    read_instr_o,
    dma_done_o,
    dma_busy_o,
    dma_st_o
    );


input         hclk_i; 
input         hreset_i;
input         hgrant_i;
input    hbusreq_o;
input     hwrite_o;
input [31:0] hwdata_o;
input [31:0] haddr_o;
input [2:0] hburst_o;
input [2:0] hsize_o;
input [ 1:0] htrans_o;
input [3:0] hprot_o;
input        hlock_o;
input         hready_i;
input  [1:0] hresp_i;
input  [31:0] hrdata_i; 
/////////////////////////
input sync_rst_i;
input [23:0] dma_ori_addr_i;
input [23:0] dma_des_addr_i;
input start_i;
input [12:0] dma_size_i;
input [1:0] endian_sel_i;// [0] ori endian  ; [1] des endian
input dma_done_o;
input reg dma_busy_o;
input [3:0] dma_st_o;
input [1:0] incr_burst_i;
input rd_instr_en_i,rd_wr_en_i;
input [31:0] read_instr_o ;
input [31:0] dir_acs_dat_i ;
input wr_only_en_i;
input dft_glb_gt_se;
input tm_i;

/* these parameters define the Transfer Type as specified by htrans */
parameter IDLE = 2'b00;
parameter BUSY = 2'b01;
parameter SEQ = 2'b11;
parameter NONSEQ = 2'b10;

/* define the transfer response signals as specified by hresp*/
parameter OKAY = 2'b00;
parameter ERROR = 2'b01;
parameter RETRY = 2'b10;
parameter SPLIT = 2'b11;





   
//Behavior: If reset is active then Transfer Type is IDLE and Resp is OKAY

   property IDLE_AND_OKAY_1_1;
      @(posedge hclk_i)
	(hreset_i==1) |-> ((htrans_o==IDLE)&&(hresp_i==OKAY));
      endproperty:IDLE_AND_OKAY_1_1
 
 CHECK_IDLE_AND_OKAY_1_1: assert property(IDLE_AND_OKAY_1_1) else
   `uvm_info("SVA",$sformatf("%m: error "),UVM_MEDIUM);
   

endmodule // trans_SVA_checker

SVA_bind

bind  NEW_DMA_10_TRANS trans_SVA_checker check1(
    hclk_i, 
    hreset_i,
    hgrant_i,
    hwrite_o,
    hwdata_o,
    hsize_o,
    haddr_o,
    htrans_o,
    hburst_o,
    hbusreq_o,
    hprot_o,
    hlock_o,
    //AHB Slave I/F
    hready_i,
    hresp_i,
    hrdata_i,
///////////////////
    sync_rst_i,
    dma_ori_addr_i,
    dma_des_addr_i,
    start_i,
    dma_size_i,
    endian_sel_i,
    rd_instr_en_i,
    rd_wr_en_i,
    wr_only_en_i,
    incr_burst_i,
    dir_acs_dat_i,
    dft_glb_gt_se,
    tm_i,

    read_instr_o,
    dma_done_o,
    dma_busy_o,
    dma_st_o);

Makefile


UVM_REGISTER ?= ../uvm_register-2.0
RTL          ?= ../../RTL/new_dma_ahb
SVA          ?=	../../RTL/Assertions	
AGENTS       ?= ../../AGENTS
TAR_PATH     ?= ../../../../
#TEST         ?= dma_test_rand_inst
TEST         ?= dma_test_reg
#TEST         ?= dma_test
#TEST         ?= dma_test_1

all: work build sim_coverage

tarball: clean tar

work:
	vlib work

build: work
	vlog -incr +incdir+$(RTL)     $(RTL)/*.v  $(RTL)/new_dma/*.v -timescale 1ns/10ps
	vlog -incr +incdir+$(AGENTS)/ahb_agent $(AGENTS)/ahb_agent/ahb_agent_pkg.sv -suppress 2263
	vlog -incr +incdir+$(AGENTS)/dma_agent $(AGENTS)/dma_agent/dma_agent_pkg.sv -suppress 2263
	vlog -incr $(AGENTS)/ahb_agent/ahb_master_if.sv -timescale 1ns/10ps -suppress 2263
	vlog -incr $(AGENTS)/ahb_agent/ahb_slave_if.sv -timescale 1ns/10ps -suppress 2263
	vlog -incr $(AGENTS)/dma_agent/dma_if.sv -timescale 1ns/10ps -suppress 2263
	vlog -incr +incdir+../env   ../env/dma_env_pkg.sv -suppress 2263
	vlog -incr +incdir+../test ../test/dma_sequence_lib_pkg.sv -suppress 2263
	vlog -incr +incdir+../test ../test/dma_virtual_seq_lib_pkg.sv -suppress 2263
	vlog -incr +incdir+../test ../test/dma_test_lib_pkg.sv -suppress 2263
	vlog -incr -timescale 1ns/10ps +incdir+$(RTL)    ../tb/top.sv

	vlog -sv -mfcu -cuname -incr +incdir+$(RTL)   ../../RTL/Assertions/sva_bind.sv  ../../RTL/Assertions/trans_SVA_checker.sv


run:
	vsim -c -do "run -all" top +UVM_TESTNAME="$(TEST)"

clean:
	@rm -rf work transcript *~ vsim.wlf *.log *.tgz *txt
	@find ../../../ -name "*~" -delete
sim_coverage:
	vsim top +UVM_TESTNAME="$(TEST)" -do "coverage save 1.ucdb -onexit;run -all" -c -l 1.log -coverage -assertdebug -voptargs=+acc  #added by Yue Li on Aug 07, 2014
	vcover report -file coverage_report.txt 1.ucdb
	vcover report -file coverage_report_detail.txt -cvg -verbose 1.ucdb
	vcover report -file assertion_report_detail.txt -assert  -verbose 1.ucdb

Report.txt only SVA in my UVM_interface

ASSERTION RESULTS:

Name Assertion Design Design Lang File(Line) Enable Failure Pass Vacuous Disable Attempt Active Peak Active ATV FPSA Failure Pass Failure EOS Formal Formal
Type Unit UnitType Count Count Count Count Count Count Count Action Log Log Limit Note Status Radius

/top/AHB_MASTER/CHK_HSEL
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(59) on 0 514 0 0 514 0 1 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_IDLE_AND_OKAY
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(73) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_NOT_SEQ_BUSY_IF_NONSEQ_SINGLE
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(84) on 0 150 364 0 514 0 1 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_IDLE_NONSEQ_AFTER_IDLE
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(94) on 0 363 150 0 514 1 2 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_BUSY_THEN_OKAY_RESPONSE
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(103) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_IDLE_THEN_OKAY_RESPONSE
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(113) on 0 363 150 0 514 1 2 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_IDLE_NONSEQ_IF_BUSY_SLAVE_UNLESS_GRANT_READY
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(124) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_OKAY_NOTOKAY_READY0
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(134) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_SPLIT_RETRY_IDLE
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(143) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_CONTROL_SAME
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(151) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_READY0_RESPONSEOK_KEEPSAME
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(159) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_FAIL_READY0_DATASAME
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(171) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_BUSY_ADDR_SAME
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(180) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_PROGRESS_1K_BOUNDARY
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(188) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_IDLE_THEN_NOTSEQ_NOTBUSY
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(197) on 0 363 150 0 514 1 2 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_RETRY_TWOCYCLES
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(206) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_SPLIT_TWOCYCLES
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(215) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/top/AHB_MASTER/CHECK_ERROR_TWOCYCLES
Concurrent ahb_master_if Verilog SVA ../../AGENTS/ahb_agent/ahb_master_if.sv(224) on 0 0 514 0 514 0 0 off CCCC - off unlimited off
/dma_virtual_seq_lib_pkg/dma_vseq_base/body/immed__32
Immediate dma_virtual_seq_lib_pkg Verilog SVA ../test/dma_virtual_seq_lib_pkg.sv(32) on 0 1 0 0 1 0 0 off CCCC - off unlimited off

13

Hi,
If I understand the original poster, he wants to see all the assertion firing/summary emerging from both interface/VIrt-if and DUT internal blocks at a single place. Typically you get this as part of run time log/transcript.

In your vxim command line you use:

vsim top +UVM_TESTNAME=“$(TEST)” -do “coverage save 1.ucdb -onexit;run -all” -c -l 1.log

So the “l.log” will contain everything.

Then you use

vcover report -file assertion_report_detail.txt -assert -verbose 1.ucdb

And I believe you are missing those SVAs that are bound to DUT in this assertion_report_detail.txt - if so, check the document for the tool. It should have an option.

HTH
Ajeetha, CVC

14

In reply to ajeetha:

yes, what u said is exactly what I want to express in my original poster. I’m trying to find solution. If I find, I will post it up

15

In reply to leapoo:

I have successfully solve this problem. I recommend to refer to this website and check
http://objectmix.com/verilog/189453-sva-use-bind-infer-all-signals-within-module.html

In this way, I changed my bind method to embedded method. And it works. Thus the problem is my bind method. It’s wrong or doesn’t fit the UVM environment.

Thanks for all your help.
Appreciate for your patience.