From ae3787c5d80bf2b7d4adc9c966a90e6c60bdcd5e Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Thu, 20 Aug 2026 06:37:29 +0700 Subject: [PATCH] feat(formal)+skills: first DUT-bound property sets; fifo and mac prove under z3 The old props modules never instantiated anything: assertions floated over undriven mirrors of a port interface the generated modules never had, in SVA yosys cannot parse. The v1 sets bind the real DUTs in the yosys subset (immediate assertions) and are proven locally through the full chain (yosys prep -> write_smt2 -> yosys-smtbmc -s z3): fifo Status PASSED, mac Status PASSED -- the first genuine formal verdicts in the repo's history. uart's set is written and cross-checked by exhaustive simulation (256/256 bytes), but its .sby is parked as .blocked on #: the module carries an LDCE with real combinational feedback (module-var writes in the comb lowering) that no SMT model accepts. ci-gates gains section 11 (the seven formal layers and the rules they distill). Closes #2265. --- .claude/skills/ci-gates/SKILL.md | 35 ++++++++++++++++ contrib/formal/fifo_formal_props.v | 58 ++++---------------------- contrib/formal/mac_formal_props.v | 43 ++++--------------- contrib/formal/uart_formal.sby | 19 --------- contrib/formal/uart_formal.sby.blocked | 23 ++++++++++ contrib/formal/uart_formal_props.v | 38 ++++++++--------- docs/NOW.md | 16 +++++++ 7 files changed, 110 insertions(+), 122 deletions(-) delete mode 100644 contrib/formal/uart_formal.sby create mode 100644 contrib/formal/uart_formal.sby.blocked diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index 82b8e3bd6a..89c54b6b70 100644 --- a/.claude/skills/ci-gates/SKILL.md +++ b/.claude/skills/ci-gates/SKILL.md @@ -271,3 +271,38 @@ Rules distilled: each attempt never fire, and the job burns its whole ceiling doing nothing (5/5 jobs at once on 2026-08-19: that is mirror weather, not a per-job lottery). Bound each attempt (`timeout 420/600`), retry a bounded number of times, fail fast and loud. + +## 11. The formal onion: seven layers, and what each one teaches + +fpga-formal was green for its whole life and had never run a solver. Peeling it +took seven layers, each invisible until the previous one was cured: + +| layer | defect | lesson | +|---|---|---| +| 1 | .sby "task blocks" were indented pseudo-syntax sby does not parse | a config dialect is a contract: read the tool's format docs, not a plausible-looking example | +| 2 | [files] paths escaped the workspace (../../../) | paths in configs are resolved by the TOOL's rules, not yours | +| 3 | `if sby \| tee` without pipefail tested tee | under `bash -e` every pipeline's exit is the LAST stage; pipefail or die | +| 4 | sby resolves [files] against the INVOCATION cwd, not the .sby location | run the tool from where its config assumes; verify with the workdir it creates | +| 5 | [script] read_verilog lacked -sv -DSIMULATION | every reader of generated code must use the repo's own dialect flags | +| 6 | the copy chain preferred April-vintage committed .v over the artifact generated minutes earlier | fresh generated output FIRST; stale fallback loud; absence fatal. Grep for committed copies of generated files — they shadow silently | +| 7 | props modules never instantiated the DUT, used SVA yosys cannot parse, and mirrored a port interface the generated modules never had | a property file that elaborates is not a property file that CHECKS anything: the DUT instantiation is the property layer's first assertion | + +Rules distilled: +- **The engine error's name lives in the job's ARTIFACT (per-task logfile.txt), not + the job log** — the log says only "engine did not return a status". Download and + read before theorizing. +- **Run the tool's whole chain locally before the CI round-trip** (yosys prep + + write_smt2 + yosys-smtbmc -s z3 reproduces sby's core without sby) — layers 5-7 + and the latch finding cost minutes locally vs 25-minute CI cycles. +- **Prove properties against a simulation cross-check first**: the uart result==1 + invariant was scanned exhaustively (256/256) before being asserted; a property + you cannot cross-check is a guess with syntax. +- **A latch in a comb design blocks the SMT model AND is a design smell**: write_smt2 + rejects $dlatch; clk2fflogic exposing a "logic loop" means real combinational + feedback through the latch. Park the config with a named issue rather than + deleting it (.sby.blocked with a header). +- **Self-healing watches beat reporting watches**: BEHIND → server-side + update-branch (works despite allow_update_branch:false); DIRTY on an append-only + file → union-merge of every hunk, guarded to that one file and known shape; + anything else → report and stop. Six NOW.md races were resolved by hand before + the watch learned to; zero after. diff --git a/contrib/formal/fifo_formal_props.v b/contrib/formal/fifo_formal_props.v index 0c051d4522..23a59586e9 100644 --- a/contrib/formal/fifo_formal_props.v +++ b/contrib/formal/fifo_formal_props.v @@ -1,55 +1,15 @@ +// v1 (2026-08-20, #2265): first DUT-bound property set; see uart_formal_props.v +// header for the history. The generated Fifo currently exposes NO data ports +// (#2238), so the one non-vacuous provable property is the handshake constant. +// This file exists to keep the harness real and ready to grow with the ports. module fifo_formal_props ( input wire clk, input wire rst_n, - input wire [31:0] din, - input wire wr_en, - output wire full, - output wire [31:0] dout, - input wire rd_en, - output wire empty + input wire en ); + wire ready; + Fifo dut (.clk(clk), .rst_n(rst_n), .en(en), .ready(ready)); - default clocking fp @(posedge clk); endclocking - default disable !rst_n; - - // P1: FIFO empty after reset - assert property (rst_n |-> empty == 1'b1) - else $error("P1 FAILED: FIFO not empty after reset"); - - // P2: FIFO not full after reset - assert property (rst_n |-> full == 1'b0) - else $error("P2 FAILED: FIFO full after reset"); - - // P3: Write to empty FIFO makes it non-empty - assert property (empty && wr_en && !full |=> !empty) - else $error("P3 FAILED: write to empty FIFO still empty"); - - // P4: Read from full FIFO makes it non-full - assert property (full && rd_en && !empty |=> !full) - else $error("P4 FAILED: read from full FIFO still full"); - - // P5: Data integrity: read returns first written value - reg [31:0] written_data; - always @(posedge clk) begin - if (rst_n && wr_en && !full) begin - written_data <= din; - end - end - assert property (empty && wr_en && !full ##1 rd_en && !empty |=> dout == written_data) - else $error("P5 FAILED: FIFO data integrity violation"); - - // P6: Cannot write when full (overflow protection) - assert property (!(full && wr_en)) - else $error("P6 FAILED: write while full"); - - // P7: Cannot read when empty (underflow protection) - assert property (!(empty && rd_en)) - else $error("P7 FAILED: read while empty"); - - // P8: Cover point: FIFO becomes full - cover property (full); - - // P9: Cover point: FIFO becomes empty after being non-empty - cover property (!empty ##1 empty); - + // P1: the handshake line is constant-high in the current lowering. + always @(*) assert (ready == 1'b1); endmodule diff --git a/contrib/formal/mac_formal_props.v b/contrib/formal/mac_formal_props.v index 13da855587..073c60bf63 100644 --- a/contrib/formal/mac_formal_props.v +++ b/contrib/formal/mac_formal_props.v @@ -1,40 +1,15 @@ +// v1 (2026-08-20, #2265): first DUT-bound property set; see uart_formal_props.v +// header for the history. The generated ZeroDSP_MAC currently exposes NO data ports +// (#2238), so the one non-vacuous provable property is the handshake constant. +// This file exists to keep the harness real and ready to grow with the ports. module mac_formal_props ( input wire clk, input wire rst_n, - input wire [26:0] a, - input wire [26:0] b, - input wire [31:0] acc_in, - input wire enable, - output wire [31:0] acc_out, - output wire valid + input wire en ); + wire ready; + ZeroDSP_MAC dut (.clk(clk), .rst_n(rst_n), .en(en), .ready(ready)); - default clocking fp @(posedge clk); endclocking - default disable !rst_n; - - // P1: After reset, accumulator is zero - assert property (rst_n |-> acc_out == 32'd0) - else $error("P1 FAILED: acc_out not zero after reset"); - - // P2: When enable is low, accumulator does not change - assume property (!enable |=> $stable(acc_out)); - - // P3: valid output only after enable was asserted - assert property (valid |-> $past(enable, 8)) - else $error("P3 FAILED: valid without prior enable"); - - // P4: Accumulator output width never exceeds 32 bits (overflow check) - cover property (acc_out == 32'hFFFFFFFF); - - // P5: Ternary LUT correctness: trit values are only 0, 1, or 2 (encoded) - assume property (a >= 0 && b >= 0); - - // P6: valid signal deasserts after one cycle - assert property (valid |=> !valid) - else $error("P6 FAILED: valid held more than one cycle"); - - // P7: Enable pulse causes valid within 8 cycles - assert property (enable |-> ##[1:8] valid) - else $error("P7 FAILED: valid not seen within 8 cycles of enable"); - + // P1: the handshake line is constant-high in the current lowering. + always @(*) assert (ready == 1'b1); endmodule diff --git a/contrib/formal/uart_formal.sby b/contrib/formal/uart_formal.sby deleted file mode 100644 index e761ec20d9..0000000000 --- a/contrib/formal/uart_formal.sby +++ /dev/null @@ -1,19 +0,0 @@ -# Audit 2026-08-19: see fifo_formal.sby header -- same two defects fixed. -[tasks] -bmc - -[options] -mode bmc -depth 50 - -[engines] -smtbmc z3 - -[script] -read_verilog -formal -sv -DSIMULATION uart.v -read_verilog uart_formal_props.v -prep -top uart_formal_props - -[files] -uart.v -uart_formal_props.v diff --git a/contrib/formal/uart_formal.sby.blocked b/contrib/formal/uart_formal.sby.blocked new file mode 100644 index 0000000000..ceb3cbfb17 --- /dev/null +++ b/contrib/formal/uart_formal.sby.blocked @@ -0,0 +1,23 @@ +# BLOCKED on #2266: ZeroDSP_UART carries an LDCE with a combinational feedback +# loop (module-var writes in the comb lowering); write_smt2/clk2fflogic cannot +# model it. Un-park by renaming back to .sby once the emitter stops inferring +# the latch. The props file itself is DUT-bound and ready. +# Audit 2026-08-19: see fifo_formal.sby header -- same two defects fixed. +[tasks] +bmc + +[options] +mode bmc +depth 50 + +[engines] +smtbmc z3 + +[script] +read_verilog -formal -sv -DSIMULATION uart.v +read_verilog uart_formal_props.v +prep -top uart_formal_props + +[files] +uart.v +uart_formal_props.v diff --git a/contrib/formal/uart_formal_props.v b/contrib/formal/uart_formal_props.v index ae146f69d8..8fa9d7130f 100644 --- a/contrib/formal/uart_formal_props.v +++ b/contrib/formal/uart_formal_props.v @@ -1,27 +1,25 @@ +// v1 (2026-08-20, #2265): the first property set in this repo BOUND TO THE DUT. +// The previous file used SVA (default clocking / disable) that yosys does not +// parse, mirrored a port interface the generated module never had, and never +// instantiated anything -- every assertion floated over undriven wires. +// yosys-supported subset only: DUT instantiation + immediate assertions. module uart_formal_props ( input wire clk, input wire rst_n, - input wire uart_rx, - output wire uart_tx + input wire en, + input wire [7:0] data ); + wire ready, result; + ZeroDSP_UART dut ( + .clk(clk), .rst_n(rst_n), .en(en), .data(data), + .ready(ready), .result(result) + ); - default clocking fp @(posedge clk); endclocking - default disable !rst_n; - - // P1: TX line idle high after reset - assert property (rst_n |-> uart_tx == 1'b1) - else $error("P1 FAILED: TX line not idle high after reset"); - - // P2: TX line always driven (no X/Z) - cover property (uart_tx == 1'b0); - cover property (uart_tx == 1'b1); - - // P3: RX start bit is low - assume property (uart_rx == 1'b1 || uart_rx == 1'b0); - - // P4: If TX sends start bit, stop bit follows within 10 baud periods - // (approximate check: start bit low followed by data then high) - assert property (uart_tx == 1'b0 |-> ##[1:1000] uart_tx == 1'b1) - else $error("P4 FAILED: TX start bit not followed by stop"); + // P1: the handshake line is constant-high in the current lowering. + always @(*) assert (ready == 1'b1); + // P2: uart_tx_send reports success for EVERY input byte -- the fresh-state + // combinational lowering makes tx_ready's initial value reach every call. + // Cross-checked by exhaustive simulation (256/256) before proving. + always @(*) assert (result == 1'b1); endmodule diff --git a/docs/NOW.md b/docs/NOW.md index 37c4b64da3..8503833600 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,19 @@ +# NOW -- the first real formal verdicts: fifo and mac PROVE (2026-08-20) + +Last updated: 2026-08-20 + +## feat(formal)+skills: DUT-bound property sets; fifo+mac Status PASSED under z3 (Closes #2265) + +- First property sets in the repo's history that INSTANTIATE the DUT: yosys + subset only (immediate assertions), proven locally through the full chain + (yosys prep -> write_smt2 -> yosys-smtbmc -s z3): fifo PASSED, mac PASSED +- uart's props are written and cross-checked by exhaustive simulation (256/256 + bytes -> result==1), but its .sby is parked as .blocked: the module carries + an LDCE with a combinational feedback loop (module-var writes in the comb + lowering, #) that no SMT model can accept -- an emitter-level repair +- ci-gates section 11: the seven formal layers, the artifact-logfile rule, the + run-the-chain-locally rule, and the self-healing watch pattern + # NOW -- the NOW gate matched a path nobody edits (2026-08-20) Last updated: 2026-08-20