feat(formal): first DUT-bound property sets — fifo and mac prove under z3

.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.

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

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

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

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

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