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