Formal verification can explore a large number of possible input sequences. Assumptions help restrict this exploration to behaviours allowed by the design environment.
However, an incorrectly placed or overly restrictive assumption can hide a real design problem.
This is known as over-constraint.
Understanding the verification boundary
Consider a FIFO design with the following signals:
wr_en: write requestrd_en: read requestfull: FIFO full statusempty: FIFO empty status
Many FIFO designs are required to handle a write request safely when the FIFO is full, for example by ignoring it without corrupting stored data.
The verification environment must model the intended interface contract correctly.
For example:
assume property (@(posedge clk) full |-> !wr_en );
This assumption is appropriate only if the interface specification guarantees that the upstream sender never writes while full is high.
If the specification instead requires the FIFO to handle writes while full, this assumption removes exactly the scenario that exercises the FIFO's own overflow-protection logic.
In that situation, writes while full should be allowed by the environment, and the FIFO's handling of them should be checked as design behaviour rather than assumed away.
How over-constraint hides defects
Suppose the FIFO's overflow protection is broken: a write while full overwrites the oldest stored entry.
If the environment assumes that writes never occur when full is high, the formal engine never explores that write. No property can fail, because the triggering scenario has been excluded.
The result may look clean even though the design behaviour is incorrect.
The issue is not with formal verification. It is with the verification model.
Maintain an assumption register
A practical formal verification flow should document every assumption.
For each assumption, record:
- The signal or interface condition being constrained
- Whether it constrains the environment or reflects the DUT's own behaviour
- The specification or interface requirement supporting it
- Why the constraint is necessary
- Which properties depend on it
- Whether the assumption affects important reachability scenarios
Assumptions should be reviewed whenever the verification boundary or design configuration changes.
Check whether important scenarios remain reachable
Cover properties can help identify whether important input sequences are still reachable.
For example:
cover property (@(posedge clk) wr_en && full );
With the assumption above in place, this cover is unreachable by construction. That is the signal to check: if the specification requires writes while full to be handled, an unreachable cover here means the overflow-protection logic has not been verified.
The purpose is not to force every possible combination to occur. It is to confirm that the assumptions have not unintentionally excluded scenarios required by the verification plan.
Conclusion
Assumptions are essential to formal verification, but they must be applied carefully.
An assumption should represent a valid environmental restriction—not a convenient way to make an assertion pass.
A strong formal verification environment checks not only whether properties pass, but also whether the assumptions allow the intended design behaviour to be explored.
