[Formal verification] Is there a way to bind some assumption to a specific assertion to reduce the stimulus for only that assertion?

In reply to tri.nguyen1123:

If the assume is anywhere in the RTL model, even in individual checkers, it applies to all assertions.
Be careful here-- even if on states, outputs, etc, an assume’s requirements will be back-propagated to drivers.
Usually tools provide a way to create separate environments with different sets of assumptions if desired. Contact your vendor.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
** 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) https://rb.gy/cwy7nb
  3. Papers: