From 52231a21e65b0ca7a95b2f5891be8399314c0227 Mon Sep 17 00:00:00 2001 From: Warren Smith <233830950+repowazdogz-droid@users.noreply.github.com> Date: Tue, 11 Aug 2026 02:49:35 +0100 Subject: [PATCH] formal: add SymbiYosys proof for cc_ecc_encode/cc_ecc_decode Prove the four cases documented in the cc_ecc_decode header for the encoder/decoder pair: clean round-trip, single-bit correction inside the Hamming codeword, a flipped extended parity bit, and double error detection. One encoder feeds four decoders so the cases cannot interfere. DataWidth 1, 2, 4, 5, 11 and 12 are proved by default, bracketing each parity-width transition on both sides. Wider parametrizations up to the module default of 64 run as a separate sweep task, not part of `make all`. The properties claim nothing about data_o under a double error, nothing beyond two flipped bits, and nothing about interoperability with another implementation of the same code. The parity width is checked against a count of the power-of-two codeword positions rather than by recomputing the cc_pkg search, so a defect there is not reproduced by the check. `make ecc.check` runs a cover task alongside the proof, so a proof resting on an unsatisfiable assumption cannot pass unnoticed. --- formal/Makefile | 16 +++- formal/README.md | 15 ++++ formal/cc_ecc_formal.sv | 169 ++++++++++++++++++++++++++++++++++ formal/cc_ecc_properties.sv | 174 ++++++++++++++++++++++++++++++++++++ formal/ecc.sby | 57 ++++++++++++ 5 files changed, 429 insertions(+), 2 deletions(-) create mode 100644 formal/cc_ecc_formal.sv create mode 100644 formal/cc_ecc_properties.sv create mode 100644 formal/ecc.sby diff --git a/formal/Makefile b/formal/Makefile index 5b6cb2e9..794b4698 100644 --- a/formal/Makefile +++ b/formal/Makefile @@ -26,7 +26,8 @@ FORMAL_BUILDDIR ?= build FORMAL_FLIST := $(FORMAL_BUILDDIR)/cdc_reset_ctrlr.flist all: fifo.check counter.check fall_through_register.check lzc.check \ - cdc_reset_ctrlr_half.check cdc_reset_ctrlr_composed.check heaviside.check + cdc_reset_ctrlr_half.check cdc_reset_ctrlr_composed.check heaviside.check \ + ecc.check $(FORMAL_BUILDDIR): mkdir -p $@ @@ -81,8 +82,19 @@ $(FORMAL_BUILDDIR)/heaviside.check: heaviside.sby ../src/cc_pkg.sv ../src/cc_hea $(SBY) -f -d $(FORMAL_BUILDDIR)/heaviside $< touch $@ +ecc.check: $(FORMAL_BUILDDIR)/ecc.check + +# The full parametrization sweep is deliberately not part of `all`; run it with +# `sby -f ecc.sby sweep`. +$(FORMAL_BUILDDIR)/ecc.check: ecc.sby ../src/cc_pkg.sv ../src/cc_ecc_encode.sv \ + ../src/cc_ecc_decode.sv cc_ecc_properties.sv cc_ecc_formal.sv \ + | $(FORMAL_BUILDDIR) + $(SBY) -f -d $(FORMAL_BUILDDIR)/ecc_prove $< prove + $(SBY) -f -d $(FORMAL_BUILDDIR)/ecc_cover $< cover + touch $@ + .PHONY: all clean fifo.check counter.check fall_through_register.check lzc.check cdc_reset_ctrlr_half.check \ - cdc_reset_ctrlr_composed.check heaviside.check + cdc_reset_ctrlr_composed.check heaviside.check ecc.check clean: $(RM) $(FORMAL_BUILDDIR) $(RM) fifo.check fifo/ diff --git a/formal/README.md b/formal/README.md index 726118cf..27a44b6f 100644 --- a/formal/README.md +++ b/formal/README.md @@ -13,3 +13,18 @@ features. ## Usage Call `make all` to run all tests. +### ECC +The `ecc` target proves the four cases documented in the header of +`cc_ecc_decode.sv` for the `cc_ecc_encode`/`cc_ecc_decode` pair, over a set of +`DataWidth` values chosen to bracket every parity-width transition that proves +quickly. `make all` runs its `cover` task as well as the proof: the properties +constrain where the injected bit errors may land, and the cover task is what +shows those positions are reachable, so a proof resting on an unsatisfiable +assumption cannot pass unnoticed. + +To repeat the proof over every parity-width transition up to the module default +of `DataWidth` 64, which took around 45 minutes in one local run and is not +part of `make all`: + + sby -f ecc.sby sweep + diff --git a/formal/cc_ecc_formal.sv b/formal/cc_ecc_formal.sv new file mode 100644 index 00000000..84216720 --- /dev/null +++ b/formal/cc_ecc_formal.sv @@ -0,0 +1,169 @@ +// Copyright 2026 ETH Zurich and University of Bologna. +// Copyright and related rights are licensed under the Solderpad Hardware +// License, Version 0.51 (the "License"); you may not use this file except in +// compliance with the License. You may obtain a copy of the License at +// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +// or agreed to in writing, software, hardware and materials distributed under +// this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +// CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. + +// Author: Warren Smith <233830950+repowazdogz-droid@users.noreply.github.com> + +// Elaboration harness for the cc_ecc_encode / cc_ecc_decode pair. +// +// Per data width one encoder feeds four decoders, each seeing a different +// corruption of the encoded word, so every case in cc_ecc_properties.sv has +// its own precondition and none of them interfere. +// +// The default width set brackets every parity-width transition that proves in +// a few seconds. cc_pkg::ecc_get_parity_width adds a parity bit going from +// DataWidth 1 to 2, 4 to 5, and 11 to 12, so each of those boundaries is +// proved on both sides. 1, 4 and 11 are also the widths whose encoded word is +// exactly a power of two bits wide, the case where an index constraint is +// easiest to get wrong. Wider parametrizations, including the module default +// of 64, are covered by the `sweep` task; see formal/README.md. +module cc_ecc_formal import cc_pkg::*; #( +`ifdef ECC_FULL_SWEEP + parameter int unsigned NumWidths = 11, + parameter int unsigned Widths [11] = '{1, 2, 4, 5, 11, 12, 26, 27, 57, 58, 64}, +`else + parameter int unsigned NumWidths = 6, + parameter int unsigned Widths [6] = '{1, 2, 4, 5, 11, 12}, +`endif + // Do not change + localparam int unsigned MaxDataWidth = Widths[NumWidths-1], + localparam int unsigned MaxEncodedWidth = cc_pkg::ecc_get_cw_width(MaxDataWidth) + 1, + localparam int unsigned MaxIdxWidth = cc_pkg::idx_width(MaxEncodedWidth) +) ( + /// Symbolic data word, one disjoint slice per width. + input logic [NumWidths*MaxDataWidth-1:0] data_i, + /// Symbolic positions of the injected bit flips, one disjoint slice per width. + /// + /// The slices must not overlap. Every width constrains its own positions to + /// its own encoded word, so sharing bits between widths would let one + /// width's assumption narrow another's reachable positions: the proof would + /// still pass, having never exercised the excluded positions. The `cover` + /// task is what makes that visible. + input logic [NumWidths*MaxIdxWidth-1:0] pos_a_i, + input logic [NumWidths*MaxIdxWidth-1:0] pos_b_i +); + + for (genvar w = 0; w < NumWidths; w++) begin : gen_width + localparam int unsigned DataWidth = Widths[w]; + localparam int unsigned CwWidth = cc_pkg::ecc_get_cw_width(DataWidth); + localparam int unsigned TotWidth = CwWidth + 1; + localparam int unsigned IdxWidth = cc_pkg::idx_width(TotWidth); + + logic [DataWidth-1:0] data; + logic [IdxWidth-1:0] pos_a, pos_b; + + assign data = data_i [w*MaxDataWidth +: DataWidth]; + assign pos_a = pos_a_i[w*MaxIdxWidth +: IdxWidth]; + assign pos_b = pos_b_i[w*MaxIdxWidth +: IdxWidth]; + + // ------------------------------------------------------------ encoder + logic [TotWidth-1:0] encoded; + + cc_ecc_encode #( + .DataWidth ( DataWidth ) + ) i_encode ( + .data_i ( data ), + .data_o ( encoded ) + ); + + // -------------------------------------------------------- corruptions + // One-hot masks built from the symbolic positions. The positions are + // constrained to the encoded word in cc_ecc_properties.sv. + logic [TotWidth-1:0] mask_a, mask_b; + assign mask_a = {{(TotWidth-1){1'b0}}, 1'b1} << pos_a; + assign mask_b = {{(TotWidth-1){1'b0}}, 1'b1} << pos_b; + + // The extended parity bit is the MSB of the packed {parity, code_word}. + localparam logic [TotWidth-1:0] ParityMask = {1'b1, {CwWidth{1'b0}}}; + + logic [TotWidth-1:0] word_clean, word_single, word_parity, word_double; + assign word_clean = encoded; + assign word_single = encoded ^ mask_a; // P2 restricts pos_a to the codeword + assign word_parity = encoded ^ ParityMask; + assign word_double = encoded ^ mask_a ^ mask_b; // P4 restricts pos_a != pos_b + + // ------------------------------------------------------------ decoders + logic [DataWidth-1:0] clean_data, sgl_data, par_data; + logic clean_single, clean_parity, clean_double; + logic sgl_single, sgl_parity, sgl_double; + logic par_single, par_parity, par_double; + logic dbl_single, dbl_parity, dbl_double; + + cc_ecc_decode #( + .DataWidth ( DataWidth ) + ) i_decode_clean ( + .data_i ( word_clean ), + .data_o ( clean_data ), + .syndrome_o ( ), + .single_error_o ( clean_single ), + .parity_error_o ( clean_parity ), + .double_error_o ( clean_double ) + ); + + cc_ecc_decode #( + .DataWidth ( DataWidth ) + ) i_decode_single ( + .data_i ( word_single ), + .data_o ( sgl_data ), + .syndrome_o ( ), + .single_error_o ( sgl_single ), + .parity_error_o ( sgl_parity ), + .double_error_o ( sgl_double ) + ); + + cc_ecc_decode #( + .DataWidth ( DataWidth ) + ) i_decode_parity ( + .data_i ( word_parity ), + .data_o ( par_data ), + .syndrome_o ( ), + .single_error_o ( par_single ), + .parity_error_o ( par_parity ), + .double_error_o ( par_double ) + ); + + // data_o is left unconnected on purpose: the decoder promises nothing about + // the recovered word under a double error, so no property may read it. + cc_ecc_decode #( + .DataWidth ( DataWidth ) + ) i_decode_double ( + .data_i ( word_double ), + .data_o ( ), + .syndrome_o ( ), + .single_error_o ( dbl_single ), + .parity_error_o ( dbl_parity ), + .double_error_o ( dbl_double ) + ); + + // ---------------------------------------------------------- properties + cc_ecc_properties #( + .DataWidth ( DataWidth ) + ) i_properties ( + .data_i ( data ), + .pos_a_i ( pos_a ), + .pos_b_i ( pos_b ), + .clean_data_i ( clean_data ), + .clean_single_i ( clean_single ), + .clean_parity_i ( clean_parity ), + .clean_double_i ( clean_double ), + .sgl_data_i ( sgl_data ), + .sgl_single_i ( sgl_single ), + .sgl_parity_i ( sgl_parity ), + .sgl_double_i ( sgl_double ), + .par_data_i ( par_data ), + .par_single_i ( par_single ), + .par_parity_i ( par_parity ), + .par_double_i ( par_double ), + .dbl_single_i ( dbl_single ), + .dbl_parity_i ( dbl_parity ), + .dbl_double_i ( dbl_double ) + ); + end + +endmodule : cc_ecc_formal diff --git a/formal/cc_ecc_properties.sv b/formal/cc_ecc_properties.sv new file mode 100644 index 00000000..f56b0079 --- /dev/null +++ b/formal/cc_ecc_properties.sv @@ -0,0 +1,174 @@ +// Copyright 2026 ETH Zurich and University of Bologna. +// Copyright and related rights are licensed under the Solderpad Hardware +// License, Version 0.51 (the "License"); you may not use this file except in +// compliance with the License. You may obtain a copy of the License at +// http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +// or agreed to in writing, software, hardware and materials distributed under +// this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +// CONDITIONS OF ANY KIND, either express or implied. See the License for the +// specific language governing permissions and limitations under the License. + +// Author: Warren Smith <233830950+repowazdogz-droid@users.noreply.github.com> + +// Property checker for the cc_ecc_encode / cc_ecc_decode pair. +// +// The four cases below are the rows of the truth table documented in the +// header of cc_ecc_decode.sv. Each row gets its own decoder instance in +// cc_ecc_formal.sv, so no precondition can weaken another row. +// +// What these properties do NOT establish: +// - nothing is asserted 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, in which case no correction is applied at all. +// - nothing is claimed for more than two flipped bits, which is beyond the +// distance of a SECDED code. +// - the encoder is exercised only through this decoder, not against an +// independent implementation of the same code, so this is a matched-pair +// proof rather than an interoperability one. +module cc_ecc_properties #( + parameter int unsigned DataWidth = 32, + localparam int unsigned ParityWidth = cc_pkg::ecc_get_parity_width(DataWidth), + localparam int unsigned CwWidth = cc_pkg::ecc_get_cw_width(DataWidth), + /// Encoded word: the Hamming codeword plus the extended parity bit. + localparam int unsigned TotWidth = CwWidth + 1, + localparam int unsigned IdxWidth = cc_pkg::idx_width(TotWidth) +) ( + /// Word presented to the encoder. + input logic [DataWidth-1:0] data_i, + /// Symbolic positions of the injected bit flips, indexing the encoded word. + input logic [IdxWidth-1:0] pos_a_i, + input logic [IdxWidth-1:0] pos_b_i, + + /// Decoder fed the untouched encoded word. + input logic [DataWidth-1:0] clean_data_i, + input logic clean_single_i, + input logic clean_parity_i, + input logic clean_double_i, + + /// Decoder fed one flipped bit inside the Hamming codeword. + input logic [DataWidth-1:0] sgl_data_i, + input logic sgl_single_i, + input logic sgl_parity_i, + input logic sgl_double_i, + + /// Decoder fed a flipped extended parity bit, codeword untouched. + input logic [DataWidth-1:0] par_data_i, + input logic par_single_i, + input logic par_parity_i, + input logic par_double_i, + + /// Decoder fed two distinct flipped bits anywhere in the encoded word. + input logic dbl_single_i, + input logic dbl_parity_i, + input logic dbl_double_i +); + + // --------------------------------------------------------------------- + // Parity-width anchor + // + // cc_ecc_encode places a Hamming parity bit at every 1-based codeword + // position that is a power of two and a data bit everywhere else. That + // layout is only consistent if the codeword contains exactly ParityWidth + // power-of-two positions and exactly DataWidth others. + // + // Counting those positions is independent of how cc_pkg::ecc_get_parity_width + // arrives at its answer, so a defect in the package search is not reproduced + // by the check meant to catch it. Recomputing the same search here would + // agree with the package for the same wrong reason. + // + // Both operands are elaboration-time constants. This is therefore an + // elaboration check, not one of the proof obligations below, and it is not + // counted among the proved properties. + function automatic int unsigned count_parity_positions(input int unsigned cw_width); + count_parity_positions = 0; + for (int unsigned i = 1; i <= cw_width; i++) begin + if (cc_pkg::is_power_of_2(i)) count_parity_positions++; + end + endfunction + + localparam int unsigned CountedParityPositions = count_parity_positions(CwWidth); + + if (CountedParityPositions != ParityWidth) begin : gen_parity_width_mismatch + $error("cc_ecc: codeword of %0d bits holds %0d parity positions, but cc_pkg reports %0d", + CwWidth, CountedParityPositions, ParityWidth); + end + if (CwWidth - CountedParityPositions != DataWidth) begin : gen_data_width_mismatch + $error("cc_ecc: codeword of %0d bits leaves %0d data positions for DataWidth %0d", + CwWidth, CwWidth - CountedParityPositions, DataWidth); + end + + // --------------------------------------------------------------------- + // Both flip positions must address a bit of the encoded word. Without this + // the solver is free to pick an index that addresses nothing, the injected + // error becomes a no-op, and P2 and P4 pass for the wrong reason. + // + // The comparison is made at 32 bits and not cast down to IdxWidth. When + // TotWidth is exactly a power of two, IdxWidth'(TotWidth) truncates to zero, + // the assumption becomes unsatisfiable, and every property below is + // vacuously true. The `cover` task exists to keep that class of mistake + // visible; see formal/README.md. + always_comb begin + assume (32'(pos_a_i) < TotWidth); + assume (32'(pos_b_i) < TotWidth); + end + + // ---------------------------------------------------------------- P1 + // No corruption: the data returns intact and no flag is raised. + always_comb begin + p1_data: assert (clean_data_i == data_i); + p1_single: assert (clean_single_i == 1'b0); + p1_parity: assert (clean_parity_i == 1'b0); + p1_double: assert (clean_double_i == 1'b0); + end + + // ---------------------------------------------------------------- P2 + // Exactly one flipped bit inside the Hamming codeword, either a data bit or + // a Hamming parity bit: corrected, and reported as a single error. + // + // The precondition excludes the extended parity bit on purpose. A flip there + // is reported through parity_error_o, so stating P2 over the whole encoded + // word would contradict the documented truth table. + always_comb begin + if (32'(pos_a_i) < CwWidth) begin + p2_data: assert (sgl_data_i == data_i); + p2_single: assert (sgl_single_i == 1'b1); + p2_parity: assert (sgl_parity_i == 1'b0); + p2_double: assert (sgl_double_i == 1'b0); + end + end + + // ---------------------------------------------------------------- P3 + // Only the extended parity bit is flipped: the data is untouched and the + // error is reported as a parity error. + always_comb begin + p3_data: assert (par_data_i == data_i); + p3_parity: assert (par_parity_i == 1'b1); + p3_single: assert (par_single_i == 1'b0); + p3_double: assert (par_double_i == 1'b0); + end + + // ---------------------------------------------------------------- P4 + // Two distinct flipped bits anywhere in the encoded word, the extended + // parity bit included: reported as an uncorrectable double error. + always_comb begin + if (pos_a_i != pos_b_i) begin + p4_double: assert (dbl_double_i == 1'b1); + p4_single: assert (dbl_single_i == 1'b0); + p4_parity: assert (dbl_parity_i == 1'b0); + end + end + + // ------------------------------------------------------------- coverage + // A property whose precondition is unreachable is not evidence. These cover + // points show that the injected-error cases are attainable at the low and + // high ends of the encoded word, that the extended parity bit is reachable + // on its own, and that representative two-bit combinations exist. + always_comb begin + c_sgl_low: cover (32'(pos_a_i) == 32'd0); + c_sgl_high: cover (32'(pos_a_i) == CwWidth - 1); + c_par_only: cover (32'(pos_a_i) == CwWidth); + c_dbl_span: cover (32'(pos_a_i) == 32'd0 && 32'(pos_b_i) == CwWidth); + c_dbl_adj: cover (32'(pos_a_i) == 32'd0 && 32'(pos_b_i) == 32'd1); + end + +endmodule : cc_ecc_properties diff --git a/formal/ecc.sby b/formal/ecc.sby new file mode 100644 index 00000000..3dd8e276 --- /dev/null +++ b/formal/ecc.sby @@ -0,0 +1,57 @@ +# Copyright 2026 ETH Zurich and University of Bologna. +# +# Copyright and related rights are licensed under the Solderpad Hardware +# License, Version 0.51 (the "License"); you may not use this file except in +# compliance with the License. You may obtain a copy of the License at +# http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law +# or agreed to in writing, software, hardware and materials distributed under +# this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR +# CONDITIONS OF ANY KIND, either express or implied. See the License for the +# specific language governing permissions and limitations under the License. +# +# Authors: +# - Warren Smith <233830950+repowazdogz-droid@users.noreply.github.com> +# +# Description: SECDED Encoder/Decoder Proof Configuration +# Configure the SymbiYosys proofs for a set of cc_ecc_encode/cc_ecc_decode +# parametrizations. +# +# `prove` proves the four documented decoder cases on the default widths. +# `cover` shows the injected-error preconditions are reachable, so a green +# `prove` cannot be the result of an unsatisfiable assumption. +# `sweep` repeats `prove` over every parity-width transition up to the module +# default of DataWidth 64. It is not part of `make all`; run it with +# `sby -f ecc.sby sweep`. + +[tasks] +prove proving default +cover default +sweep proving + +[options] +proving: mode prove +cover: mode cover +depth 1 + +[engines] +# The encoder/decoder pair is purely combinational, so depth 1 already covers +# all reachable behaviour; `mode prove` is used so the result is not reported +# as a bounded check. `abc pdr` replaces the `smtbmc` engine the other proofs +# use purely for runtime: on the default width set this proof takes about 7 s +# with PDR against about 3 min with smtbmc, and the gap widens with width. +# The cover task needs a BMC engine, so it stays on smtbmc. +proving: abc pdr +cover: smtbmc + +[script] +plugin -i slang.so +sweep: read_slang --std 1800-2017 -I../../../../include -DECC_FULL_SWEEP --top cc_ecc_formal cc_pkg.sv cc_ecc_encode.sv cc_ecc_decode.sv cc_ecc_properties.sv cc_ecc_formal.sv +~sweep: read_slang --std 1800-2017 -I../../../../include --top cc_ecc_formal cc_pkg.sv cc_ecc_encode.sv cc_ecc_decode.sv cc_ecc_properties.sv cc_ecc_formal.sv +prep -top cc_ecc_formal + +[files] +../src/cc_pkg.sv +../src/cc_ecc_encode.sv +../src/cc_ecc_decode.sv +cc_ecc_properties.sv +cc_ecc_formal.sv