Skip to content

formal: add SymbiYosys proof for cc_ecc_encode/cc_ecc_decode #355

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
repowazdogz-droid wants to merge 1 commit into
base: master
Choose a base branch
from
Open

formal: add SymbiYosys proof for cc_ecc_encode/cc_ecc_decode #355

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 14 additions & 2 deletions formal/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 $@
Expand Down Expand Up @@ -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/
Expand Down
15 changes: 15 additions & 0 deletions formal/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

169 changes: 169 additions & 0 deletions formal/cc_ecc_formal.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
174 changes: 174 additions & 0 deletions formal/cc_ecc_properties.sv
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Loading