formal: add SymbiYosys proof for cc_heaviside

[briann-bui]

Summary

Add open-source formal verification for cc_heaviside (Closes #350, subtask of #288).

Changes

Formal verification

• Add formal/cc_heaviside_properties.sv, a bound property checker that proves full functional
  equivalence against a loop-based reference model.
• Add formal/cc_heaviside_formal.sv, an elaboration harness covering widths 1 through 33,
  including power-of-two and non-power-of-two configurations.
• Add formal/heaviside.sby, a depth-1 SymbiYosys proof using the smtbmc engine.
• Add heaviside.check to formal/Makefile.

Documented behavior

• Document that inputs greater than or equal to Width saturate mask_o to all ones.
• Capture the same saturation behavior explicitly in the formal reference model.

How to run

cd formal
make heaviside.check

Validation

• The property covers widths 1 through 33, including out-of-range encodings for
  non-power-of-two widths.
• Verible lint passes.
• The formal harness compiles and elaborates successfully with VCS X-2025.06.

[phsauter]

As far as I can tell Property 1 already proves the complete function, Properties 2–6 are logically redundant.
It can make sense to add redundant checks but really only if one property would be difficult to debug due to complex temporal effects. For this small, combinational proof I do not think they are needed.

Please also clarify the behavior for non-power-of-two Width values. Since idx_width(Width) can represent values greater than or equal to Width, the current unconditional equivalence property effectively makes it so that all out-of-range indices produce an all-ones mask. I actually think this saturation is good and makes it more like a finite-width heaviside function and it preserves monotonicity but it should be documented (in the module as well, we should just make the behavior explicit).

[briann-bui]

@phsauter, I addressed your review in commit 337ff0d:

• removed the redundant Properties 2–6, leaving the full functional equivalence property;
• documented that x_i >= Width saturates mask_o to all ones in cc_heaviside;
• documented the same behavior in the formal checker and reference model;
• updated the PR description to match the revised proof.

Validation: Verible lint passes, and the formal harness compiles/elaborates successfully with VCS X-2025.06. The local SymbiYosys run could not be repeated because this environment does not provide the required sby/Yosys-Slang toolchain.

Could you please review again when convenient? Thanks!

[phsauter]

Looks good to me, thanks for the help!

[phsauter]

The local SymbiYosys run could not be repeated because this environment does not provide the required sby/Yosys-Slang toolchain.

Btw you can get all the open-source tools even with the open-source PDKs in a nice docker container, see here: https://github.com/iic-jku/IIC-OSIC-TOOLS
This is super useful for local work on laptops etc and also very useful to give AI agents etc.