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

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:

In reply to tri.nguyen1123:

This is quite popular in Formal flow, tools have TCL commands to enable/disable assumptions, assertions and even to treat assert as assume etc. Most tools also allow you to create “tasks” to group such checkers and constraints and manage convergence time.

Good luck
Srini