diff --git a/.claude/skills/ci-gates/SKILL.md b/.claude/skills/ci-gates/SKILL.md index 82b8e3bd6..89c54b6b7 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 0c051d452..23a59586e 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 13da85558..073c60bf6 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 e761ec20d..000000000 --- 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 000000000..ceb3cbfb1 --- /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 ae146f69d..8fa9d7130 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 37c4b64da..850383360 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