formal: add SymbiYosys proof for cc_heaviside

[briann-bui]

Summary

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

Changes

New Files

• **ormal/cc_heaviside_properties.sv** – Property checker using �ind to automatically attach to every cc_heaviside instance. Contains:
  • Full functional equivalence assertion against a loop-based reference model
  • Bit 0 always-asserted check
  • All-ones boundary check (x_i == Width-1)
  • Single-bit boundary check (x_i == 0)
  • Monotonicity check (bit at position x_i is set)
  • Upper-bits-zero check (bits above x_i are cleared)
• **ormal/cc_heaviside_formal.sv** – Elaboration harness instantiating cc_heaviside for widths 1 through 33, covering both power-of-two and non-power-of-two parameterizations.
• **ormal/heaviside.sby** – SymbiYosys configuration using smtbmc engine with depth 1 (combinational-only module).

Modified Files

• **ormal/Makefile** – Added heaviside.check target to the �ll rule and .PHONY list, following the existing lzc.check convention.

How to Run

\\�ash
cd formal
make heaviside.check
\\

Checklist

• Properties pass with the documented open-source formal flow
• Boundary cases (first and final valid indices) are covered
• Non-power-of-two widths exercised (widths 1-33)
• Integrated into existing ormal/Makefile
• Existing formal checks unmodified