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

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