Reducing the design: parameters, black boxes, cut points
Sound vs unsound reductions
Every reduction either adds behaviours to the model (an over-approximation) or removes some (an under-approximation). For safety assertions:
| Reduction | Effect | Can it hide a bug? | Can it create a false failure? |
|---|---|---|---|
| Black-box a sub-module | Its outputs become free inputs | No | Yes — free outputs may do things the real module never does |
| Cut point on an internal signal | Signal becomes a free input | No | Yes |
| Smaller parameters (depth, width) | Different, smaller design | Yes | Rarely |
| Extra assumption / case split | Fewer input behaviours | Yes | No |
Over-approximations are "safe": if the assertion proves with them, it proves for the real design. If they cause a spurious failure, add a few assumptions on the cut signals that capture what the real logic guarantees (and ideally assert those on the real logic separately).
Cut points in practice
A typical example: an error-detection block computes a CRC over a 512-bit packet and raises crc_err. The
control FSM that reacts to crc_err is what you want to verify. Cut crc_err — it can now be 0 or 1 on
any cycle — and the CRC tree disappears from the cone. If the FSM is correct for any value of crc_err, it is
correct for the real one.