diff --git a/docs/now/2026-09-20-published-test-the-1-untested-function-in-specs-fpga-router-t27.md b/docs/now/2026-09-20-published-test-the-1-untested-function-in-specs-fpga-router-t27.md new file mode 100644 index 000000000..569501aa4 --- /dev/null +++ b/docs/now/2026-09-20-published-test-the-1-untested-function-in-specs-fpga-router-t27.md @@ -0,0 +1,11 @@ +# NOW -- Test the 1 untested function in specs/fpga/router.t27 (published 2026-09-20) + +## A bee's work on #4448, published from `queen-4448` (Closes #4448) + +- The branch changes 1 file(s): `specs/fpga/router.t27`. +- `git diff --stat origin/master...queen-4448` reads: 1 file changed, 15 insertions(+) +- This entry is written by the publisher, not by the bee. A pull request must + add exactly one `docs/now/` entry and a bee has no way to know that: its brief + names a boundary file and acceptance criteria, and `docs/now/` is neither. +- What this entry does NOT establish: that the work is correct. The gates on the + pull request judge that, and they are the same gates every other change meets. diff --git a/docs/now/2026-09-22-published-test-the-1-untested-function-in-specs-fpga-router-t27.md b/docs/now/2026-09-22-published-test-the-1-untested-function-in-specs-fpga-router-t27.md new file mode 100644 index 000000000..78fac1597 --- /dev/null +++ b/docs/now/2026-09-22-published-test-the-1-untested-function-in-specs-fpga-router-t27.md @@ -0,0 +1,11 @@ +# NOW -- Test the 1 untested function in specs/fpga/router.t27 (published 2026-09-22) + +## A bee's work on #4448, published from `queen-4448` (Closes #4448) + +- The branch changes 2 file(s): `docs/now/2026-09-20-published-test-the-1-untested-function-in-specs-fpga-router-t27.md`, `specs/fpga/router.t27`. +- `git diff --stat origin/master...queen-4448` reads: 2 files changed, 26 insertions(+) +- This entry is written by the publisher, not by the bee. A pull request must + add exactly one `docs/now/` entry and a bee has no way to know that: its brief + names a boundary file and acceptance criteria, and `docs/now/` is neither. +- What this entry does NOT establish: that the work is correct. The gates on the + pull request judge that, and they are the same gates every other change meets. diff --git a/specs/fpga/router.t27 b/specs/fpga/router.t27 index 2423b268c..f9a6fc981 100644 --- a/specs/fpga/router.t27 +++ b/specs/fpga/router.t27 @@ -233,6 +233,21 @@ module Router { given e = ConnEdge{.source = "", .sink = "", .kind = 0, .bit_width = 0} then validate_edge(e) > 0 + test est_total_wire_basic + given edges = [data_edge("a", "b", 32), data_edge("c", "d", 16)] + and fanouts = [fanout("net1", 2, 32), fanout("net2", 8, 16), fanout("net3", 32, 8)] + then est_total_wire(edges, 2, fanouts, 3) == 88000 + + test est_total_wire_zero_fcount + given edges = [data_edge("a", "b", 32)] + and fanouts = [fanout("net1", 4, 32)] + then est_total_wire(edges, 1, fanouts, 0) == 0 + + test est_total_wire_zero_fanout + given edges = [data_edge("a", "b", 32)] + and fanouts = [fanout("net1", 0, 32)] + then est_total_wire(edges, 1, fanouts, 1) == 0 + // === Invariants === invariant wire_length_non_negative