Can we use internal signal of DUT while writing the assertion property

SystemVerilog
,
1

Hi,

While writing the assertion, Can we use the internal signal of DUT. or we should only use the input, output of DUT ?

Is their any recommendation ?

Thanks,

2

In reply to rkg_:

While writing the assertion, Can we use the internal signal of DUT. or we should only use the input, output of DUT ? Are there recommendations?

  1. When designing a DUT, write the assertions in a separate checker (or module) and bind it to the DUT.
    (see below for sample code).
  • 2. Binding isolates the verification code from RTL code.
    3. Verification code may include global local variables, not to be confused with the RTL.
    4. With binding, changes can be made to the verification without changing the timestamp of the RTL.

  • Assertions can (and should) address both the black-box and the white-box of the model.

    - Black-box verification address the requirements from an external viewpoint of the DUT.
    They also address assumptions imposed on the model. For example, sig_x[3]==0 in the mode that the DUT is intended to be used; sig_y is never asserted when sig_z==1.
    - A good place to put the black-box assertions is in the interface or a checker bound to the interface.
    - White-box assertions and assumptions address items specific to the design. For example, when the FSM is in state_X, sig_Z is zero at the next cycle. State machines are internal to the DUT.

Example uses a module instead of a checker.

1152×648 18.4 KB

1152×648 18.4 KB

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:
1 Like
3

In reply to ben@SystemVerilog.us:

Thanks Ben :)

let me reframe my question in slightly diffrent way :-

  • lets say design has output signal inc and dec. i need to write property where I have to use inc and dec signal. and condition is like if inc or dec happen consecutively 4 times lock will be de- asserted

  • But in DUT they have used internal signal(fll_unlock_check_timer) to detect inc or dec. and every inc or dec fll_unlock check timer will change.

So my question is, Can i directly use (fll_unlock_check_timer == 4) lock should be de-asserted ?

4

In reply to rkg_:
I would write two assertions

  1. An assertion based on the inc, dec, that impacts the lock.
  2. An assertion on how inc, dec are generated based on fll_unlock_check_timer.
    In other words, you need to check the creation of the outputs, making sure that they are according to spec. That spec may be other factors besides the timer. The timer is an implementation. In general, for black-box the implementation is irrelevant.
    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
    …
  3. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  4. 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
  5. Papers:
5

Hi Ben,

/**

  • Here we define any top-level constraints, auxiliary code
  • and top-level properties.
  • Note that it is fine to bind properties at various levels of the DUT’s
  • hierarchy. Not all properties necessarily need to be instantiated here.
    */

module formal_tb(
// clocks and resets
input Cpl_VDDCR_SOC_REFCLK,
input Cpl_VDDCR_SOC_REFCLK_100,
input Cpl_VDDCR_SOC_GAP_REFCLK,
input FCH_SIB_S5_RESETn,

                  input SOC_SIB_PWROK

                  // APB

// input PSEL,
// input PENABLE,
// input PREADY
);

/**
* Constrain pwrok
*/
default clocking clk_cb @(posedge Cpl_VDDCR_SOC_REFCLK_100); endclocking
default disable iff(!FCH_SIB_S5_RESETn);

property p_SOC_SIB_PWROK();
@(posedge Cpl_VDDCR_SOC_REFCLK_100) disable iff (!FCH_SIB_S5_RESETn)
FCH_SIB_S5_RESETn == 1;
endproperty // p_SOC_SIB_PWROK
asm_p_SOC_SIB_PWROK: assume property(p_SOC_SIB_PWROK());

property p_axi_always_ready(axready);
axready == 1;
endproperty // p_axi_always_ready

asm_p_axi_always_arready_TM_to_ROM:
assume property(p_axi_always_ready(secipsys.art.mpART.mpART_core.rom_axi_arready));

/**
* This property is made up, it is not based on specs. We just
* want to see something in the VCF task list.
/
/ property p_pready_max_wait_time();
@(posedge Cpl_VDDCR_SOC_REFCLK_100) disable iff (!FCH_SIB_S5_RESETn)
PSEL && PENABLE |-> ##[1:15] PREADY;
endproperty // p_pready_max_wait_time
ast_p_pready_max_wait_time: assert property(p_pready_max_wait_time());
*/
endmodule

bind secipsys formal_tb formal_tb_inst(.*);

/**

  • We do not yet have licenses for AXI4 AIP:
  • [Fatal] MISSING_AIP_LICENSE2: Neither required license feature key for AIP ‘AIP-AXI-SVA’ or ‘AIP-ACE-SVA’ could be checked out.
    */
    //bind sib_32_art_mid_ksb_top snps_axi4_aip #(.ENABLE_ASSERT(ksb_aip_pkg::KSB_AXI_AIP_ENABLE_ASSERT)) snps_axi4_aip_inst();

This is the code that i ahve written to access the internal module signals , I need to write the assert/assume to internal module signlas.

I am facing the segmentation fault issue .

Where i am stuck and not known the exact cause of segmentation fault.

Could you please point what is the mistake i have done .
if i need to provide more details i can provide .

Thanks,
Ambika M

6

Hi @ben2 ,

Could you please check the above comment .

Thanks,
Ambika M