From 341b1b3f3c12d72719788244fcc4f2bc3a1e8eca Mon Sep 17 00:00:00 2001 From: Noam Cohen Date: Thu, 1 Oct 2026 00:20:06 +0200 Subject: [PATCH] Take the naja fix for arrays written from several always blocks Issue #250, third report: on Systolic_MAC_with_DFT the self compare covered 15 of 24 outputs. The result array is written by one always block per element from a generate loop. naja's memory inference made the first block the memory's write port and lowered the second as a flop, so the memory's read data net had two drivers and every cone through it was unverifiable. naja main now leaves an array with several writer blocks to the generic sequential lowering (nanocoh/naja bca04489). The design proves 24 of 24 outputs at k = 1. A CLI test adds the pattern as a self compare gated on full coverage, next to the two earlier #250 tests. --- .../strategies/miter/KeplerFormalCliTests.cpp | 35 +++++++++++++++++++ thirdparty/naja | 2 +- 2 files changed, 36 insertions(+), 1 deletion(-) diff --git a/test/strategies/miter/KeplerFormalCliTests.cpp b/test/strategies/miter/KeplerFormalCliTests.cpp index a5d1dc00..92f93f1f 100644 --- a/test/strategies/miter/KeplerFormalCliTests.cpp +++ b/test/strategies/miter/KeplerFormalCliTests.cpp @@ -4225,6 +4225,34 @@ module three_cycle(input [7:0] A, endmodule : three_cycle )"; +// Issue #250, third report (Systolic_MAC_with_DFT): an unpacked array written +// by one always block per element, as a generate loop produces. The frontend +// used to infer a memory from the first block only and lower the second as a +// flop, so the memory's read data net had two drivers and every output +// through it was skipped. +const char* const kArrayWrittenPerElementSource = R"(module top ( + input wire clk, + input wire [1:0] we, + input wire sel, + input wire [7:0] d0, + input wire [7:0] d1, + output wire [7:0] q +); + wire [7:0] d [1:0]; + assign d[0] = d0; + assign d[1] = d1; + reg [7:0] r [1:0]; + genvar x; + generate + for (x = 0; x < 2; x = x + 1) begin : g + always @(posedge clk) + if (we[x]) r[x] <= d[x]; + end + endgenerate + assign q = sel ? r[1] : r[0]; +endmodule +)"; + // Runs the issue #250 command line: the same file on both sides, dual-rail // PDR with default options, and checks that every output is proved. void expectSelfCompareProvesAllOutputs( @@ -4275,6 +4303,13 @@ TEST_F(KeplerFormalCliTests, expectSelfCompareProvesAllOutputs(kTinyAluSource, "tinyalu", 17u); } +// Issue #250: an array written from several always blocks must not become a +// memory with a second, competing driver. Used to skip all 8 outputs. +TEST_F(KeplerFormalCliTests, + CliSystemVerilogSecSelfCompareArrayWrittenPerElementProvesEveryOutput) { + expectSelfCompareProvesAllOutputs(kArrayWrittenPerElementSource, "top", 8u); +} + TEST_F(KeplerFormalCliTests, CliSystemVerilogVariableIndexMatchesExplicitMux) { const auto fixture = createDesignFixture( diff --git a/thirdparty/naja b/thirdparty/naja index 6331960c..bca04489 160000 --- a/thirdparty/naja +++ b/thirdparty/naja @@ -1 +1 @@ -Subproject commit 6331960cb372ef6d332d07a42fb449d0bea01bbe +Subproject commit bca044899de6d24b51ae5ec92d66bc855e262751