Questa Formal - "Design Checks" Fix

Created by: silabs-robin

This PR adds a few constraints to the Questa Formal setup. (Rationale below.)

I think I figured out why the counter-examples looked so nonsensical. At first I thought it was a problem with the reset initialization sequence, but it was only partially that...

"Free nets" seems to be treated differently in Jasper and Questa. Jasper goes "it's a free net, it can do whatever, and Questa goes "this is not a valid control point, whoops there goes gravity". Free nets needs to be turned into valid "control points", and one can do that by explicitly setting a cutpoint. Before this change you could get e.g. rvfi_valid on cycle 0 and all kinds of weird behavior that seems to completely ignore what is written in the rtl.