Chipress

We discussed how SEC works using clock gating FV in a previous post, and introduced cutpoint mapping. We will extend the discussion about the SEC mapping types in this post.

A cutpoint is a pair of internal signals that you expect to be equal. The SEC tool auto-generates assertions to make sure they match, for example, foreach(map): assert (signal_spec == signal_imp).

Cutpoints reduce design complexity by dropping the upstream logic cone of the mapped signals. Note, cutpoints are not safe unless you prove them to be equal. A proof in a design with cutpoints are only considered valid, when you have full proof on all cutpoints.

When you cannot get full proof on all cutpoints, you should remove the failing cutpoints and restart the proof without them. Keeping only the proven cutpoints can significantly reduce design complexity.

A stopat mapping also creates a connection between spec and imp designs. However, it does not instruct the SEC tool to auto-generate assertions, and you are taking the risk that this mapping might not be safe or equal.