This chip-hardening project now proves that its optimized multiply-accumulate (MAC) block matches the baseline using the real multiplier, then repeats the proof against a deliberately broken copy. The first run must pass. The planted bug, which changes the condition that updates the accumulator, must produce a counterexample or continuous integration (CI) turns red.
This checks the checker. Formal equivalence builds a comparison circuit from two register-transfer-level (RTL) designs and asks a model checker whether any input sequence makes their outputs differ. A passing answer can still be worthless if the comparison omitted a signal, assumed away a state, or never exercised the property. The mutant run proves that this setup can detect at least one realistic error in the exact path under test.
The project also moved the unbounded proof from a slow manual experiment into the normal CI job with a 30-minute limit. Hardware teams adding formal checks should plant one small defect beside each important proof and require the tool to find it; when a future script change makes the defect pass, the broken proof fails before the chip does.