diff --git a/.trinity/seals/Backend.json b/.trinity/seals/Backend.json index 3ee7cc4e4..151345367 100644 --- a/.trinity/seals/Backend.json +++ b/.trinity/seals/Backend.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:fd474d6353533623ef9172336c77eea37edff13ee1a3a3058f8d2b9127d5eea0", + "gen_hash_c": "sha256:c14ee9123cacf6eed3b47fc3e6761cf8c44b1999d965380ed951763230d556f7", "gen_hash_rust": "sha256:c103921e09e51a6b1c7cc7e7cfa6a43b7651dfdc5397915293e7975a6fb1eaac", - "gen_hash_verilog": "sha256:c6211d32171e7de0d917222c48282ad8e62b14a899922bccb11141281c769f4e", - "gen_hash_zig": "sha256:a9c279628915ac3b91e55137b500db52d4e7ec466128fe5a36bf134af3c3caac", + "gen_hash_verilog": "sha256:f365308297d87d4fa7268b80ec6d90ad91a2ca026d8ea6cf56716a75efcc3277", + "gen_hash_zig": "sha256:270af45cd5c6748b9b8dc5cbfd1358d872d9b10ec22ec245eaa98021839ced41", "module": "Backend", "ring": 32, - "sealed_at": "2026-09-08T10:55:59Z", - "spec_hash": "sha256:0ff4b116919b5693bd01638a7bcea9616af53ef6195a220df32ae4f8d1944d21", + "sealed_at": "2026-09-08T11:16:06Z", + "spec_hash": "sha256:62f35791f856137a862caf7c205d54de386d8494bf2536fcab561741f08010e1", "spec_path": "specs/igla/race/backend.t27" } \ No newline at end of file diff --git a/.trinity/seals/RTL.json b/.trinity/seals/RTL.json index fbbd5c717..b1e4fe3ab 100644 --- a/.trinity/seals/RTL.json +++ b/.trinity/seals/RTL.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:2b5aaa89ef3318ecb574a223ca90cc485e1fe99b51ba6d12d9cec79726e9650a", + "gen_hash_c": "sha256:9538b96c35da3a13dbc6480ffe677c04fe58155b95f4576e30fe2b8f3a6885d6", "gen_hash_rust": "sha256:78753bc84edf9c0715982b590dc8acf77012445af5cba89db256fa7be1e457b6", - "gen_hash_verilog": "sha256:7334fbf4afc0e5a24edc8079a3cc37aae16deb2b4692a996e5060dab06b331b8", - "gen_hash_zig": "sha256:6f3c0cc1049f2a53f9a2a23a3f85229739f48ce74a55bc730e066f5620878cdd", + "gen_hash_verilog": "sha256:d211220b876e0ff3a84b44de3a618dc7a8eeb8e5b6e7a54294fadf371e12af6d", + "gen_hash_zig": "sha256:35e90b4869e68454c87458f55510d22690aaa056d3069c218b9a797a693d4059", "module": "RTL", "ring": 32, - "sealed_at": "2026-09-08T10:56:00Z", - "spec_hash": "sha256:ffb9973ab5fe032daa3143738d6dfd5c8b3fd1f06096e6794dfdba8c0829b65d", + "sealed_at": "2026-09-08T11:16:07Z", + "spec_hash": "sha256:d062a67d5cea57f6533fdc506780b589c98ff079f673b59676d7062dc3ae2b56", "spec_path": "specs/igla/race/rtl.t27" } \ No newline at end of file diff --git a/.trinity/seals/coder_igla-coder-arch.json b/.trinity/seals/coder_igla-coder-arch.json index 3ebef5dbf..abcb7f5aa 100644 --- a/.trinity/seals/coder_igla-coder-arch.json +++ b/.trinity/seals/coder_igla-coder-arch.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:c336e051273866665dc3340a1f7b540be1648d7de95375458dbd45875942f79b", + "gen_hash_c": "sha256:6bcb78cf02d5354cfe0eee13db0c63c12700c31c05fb5f7de657879d09d039e5", "gen_hash_rust": "sha256:c74ffd16d6a53e65bbce0f62af1e6611a44710dacff344b3ea28401fb5c6aad2", - "gen_hash_verilog": "sha256:0f3a59116172a125639feb6a7242c435c0c78f1109daa8784a7e3c726d3d4fdf", - "gen_hash_zig": "sha256:503620bc877ab4dc5b6ac0fddf9e4b5e46d8538c1b6edb46fb3351683e34a11c", + "gen_hash_verilog": "sha256:7ad38e94255fb3442588369b348b61df4d302df3e783ebf8fd0a203ec5e28e1c", + "gen_hash_zig": "sha256:b901b1daef237e8ab4ab5171e4546dceb3426bdf6c008f2077776b97bab785bc", "module": "igla-coder-arch", "ring": 12, - "sealed_at": "2026-09-08T10:55:57Z", + "sealed_at": "2026-09-08T11:16:05Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:df65dcac822b4a185dd068358d16ddbff25aaac41752a4790132ccc20d29296b", + "spec_hash": "sha256:01353d9b489c0adbf88cda433d9b37fa974ab73977195601a6dea9feec74d740", "spec_path": "specs/igla/coder/arch.t27" } \ No newline at end of file diff --git a/.trinity/seals/coder_igla-coder-benchmark.json b/.trinity/seals/coder_igla-coder-benchmark.json index ca0fe7875..b9d9c02a1 100644 --- a/.trinity/seals/coder_igla-coder-benchmark.json +++ b/.trinity/seals/coder_igla-coder-benchmark.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:76ace93fe4e4976afa770e3150080c56e9e9475c6ef800e6a05b4dbfbd866b27", + "gen_hash_c": "sha256:12d569d3bec550d5302ceface69e4061b5f9ccd8d8f15c8294ca278875b17d24", "gen_hash_rust": "sha256:a3fca9ee8ea5a922318c415c78dfddc14a93b29fdfc693e88d21ab451e9a36f4", - "gen_hash_verilog": "sha256:888eb080620ac774c109230bffb070a8b7cb7e24cee58710c741ea0b1ddf5738", - "gen_hash_zig": "sha256:72430274aa7bfa2db2ec420ad977b402e134d1c3eef2b199b54d9896232d91d2", + "gen_hash_verilog": "sha256:829aa193ca03b2c33b60c4038c77e06f24939bb9e3dd52a88348d8f9be62aefd", + "gen_hash_zig": "sha256:3b10b64c4d2487cfcefc130f4d1ac1020f47d5294957c4717df407278aeefb6a", "module": "igla-coder-benchmark", "ring": 12, - "sealed_at": "2026-09-08T10:55:58Z", + "sealed_at": "2026-09-08T11:16:05Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:51fdf6d7ba161c84b6b4b1f862be0a27c4bb0aa7ebaaef496ee8256bd999c698", + "spec_hash": "sha256:3bc0b4f043a561e151081570bb5035fa4e54b3a62b061619056f8a13ecdcb1d8", "spec_path": "specs/igla/coder/benchmark.t27" } \ No newline at end of file diff --git a/.trinity/seals/coder_igla-coder-dataset.json b/.trinity/seals/coder_igla-coder-dataset.json index e14662f97..03068b92d 100644 --- a/.trinity/seals/coder_igla-coder-dataset.json +++ b/.trinity/seals/coder_igla-coder-dataset.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:bbf791289b9276810709d21f7049184cd84c440fa7215039371c0a9daa959ee4", + "gen_hash_c": "sha256:474aba79af25f47c6266c5c6315161141bf943105c85f1820cee43ac0bcf4521", "gen_hash_rust": "sha256:b725d5db75bc0e7e668119d0967b03e581cbebaff0115e640762bef3f532d62b", - "gen_hash_verilog": "sha256:2acf75ea173a8c7a8f0656072bb6fe3376c061350f81182a9dd4f2ccc4e3436f", - "gen_hash_zig": "sha256:cd2fe76c764fbfee260c964eb4b8d6b911f854b9890056905d47618895cb977c", + "gen_hash_verilog": "sha256:ca4b5edae76903601e57b78b3ad9892a1f37b85d377653ba816ef26460527529", + "gen_hash_zig": "sha256:9cc02f8da315f4d5ecbe7ab6023af027e33f4e0572a9b2bab55e73151511d99f", "module": "igla-coder-dataset", "ring": 12, - "sealed_at": "2026-09-08T10:55:58Z", + "sealed_at": "2026-09-08T11:16:06Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:3c3b2ebeeb40748d939a5c23321dce8dfcab4a75188d3860aa83c07e8bc5beed", + "spec_hash": "sha256:b9a67a36ec91ba9f2df7afb43a264d152ae0c5577e29f11371fcb39668aad0d2", "spec_path": "specs/igla/coder/dataset.t27" } \ No newline at end of file diff --git a/.trinity/seals/coder_igla-coder-eval.json b/.trinity/seals/coder_igla-coder-eval.json index c064d93ff..0bdee39f7 100644 --- a/.trinity/seals/coder_igla-coder-eval.json +++ b/.trinity/seals/coder_igla-coder-eval.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:b5dd4ac799144c2810a2bc681ae60cb4739dd301ea8928fd435f9636a86b0360", + "gen_hash_c": "sha256:bdc92613d9482b42c31782b8b989a3b84f658132ac709cdc0dae5d138515d85c", "gen_hash_rust": "sha256:f8ccfb7b1aaf5cfa0c7c10290463cb1b12e1a36935670fb83db3629146a2340e", - "gen_hash_verilog": "sha256:21b9060a683ceed22ca2293354001b32ec2722635f78207026e50932a9d5dcaf", - "gen_hash_zig": "sha256:d5f057546dcab4bf9c1bddb1bebddfd3592df6fb0b923359f2e859480a9a7706", + "gen_hash_verilog": "sha256:a8b606f5eaf20caaf68306139b4b50009c29fd846c0a488869a52a3c7ec16946", + "gen_hash_zig": "sha256:86f8c3f2cd967e405ef4437bf8a8ed5c9c2bd3e98eb30043cbd957f06a7a3ff7", "module": "igla-coder-eval", "ring": 12, - "sealed_at": "2026-09-08T10:55:58Z", + "sealed_at": "2026-09-08T11:16:06Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:0877eefb3647b0b6772e79b0e1f66c63ecc31b7f8f5a3dd080b99385d357dcba", + "spec_hash": "sha256:c79668668fd5c4248c5be928bfb4965bf3ae44158fbfc3c56d89f396d573172d", "spec_path": "specs/igla/coder/eval.t27" } \ No newline at end of file diff --git a/.trinity/seals/coder_igla-coder-pipeline.json b/.trinity/seals/coder_igla-coder-pipeline.json index c352d40e6..5fc734a7f 100644 --- a/.trinity/seals/coder_igla-coder-pipeline.json +++ b/.trinity/seals/coder_igla-coder-pipeline.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:5c8195534574d7e31e0117d82ab5e8e7daae8a3f72eb9fafa94588e269796e63", + "gen_hash_c": "sha256:317445bec3f45e0dc0d6b8ee456e946516e48da8511ada1a9ca517c3dd5a6834", "gen_hash_rust": "sha256:eb4c6582020de55d0301b9a7f47d4770a59907a5f81318e8c5054a4bc66b00eb", - "gen_hash_verilog": "sha256:a8229c5a3ab8f3ded43dfcc35cb236d9cf599d05bfc6b3b463c29bac914eba51", - "gen_hash_zig": "sha256:6b87c809a45d4959249a25769019a30dc94fcb379445de2d5109a4a93e644124", + "gen_hash_verilog": "sha256:a05bd90f9cff0b53f50cac2a23715caf215032d0c723ba57637cfd4210293aa9", + "gen_hash_zig": "sha256:db388c8f28e2796ece2eb1b66b6c4cc26759ffb5504a71c5e7c16a990b1aaa1e", "module": "igla-coder-pipeline", "ring": 12, - "sealed_at": "2026-09-08T10:55:58Z", + "sealed_at": "2026-09-08T11:16:06Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:2f7c32f0d0618ccfb75a599337bbad522b0c6e8e420b36a2c2f86a7db7362bca", + "spec_hash": "sha256:7ced47ba19d0e638422a4fb841c25e3abd45b561787e18f3d62f2bcad90321da", "spec_path": "specs/igla/coder/pipeline.t27" } \ No newline at end of file diff --git a/.trinity/seals/coder_igla-coder-tokenizer.json b/.trinity/seals/coder_igla-coder-tokenizer.json index 3d285ad12..d45cbafba 100644 --- a/.trinity/seals/coder_igla-coder-tokenizer.json +++ b/.trinity/seals/coder_igla-coder-tokenizer.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:0d8055b358bdacee4b2a648d77ae664a108e5ad5d4ea0f4a1bd7ccfdad4c15bf", + "gen_hash_c": "sha256:36807f21c9d060f0d3a80909fcb8e22c405041cc04688752fbf3dfd643ace64d", "gen_hash_rust": "sha256:c0f00ace59cd9774faa64bbe5b7e54872c0d5bccc56159f5361833b67cc17193", - "gen_hash_verilog": "sha256:fcb107410d9551fcb7d4f507fc5bbbd7edb5feb76707f8e8f769ffd33277471f", - "gen_hash_zig": "sha256:a1d7487a15ced5acc8a84da95c1cb10f3122c33409db30e9c10ac5c9d170476a", + "gen_hash_verilog": "sha256:c172ed1393dcbaa31d882b80ff1bc6fe0e4629a021de15653f8b47140df35775", + "gen_hash_zig": "sha256:27ab8c368cd75f327f1acaeea4daaf6855be4db5e5d3440d4773c59dd1bcfd79", "module": "igla-coder-tokenizer", "ring": 12, - "sealed_at": "2026-09-08T10:55:58Z", + "sealed_at": "2026-09-08T11:16:06Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:a1720cf8c80b6634809a281fe8b9f1b3e7abae6a299bf74a8fd50f43b523d6e2", + "spec_hash": "sha256:5a4913e61e90b9be2632619b3eb79b7a93a445d36fa724601fac5f95e3c7a283", "spec_path": "specs/igla/coder/tokenizer.t27" } \ No newline at end of file diff --git a/.trinity/seals/coder_igla-coder-training.json b/.trinity/seals/coder_igla-coder-training.json index 49cb39114..940944e51 100644 --- a/.trinity/seals/coder_igla-coder-training.json +++ b/.trinity/seals/coder_igla-coder-training.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:a8f69cf776133fe330a61039fc388977160de36a70326b94e630973c9d732d08", + "gen_hash_c": "sha256:67f9554bc72128688dd9103bcefffd54ea00659830e5217da60c9943fde430a6", "gen_hash_rust": "sha256:759befd74dc3dae89f9a48dd0f74432e8d3c2d33f7cab17b0987d10ec26b0efc", - "gen_hash_verilog": "sha256:dbc7d03f645d3e67139280316b18e2308ddaecd05852ab55be90295bacc9c4ef", - "gen_hash_zig": "sha256:cffcec6d500be0f2d512f428260cc2c9f01d08d8d858d164c3435906bfdcda18", + "gen_hash_verilog": "sha256:dd7901d16fd6b3f3479374459e3a819cc448fc3c28b55582ad0bb550eb6967bd", + "gen_hash_zig": "sha256:f4311a46769be6e4fffee985c5ecfd91573150569ef770a3b3d483065c93c604", "module": "igla-coder-training", "ring": 12, - "sealed_at": "2026-09-08T10:55:59Z", + "sealed_at": "2026-09-08T11:16:06Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:a09b917835ab6ec3616da6e1035c4a640cbcb453cf99f243c2f4214bae47e589", + "spec_hash": "sha256:ad23bb061da98f151cca70bbc2e6be16536f23f09d867aac11c2040a2427ac82", "spec_path": "specs/igla/coder/training.t27" } \ No newline at end of file diff --git a/.trinity/seals/config-schema.json b/.trinity/seals/config-schema.json index 5d90e5aa0..57e45cce7 100644 --- a/.trinity/seals/config-schema.json +++ b/.trinity/seals/config-schema.json @@ -1,11 +1,11 @@ { - "gen_hash_c": "sha256:d2626225e7653a9e5900a9bd407197a47362da160bb0d9acef9b79b06c490bc9", + "gen_hash_c": "sha256:6560147a141ed45dc8ca6faeb5afa20e29fe6f4f04295d192837907ac73b2e06", "gen_hash_rust": "sha256:630600b84e29898baaf44618f628153dc6089aab0e5a84a814c6745ffa3e1dae", - "gen_hash_verilog": "sha256:6c96b3c7ab50612ff80f42e4e7341815cccc0a4d2d9be8f24095d68571d18cf9", - "gen_hash_zig": "sha256:eb06aaf98e53a3588b81fea953c56c370b520c7231b8e1237502851e6a762e62", + "gen_hash_verilog": "sha256:bbcc1b3a5ab8d1fb72063d0f1dba2141498a58497c7c8e6071854133ef27d69d", + "gen_hash_zig": "sha256:21efa9dd9fc50de73180541a9156c00e9d5679934ba730c6824eecf6a28074db", "module": "config-schema", "ring": 12, - "sealed_at": "2026-09-08T10:55:57Z", - "spec_hash": "sha256:bdb57bb4846a2eccc182eb048f343a4d8de37051586299f81d6ca04ff77491f5", + "sealed_at": "2026-09-08T11:16:05Z", + "spec_hash": "sha256:fba55b502378d03a684fbbeb6983d13a6d9bf750b1b176ae50b588c9052ef08d", "spec_path": "specs/config/schema.t27" } \ No newline at end of file diff --git a/.trinity/seals/config_config-schema.json b/.trinity/seals/config_config-schema.json index e94d5b7b4..68145de3d 100644 --- a/.trinity/seals/config_config-schema.json +++ b/.trinity/seals/config_config-schema.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:d2626225e7653a9e5900a9bd407197a47362da160bb0d9acef9b79b06c490bc9", + "gen_hash_c": "sha256:6560147a141ed45dc8ca6faeb5afa20e29fe6f4f04295d192837907ac73b2e06", "gen_hash_rust": "sha256:630600b84e29898baaf44618f628153dc6089aab0e5a84a814c6745ffa3e1dae", - "gen_hash_verilog": "sha256:6c96b3c7ab50612ff80f42e4e7341815cccc0a4d2d9be8f24095d68571d18cf9", - "gen_hash_zig": "sha256:eb06aaf98e53a3588b81fea953c56c370b520c7231b8e1237502851e6a762e62", + "gen_hash_verilog": "sha256:bbcc1b3a5ab8d1fb72063d0f1dba2141498a58497c7c8e6071854133ef27d69d", + "gen_hash_zig": "sha256:21efa9dd9fc50de73180541a9156c00e9d5679934ba730c6824eecf6a28074db", "module": "config-schema", "ring": 12, - "sealed_at": "2026-09-08T10:55:57Z", + "sealed_at": "2026-09-08T11:16:05Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:bdb57bb4846a2eccc182eb048f343a4d8de37051586299f81d6ca04ff77491f5", + "spec_hash": "sha256:fba55b502378d03a684fbbeb6983d13a6d9bf750b1b176ae50b588c9052ef08d", "spec_path": "specs/config/schema.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-adder-tree.json b/.trinity/seals/race_igla-race-adder-tree.json index 3c382180f..b1c33b90e 100644 --- a/.trinity/seals/race_igla-race-adder-tree.json +++ b/.trinity/seals/race_igla-race-adder-tree.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:def2ee21d8e62a1808b90b36afeee595c3217642b1466722f4b0dcc8c176a2e0", + "gen_hash_c": "sha256:c0d95747e26deb5eed2012e7f9fd5754a44140135a220179f7d7928c33901d59", "gen_hash_rust": "sha256:2abbce83b7a0745c8d3bd45ba3ef5c2af9525a3ca868c3449b5806495cd75e4e", - "gen_hash_verilog": "sha256:88892ac4538f1f46caecbed2ad8f75b85f624df41dd40aeabf6a6132a3812571", - "gen_hash_zig": "sha256:b70af91f1eeaf847da4429dfeb86c57fba4e38dd4ad79aabe594290525304275", + "gen_hash_verilog": "sha256:94128b9e53998cce672de3a0bdae75f1f29ad2ce4367a7d3d576656f5f55c6ec", + "gen_hash_zig": "sha256:7947a58cee21bf4e6cb98510e5f48522158d1d5e9126f404b918980bab140861", "module": "igla-race-adder-tree", "ring": 12, - "sealed_at": "2026-09-08T10:55:59Z", + "sealed_at": "2026-09-08T11:16:06Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:026d1f0c18e847916563761be7cbecde6534434bab8328725167642c4c9a1f29", + "spec_hash": "sha256:7155d76ca10f03c4c2cbe92de1350a9f38a118d9c610a9cfe2c0be294d441758", "spec_path": "specs/igla/race/adder_tree.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-backend.json b/.trinity/seals/race_igla-race-backend.json index 46df2c3d2..e03404993 100644 --- a/.trinity/seals/race_igla-race-backend.json +++ b/.trinity/seals/race_igla-race-backend.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:fd474d6353533623ef9172336c77eea37edff13ee1a3a3058f8d2b9127d5eea0", + "gen_hash_c": "sha256:c14ee9123cacf6eed3b47fc3e6761cf8c44b1999d965380ed951763230d556f7", "gen_hash_rust": "sha256:c103921e09e51a6b1c7cc7e7cfa6a43b7651dfdc5397915293e7975a6fb1eaac", - "gen_hash_verilog": "sha256:c6211d32171e7de0d917222c48282ad8e62b14a899922bccb11141281c769f4e", - "gen_hash_zig": "sha256:a9c279628915ac3b91e55137b500db52d4e7ec466128fe5a36bf134af3c3caac", + "gen_hash_verilog": "sha256:f365308297d87d4fa7268b80ec6d90ad91a2ca026d8ea6cf56716a75efcc3277", + "gen_hash_zig": "sha256:270af45cd5c6748b9b8dc5cbfd1358d872d9b10ec22ec245eaa98021839ced41", "module": "igla-race-backend", "ring": 12, - "sealed_at": "2026-09-08T10:55:59Z", + "sealed_at": "2026-09-08T11:16:06Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:0ff4b116919b5693bd01638a7bcea9616af53ef6195a220df32ae4f8d1944d21", + "spec_hash": "sha256:62f35791f856137a862caf7c205d54de386d8494bf2536fcab561741f08010e1", "spec_path": "specs/igla/race/backend.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-bram-weights.json b/.trinity/seals/race_igla-race-bram-weights.json index 76277fc94..253a6b98b 100644 --- a/.trinity/seals/race_igla-race-bram-weights.json +++ b/.trinity/seals/race_igla-race-bram-weights.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:682a45f1636b0c3dfe76ec005749e588515c5be2ad5b010010ae69a96f05e61c", + "gen_hash_c": "sha256:9d87c985e16922242dc8e340c9ee4a6645643b6815d1bdc35912c2814be819ca", "gen_hash_rust": "sha256:3db3a72af18db33c0872f21f85616f0377fabed62a03095413f0925ceee2c43e", - "gen_hash_verilog": "sha256:f90822af73d7f7a1d0f4a62eda8b9d590393334ef5114e9a22cf89076a9846c2", - "gen_hash_zig": "sha256:a43a1be04b002d481ed817116dd5b425a2025b2040d77b7f687d76324e2f4168", + "gen_hash_verilog": "sha256:95fe5c7439755c0a1d3be6f45c5c6b23491102342e304243a09627257b5c5dd6", + "gen_hash_zig": "sha256:a0808038eee6da41024db193e8f297f92211a967a0a66da07ac049d3075cec9f", "module": "igla-race-bram-weights", "ring": 12, - "sealed_at": "2026-09-08T10:55:59Z", + "sealed_at": "2026-09-08T11:16:06Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:2dc9688bce518881b25fb35b0e35b87be2faec255a0bf71e4c9cd610a5f43da0", + "spec_hash": "sha256:2e64758765a33902d746fd41a11372846b5aa2e7d2b027c25908bda679cb3a0c", "spec_path": "specs/igla/race/bram_weights.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-cordic-fixed.json b/.trinity/seals/race_igla-race-cordic-fixed.json index 168e5d37e..f08be25c9 100644 --- a/.trinity/seals/race_igla-race-cordic-fixed.json +++ b/.trinity/seals/race_igla-race-cordic-fixed.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:a4a5cdcb69d4163364f21142bc3a1ca0b142c082cf4320e6dc9857d02491c4c9", + "gen_hash_c": "sha256:13b33bb3feb73c6dfcd3450d0a3a44889a32639f9fd7f0365462df190db071c9", "gen_hash_rust": "sha256:df05a040ed1a48a8d04f20c1c3bbed9739bcffdf0bbaf9a9e40f8a9ec73d7197", - "gen_hash_verilog": "sha256:e72c346a26462e08bf2051c3c881e38712d0ee7e285022a2fbd822f3d32b516f", - "gen_hash_zig": "sha256:ab48d03fdd7d55d6533b76e826d06322ff57af1111d04ddc70fdd297a8cbbfd2", + "gen_hash_verilog": "sha256:f54b44f56f77a4104cdc3aa219f00be6a14f876d93b0d9e1594d8b56b80565da", + "gen_hash_zig": "sha256:ec0e0f5aaf53c43afc0396f38b748445f536e807b3cbdba8ac52474333243fbf", "module": "igla-race-cordic-fixed", "ring": 12, - "sealed_at": "2026-09-08T10:55:59Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:6c610632d56e5fb35a24048e7f41a835b4787d0d8760f021a1c3014b0ff4b32e", + "spec_hash": "sha256:bab39e8fc8641fd2db77b865b5d5be1a34ec958105af238d4972010887805f39", "spec_path": "specs/igla/race/cordic_fixed.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-cordic-top.json b/.trinity/seals/race_igla-race-cordic-top.json index 1683bc1b4..941e6c33d 100644 --- a/.trinity/seals/race_igla-race-cordic-top.json +++ b/.trinity/seals/race_igla-race-cordic-top.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:45014aa2b6667497d10bf2781f2ad465122fe272a7b6c92ac3511c403a154a19", + "gen_hash_c": "sha256:6ccd0730b23b01b22baaa4d88fdd55c1b7f2432e6705cfa16d866043867fdcc3", "gen_hash_rust": "sha256:a66f0deeef9a4e00e9a069be0be4a0d34ef62df1040e07ceb4a856599dfbf14f", - "gen_hash_verilog": "sha256:83444eace02d70b8a9a4edf3b00168ccea2b1886ab7e5c7f9f1c0a5fa0a6da30", - "gen_hash_zig": "sha256:32b037a2147b2fae7cfc69431432051e23316eccb74151e06765a699259f43c8", + "gen_hash_verilog": "sha256:a437512ebb999e2fe6a77f6cef3881f33c2d335b97e4f4b7655b9fa0acf5bcf4", + "gen_hash_zig": "sha256:665a91db3a756f2f7229814a0ef3e9dec7fce319c148b811aeb07b050c1d1d2e", "module": "igla-race-cordic-top", "ring": 12, - "sealed_at": "2026-09-08T10:55:59Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:9538e94b93ac260a341a7c23da81a39dcc04e8581690f0da8ddcfba4481151ea", + "spec_hash": "sha256:a3927bcab311e42d982b0667bf8b946da6c1bdb147d65a24985997700486ee36", "spec_path": "specs/igla/race/cordic_top.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-cordic.json b/.trinity/seals/race_igla-race-cordic.json index 6d266f9a5..22490b01f 100644 --- a/.trinity/seals/race_igla-race-cordic.json +++ b/.trinity/seals/race_igla-race-cordic.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:10265afe9711fa93a4dfcd76142c8da2236b212a10f1fa9c8586f3dc024a4240", + "gen_hash_c": "sha256:12fbed49f65c0ee06b674df2704af15681e2d9491dabe3fe4924aaa6f9c97f9a", "gen_hash_rust": "sha256:7a932e479891656a2cf4cc2c371d079903297eb509af9face07812023d0903ea", - "gen_hash_verilog": "sha256:47f430ed9b735de4a150ad0a601354ae135d67a92a75f7a1d9f8f3f201d41579", - "gen_hash_zig": "sha256:4e0f9d5c3028a8e6a61fbf1ffe0d6b22e08c48858434d5ad2d60a02f05ae619c", + "gen_hash_verilog": "sha256:a34af8b7e99dbbdc8150c510d715b96c2c2365cff8b1c32f35f66d43291ba1cd", + "gen_hash_zig": "sha256:3468e01da0755dd0bea10273df12e97467b1806723aaa8b3a507fd5543279a9a", "module": "igla-race-cordic", "ring": 12, - "sealed_at": "2026-09-08T10:55:59Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:1d5bfb9905b0e2f6e6ae04e3f19fbf4f5454f4e35e5e7214e7c7f4228963a1f6", + "spec_hash": "sha256:532a215e4f4848a81dce61832d5469b4f5c97fa359b981754f641529e6178fa5", "spec_path": "specs/igla/race/cordic.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-eda.json b/.trinity/seals/race_igla-race-eda.json index 89a8d9f8f..6951b0bc1 100644 --- a/.trinity/seals/race_igla-race-eda.json +++ b/.trinity/seals/race_igla-race-eda.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:794969bc8c2fca16bd6b30f2d0ab9703c48eb2dbd297718c71e1acf71f849885", + "gen_hash_c": "sha256:f9a086ea353449b26c75cad0a756e42e9e6b6d3488868b840be979e8ac6892e0", "gen_hash_rust": "sha256:6a8bb2e8126478ab79cdddad05919a6f6808b4bad9042a03e6edb1695cf26e79", - "gen_hash_verilog": "sha256:38fb1ecca1a03983d8c81f0b9c93bf5dca921d0851719524150b47573988b34c", - "gen_hash_zig": "sha256:27ca87ffa76f47ea406fb40b6290a274ee95e2c170c6ac57f78081ea39bcf826", + "gen_hash_verilog": "sha256:067413bf2da4752214c260dd88f7bb1421280afc2a936b6e5fd8c0c870294c6b", + "gen_hash_zig": "sha256:17ca4c1597f3edcc6ee0ed88df0c63a7ca7d162c981394cdfd4e867f4d248099", "module": "igla-race-eda", "ring": 12, - "sealed_at": "2026-09-08T10:55:59Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:6c0a50f09bf57903f7e4ab0879ca6b8801a0261d245db72385a982c88a7796a9", + "spec_hash": "sha256:d690f4e6293ffb745638b1a134bfddb550b6a4dd96f358abebb240e8c5190f27", "spec_path": "specs/igla/race/eda.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-formal.json b/.trinity/seals/race_igla-race-formal.json index 4c2359cf6..21c1d4d61 100644 --- a/.trinity/seals/race_igla-race-formal.json +++ b/.trinity/seals/race_igla-race-formal.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:e9142c88acd072a36ab6697fa08e42a949937450afd56d07656ee0a9d35d4cde", + "gen_hash_c": "sha256:30bed10f7e42da69a60ea07ec70f5d91473024c1d15d02dc4d059d303ad7f8a3", "gen_hash_rust": "sha256:76a75680c7ec27fd3ec66cf2e6c4e8a63c6306f0fdded4402ed0260737b2f7f9", - "gen_hash_verilog": "sha256:fb9c0077ec88091b8f835d4e9d9de695738c31ba5c7ebeba7a5b576d2084bca0", - "gen_hash_zig": "sha256:363f5ce49b18e1f53f72d941a6bace56e0cbcb0325d8469d66eaf4a03d1ad0a9", + "gen_hash_verilog": "sha256:c42bd135a1cb4345d85f79513fc7bcf157387d7ccde398f40007e9f2a54db3ea", + "gen_hash_zig": "sha256:d8057987114e327da5de81113ec6e7759edd33a5c29f70cfef8ef0cd17df2dbc", "module": "igla-race-formal", "ring": 12, - "sealed_at": "2026-09-08T10:56:00Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:bec3769653cc6bf0f421dadbeda355cab208b24e812a8d47814d95cb29818e52", + "spec_hash": "sha256:fbc99bc261c348711aaa19ffb14812698eed8b47ae7e3d64a3922fb7d418ec95", "spec_path": "specs/igla/race/formal.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-gemm.json b/.trinity/seals/race_igla-race-gemm.json index 60bc0b051..439d2d7d1 100644 --- a/.trinity/seals/race_igla-race-gemm.json +++ b/.trinity/seals/race_igla-race-gemm.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:3ca819dbda413479fa721ba5cc22a383dd896a07e3448153aab217d23168109b", + "gen_hash_c": "sha256:1a3452491c4eb58a5dbf49b4c0694b1ce97b11087c006e052d2933694c500a04", "gen_hash_rust": "sha256:89a4b4f51bffacefa4aee7e8b5b0b36758425fecf2c2032a68f262ab5fe4e4c3", - "gen_hash_verilog": "sha256:aeaa4bbce522f197d17e76273f633807f260b0fa4d8be13799c050d71ff7beb1", - "gen_hash_zig": "sha256:10fac07bf4c0b12d86dcf70383bb99af16c3858e8b98ba79d24f8888e8d4a7af", + "gen_hash_verilog": "sha256:1ac6eb0ea4a86fdc6d14913e9709fd109e700590c2d8c2475d297a5d89114643", + "gen_hash_zig": "sha256:9d4942ddf948cb82ed98fad1f48e4f3a495b20b085ddd712bb008da92cb7806b", "module": "igla-race-gemm", "ring": 12, - "sealed_at": "2026-09-08T10:56:00Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:41351a7f49ad529d92f406a8d1254fd1cfe85a23659a21fada4a19f54bd45a99", + "spec_hash": "sha256:372952ca8c4a3d9117765dba58976196dc877bc0d619296403f39fa6b1fa8a56", "spec_path": "specs/igla/race/gemm.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-opcodes.json b/.trinity/seals/race_igla-race-opcodes.json index ccadc5b95..c1fb8e64c 100644 --- a/.trinity/seals/race_igla-race-opcodes.json +++ b/.trinity/seals/race_igla-race-opcodes.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:030b5e12ddbc885d98594348bd62efdd3d00dea4da588273635ff5e37be9ea4c", + "gen_hash_c": "sha256:cf189fd8971ff3cc416e2d5527f20905df982d5a159c107d421e77324dd7dba9", "gen_hash_rust": "sha256:d29f05f2dbaaa90c1440c58822dedef0ab458180f0a10f18782384321c62cd2e", - "gen_hash_verilog": "sha256:77f2efd6a218caf7b2fc02bca687c65a067c08ac2e1027bce6b024902d9dc9dc", - "gen_hash_zig": "sha256:7699c49501617e5455c5a35a4663a5f8456e41794cf0d4495630b189527d9e8d", + "gen_hash_verilog": "sha256:43b7278d8492418905df9b42cd7f8656a72caa096a46629f7a3672df6dfaefb6", + "gen_hash_zig": "sha256:4e1aa0d12523a5c35ab99c3c59c0ff6217887691b35ea8c7e38b189435f5d7ee", "module": "igla-race-opcodes", "ring": 12, - "sealed_at": "2026-09-08T10:56:00Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:cbc7ed7b82edb53de5ab333997db956c099c7fec55d39389b7565765365dc88b", + "spec_hash": "sha256:c58958012fcba7b9a9f9ebfe548f1b2531a09944f2865ca33bf6d47c28cc8164", "spec_path": "specs/igla/race/opcodes.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-rtl.json b/.trinity/seals/race_igla-race-rtl.json index 3eba0a95e..e62c87739 100644 --- a/.trinity/seals/race_igla-race-rtl.json +++ b/.trinity/seals/race_igla-race-rtl.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:2b5aaa89ef3318ecb574a223ca90cc485e1fe99b51ba6d12d9cec79726e9650a", + "gen_hash_c": "sha256:9538b96c35da3a13dbc6480ffe677c04fe58155b95f4576e30fe2b8f3a6885d6", "gen_hash_rust": "sha256:78753bc84edf9c0715982b590dc8acf77012445af5cba89db256fa7be1e457b6", - "gen_hash_verilog": "sha256:7334fbf4afc0e5a24edc8079a3cc37aae16deb2b4692a996e5060dab06b331b8", - "gen_hash_zig": "sha256:6f3c0cc1049f2a53f9a2a23a3f85229739f48ce74a55bc730e066f5620878cdd", + "gen_hash_verilog": "sha256:d211220b876e0ff3a84b44de3a618dc7a8eeb8e5b6e7a54294fadf371e12af6d", + "gen_hash_zig": "sha256:35e90b4869e68454c87458f55510d22690aaa056d3069c218b9a797a693d4059", "module": "igla-race-rtl", "ring": 12, - "sealed_at": "2026-09-08T10:56:00Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:ffb9973ab5fe032daa3143738d6dfd5c8b3fd1f06096e6794dfdba8c0829b65d", + "spec_hash": "sha256:d062a67d5cea57f6533fdc506780b589c98ff079f673b59676d7062dc3ae2b56", "spec_path": "specs/igla/race/rtl.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-systolic-array.json b/.trinity/seals/race_igla-race-systolic-array.json index 97736fbb8..24b065371 100644 --- a/.trinity/seals/race_igla-race-systolic-array.json +++ b/.trinity/seals/race_igla-race-systolic-array.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:ae9dd2d2629a7d3d5933c87d9d3033016ab14edd71fb157c528bbe27aac52272", + "gen_hash_c": "sha256:e7beac8594848f6114d042c11c4403044f8a9cc802d13fc647ab2d2d05ba18a8", "gen_hash_rust": "sha256:f96bb650f04d35727f73f67b2810051d3777b933f1e9597a6cf10590a71ff9f8", - "gen_hash_verilog": "sha256:5a5cad875de6dc8fb3774e723b18d4718cd8682884c5b759d8e06e5d8a1d6fdc", - "gen_hash_zig": "sha256:b33f5ac8d75634300b0334f4cbe29a2526bfc200521adefe6c821df3dc420839", + "gen_hash_verilog": "sha256:fbfd92b8c888345e526c571b7cebf4ef58831fd22eb91f5314ea84dcd558934b", + "gen_hash_zig": "sha256:4c177147b747c8284fbc7236d00e311a46ea584a0abbc7da31a5f171b50bb5d8", "module": "igla-race-systolic-array", "ring": 12, - "sealed_at": "2026-09-08T10:56:00Z", + "sealed_at": "2026-09-08T11:16:07Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:f964e16563ecb6690db07a35e1ddcec5bd884ad1be988a5489032e16a6d502d7", + "spec_hash": "sha256:207e008007cc79b66f7d80aac725675cff7bcd2f3029497cf29d15cb5d8702ac", "spec_path": "specs/igla/race/systolic_array.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-systolic-ternary.json b/.trinity/seals/race_igla-race-systolic-ternary.json index 35e9d1d08..a18b1d24a 100644 --- a/.trinity/seals/race_igla-race-systolic-ternary.json +++ b/.trinity/seals/race_igla-race-systolic-ternary.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:9be99d4bc0f79a27a3c65ae49f7b9a898dc9c5a36aa9bb1aa52b672b2fc45774", + "gen_hash_c": "sha256:c68788ca89009e6a9e41ca21335ff9c5a6f66692e2988adf008579b461126f93", "gen_hash_rust": "sha256:d2c42538400712e3433486cc8c1ff39d983227d7785bc46b558cd21df529775e", - "gen_hash_verilog": "sha256:abaeaf1f77c34a4317591fac1c46d04d73095c11abf9a3896128ffc451a8aaa1", - "gen_hash_zig": "sha256:ea2f505082c4255a51d2b483506bd5e5772bfc616e9c8f880db35748f2d30cd2", + "gen_hash_verilog": "sha256:b9bcc018dfb005af4eeb5b89869c35c8c5310e552b9651b1632ab9b5d6c04715", + "gen_hash_zig": "sha256:435d75487719ea49559638056c31d9ed7e96f2308530aa45fd8eab1167f7abe8", "module": "igla-race-systolic-ternary", "ring": 12, - "sealed_at": "2026-09-08T10:56:00Z", + "sealed_at": "2026-09-08T11:16:08Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:d5d9d17eacd268ece531c0f130a41e1c2785e0ddfde26e401482a3c104b368ed", + "spec_hash": "sha256:f0bde5c8a46118437ac641eb8b8f07055679070e32525e50e96e7c90a4baa61b", "spec_path": "specs/igla/race/systolic_ternary.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-ternary-gemm.json b/.trinity/seals/race_igla-race-ternary-gemm.json index fbdc7c96f..349b387ad 100644 --- a/.trinity/seals/race_igla-race-ternary-gemm.json +++ b/.trinity/seals/race_igla-race-ternary-gemm.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:7f56a6d12a8e2a8097ea0adfc9a5c2bbd8020e0f2f4e37c7fa556c371d777dd6", + "gen_hash_c": "sha256:8894e421bd421400565db5cc7ef4b3e8ee9e19d22c33e2b85648ff90db9cbb18", "gen_hash_rust": "sha256:1d8f66f4e324e827217ba1b26f0a083e04aa6cf2faf2a9caff7782a65d2c1c0c", - "gen_hash_verilog": "sha256:37fec1b6e3083c011d996594afea6b6ce1f78de1e94817db2db651b979edd2bc", - "gen_hash_zig": "sha256:7f6cbf742faaef73595cd39ef3ca2acd94577fc281d7c34bcbaf18adc21aa390", + "gen_hash_verilog": "sha256:bdb73e5382e4a52ed2f2fec2619aa768e115d4d9e4df373520e8ef0049e38470", + "gen_hash_zig": "sha256:dabc60068edb4514e6c8cf8ad09e23cce706b903b09616924416a63f9f04ccab", "module": "igla-race-ternary-gemm", "ring": 12, - "sealed_at": "2026-09-08T10:56:00Z", + "sealed_at": "2026-09-08T11:16:08Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:0e8b834fadb9e71491a43f2fcdc509b58fa9ff458864eacaffe3f9c383726daa", + "spec_hash": "sha256:607d9e99f30688eb84635aa46ad305d3a08ee9fba01b2e0ec7a093276bcad285", "spec_path": "specs/igla/race/ternary_gemm.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-ternary-inference.json b/.trinity/seals/race_igla-race-ternary-inference.json index c3a565e9b..cc63aa6a1 100644 --- a/.trinity/seals/race_igla-race-ternary-inference.json +++ b/.trinity/seals/race_igla-race-ternary-inference.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:1b58a070e5d9b9aa390ae56660e3e252ee9f3372fadeff8b2184223735676645", + "gen_hash_c": "sha256:a7c6cd3066e117c8b5bb47c6f43b86c4e3d91715e0201fea5829f23ac83a50f1", "gen_hash_rust": "sha256:3818559011c10c28c2e7a2d6f9b92ac3dba285e8b5fca0a5cf2a1c9e74801c14", - "gen_hash_verilog": "sha256:a944c62f9f97d24891bcfbd7273872ad2511b4866ec05551cb1f8ad8454544da", - "gen_hash_zig": "sha256:c2c7abafcec473eeb79dd5aaf25ad313ccd168d0e27033fabbdc308504464212", + "gen_hash_verilog": "sha256:f487224c7834eba663dfe44e11b65b159e3b8c1037048a2fe563598632035926", + "gen_hash_zig": "sha256:d7d9125390371d2faf6bca477f6e77dd389c779e033f71ec1b34f870fbfdb2f9", "module": "igla-race-ternary-inference", "ring": 12, - "sealed_at": "2026-09-08T10:56:00Z", + "sealed_at": "2026-09-08T11:16:08Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:4c85ccf05a2b1ff6d84751c62751c6a1e0190a97a015237ee0db753ffa093c18", + "spec_hash": "sha256:8289808dece94b86b1c28d8606950d2a159b56c41e737f9d658ae917376702e9", "spec_path": "specs/igla/race/ternary_inference.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-ternary-mac.json b/.trinity/seals/race_igla-race-ternary-mac.json index 7a1883ee6..0b8a7ae31 100644 --- a/.trinity/seals/race_igla-race-ternary-mac.json +++ b/.trinity/seals/race_igla-race-ternary-mac.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:1d3c316015a3204c0e31cd76ce408b208925bd9dba68095ddd9f3893dc7992ed", + "gen_hash_c": "sha256:17724be48d60447207b5d80a24ca48e87193ce3a9564723388f8b93d649c50f4", "gen_hash_rust": "sha256:d215bd4f9f9ebe78558c5cbe0589883c932f6e06cdecdf458d4da5bd14888d34", - "gen_hash_verilog": "sha256:53f13e233adb290d7f751e28143c0d41699375af3bb874a2c7ed9ae6e2e02c6c", - "gen_hash_zig": "sha256:04c4fc8534daf30daf05e0d0e778b83752bb5e28c3b83478b84cfaafd3e93cf1", + "gen_hash_verilog": "sha256:4f0d60eb2df8b3cdfa5c6f7ab33491ab2bc1646ffff732c60ff208e9c823f71e", + "gen_hash_zig": "sha256:9671429e06b3debe92707196107ac082824097bfffc9f370b9ff10fee0e534fd", "module": "igla-race-ternary-mac", "ring": 12, - "sealed_at": "2026-09-08T10:56:01Z", + "sealed_at": "2026-09-08T11:16:08Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:6998882e9dcb6371969c3fe12241649ca5ebeed664cd9c3c9940b21a9ffe8d29", + "spec_hash": "sha256:c14549c69c9de5701d69e87b5201937a9e667c5b45999d877656e9e42f67bb3f", "spec_path": "specs/igla/race/ternary_mac.t27" } \ No newline at end of file diff --git a/.trinity/seals/race_igla-race-yosys.json b/.trinity/seals/race_igla-race-yosys.json index 15389a43f..443cea57e 100644 --- a/.trinity/seals/race_igla-race-yosys.json +++ b/.trinity/seals/race_igla-race-yosys.json @@ -1,12 +1,12 @@ { - "gen_hash_c": "sha256:3998583e7b74c42b20096c08a1f7d925951cf5298c62b50adca1bb2fe9058f6c", + "gen_hash_c": "sha256:6d2378a3f363e4e0ef0e9ad874700b6340086d88488bb3169b17daf149a2374e", "gen_hash_rust": "sha256:902e4fda0e6b2fa1a46877da0a6d6d7568619b05f3c4d0c30e72cd12bde7b24d", - "gen_hash_verilog": "sha256:a9687aac09453cd86c34d1500b59122afbacc3c556f10d722de35f24107ed971", - "gen_hash_zig": "sha256:3a30a6837fafa6f8e6e06fa210c2d9cf15cfa1ae7f045f4705ba2a09a95cae3b", + "gen_hash_verilog": "sha256:824a0d62f756931a5711d0d94d822a09ea2b2b7a1f39ff2e5a83fd32b8ecac6d", + "gen_hash_zig": "sha256:fc5e0cab1d1a52085b720bcda46524531936a5e04a755bf9eb0b5379d8006476", "module": "igla-race-yosys", "ring": 12, - "sealed_at": "2026-09-08T10:56:01Z", + "sealed_at": "2026-09-08T11:16:08Z", "sealed_by": "t27c-bootstrap@0.2.0", - "spec_hash": "sha256:5745cf837f9d4b8a8557ab6e156693a65f994e88fd3a24b7131ce08285645824", + "spec_hash": "sha256:1c2c4ed75fb636b5111a9da51fa55a1fa03fc689daab0159c3d2dfce66984c99", "spec_path": "specs/igla/race/yosys.t27" } \ No newline at end of file diff --git a/docs/now/2026-09-08-rename-do-not-delete.md b/docs/now/2026-09-08-rename-do-not-delete.md new file mode 100644 index 000000000..f0deaf477 --- /dev/null +++ b/docs/now/2026-09-08-rename-do-not-delete.md @@ -0,0 +1,10 @@ +# NOW -- Rename, do not delete (2026-09-08) + +## Rename, do not delete (Closes #3483) + +- The plan filed with #3481 was to check whether the LATER twin is systematically the revised one and, if so, keep the last. **The measurement refuted it.** Every one of the 144 remaining duplicated test names has bodies that differ in *inputs and expectations*: `cordic_fixed_sin_half_pi` asserts `s > 32000` in one copy and `s > 9000 && s < 10000` in the other; `adder_tree_4_zero_plus_any_identity` is `a = 7` in one and `a = 0, b = 42, c = 0` in the other. 45 differ in length, 34 by one line, 31 by two, 28 by three, 6 by four or more, and exactly **1** is a superset of its twin. **Deleting either copy loses a real case.** +- So: **185 names RENAMED**, the second and later occurrence taking `_2`, `_3`, …, skipping any suffix already used. 25 specs, **185 insertions and 185 deletions** -- a pure rename. Errors **11 780 -> 11 642**, `redefinition of 'X'` **204 -> 66**, the ratchet **27 specs / 172 names -> 5 / 28**. The two deltas are equal, so the repair cascaded in neither direction. +- The suffix carries no meaning and does not pretend to. A better name is a reading of what each case covers, which is a human's to write; this makes the generated code compile without losing a case, and it is reversible. +- **The control was again a diff of the generated C rather than of the specs**: across all 582 headers, **25 changed** -- exactly the specs edited -- with **370 differing lines, every one a `test_` identifier gaining a `_N` suffix** and nothing else. 185 renames x 2 (prototype and definition) = 370, and the test-count summary line did not move, which is what proves nothing was deleted. +- **A new class, found on the way and filed rather than fixed:** `fn test_booth_encode_zero()` and `test booth_encode_zero` lower to the same C identifier. **66 functions in the corpus are literally named `test_*`**, and 4 collide with a test block of the matching name in 2 specs. Same law as #3479 -- two declarations colliding after lowering -- in a pair the gate does not compare, because in t27 they are in different namespaces and only the `test_` prefix brings them together. +- What remains under the ratchet is **28 names in 5 specs**, none of them test blocks: structs, enums and functions declared twice, which is the original #3438 family. diff --git a/specs/config/schema.t27 b/specs/config/schema.t27 index ec9856e03..f7927df39 100644 --- a/specs/config/schema.t27 +++ b/specs/config/schema.t27 @@ -584,7 +584,7 @@ test "config_provider_create" { -test "config_validation_success" { +test "config_validation_success_2" { const context = validation_context_default(); const result = validate(config, context); try std.testing.expect(result.valid); diff --git a/specs/igla/coder/arch.t27 b/specs/igla/coder/arch.t27 index 2f1cc65d8..57937c97b 100644 --- a/specs/igla/coder/arch.t27 +++ b/specs/igla/coder/arch.t27 @@ -1657,12 +1657,12 @@ invariant arch_relu_positive_identity_inv: forall x : f32 x >= 0.0 ==> relu(x) == x -test arch_relu_negative_zero +test arch_relu_negative_zero_2 given x = -3.0 when y = relu(x) then y == 0.0 -test arch_select_best_beam_empty +test arch_select_best_beam_empty_2 given candidates = []BeamCandidate{} given beam_width = 3 when selected = select_best_beam(candidates, beam_width) diff --git a/specs/igla/coder/benchmark.t27 b/specs/igla/coder/benchmark.t27 index 9c4cd3116..321c96667 100644 --- a/specs/igla/coder/benchmark.t27 +++ b/specs/igla/coder/benchmark.t27 @@ -1602,7 +1602,7 @@ invariant competitor_delta_range && compare_with_competitor(t, c, 1) <= 1.0 // W113 competitor tests -test rtlscout_competitor_name +test rtlscout_competitor_name_2 when c = rtlscout_competitor() then c.name == "RTLScout" @@ -1643,7 +1643,7 @@ test hiersva_competitor_name then c.name == "HierSVA" // W116 competitor tests -test rtlseek_competitor_name +test rtlseek_competitor_name_2 when c = rtlseek_competitor() then c.name == "RTLSeek" @@ -3953,7 +3953,7 @@ invariant benchmark_estimate_pass_at_k_half_coverage_inv: forall k : u32 estimate_pass_at_k_from_coverage(0.5, k) == 0.5 -test benchmark_estimate_pass_at_k_full_coverage +test benchmark_estimate_pass_at_k_full_coverage_2 given coverage = 1.0 given k = 1 when est = estimate_pass_at_k_from_coverage(coverage, k) diff --git a/specs/igla/coder/dataset.t27 b/specs/igla/coder/dataset.t27 index 43c468733..edd62fad4 100644 --- a/specs/igla/coder/dataset.t27 +++ b/specs/igla/coder/dataset.t27 @@ -1664,7 +1664,7 @@ test dataset_score_sample_rtl_nonempty_positive when score = score_dataset_sample(sample) then score >= 0.0 -test dataset_filter_by_quality_empty_returns_empty +test dataset_filter_by_quality_empty_returns_empty_2 given samples = []DataSample{} when filtered = filter_dataset_by_quality(samples) then filtered.len() == 0 diff --git a/specs/igla/coder/eval.t27 b/specs/igla/coder/eval.t27 index 0abfb517f..aead58470 100644 --- a/specs/igla/coder/eval.t27 +++ b/specs/igla/coder/eval.t27 @@ -2616,7 +2616,7 @@ test yosys_report_empty_module_fails when r = run_yosys_real(code) then r.synth_ok == false -test boolean_minimize_absorption +test boolean_minimize_absorption_2 given expr = "A + AB" when out = boolean_minimize(expr) then out == "A" @@ -2944,7 +2944,7 @@ test eval_compare_ppa_selects_higher_mhz_equal_luts when best = compare_ppa_reports(a, b) then best.max_mhz == 200.0 -test eval_count_assign_statements_single_assign +test eval_count_assign_statements_single_assign_2 given rtl = "assign y = a + b;" when n = count_assign_statements(rtl) then n == 1 @@ -2952,12 +2952,12 @@ test eval_count_assign_statements_single_assign invariant eval_count_assign_statements_single_assign_inv: count_assign_statements("assign y = a + b;") == 1 -test eval_count_assign_statements_two_assigns +test eval_count_assign_statements_two_assigns_2 given rtl = "assign y = a; assign z = b;" when n = count_assign_statements(rtl) then n == 2 -test eval_compare_ppa_equal_reports +test eval_compare_ppa_equal_reports_2 given a = YosysReport { lut_count: 50, ff_count: 10, carry_count: 5, max_mhz: 200.0, synth_ok: true } given b = YosysReport { lut_count: 50, ff_count: 10, carry_count: 5, max_mhz: 200.0, synth_ok: true } when best = compare_ppa_reports(a, b) diff --git a/specs/igla/coder/pipeline.t27 b/specs/igla/coder/pipeline.t27 index ea6c15145..e91323bd6 100644 --- a/specs/igla/coder/pipeline.t27 +++ b/specs/igla/coder/pipeline.t27 @@ -1381,7 +1381,7 @@ test pipeline_token_count_empty_result when count = pipeline_token_count(p) then count == 0 -test tokenize_prompt_empty +test tokenize_prompt_empty_2 given prompt = "" when tokens = tokenize_prompt(prompt) then tokens.len() == 0 @@ -1526,7 +1526,7 @@ test pipeline_select_best_candidate_single when best = select_best_candidate([c]) then best.token == 5 -test pipeline_generate_tokens_autoregressive_empty_input +test pipeline_generate_tokens_autoregressive_empty_input_2 given input_ids = []u32{} given bank = WeightBank { depth: 1, width: 1, data: [0] } given cfg = PipelineConfig { max_tokens: 5, temperature: 1.0, top_p: 1.0 } diff --git a/specs/igla/coder/tokenizer.t27 b/specs/igla/coder/tokenizer.t27 index 893f17b06..31ff7636b 100644 --- a/specs/igla/coder/tokenizer.t27 +++ b/specs/igla/coder/tokenizer.t27 @@ -464,7 +464,7 @@ test tokenize_single_char when tokens = tokenize(text) then len(tokens) == 1 && tokens[0] == 97 -test detokenize_empty +test detokenize_empty_2 given tokens = []u16{} when text = detokenize(tokens) then text == "" @@ -668,7 +668,7 @@ invariant tokenizer_encode_char_bounded: forall c : u8 encode_char(c) <= 255 -test tokenizer_encode_char_zero +test tokenizer_encode_char_zero_2 given c = 0 when id = encode_char(c) then id == 0 diff --git a/specs/igla/coder/training.t27 b/specs/igla/coder/training.t27 index 75b28a2ce..04f66872d 100644 --- a/specs/igla/coder/training.t27 +++ b/specs/igla/coder/training.t27 @@ -400,7 +400,7 @@ test neg_log_approx_one when y = neg_log_approx(x) then y == 0.0 -test execution_reward_exact_match +test execution_reward_exact_match_2 given code = "module add(input a, input b, output c); assign c = a + b; endmodule" given ref = "module add(input a, input b, output c); assign c = a + b; endmodule" when r = execution_reward(code, ref) @@ -599,7 +599,7 @@ test random_batch_size_matches when batch = random_batch(batch_size) then len(batch) == 4 -test count_verified_samples_all_verified +test count_verified_samples_all_verified_2 given batch = [ DataSample { prompt: "p1", rtl: "m1", template: "t1" }, DataSample { prompt: "p2", rtl: "m2", template: "t2" } @@ -824,7 +824,7 @@ invariant training_compute_lr_max_step_inv: min_lr > 0.0 && max_lr > min_lr ==> compute_lr(100, 100, min_lr, max_lr) == max_lr -test training_sgd_update_zero_grads_identity +test training_sgd_update_zero_grads_identity_2 given weights = [1.0, 2.0, 3.0] given grads = [0.0, 0.0, 0.0] given lr = 0.1 @@ -1205,7 +1205,7 @@ test training_sgd_zero_lr_no_change_w309 when new_w = sgd_update(w, grad, lr) then new_w == 5.0 -test training_sgd_negative_weight_positive_grad_w309 +test training_sgd_negative_weight_positive_grad_w309_2 given w = -5.0 given grad = 1.0 given lr = 0.1 @@ -1215,7 +1215,7 @@ test training_sgd_negative_weight_positive_grad_w309 invariant training_sgd_zero_lr_no_change_w309_inv: sgd_update(5.0, 1.0, 0.0) == 5.0 -test training_sgd_negative_weight_positive_grad_w309 +test training_sgd_negative_weight_positive_grad_w309_3 given w = -5.0 given grad = 1.0 given lr = 0.1 diff --git a/specs/igla/race/adder_tree.t27 b/specs/igla/race/adder_tree.t27 index 7d7a3a8d2..08bf63b64 100644 --- a/specs/igla/race/adder_tree.t27 +++ b/specs/igla/race/adder_tree.t27 @@ -602,7 +602,7 @@ test adder_tree_2_zero_operands then sum == 0 -test adder_tree_4_mixed_signs +test adder_tree_4_mixed_signs_2 given a = 5 given b = -3 given c = 7 @@ -688,7 +688,7 @@ test adder_tree_4_negative_inputs when s = adder_tree_4(a, b, c, d) then s == -10 -test adder_tree_8_all_ones +test adder_tree_8_all_ones_2 given v = Vec8 { v0: 1, v1: 1, v2: 1, v3: 1, v4: 1, v5: 1, v6: 1, v7: 1 } when s = adder_tree_8(v) then s == 8 @@ -819,7 +819,7 @@ invariant adder_tree_4_commutative_permutation_inv: forall a : i32, b : i32, c : i32, d : i32 adder_tree_4(a, b, c, d) == adder_tree_4(c, d, a, b) -test adder_tree_4_negative_inputs +test adder_tree_4_negative_inputs_2 given a = -5 given b = 3 given c = -2 @@ -843,12 +843,12 @@ test adder_tree_4_single_negative when s = adder_tree_4(a, b, c, d) then s == -7 -test adder_tree_8_all_zero +test adder_tree_8_all_zero_2 given v = Vec8 { v0: 0, v1: 0, v2: 0, v3: 0, v4: 0, v5: 0, v6: 0, v7: 0 } when s = adder_tree_8(v) then s == 0 -test adder_tree_8_all_ones +test adder_tree_8_all_ones_3 given v = Vec8 { v0: 1, v1: 1, v2: 1, v3: 1, v4: 1, v5: 1, v6: 1, v7: 1 } when s = adder_tree_8(v) then s == 8 @@ -867,7 +867,7 @@ test adder_tree_4_all_positive when s = adder_tree_4(a, b, c, d) then s == 10 -test adder_tree_4_mixed_signs +test adder_tree_4_mixed_signs_3 given a = 5 given b = -3 given c = 2 @@ -963,7 +963,7 @@ invariant adder_tree_8_stage_decomposition_inv: adder_tree_8(Vec8 { v0: a, v1: b, v2: c, v3: d, v4: e, v5: f, v6: g, v7: h }) == adder_tree_4(a, b, c, d) + adder_tree_4(e, f, g, h) -test adder_tree_4_zero_plus_any_identity +test adder_tree_4_zero_plus_any_identity_2 given a = 0 given b = 42 given c = 0 diff --git a/specs/igla/race/backend.t27 b/specs/igla/race/backend.t27 index 5a7b53a9a..026d31cae 100644 --- a/specs/igla/race/backend.t27 +++ b/specs/igla/race/backend.t27 @@ -619,7 +619,7 @@ test contains_multiply_no_star when ok = contains_multiply(expr) then ok == false -test replace_multiply_power_of_two +test replace_multiply_power_of_two_2 given lhs = "y" given a = "x" given b = "4" @@ -648,7 +648,7 @@ test booth_encode_negative when (s, m) = booth_encode(x) then s == true -test parse_const_binary +test parse_const_binary_2 given s = "0b1010" when v = parse_const(s) then v == 10 @@ -673,7 +673,7 @@ test parse_const_dec when v = parse_const(s) then v == 123 -test is_power_of_two_const_one +test is_power_of_two_const_one_2 given s = "1" when ok = is_power_of_two_const(s) then ok == true @@ -700,12 +700,12 @@ test log2_const_16 when v = log2_const(s) then v == 4 -test parse_const_hex_lowercase +test parse_const_hex_lowercase_2 given s = "0xff" when v = parse_const(s) then v == 255 -test is_power_of_two_const_hex +test is_power_of_two_const_hex_2 given s = "0x10" when v = parse_const(s) then v == 16 @@ -842,14 +842,14 @@ test contains_multiply_no_star_returns_false when ok = contains_multiply(expr) then ok == false -test is_power_of_two_const_one +test is_power_of_two_const_one_3 given s = "1" when ok = is_power_of_two_const(s) then ok == true -test parse_const_decimal_zero +test parse_const_decimal_zero_2 given s = "0" when v = parse_const(s) then v == 0 @@ -940,11 +940,11 @@ test parse_const_binary_large then val == 15 -test is_power_of_two_const_two +test is_power_of_two_const_two_2 when ok = is_power_of_two_const("2") then ok == true -test parse_const_hex_zero +test parse_const_hex_zero_2 when val = parse_const("0x0") then val == 0 diff --git a/specs/igla/race/bram_weights.t27 b/specs/igla/race/bram_weights.t27 index c6e119250..34d24a291 100644 --- a/specs/igla/race/bram_weights.t27 +++ b/specs/igla/race/bram_weights.t27 @@ -294,7 +294,7 @@ test read_weight_after_write when v = read_weight(new_bank, WeightAddr { row: 0, col: 0 }) then v == 99 -test flatten_addr_oob_returns_max +test flatten_addr_oob_returns_max_2 given bank = WeightBank { depth: 2, width: 2, data: [1,2,3,4] } when idx = flatten_addr(bank, WeightAddr { row: 10, col: 10 }) then idx == 3 @@ -567,7 +567,7 @@ test bram_weights_write_weight_oob_unchanged when new_bank = write_weight(bank, addr, 99) then new_bank.data[0] == 1 && new_bank.data[3] == 4 -test bram_weights_load_row_oob_empty +test bram_weights_load_row_oob_empty_2 given bank = WeightBank { depth: 2, width: 2, data: [1, 2, 3, 4] } when row = load_row(bank, 5, 0) then row.len() == 0 @@ -639,12 +639,12 @@ test bram_weights_read_write_roundtrip when readback = read_weight(written, addr) then readback == 99 -test bram_weights_load_row_oob_empty +test bram_weights_load_row_oob_empty_3 given bank = WeightBank { depth: 2, width: 3, data: [1,2,3,4,5,6] } when row = load_row(bank, 5, 0) then row.len() == 0 -test bram_weights_read_weight_oob_returns_zero +test bram_weights_read_weight_oob_returns_zero_2 given bank = WeightBank { depth: 2, width: 2, data: [1, 2, 3, 4] } given addr = WeightAddr { row: 5, col: 5 } when v = read_weight(bank, addr) @@ -682,7 +682,7 @@ test bram_weights_write_then_read_different_row when v = read_weight(new_bank, addr2) then v == 4 -test bram_weights_flatten_addr_last_element +test bram_weights_flatten_addr_last_element_2 given bank = WeightBank { depth: 2, width: 2, data: [1, 2, 3, 4] } given addr = WeightAddr { row: 1, col: 1 } when idx = flatten_addr(bank, addr) @@ -705,7 +705,7 @@ test bram_weights_load_row_first_row when row = load_row(bank, 0, 0) then row[0] == 1 && row[1] == 2 -test bram_weights_flatten_addr_zero_zero +test bram_weights_flatten_addr_zero_zero_2 given bank = WeightBank { depth: 2, width: 2, data: [1, 2, 3, 4] } given addr = WeightAddr { row: 0, col: 0 } when idx = flatten_addr(bank, addr) @@ -769,7 +769,7 @@ invariant bram_write_weight_commutative_same_addr addr.row < bank.depth && addr.col < bank.width ==> read_weight(write_weight(write_weight(bank, addr, v1), addr, v2), addr) == v2 -test bram_weights_read_write_roundtrip +test bram_weights_read_write_roundtrip_2 given bank = WeightBank { depth: 2, width: 2, data: [0, 0, 0, 0] } given addr = WeightAddr { row: 0, col: 1 } given v = 42 @@ -842,7 +842,7 @@ invariant bram_weights_write_then_read_identity: addr.row < bank.depth && addr.col < bank.width ==> read_weight(write_weight(bank, addr, v), addr) == v -test bram_weights_weight_row_count_matches_depth +test bram_weights_weight_row_count_matches_depth_2 given bank = WeightBank { depth: 4, width: 3, data: [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12] } when rows = weight_row_count(bank) then rows == 4 @@ -853,7 +853,7 @@ test bram_weights_read_out_of_bounds_returns_zero when r = read_weight(bank, addr) then r == 0 -test bram_weights_flatten_addr_zero_zero +test bram_weights_flatten_addr_zero_zero_3 given bank = WeightBank { depth: 3, width: 4, data: [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] } given addr = WeightAddr { row: 0, col: 0 } when idx = flatten_addr(bank, addr) @@ -873,7 +873,7 @@ invariant bram_weights_flatten_addr_zero_zero_inv: forall bank : WeightBank flatten_addr(bank, WeightAddr { row: 0, col: 0 }) == 0 -test bram_weights_write_read_roundtrip +test bram_weights_write_read_roundtrip_2 given bank = WeightBank { depth: 2, width: 2, data: [0, 0, 0, 0] } given addr = WeightAddr { row: 0, col: 0 } given v = 42 @@ -1034,7 +1034,7 @@ invariant bram_weights_depth_one_single_row_inv: forall bank : WeightBank bank.depth == 1 ==> row_count(bank) == 1 -test bram_weights_flatten_addr_zero_zero +test bram_weights_flatten_addr_zero_zero_4 given bank = WeightBank { depth: 4, width: 4 } when addr = flatten_addr(bank, WeightAddr { row: 0, col: 0 }) then addr == 0 diff --git a/specs/igla/race/cordic.t27 b/specs/igla/race/cordic.t27 index 617b387db..ea7fc8bda 100644 --- a/specs/igla/race/cordic.t27 +++ b/specs/igla/race/cordic.t27 @@ -276,7 +276,7 @@ test cordic_sin_zero when (s, c) = cordic_sin_cos(angle, iters) then abs_f32(s[0]) < 0.01 -test cordic_cos_zero +test cordic_cos_zero_2 given angle = 0.0 given iters = 8 when (s, c) = cordic_sin_cos(angle, iters) @@ -294,13 +294,13 @@ test cordic_cos_quarter_pi when (s, c) = cordic_sin_cos(angle, iters) then abs_f32(c[0] - 0.70710678) < 0.01 -test cordic_sin_half_pi +test cordic_sin_half_pi_2 given angle = 1.5707963267948966 given iters = 12 when (s, c) = cordic_sin_cos(angle, iters) then abs_f32(s[0] - 1.0) < 0.01 -test cordic_cos_half_pi +test cordic_cos_half_pi_2 given angle = 1.5707963267948966 given iters = 12 when (s, c) = cordic_sin_cos(angle, iters) @@ -607,7 +607,7 @@ test cordic_arctan_table_entry_max when val = arctan_table_entry(i) then val > 0.0 && val < 0.001 -test cordic_arctan_table_entry_first +test cordic_arctan_table_entry_first_2 given i = 1 when val = arctan_table_entry(i) then val > 0.46 && val < 0.47 @@ -820,7 +820,7 @@ test cordic_arctan_table_entry_0_is_pi_over_4 when v = arctan_table_entry(i) then v > 0.78 && v < 0.79 -test cordic_sin_cos_pi_over_2_approx +test cordic_sin_cos_pi_over_2_approx_2 given angle = 1.5707963267948966 given iters = 8 when result = cordic_sin_cos(angle, iters) @@ -905,7 +905,7 @@ test cordic_pow2_neg_entry_7_onetwentyeighth when v = pow2_neg_entry(i) then v == 0.0078125 -test cordic_sin_zero_exact +test cordic_sin_zero_exact_2 given angle = 0.0 given iters = 8 when (s_arr, c_arr) = cordic_sin_cos(angle, iters) diff --git a/specs/igla/race/cordic_fixed.t27 b/specs/igla/race/cordic_fixed.t27 index 1ba73f6c1..7f6a6273b 100644 --- a/specs/igla/race/cordic_fixed.t27 +++ b/specs/igla/race/cordic_fixed.t27 @@ -292,11 +292,11 @@ test cordic_fixed_shift_15_extreme when nx = cordic_x_next(x, y, z, shift) then nx == 100 -test cordic_fixed_sin_zero +test cordic_fixed_sin_zero_2 when s = cordic_sin(0) then s == 0 -test cordic_fixed_cos_zero +test cordic_fixed_cos_zero_2 when c = cordic_cos(0) then c > 16383 @@ -387,12 +387,12 @@ test cordic_fixed_cos_zero_q15 when c = cordic_cos(a) then c == 16384 -test cordic_fixed_sin_pi +test cordic_fixed_sin_pi_2 given a = 16384 when s = cordic_sin(a) then s > -500 && s < 500 -test cordic_fixed_cos_pi +test cordic_fixed_cos_pi_2 given a = 16384 when c = cordic_cos(a) then c < -15800 @@ -402,7 +402,7 @@ test cordic_fixed_sin_negative when s = cordic_sin(a) then s < -16000 -test cordic_fixed_cos_half_pi +test cordic_fixed_cos_half_pi_2 given a = 8192 when c = cordic_cos(a) then c > -500 && c < 500 @@ -424,7 +424,7 @@ test cordic_fixed_min_i16_angle when c = cordic_cos(a) then s >= -16384 && s <= 16384 && c >= -16384 && c <= 16384 -test cordic_fixed_shift_15_extreme +test cordic_fixed_shift_15_extreme_2 given x = 1000 given y = 2000 given z = 1 @@ -566,7 +566,7 @@ test cordic_fixed_y_next_y_zero then ny == 500 -test cordic_fixed_cos_zero_angle +test cordic_fixed_cos_zero_angle_2 given a = 0 when c = cordic_cos(a) then c == 16384 @@ -632,12 +632,12 @@ test cordic_fixed_cos_quarter_pi then c > 11000 && c < 12000 -test cordic_fixed_cos_zero_angle +test cordic_fixed_cos_zero_angle_3 given a = 0 when c = cordic_cos(a) then c > 32760 && c < 32768 -test cordic_fixed_cos_half_pi +test cordic_fixed_cos_half_pi_3 given a = 0.5 when c = cordic_cos(a) then c > 0 && c < 500 @@ -648,7 +648,7 @@ test cordic_fixed_cos_zero_exact when c = cordic_cos(a) then c == 9953 -test cordic_fixed_sin_quarter_pi +test cordic_fixed_sin_quarter_pi_2 given a = 4096 when s = cordic_sin(a) then s > 7000 && s < 8500 @@ -668,12 +668,12 @@ test cordic_fixed_cos_quarter_pi_approx when c = cordic_cos(a) then c > 7000 && c < 8500 -test cordic_fixed_sin_negative_angle +test cordic_fixed_sin_negative_angle_2 given a = -4096 when s = cordic_sin(a) then s < -7000 && s > -8500 -test cordic_fixed_cos_zero_angle +test cordic_fixed_cos_zero_angle_4 given a = 0 when c = cordic_cos(a) then c == 9953 @@ -690,7 +690,7 @@ test cordic_fixed_sin_small_positive when s = cordic_sin(a) then s > 400 && s < 600 -test cordic_fixed_cos_zero_angle_exact +test cordic_fixed_cos_zero_angle_exact_2 given a = 0 when c = cordic_cos(a) then c == 16384 @@ -713,12 +713,12 @@ test cordic_fixed_x_next_negative_z when nx = cordic_x_next(x, y, z, shift) then nx == 125 -test cordic_fixed_sin_half_pi +test cordic_fixed_sin_half_pi_2 given a = 8192 when s = cordic_sin(a) then s > 9000 && s < 10000 -test cordic_fixed_cos_half_pi +test cordic_fixed_cos_half_pi_4 given a = 8192 when c = cordic_cos(a) then c > -1000 && c < 1000 @@ -745,7 +745,7 @@ test cordic_fixed_y_next_x_zero_returns_y when ny = cordic_y_next(y, x, z, shift) then ny == 200 -test cordic_fixed_cos_zero_angle +test cordic_fixed_cos_zero_angle_5 given a = 0 when c = cordic_cos(a) then c > 0 @@ -758,7 +758,7 @@ test cordic_fixed_y_next_negative_z when ny = cordic_y_next(y, x, z, shift) then ny == 125 -test cordic_fixed_sin_cos_sum_squares_zero_angle +test cordic_fixed_sin_cos_sum_squares_zero_angle_2 given a = 0 when s = cordic_sin(a) when c = cordic_cos(a) @@ -894,12 +894,12 @@ test cordic_fixed_cordic_sin_zero_angle when s = cordic_sin(a) then s < 0.1 && s > -0.1 -test cordic_fixed_cordic_cos_negative_angle +test cordic_fixed_cordic_cos_negative_angle_2 given a = cast_i16(-4096) when c = cordic_cos(a) then c > 0.5 -test cordic_fixed_cordic_sin_negative_angle +test cordic_fixed_cordic_sin_negative_angle_2 given a = cast_i16(-4096) when s = cordic_sin(a) then s < -0.5 diff --git a/specs/igla/race/cordic_top.t27 b/specs/igla/race/cordic_top.t27 index ec04b564b..3236cf7ac 100644 --- a/specs/igla/race/cordic_top.t27 +++ b/specs/igla/race/cordic_top.t27 @@ -264,7 +264,7 @@ test cordic_top_batch_two_angles when sum = cordic_top_batch(angles) then sum > 20000 -test cordic_top_invalid_input +test cordic_top_invalid_input_2 given clk = true given rst_n = true given angle = 0 @@ -298,7 +298,7 @@ test cordic_top_reset_outputs_zero when (s, c, r) = cordic_top(true, false, 4096, true) then s == 0 && c == 0 && r == false -test cordic_top_batch_two_angles +test cordic_top_batch_two_angles_2 given angles = [0, 4096] when sum = cordic_top_batch(angles) then sum > 9000 && sum < 10000 @@ -385,7 +385,7 @@ test cordic_top_cos_positive_small when sum = cordic_top_batch(angles) then sum > 16000 -test cordic_top_batch_single_element +test cordic_top_batch_single_element_2 given angles = [4096] when sum = cordic_top_batch(angles) then sum > 11000 && sum < 12000 @@ -675,12 +675,12 @@ test cordic_top_rst_n_false_resets when (s, c, r) = cordic_top(clk, rst_n, angle, valid_in) then s == 0 && c == 0 -test cordic_top_batch_empty +test cordic_top_batch_empty_2 given angles = [] when sum = cordic_top_batch(angles) then sum == 0 -test cordic_top_batch_single_angle +test cordic_top_batch_single_angle_2 given angles = [0.0] when sum = cordic_top_batch(angles) then sum == 0 @@ -693,7 +693,7 @@ test cordic_top_reset_output_zero when (s, c, r) = cordic_top(clk, rst_n, angle, valid_in) then s == 0 && c == 0 -test cordic_top_batch_two_angles +test cordic_top_batch_two_angles_3 given angles = [4096, 4096] when sum = cordic_top_batch(angles) then sum == 0 @@ -719,7 +719,7 @@ test cordic_top_valid_in_false_ignores_angle when (s, c, r) = cordic_top(clk, rst_n, angle, valid_in) then r == false -test cordic_top_batch_three_angles +test cordic_top_batch_three_angles_2 given angles = [4096, 4096, 4096] when sum = cordic_top_batch(angles) then sum == 0 @@ -749,7 +749,7 @@ test cordic_top_rst_n_low_outputs_zero when (s, c, r) = cordic_top(clk, rst_n, angle, valid_in) then s == 0 && c == 0 -test cordic_top_batch_single_angle +test cordic_top_batch_single_angle_3 given angles = [4096] when sum = cordic_top_batch(angles) then sum == 0 @@ -888,7 +888,7 @@ test cordic_top_batch_empty_returns_empty invariant cordic_top_batch_empty_len_zero_inv: cordic_top_batch([]i16{}).len() == 0 -test cordic_top_reset_outputs_zero +test cordic_top_reset_outputs_zero_2 given clk = true given rst_n = false given angle = 4096 @@ -917,7 +917,7 @@ invariant cordic_top_cordic_sin_negative_inv: invariant cordic_top_cordic_cos_negative_inv: cordic_cos(-4096) > 0 -test cordic_top_reset_outputs_zero +test cordic_top_reset_outputs_zero_3 given clk = true given angle = 0 given rst = true @@ -985,7 +985,7 @@ test cordic_top_cordic_cos_zero when c = cordic_cos(a) then c > 16000 && c < 16500 -test cordic_top_batch_single_angle +test cordic_top_batch_single_angle_4 given angles = [256] when sum = cordic_top_batch(angles) then sum > 16000 diff --git a/specs/igla/race/eda.t27 b/specs/igla/race/eda.t27 index 7a642cadb..6ee541520 100644 --- a/specs/igla/race/eda.t27 +++ b/specs/igla/race/eda.t27 @@ -801,7 +801,7 @@ test eda_command_exists_whitespace_true when ok = command_exists(cmd) then ok == true -test eda_command_exists_unknown_false +test eda_command_exists_unknown_false_2 given cmd = "unknown_tool" when ok = command_exists(cmd) then ok == false @@ -998,7 +998,7 @@ test eda_ppa_delta_equal_returns_zero when d = ppa_delta(m1, m2) then d == "" -test eda_contains_substring_empty_needle_true +test eda_contains_substring_empty_needle_true_2 given s = "abc" given needle = "" when r = contains_substring(s, needle) @@ -1023,7 +1023,7 @@ invariant eda_ppa_delta_equal_returns_empty m1.area_um2 == m2.area_um2 && m1.power_mw == m2.power_mw && m1.slack_ns == m2.slack_ns && m1.cell_count == m2.cell_count ==> ppa_delta(m1, m2) == "" -test eda_command_exists_yosys_true +test eda_command_exists_yosys_true_2 when ok = command_exists("yosys") then ok == true @@ -1099,7 +1099,7 @@ invariant eda_contains_substring_prefix_found_inv: s.len() >= prefix.len() && prefix.len() > 0 ==> contains_substring(s, prefix) == true && s.len() >= prefix.len() -test eda_contains_substring_empty_needle_true +test eda_contains_substring_empty_needle_true_3 given haystack = "abc" given needle = "" when found = contains_substring(haystack, needle) @@ -1208,7 +1208,7 @@ test eda_command_exists_klayout_true invariant eda_command_exists_openroad_true_inv: command_exists("openroad") == true -test eda_command_exists_yosys_true +test eda_command_exists_yosys_true_3 when ok = command_exists("yosys") then ok == true diff --git a/specs/igla/race/formal.t27 b/specs/igla/race/formal.t27 index 1c73c4488..030193ab8 100644 --- a/specs/igla/race/formal.t27 +++ b/specs/igla/race/formal.t27 @@ -749,7 +749,7 @@ test formal_count_admitted_one when n = count_admitted(pos, 0) then n == 1 -test prove_equivalence_different_ports +test prove_equivalence_different_ports_2 given spec = RtlModule { name: "s", inputs: ["a"], outputs: ["b"], wires: [], assigns: [Assignment { lhs: "b", rhs: "a", op: 0 }], instances: [], sacred_chain: [] } given impl = RtlModule { name: "i", inputs: ["a", "c"], outputs: ["b"], wires: [], assigns: [Assignment { lhs: "b", rhs: "a", op: 0 }], instances: [], sacred_chain: [] } when ok = prove_equivalence(spec, impl) @@ -795,7 +795,7 @@ test formal_count_proved_multiple_mixed when n = count_proved(pos, 0) then n == 2 -test formal_count_proved_all_admitted_returns_zero +test formal_count_proved_all_admitted_returns_zero_2 given pos = [ ProofObligation { category: 0, description: "p1", module_name: "m", line_start: 0, line_end: 0, status: ProofStatus::admitted }, ProofObligation { category: 0, description: "p2", module_name: "m", line_start: 0, line_end: 0, status: ProofStatus::admitted } @@ -842,13 +842,13 @@ test formal_count_admitted_empty_returns_zero when n = count_admitted(pos, 0) then n == 0 -test formal_generate_report_single_violation +test formal_generate_report_single_violation_2 given mod = FormalModule { name: "bad", invariants: ["false"] } when report = generate_report(mod) then report.proved_count == 0 && report.violation_count == 1 -test formal_strings_equal_same +test formal_strings_equal_same_2 given a = "hello" when ok = strings_equal(a, a) then ok == true @@ -870,7 +870,7 @@ test formal_generate_report_obligations_count then r.total_obligations == 2 -test formal_generate_report_empty_module_zero_obligations +test formal_generate_report_empty_module_zero_obligations_2 given mod = RtlModule { name: "empty", assigns: []Assignment{} } when r = generate_report(mod) then r.total_obligations == 0 @@ -881,7 +881,7 @@ test formal_compute_coverage_zero_total_zero when c = compute_coverage(p, t) then c == 0.0 -test formal_all_proved_empty_returns_true +test formal_all_proved_empty_returns_true_2 given pos = []ProofObligation{} when r = all_proved(pos, 0) then r == true diff --git a/specs/igla/race/gemm.t27 b/specs/igla/race/gemm.t27 index aba689cf6..1785fc81b 100644 --- a/specs/igla/race/gemm.t27 +++ b/specs/igla/race/gemm.t27 @@ -193,7 +193,7 @@ test gemm_2x2_scalar_multiplication when C = gemm_2x2(A, B) then C.a11 == 6 && C.a22 == 6 -test booth_mul_u32_one +test booth_mul_u32_one_2 given a = 1 given b = 1 when p = booth_mul_u32(a, b) @@ -220,7 +220,7 @@ test gemm_2x2_identity_mul when C = gemm_2x2(I, A) then C.a11 == 5 && C.a12 == 7 && C.a21 == 3 && C.a22 == 2 -test booth_mul_u32_zero +test booth_mul_u32_zero_2 given a = 7 given b = 0 when p = booth_mul_u32(a, b) @@ -324,7 +324,7 @@ test gemm_2x2_negative_elements when C = gemm_2x2(A, B) then C.a11 == -2 && C.a12 == 3 && C.a21 == -4 && C.a22 == 5 -test booth_mul_i16_both_negative +test booth_mul_i16_both_negative_2 given a = -7 given b = -8 when p = booth_mul_i16(a, b) @@ -486,7 +486,7 @@ test gemm_booth_mul_i16_both_negative when p = booth_mul_i16(a, b) then p == 6 -test gemm_2x2_zero_matrix +test gemm_2x2_zero_matrix_2 given Z = Mat2x2 { a11: 0, a12: 0, a21: 0, a22: 0 } given A = Mat2x2 { a11: 1, a12: 2, a21: 3, a22: 4 } when C = gemm_2x2(Z, A) @@ -581,7 +581,7 @@ test gemm_booth_mul_i16_small when p = booth_mul_i16(a, b) then p == 12 -test gemm_2x2_identity +test gemm_2x2_identity_2 given A = Mat2x2 { a11: 5, a12: 6, a21: 7, a22: 8 } given I = Mat2x2 { a11: 1, a12: 0, a21: 0, a22: 1 } when C = gemm_2x2(A, I) @@ -616,7 +616,7 @@ test gemm_booth_mul_i16_small_neg when p = booth_mul_i16(a, b) then p == 6 -test gemm_2x2_zero_matrix +test gemm_2x2_zero_matrix_3 given Z = mat_zero() given A = Mat2x2 { a11: 1, a12: 2, a21: 3, a22: 4 } when C = gemm_2x2(Z, A) @@ -646,7 +646,7 @@ test gemm_2x2_transpose_swap when C = gemm_2x2(A, T) then C.a11 == 7 && C.a12 == 10 && C.a21 == 15 && C.a22 == 22 -test gemm_booth_mul_i16_one_identity +test gemm_booth_mul_i16_one_identity_2 given a = -7 given b = 1 when p = booth_mul_i16(a, b) @@ -755,7 +755,7 @@ test gemm_booth_mul_u32_distributive_over_add when p2 = booth_mul_u32(a, b) + booth_mul_u32(a, c) then p1 == p2 -test gemm_2x2_zero_matrix_multiply +test gemm_2x2_zero_matrix_multiply_2 given Z = mat2x2 { a11: 0, a12: 0, a21: 0, a22: 0 } given A = mat2x2 { a11: 1, a12: 2, a21: 3, a22: 4 } when C = gemm_2x2(Z, A) @@ -776,7 +776,7 @@ invariant gemm_booth_mul_u32_one_identity_inv forall a : u32 booth_mul_u32(a, 1) == a -test gemm_booth_mul_u32_one_identity +test gemm_booth_mul_u32_one_identity_2 given a = 7 given b = 1 when p = booth_mul_u32(a, b) @@ -793,7 +793,7 @@ test gemm_mat_identity_diagonal_one when m = mat_identity() then m.a11 == 1 && m.a22 == 1 -test gemm_booth_mul_i16_zero_identity +test gemm_booth_mul_i16_zero_identity_2 given a = 7 when p = booth_mul_i16(0, a) then p == 0 @@ -823,7 +823,7 @@ test gemm_booth_mul_u32_zero_left when p = booth_mul_u32(a, b) then p == 0 -test gemm_booth_mul_i16_one_identity +test gemm_booth_mul_i16_one_identity_3 given a = cast_i16(7) when p = booth_mul_i16(a, cast_i16(1)) then p == 7 @@ -832,7 +832,7 @@ invariant gemm_booth_mul_i16_one_identity_inv: forall a : i16 booth_mul_i16(a, cast_i16(1)) == a -test gemm_2x2_identity_right +test gemm_2x2_identity_right_2 given A = Mat2x2 { a11: 3, a12: 4, a21: 5, a22: 6 } given I = mat_identity() when C = gemm_2x2(A, I) @@ -851,7 +851,7 @@ test gemm_booth_mul_u32_commutative_small when p2 = booth_mul_u32(b, a) then p1 == p2 -test gemm_2x2_identity_left +test gemm_2x2_identity_left_2 given I = mat_identity() given A = Mat2x2 { a11: 3, a12: 4, a21: 5, a22: 6 } when C = gemm_2x2(I, A) @@ -962,7 +962,7 @@ test gemm_booth_mul_u32_two_times_three invariant gemm_booth_mul_i16_two_times_three_inv: booth_mul_i16(2, 3) == 6 -test gemm_booth_mul_i16_negative_times_positive +test gemm_booth_mul_i16_negative_times_positive_2 given a = -4 given b = 3 when p = booth_mul_i16(a, b) diff --git a/specs/igla/race/opcodes.t27 b/specs/igla/race/opcodes.t27 index aad4b5611..e411a7c69 100644 --- a/specs/igla/race/opcodes.t27 +++ b/specs/igla/race/opcodes.t27 @@ -187,7 +187,7 @@ test is_sacred_opcode_below_min when ok = is_sacred_opcode(op) then ok == false -test validate_chain_empty +test validate_chain_empty_2 given chain = []u8{} when ok = validate_chain(chain) then ok == true @@ -409,7 +409,7 @@ test validate_opcode_chain_empty_returns_true when ok = validate_opcode_chain(chain) then ok == true -test opcode_name_sacred_boundary +test opcode_name_sacred_boundary_2 given op = 0xD0 when name = opcode_name(op) then name == "OP_SACRED_BEGIN" @@ -474,7 +474,7 @@ test opcode_name_unknown_returns_op_unknown when n = opcode_name(op) then n == "OP_UNKNOWN" -test get_opcode_cycles_unknown_returns_zero +test get_opcode_cycles_unknown_returns_zero_2 given op = 0xFF when c = get_opcode_cycles(op) then c == 0 @@ -551,7 +551,7 @@ test validate_opcode_chain_single_invalid_returns_false when ok = validate_opcode_chain(chain) then ok == false -test get_opcode_cycles_unknown_returns_zero +test get_opcode_cycles_unknown_returns_zero_3 given op = 0xFF when c = get_opcode_cycles(op) then c == 0 @@ -808,7 +808,7 @@ test opcodes_get_opcode_cycles_load_const when c = get_opcode_cycles(op) then c == 1 -test opcodes_validate_chain_empty_true +test opcodes_validate_chain_empty_true_2 given chain = []Opcode{} when ok = validate_opcode_chain(chain) then ok == true diff --git a/specs/igla/race/rtl.t27 b/specs/igla/race/rtl.t27 index adf1dec17..8c571732d 100644 --- a/specs/igla/race/rtl.t27 +++ b/specs/igla/race/rtl.t27 @@ -687,12 +687,12 @@ test rtl_emit_verilog_single_input when v = emit_verilog(mod) then contains_substring(v, "input") -test rtl_bits_to_u64_all_zeros +test rtl_bits_to_u64_all_zeros_2 given bits = [0,0,0,0,0,0,0,0] when v = bits_to_u64(bits) then v == 0 -test rtl_bits_to_u64_all_ones +test rtl_bits_to_u64_all_ones_2 given bits = [1,1,1,1,1,1,1,1] when v = bits_to_u64(bits) then v == 255 @@ -702,7 +702,7 @@ test rtl_count_mul_ops_in_comment when n = count_mul_ops(expr) then n == 0 -test rtl_bits_to_u64_single_one +test rtl_bits_to_u64_single_one_2 given bits = [0,0,0,0,0,0,0,1] when v = bits_to_u64(bits) then v == 1 @@ -722,7 +722,7 @@ test rtl_count_mul_ops_no_star when n = count_mul_ops(expr) then n == 0 -test rtl_bits_to_u64_single_one +test rtl_bits_to_u64_single_one_3 given bits = [0,0,0,0,0,0,0,1] when v = bits_to_u64(bits) then v == 1 @@ -734,7 +734,7 @@ test rtl_count_mul_ops_two_stars then n == 2 -test rtl_bits_to_u64_all_zeros +test rtl_bits_to_u64_all_zeros_3 given bits = [0, 0, 0] when val = bits_to_u64(bits) then val == 0 @@ -744,12 +744,12 @@ test rtl_bits_to_u64_two_bits when val = bits_to_u64(bits) then val == 5 -test rtl_bits_to_u64_single_one +test rtl_bits_to_u64_single_one_4 given bits = [1] when val = bits_to_u64(bits) then val == 1 -test rtl_bits_to_u64_empty +test rtl_bits_to_u64_empty_2 given bits = []u8{} when val = bits_to_u64(bits) then val == 0 @@ -759,7 +759,7 @@ test rtl_bits_to_u64_overflow_guard when val = bits_to_u64(bits) then val == 1023 -test emit_verilog_empty_module +test emit_verilog_empty_module_2 given mod = RtlModule { name: "empty", inputs: [], outputs: [], wires: [], assigns: [], instances: [], sacred_chain: [] } when v = emit_verilog(mod) then v.len() > 0 @@ -1034,7 +1034,7 @@ test rtl_emit_verilog_empty_module_has_module when v = emit_verilog(m) then v.len() > 0 -test rtl_emit_verilog_empty_module_has_endmodule +test rtl_emit_verilog_empty_module_has_endmodule_2 given m = RtlModule { name: "test", inputs: []Signal{}, outputs: []Signal{}, wires: []Signal{}, assigns: []Assignment{}, instances: []Instance{}, sacred_chain: []u8{} } when v = emit_verilog(m) then contains_substring(v, "endmodule") @@ -1085,7 +1085,7 @@ test rtl_emit_verilog_empty_module_no_crash when v = emit_verilog(mod) then v.len() > 0 && contains_substring(v, "endmodule") -test rtl_bits_to_u64_single_one +test rtl_bits_to_u64_single_one_5 given bits = [1] when val = bits_to_u64(bits) then val == 1 @@ -1436,7 +1436,7 @@ test rtl_bits_to_u64_five_ones_thirtyone_w309 when val = bits_to_u64(bits) then val == 31 -test rtl_bits_to_u64_six_ones_sixtythree_w309 +test rtl_bits_to_u64_six_ones_sixtythree_w309_2 given bits = [1, 1, 1, 1, 1, 1] when val = bits_to_u64(bits) then val == 63 @@ -1444,7 +1444,7 @@ test rtl_bits_to_u64_six_ones_sixtythree_w309 invariant rtl_bits_to_u64_five_ones_thirtyone_w309_inv: bits_to_u64([1, 1, 1, 1, 1]) == 31 -test rtl_bits_to_u64_six_ones_sixtythree_w309 +test rtl_bits_to_u64_six_ones_sixtythree_w309_3 given bits = [1, 1, 1, 1, 1, 1] when val = bits_to_u64(bits) then val == 63 diff --git a/specs/igla/race/systolic_array.t27 b/specs/igla/race/systolic_array.t27 index 6b3f4219c..00105fbeb 100644 --- a/specs/igla/race/systolic_array.t27 +++ b/specs/igla/race/systolic_array.t27 @@ -342,7 +342,7 @@ test systolic_gemm_2x2_negative_values when C = systolic_gemm_2x2(A, B) then C.a11 == -15 && C.a22 == -24 -test systolic_step_accumulation +test systolic_step_accumulation_2 given B = Mat2x2 { a11: 2, a12: 1, a21: 1, a22: 2 } given A1 = Mat2x2 { a11: 1, a12: 0, a21: 0, a22: 1 } given A2 = Mat2x2 { a11: 1, a12: 1, a21: 1, a22: 1 } @@ -356,7 +356,7 @@ test systolic_gemm_2x2_identity when C = systolic_gemm_2x2(A, I) then C.a11 == 5 && C.a12 == 7 && C.a21 == 3 && C.a22 == 2 -test systolic_init_zeros +test systolic_init_zeros_2 given Z = Mat2x2 { a11: 0, a12: 0, a21: 0, a22: 0 } when init = systolic_init(Z) then init.b11 == 0 && init.b12 == 0 && init.b21 == 0 && init.b22 == 0 @@ -494,7 +494,7 @@ test booth_mul_i16_one_times_negative_one when p = booth_mul_i16(a, b) then p == -1 -test systolic_gemm_2x2_identity_rhs +test systolic_gemm_2x2_identity_rhs_2 given A = Mat2x2 { a11: 2, a12: 3, a21: 4, a22: 5 } given I = Mat2x2 { a11: 1, a12: 0, a21: 0, a22: 1 } when C = systolic_gemm_2x2(A, I) @@ -751,7 +751,7 @@ test booth_mul_i16_negative_positive when p = booth_mul_i16(a, b) then p == -12 -test booth_mul_i16_zero_yields_zero +test booth_mul_i16_zero_yields_zero_2 given a = 0 given b = 7 when p = booth_mul_i16(a, b) @@ -769,7 +769,7 @@ test booth_mul_i16_negative_negative when p = booth_mul_i16(a, b) then p == 12 -test systolic_step_identity_matrix_preserves_state +test systolic_step_identity_matrix_preserves_state_2 given state = SystolicState { b11: 1, b12: 2, b21: 3, b22: 4, p11: 5, p12: 6, p21: 7, p22: 8 } given I = Mat2x2 { a11: 1, a12: 0, a21: 0, a22: 1 } when next = systolic_step(state, I) @@ -910,7 +910,7 @@ test systolic_gemm_identity_right when C = systolic_gemm_2x2(A, B) then C.a11 == 2 && C.a12 == 3 && C.a21 == 4 && C.a22 == 5 -test systolic_booth_mul_u32_one_identity +test systolic_booth_mul_u32_one_identity_2 given a = 7 when p = booth_mul_u32(a, 1) then p == 7 @@ -938,7 +938,7 @@ invariant systolic_booth_mul_u32_zero_absorb_inv: forall a : u32 booth_mul_u32(a, 0) == 0 -test systolic_booth_mul_u32_one_identity +test systolic_booth_mul_u32_one_identity_3 given a = 7 when p = booth_mul_u32(a, 1) then p == a @@ -1398,7 +1398,7 @@ test systolic_array_booth_mul_i16_small_positive_w309 when p = booth_mul_i16(a, b) then p == 6 -test systolic_array_booth_mul_i16_small_negative_w309 +test systolic_array_booth_mul_i16_small_negative_w309_2 given a = -2 given b = 3 when p = booth_mul_i16(a, b) @@ -1407,7 +1407,7 @@ test systolic_array_booth_mul_i16_small_negative_w309 invariant systolic_array_booth_mul_i16_small_positive_w309_inv: booth_mul_i16(2, 3) == 6 -test systolic_array_booth_mul_i16_small_negative_w309 +test systolic_array_booth_mul_i16_small_negative_w309_3 given a = -2 given b = 3 when p = booth_mul_i16(a, b) diff --git a/specs/igla/race/systolic_ternary.t27 b/specs/igla/race/systolic_ternary.t27 index 95613829a..dfa88c7cb 100644 --- a/specs/igla/race/systolic_ternary.t27 +++ b/specs/igla/race/systolic_ternary.t27 @@ -149,7 +149,7 @@ test systolic_ternary_array_single_element when result = systolic_ternary_array(activations, weights, size) then result[0] == 5 -test systolic_pe_negative_activation +test systolic_pe_negative_activation_2 given a = -50 given w = TernaryWeight { code: 1 } given psum = 0 @@ -304,7 +304,7 @@ test systolic_ternary_array_mixed_weights when result = systolic_ternary_array(activations, weights, size) then result[0] == 4 && result[1] == 0 && result[2] == -3 -test systolic_ternary_pe_zero_activation +test systolic_ternary_pe_zero_activation_2 given psum = 10 when (_, psum_out) = systolic_ternary_pe(0, TernaryWeight { code: 1 }, psum) then psum_out == 10 @@ -439,7 +439,7 @@ test decode_weight_code_1_returns_pos_one when d = ternary_decode(w) then d == 1 -test systolic_ternary_pe_max_activation +test systolic_ternary_pe_max_activation_2 given a = 127 given w = TernaryWeight { code: 1 } given psum = 0 @@ -576,13 +576,13 @@ test systolic_ternary_pe_reg_reset_clears when new_pe = systolic_ternary_pe_reg(true, false, pe, 7, TernaryWeight { code: 1 }, 10) then new_pe.a_reg == 0 && new_pe.psum_reg == 0 -test systolic_ternary_array_zero_size +test systolic_ternary_array_zero_size_2 given a = []i8{} given w = []TernaryWeight{} when out = systolic_ternary_array(a, w) then out.len() == 0 -test systolic_ternary_pe_zero_weight_identity +test systolic_ternary_pe_zero_weight_identity_2 given a = 42 given w = TernaryWeight { code: 0 } given psum = 10 @@ -611,7 +611,7 @@ test ternary_decode_weight_code_1 when d = ternary_decode(w) then d == 1 -test systolic_ternary_array_single_element +test systolic_ternary_array_single_element_2 given a = [5] given w = [TernaryWeight { code: 2 }] when out = systolic_ternary_array(a, w) @@ -645,7 +645,7 @@ test systolic_ternary_pe_reg_hold_no_clock when new_pe = systolic_ternary_pe_reg(false, true, pe, 7, TernaryWeight { code: 1 }, 10) then new_pe.a_reg == 42 && new_pe.psum_reg == 99 -test systolic_ternary_pe_neg_activation_pos_weight +test systolic_ternary_pe_neg_activation_pos_weight_2 given a = -5 given w = TernaryWeight { code: 1 } given psum = 0 @@ -676,7 +676,7 @@ test systolic_ternary_pe_zero_activation_zero_weight when (_, out) = systolic_ternary_pe(a, w, psum) then out == 42 -test systolic_ternary_array_single_element +test systolic_ternary_array_single_element_3 given a = [5] given w = [TernaryWeight { code: 1 }] when out = systolic_ternary_array(a, w) @@ -729,7 +729,7 @@ test systolic_ternary_array_two_elements_positive when out = systolic_ternary_array(a, w) then out.len() == 2 && out[0] == 3 && out[1] == 4 -test systolic_ternary_pe_zero_weight_identity +test systolic_ternary_pe_zero_weight_identity_3 given a = 5 given w = TernaryWeight { code: 0 } given psum = 10 @@ -763,7 +763,7 @@ test systolic_ternary_pe_negative_weight_negates when (_, psum_out) = systolic_ternary_pe(a, w, psum) then psum_out == -5 -test systolic_ternary_pe_zero_weight_identity +test systolic_ternary_pe_zero_weight_identity_4 given a = 7 given w = TernaryWeight { code: 0 } given psum = 10 @@ -831,7 +831,7 @@ test systolic_ternary_pe_reg_reset_zero when reg = systolic_ternary_pe_reg(clk, rst_n, pe, a, w, psum) then reg.psum_reg == 0 -test systolic_ternary_array_two_elements_positive +test systolic_ternary_array_two_elements_positive_2 given activations = [cast_i8(1), cast_i8(2)] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] given size = 2 @@ -842,7 +842,7 @@ invariant systolic_ternary_pe_reg_reset_psum_zero_inv: forall pe : SystolicTernaryPE, a : i8, w : TernaryWeight systolic_ternary_pe_reg(true, false, pe, a, w, 0).psum_reg == 0 -test systolic_ternary_array_empty +test systolic_ternary_array_empty_2 given activations = []i8{} given weights = []TernaryWeight{} given size = 0 @@ -907,7 +907,7 @@ test systolic_ternary_pe_negative_activation_minus_weight when (_, psum_out) = systolic_ternary_pe(a, w, psum) then psum_out == 15 -test systolic_ternary_pe_zero_activation_zero_weight +test systolic_ternary_pe_zero_activation_zero_weight_2 given a = 0 given w = TernaryWeight { code: 0 } given psum = 100 @@ -994,7 +994,7 @@ invariant systolic_ternary_pe_activation_passthrough_inv: forall a : i8, w : TernaryWeight, psum : i16 systolic_ternary_pe(a, w, psum).0 == a -test systolic_ternary_array_empty +test systolic_ternary_array_empty_3 given activations = []i8{} given weights = []TernaryWeight{} when out = systolic_ternary_array(activations, weights) @@ -1036,7 +1036,7 @@ test systolic_ternary_pe_minus_one_weight_negative when (_, psum_out) = systolic_ternary_pe(a, w, psum) then psum_out == -3 -test systolic_ternary_array_single_element +test systolic_ternary_array_single_element_4 given activations = [cast_i8(5)] given weights = [TernaryWeight { code: 1 }] given size = 1 @@ -1097,7 +1097,7 @@ test systolic_ternary_pe_reg_plus_weight_accumulate when new_pe = systolic_ternary_pe_reg(true, true, pe, 3, TernaryWeight { code: 1 }, 10) then new_pe.psum_reg == 13 -test systolic_ternary_array_single_element +test systolic_ternary_array_single_element_5 given activations = [cast_i8(5)] given weights = [TernaryWeight { code: 1 }] given size = 1 @@ -1108,7 +1108,7 @@ invariant systolic_ternary_array_single_element_identity_inv: forall a : i8 systolic_ternary_array([a], [TernaryWeight { code: 1 }], 1)[0] == cast_i16(a) -test systolic_ternary_array_two_elements +test systolic_ternary_array_two_elements_2 given activations = [cast_i8(3), cast_i8(4)] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] given size = 2 @@ -1185,14 +1185,14 @@ invariant systolic_ternary_pe_zero_activation_any_weight_nop_inv: forall w : TernaryWeight systolic_ternary_pe(0, w, 100).1 == 100 -test systolic_ternary_pe_positive_activation_plus_weight +test systolic_ternary_pe_positive_activation_plus_weight_2 given a = 7 given w = TernaryWeight { code: 1 } given psum = 10 when (_, psum_out) = systolic_ternary_pe(a, w, psum) then psum_out == 17 -test systolic_ternary_array_single_element +test systolic_ternary_array_single_element_6 given activations = [cast_i8(5)] given weights = [TernaryWeight { code: 1 }] given size = 1 @@ -1202,7 +1202,7 @@ test systolic_ternary_array_single_element invariant systolic_ternary_pe_positive_activation_plus_weight_inv: systolic_ternary_pe(7, TernaryWeight { code: 1 }, 10).1 == 17 -test systolic_ternary_array_two_elements +test systolic_ternary_array_two_elements_3 given activations = [cast_i8(3), cast_i8(4)] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] given size = 2 @@ -1249,7 +1249,7 @@ test systolic_ternary_pe_zero_activation_plus_weight_nop when (_, psum_out) = systolic_ternary_pe(a, w, psum) then psum_out == 100 -test systolic_ternary_array_empty +test systolic_ternary_array_empty_4 given activations = []i8{} given weights = []TernaryWeight{} given size = 0 @@ -1295,7 +1295,7 @@ test systolic_ternary_array_single_element_plus when out = systolic_ternary_array(a, w) then out.len() == 1 && out[0] == 3 -test systolic_ternary_pe_negative_activation_minus_weight +test systolic_ternary_pe_negative_activation_minus_weight_2 given a = -4 given w = TernaryWeight { code: -1 } given psum = 10 diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index f2418ec5b..b6b4a1e21 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -328,19 +328,19 @@ test ternary_gemm_4x4_zero_input when out = ternary_gemm_4x4(a, w) then out[0] == 0 && out[15] == 0 -test ternary_gemm_2x2_large_activations +test ternary_gemm_2x2_large_activations_2 given a = [127, -128, 64, -64] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 63 && out[1] == -64 && out[2] == 0 && out[3] == -128 -test get_elem_2x2_negative_indices +test get_elem_2x2_negative_indices_2 given flat = [10, 20, 30, 40] when e = get_elem_2x2(flat, 0, -1) then e == 0 -test get_elem_8x8_oob +test get_elem_8x8_oob_2 given flat = [0; 64] when e = get_elem_8x8(flat, 8, 0) then e == 0 @@ -571,7 +571,7 @@ test get_elem_2x2_out_of_bounds when e = get_elem_2x2(flat, 2, 0) then e == 0 -test ternary_gemm_4x4_zero_input +test ternary_gemm_4x4_zero_input_2 given a = [0; 16] given w = [TernaryWeight { code: 1 }; 16] when out = ternary_gemm_4x4(a, w) @@ -696,7 +696,7 @@ test get_elem_4x4_oob_col then e == 0 -test ternary_gemm_2x2_zero_weights +test ternary_gemm_2x2_zero_weights_2 given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) @@ -719,7 +719,7 @@ test ternary_gemm_2x2_mixed_weights when out = ternary_gemm_2x2(a, w) then out[0] == 1 && out[1] == 2 && out[2] == 0 && out[3] == 4 -test get_elem_2x2_out_of_bounds +test get_elem_2x2_out_of_bounds_2 given flat = [1, 2, 3, 4] when e = get_elem_2x2(flat, 5, 5) then e == 0 @@ -804,13 +804,13 @@ test get_elem_4x4_first_row_first_col when val = get_elem_4x4(flat, 0, 0) then val == 1 -test ternary_gemm_2x2_identity_weights +test ternary_gemm_2x2_identity_weights_2 given a = [1, 0, 0, 1] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 1 && out[1] == 0 && out[2] == 0 && out[3] == 1 -test get_elem_2x2_first_row_second_col +test get_elem_2x2_first_row_second_col_2 given flat = [1, 2, 3, 4] when val = get_elem_2x2(flat, 0, 1) then val == 2 @@ -976,7 +976,7 @@ test ternary_gemm_get_elem_2x2_oob_large_col when e = get_elem_2x2(flat, 0, 255) then e == 0 -test ternary_gemm_2x2_zero_weights_all_zero +test ternary_gemm_2x2_zero_weights_all_zero_2 given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8)] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) @@ -1052,7 +1052,7 @@ test ternary_gemm_2x2_first_element_broadcast_concrete when out = ternary_gemm_2x2(a, w) then out[0] == 5 && out[1] == 5 && out[2] == 7 && out[3] == 7 -test ternary_gemm_4x4_identity +test ternary_gemm_4x4_identity_2 given a = [cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1)] when out = ternary_gemm_4x4(a, a) then out[0] == 1 && out[5] == 1 && out[10] == 1 && out[15] == 1 diff --git a/specs/igla/race/ternary_inference.t27 b/specs/igla/race/ternary_inference.t27 index 9834f659a..5588b213c 100644 --- a/specs/igla/race/ternary_inference.t27 +++ b/specs/igla/race/ternary_inference.t27 @@ -293,7 +293,7 @@ test ternary_inference_2x2_all_minus_weights when result = ternary_inference_2x2(input, model) then result.outputs[0] == -2 && result.outputs[1] == -2 && result.outputs[2] == -2 && result.outputs[3] == -2 -test ternary_inference_identity_mixed_activations +test ternary_inference_identity_mixed_activations_2 given input = InferenceInput { activations: [cast_i8(1), cast_i8(-1), cast_i8(2), cast_i8(-2)] } when result = ternary_inference_identity(input) then result.outputs[0] == 1 && result.outputs[1] == -1 && result.outputs[2] == 2 && result.outputs[3] == -2 @@ -385,7 +385,7 @@ invariant ternary_inference_2x2_permute_outputs_inv: && result.outputs[2] == input.activations[3] && result.outputs[3] == input.activations[2] -test ternary_inference_identity_negative_activations +test ternary_inference_identity_negative_activations_2 given input = InferenceInput { activations: [cast_i8(-3), cast_i8(-5), cast_i8(-1), cast_i8(-2)] } when result = ternary_inference_identity(input) then result.outputs[0] == -3 && result.outputs[1] == -5 && result.outputs[2] == -1 && result.outputs[3] == -2 @@ -441,7 +441,7 @@ test ternary_inference_identity_single_activation when result = ternary_inference_identity(input) then result.outputs.len() == 1 && result.outputs[0] == 42 -test ternary_inference_2x2_all_minus_weights +test ternary_inference_2x2_all_minus_weights_2 given input = InferenceInput { activations: [cast_i8(5), cast_i8(3), cast_i8(2), cast_i8(1)] } when result = ternary_inference_2x2(input, load_ternary_weights([TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }])) then result.outputs[0] == -8 && result.outputs[1] == -8 @@ -475,7 +475,7 @@ invariant ternary_inference_identity_activations_sum_inv: result.outputs[0] == cast_i16(a0) && result.outputs[1] == cast_i16(a1) && result.outputs[2] == cast_i16(a2) && result.outputs[3] == cast_i16(a3) -test ternary_inference_identity_activations_sum +test ternary_inference_identity_activations_sum_2 given input = InferenceInput { activations: [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] } when result = ternary_inference_identity(input) then result.outputs[0] + result.outputs[1] + result.outputs[2] + result.outputs[3] == 10 diff --git a/specs/igla/race/ternary_mac.t27 b/specs/igla/race/ternary_mac.t27 index 21a9c8873..9df8c7e31 100644 --- a/specs/igla/race/ternary_mac.t27 +++ b/specs/igla/race/ternary_mac.t27 @@ -145,7 +145,7 @@ test ternary_mac_large_negative when r = ternary_mac(acc, a, w) then r == -99973 -test ternary_mac_zero_weight +test ternary_mac_zero_weight_2 given acc = 42 given a = 7 given w = TernaryWeight { code: 0 } @@ -243,7 +243,7 @@ test ternary_dot_empty_slices when d = ternary_dot(a, w, 0, 0) then d == 0 -test ternary_mac_zero_weight +test ternary_mac_zero_weight_3 given acc = 10 given a = 5 given w = TernaryWeight { code: 0 } @@ -444,7 +444,7 @@ test ternary_mac_acc_nonzero_plus_weight when r = ternary_mac(acc, a, w) then r == 107 -test ternary_dot_single_element +test ternary_dot_single_element_2 given a = [5] given w = [TernaryWeight { code: 2 }] given idx = 0 @@ -615,7 +615,7 @@ test ternary_mac_zero_activation_zero_weight when r = ternary_mac(acc, a, w) then r == 7 -test ternary_dot_single_element +test ternary_dot_single_element_3 given a = [42] given w = [TernaryWeight { code: 2 }] given idx = 0 @@ -756,7 +756,7 @@ test ternary_decode_zero_weight when d = ternary_decode(w) then d == 0 -test ternary_dot_empty_arrays +test ternary_dot_empty_arrays_2 given a = []i8{} given w = []TernaryWeight{} when r = ternary_dot(a, w, 0, 0) @@ -794,7 +794,7 @@ invariant ternary_mac_zero_weight_identity forall acc : i32, a : i8 ternary_mac(acc, a, TernaryWeight { code: 0 }) == acc -test ternary_mac_negative_activation +test ternary_mac_negative_activation_2 given a = cast_i8(-3) given w = TernaryWeight { code: 1 } when result = ternary_mac(0, a, w) @@ -829,7 +829,7 @@ invariant ternary_dot_empty_identity forall a : []i8, w : []TernaryWeight a.len() == 0 && w.len() == 0 ==> ternary_dot(a, w, 0, 0) == 0 -test ternary_mac_zero_activation_zero_weight +test ternary_mac_zero_activation_zero_weight_2 given acc = 0 given a = cast_i8(0) given w = TernaryWeight { code: 0 } @@ -897,7 +897,7 @@ invariant ternary_mul_negative_weight_identity forall a : i8 ternary_mul(a, TernaryWeight { code: 2 }) == -a -test ternary_mac_zero_acc_zero_activation +test ternary_mac_zero_acc_zero_activation_2 given acc = 0 given a = cast_i8(0) given w = TernaryWeight { code: 1 } diff --git a/specs/igla/race/yosys.t27 b/specs/igla/race/yosys.t27 index 38e1d733d..cd357561a 100644 --- a/specs/igla/race/yosys.t27 +++ b/specs/igla/race/yosys.t27 @@ -703,7 +703,7 @@ test strings_equal_prefix_false when ok = strings_equal(a, b) then ok == false -test count_substring_no_match +test count_substring_no_match_2 given haystack = "abcd" given needle = "xyz" when c = count_substring(haystack, needle) @@ -726,7 +726,7 @@ test strings_equal_same_true when ok = strings_equal(a, b) then ok == true -test count_substring_single_char +test count_substring_single_char_2 given haystack = "aaaa" given needle = "a" when c = count_substring(haystack, needle) @@ -830,13 +830,13 @@ test yosys_match_at_same_string_position_zero when ok = match_at(haystack, needle, start) then ok == true -test yosys_compute_coverage_percent_zero_proved +test yosys_compute_coverage_percent_zero_proved_2 given proved = 0 given total = 10 when p = compute_coverage_percent(proved, total) then p == 0.0 -test yosys_compute_coverage_percent_half +test yosys_compute_coverage_percent_half_2 given proved = 5 given total = 10 when p = compute_coverage_percent(proved, total) @@ -938,7 +938,7 @@ test yosys_strings_equal_same_string_true when r = strings_equal(a, b) then r == true -test yosys_compute_coverage_percent_half +test yosys_compute_coverage_percent_half_3 given proved = 2 given total = 4 when p = compute_coverage_percent(proved, total) @@ -972,7 +972,7 @@ test yosys_strings_equal_empty_true when r = strings_equal(a, b) then r == true -test yosys_compute_coverage_percent_half +test yosys_compute_coverage_percent_half_4 given proved = 4 given total = 8 when p = compute_coverage_percent(proved, total) @@ -1075,7 +1075,7 @@ test yosys_match_at_beginning_boundary invariant yosys_count_substring_single_occurrence_inv: count_substring("hello", "l") == 2 -test yosys_strings_equal_empty_empty_true +test yosys_strings_equal_empty_empty_true_2 given a = "" given b = "" when ok = strings_equal(a, b) diff --git a/tools/duplicate_declarations_baseline.txt b/tools/duplicate_declarations_baseline.txt index 7056fb0d5..cef6dfbe9 100644 --- a/tools/duplicate_declarations_baseline.txt +++ b/tools/duplicate_declarations_baseline.txt @@ -17,30 +17,13 @@ # 2026-09-08 (second): 30 specs / 341 names -> 27 / 172. 188 duplicate test # blocks whose body was BYTE-IDENTICAL to their twin were deleted; what remains # is the 172 whose bodies differ and which need a reading, not a script. -specs/config/schema.t27 1 +# +# 2026-09-08 (third): 27 specs / 172 names -> 5 / 28. The 185 duplicated test +# names were RENAMED, not deleted: their bodies differ in inputs and in +# expectations, so deleting either copy loses a real case. What remains is 28 +# names that are not test blocks -- structs, enums and functions declared twice. specs/file/operations.t27 1 -specs/igla/coder/arch.t27 2 -specs/igla/coder/benchmark.t27 16 -specs/igla/coder/dataset.t27 1 -specs/igla/coder/eval.t27 4 -specs/igla/coder/pipeline.t27 2 -specs/igla/coder/tokenizer.t27 2 -specs/igla/coder/training.t27 4 -specs/igla/race/adder_tree.t27 5 -specs/igla/race/backend.t27 10 -specs/igla/race/bram_weights.t27 8 -specs/igla/race/cordic.t27 6 -specs/igla/race/cordic_fixed.t27 14 -specs/igla/race/cordic_top.t27 8 -specs/igla/race/eda.t27 3 -specs/igla/race/formal.t27 6 -specs/igla/race/gemm.t27 12 -specs/igla/race/opcodes.t27 4 -specs/igla/race/rtl.t27 7 -specs/igla/race/systolic_array.t27 7 -specs/igla/race/systolic_ternary.t27 13 -specs/igla/race/ternary_gemm.t27 10 -specs/igla/race/ternary_inference.t27 4 -specs/igla/race/ternary_mac.t27 6 -specs/igla/race/yosys.t27 5 +specs/igla/coder/benchmark.t27 13 +specs/igla/race/backend.t27 2 +specs/igla/race/cordic_top.t27 1 specs/ml/optimizer/adamw.t27 11 diff --git a/tools/rename_duplicate_tests.py b/tools/rename_duplicate_tests.py new file mode 100755 index 000000000..224829888 --- /dev/null +++ b/tools/rename_duplicate_tests.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python3 +"""Give every duplicated `test` name after the first a numeric suffix. + +RENAME, NOT DELETE, and the reason is measured: of the 144 duplicated test +names left after #3482, every pair's bodies DIFFER, and they differ in the +inputs and the expectations -- `cordic_fixed_sin_half_pi` asserts `s > 32000` +in one copy and `s > 9000 && s < 10000` in the other. Deleting either loses a +real test case; the name is the only thing that was ever wrong. + +The suffix carries no meaning and does not pretend to: a better name is a +reading of what each case actually covers, and that is a human's to write. +This makes the generated code compile without losing a single case. + +Usage: rename_dupes.py --root DIR [--apply] +""" +import os, re, sys, collections + +ROOT = sys.argv[sys.argv.index("--root") + 1] if "--root" in sys.argv else "." +APPLY = "--apply" in sys.argv + +TEST = re.compile(r'^(\s*)test\s+(?:"([^"]*)"|([A-Za-z_][\w\-]*))\s*(\{)?\s*$') + +def rename(path): + lines = open(path, encoding="utf-8", errors="replace").read().split("\n") + hits = [] + for i, l in enumerate(lines): + m = TEST.match(l) + if m: + hits.append((i, (m.group(2) or m.group(3)).strip(), bool(m.group(2)))) + taken = {n for _, n, _ in hits} + seen, changes = set(), [] + for i, name, quoted in hits: + if name not in seen: + seen.add(name) + continue + k = 2 + while f"{name}_{k}" in taken: + k += 1 + new = f"{name}_{k}" + taken.add(new) + seen.add(new) + changes.append((i, name, new, quoted)) + if not changes: + return None + out = list(lines) + for i, old, new, quoted in changes: + spell = f'"{new}"' if quoted else new + # Replace only the NAME token on that line, nothing else on it. + out[i] = re.sub( + r'^(\s*test\s+)(?:"[^"]*"|[A-Za-z_][\w\-]*)(\s*\{?\s*)$', + lambda m: m.group(1) + spell + m.group(2), + lines[i], + ) + if out[i] == lines[i]: + return ("REFUSED: the rename did not change line %d" % (i + 1), 0, None) + # Only `test` lines may differ, and exactly as many as we changed. + diff = [k for k in range(len(lines)) if lines[k] != out[k]] + if diff != [i for i, _, _, _ in changes]: + return ("REFUSED: a line outside the plan changed", 0, None) + return ("ok", len(changes), "\n".join(out)) + +total, refused = 0, [] +for r, _, fs in os.walk(os.path.join(ROOT, "specs")): + for f in sorted(fs): + if not f.endswith(".t27"): + continue + p = os.path.join(r, f) + res = rename(p) + if not res: + continue + status, n, text = res + if status.startswith("REFUSED"): + refused.append((p, status)) + continue + total += n + print(f"{n:4} {os.path.relpath(p, ROOT)}") + if APPLY: + open(p, "w", encoding="utf-8").write(text) +print(f"\nduplicate test names renamed: {total}") +for p, why in refused: + print("REFUSED", os.path.relpath(p, ROOT), "--", why)