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

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,

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.

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

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 ?

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: