More and better formal proofs - #354
Draft
phsauter wants to merge 9 commits into
Draft
Conversation
This was referenced Aug 10, 2026
phsauter
pushed a commit
that referenced
this pull request
Sep 3, 2026
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.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.