Add formal verification for the handshake protocol and CMD codec

[jyrj]

Adds a passive checker for the UMI README 4.2 ready/valid rules as a normal sumi block (umi_checker), plus SymbiYosys proofs that run against the RTL in place:

umi_pack/umi_unpack round-trip for all 13 structured opcodes, both directions, including the ATYPE/LEN and USER/ERR aliases
umi_buffer (both MODEs) against handshake rules 2/3, with rules 1/4 as reachability covers; rules 5/6 are structural and documented as out of scope for a runtime monitor
Every proof ships fault_* tasks that corrupt something and must FAIL; the checker's own regression. Run:

source <oss-cad-suite>/environment
pytest -m formal tests/sumi/test_formal.py     # 10 passed

Tests skip when sby isn't on PATH, so existing CI lanes are unaffected. SiliconCompiler's sby flow can generate these jobs from the filesets; planned as the CI lane once its formal API stabilizes (currently engine-locked to boolector).

[RiceShelley]

Hi Jay, great work! I was able to run all of these on my machine.

Couple questions for you before approving the PR.

1. Can we get this added to CI before merging? Ideally the tests would be launched via a pytest entry point and make use of a silicon compiler flow.

2. Is there anyway where applicable to test for valid / ready handshake rule 4.2.5
   "The assertion of VALID must not depend on the assertion of READY. In other words, it is not legal for the VALID assertion to wait for the READY assertion."

[jyrj]

Thank you @RiceShelley for the review.

CI now runs the formal proofs through a pytest entry point in the sc_tools container, including a SiliconCompiler PropertyCheckFlow. And 4.2.5 is covered, the buffer proof reaches out_valid asserting with out_ready held low for the whole trace (so VALID never waits on READY), plus a must-fail fault case to keep it honest.

[RiceShelley]

Great work!