formal: add SymbiYosys proof for cc_ecc_encode/cc_ecc_decode

[repowazdogz-droid]

Adds a SymbiYosys proof for the cc_ecc_encode / cc_ecc_decode pair, as a subtask of #288.

Following your note on #288, this does not wait on #354. I used #354 only as a rough reference and kept the layout to what current master already uses for lzc and heaviside, so it should rebase cleanly onto whatever #354 settles on.

cc_ecc_decode suits formal work because its header already carries the specification. The syndrome and parity truth table gives four cases over a combinational pair with no protocol and no state, so the properties are a transcription of documented behaviour rather than a new model.

What is proved

One encoder feeds four decoders, each seeing a different corruption of the encoded word, so no case can weaken another.

	condition	proved
P1	no corruption	data_o == data_i, all three flags low
P2	one flipped bit inside the Hamming codeword	data_o == data_i, single_error_o high, other flags low
P3	extended parity bit flipped, codeword untouched	data_o == data_i, parity_error_o high, other flags low
P4	two distinct flipped bits anywhere in the encoded word	double_error_o high, other flags low

P2 excludes the extended parity bit deliberately, since a flip there is reported through parity_error_o and stating P2 over the whole encoded word would contradict the truth table.

What is not claimed

• Nothing about data_o under a double error. The decoder does not promise a value there, and the syndrome can address a position outside the codeword. That decoder instance has its data_o left unconnected so no property can read it.
• Nothing beyond two flipped bits, which is outside the distance of a SECDED code.
• The encoder is exercised only through this decoder, not against a separate implementation of the same code, so this is a matched-pair proof and not an interoperability one.

One check is not matched-pair. cc_ecc_properties.sv counts the power-of-two positions in the codeword and compares that count against cc_pkg::ecc_get_parity_width, rather than recomputing the same search, which would agree with the package for the same wrong reason. Both operands are elaboration-time constants, so it is an elaboration check and not a proof obligation, and the comment says so.

Widths and engine

make ecc.check proves DataWidth 1, 2, 4, 5, 11 and 12. cc_pkg::ecc_get_parity_width adds a parity bit going from 1 to 2, from 4 to 5 and from 11 to 12, so each transition is proved on both sides. 1, 4 and 11 are also the widths whose encoded word is exactly a power of two bits wide, where an index constraint is easiest to get wrong.

Engine is abc pdr rather than the smtbmc the other proofs use. The pair is purely combinational, so depth 1 is already exhaustive, and PDR is chosen only for runtime: on the default width set the proof takes about 10 s with PDR against about 3 min with smtbmc. I did not run smtbmc to completion on the full sweep, so I am not putting a number on that.

Wider parametrizations up to the module default of 64 are a separate task, not part of make all. It proved all 128 properties in 46 min 47 s here:

sby -f ecc.sby sweep

Vacuity

make ecc.check runs a cover task alongside the proof. The properties constrain where the injected errors may land, so the cover task is what shows those positions are reachable; abc pdr reports no PREUNSAT, so a proof resting on an unsatisfiable assumption would otherwise pass silently.

That is not hypothetical. An earlier version of this harness shared the error-position inputs across widths, which let one width's constraint narrow another's reachable positions while the proof stayed green. The cover task is what caught it, which is why it runs by default rather than on request.

[phsauter]

Coverage for syndrome_o seems to be missing, otherwise this looks good.

[repowazdogz-droid]

Thanks — syndrome_o coverage is added now: zero for a clean word, the 1-based position for a single flipped codeword bit, zero for an extended-parity-only error, and non-zero for a double error, without constraining the exact double-error syndrome.

While wiring this up I found that cc_ecc_decode declares syndrome_o but never drives it, so the patch now assigns the decoder's internal syndrome to the output. Verilator also flags the original output as undriven. The formal checks and width sweep pass with the fix.

[phsauter]

Looks all good, also cool that we found a real bug, more verification is doing something!

[repowazdogz-droid]

Very cool indeed! 🙌