diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ee09c40..fe2f350 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -77,6 +77,12 @@ jobs: select -assert-min 4 leanvm_b_mul_pulse_check*/t:$check' - name: Multiplier pulse mutual-exclusion proof on shipped RTL run: cd formal && sby -f stream_alu_mul_pulse.sby + - name: LSC-1u protocol and retained-boundary proofs + run: cd formal && sby -f lsc1u_protocol.sby + - name: LSC-1u retained-operation reachability + run: cd formal && sby -f lsc1u_reachability.sby + - name: Mutation sensitivity of retained safety and arithmetic properties + run: make formal-mutations - name: Yosys lint and synthesis run: >- yosys -p 'read_verilog -sv asic_core/rtl/gf2n_mul_bitstream.sv asic_core/rtl/gf128_mul_bitstream.sv asic_core/rtl/leanvm_b_stream_alu.sv diff --git a/.github/workflows/gds.yaml b/.github/workflows/gds.yaml new file mode 100644 index 0000000..3774aec --- /dev/null +++ b/.github/workflows/gds.yaml @@ -0,0 +1,45 @@ +name: gds + +on: + push: + workflow_dispatch: + +jobs: + gds: + runs-on: ubuntu-24.04 + steps: + - name: checkout repo + uses: actions/checkout@v6 + with: + submodules: recursive + - name: Build GDS + uses: TinyTapeout/tt-gds-action@30d38a7dfc6fda561d452b196fc822af0332ec23 # ttsky26c + with: + pdk: sky130A + + precheck: + needs: gds + runs-on: ubuntu-24.04 + steps: + - name: Run Tiny Tapeout Precheck + uses: TinyTapeout/tt-gds-action/precheck@30d38a7dfc6fda561d452b196fc822af0332ec23 # ttsky26c + + gl_test: + needs: gds + runs-on: ubuntu-24.04 + steps: + - name: checkout repo + uses: actions/checkout@v6 + with: + submodules: recursive + - name: GL test + uses: TinyTapeout/tt-gds-action/gl_test@30d38a7dfc6fda561d452b196fc822af0332ec23 # ttsky26c + + viewer: + needs: gds + runs-on: ubuntu-24.04 + permissions: + pages: write + id-token: write + steps: + - uses: TinyTapeout/tt-gds-action/viewer@30d38a7dfc6fda561d452b196fc822af0332ec23 # ttsky26c diff --git a/.github/workflows/tt-test.yaml b/.github/workflows/tt-test.yaml new file mode 100644 index 0000000..6eacc93 --- /dev/null +++ b/.github/workflows/tt-test.yaml @@ -0,0 +1,20 @@ +name: Tiny Tapeout RTL test +on: [push, workflow_dispatch] + +jobs: + test: + runs-on: ubuntu-24.04 + steps: + - name: Checkout repo + uses: actions/checkout@v6 + - name: Install iverilog + run: sudo apt-get update && sudo apt-get install -y iverilog + - name: Setup Python + uses: actions/setup-python@v6 + with: + python-version: "3.11" + - name: Install test dependencies + run: pip install -r test/requirements.txt + - name: Run Tiny Tapeout RTL test + working-directory: test + run: make diff --git a/.gitignore b/.gitignore index 3aad9b5..6d347a2 100644 --- a/.gitignore +++ b/.gitignore @@ -19,6 +19,11 @@ formal/gf128_serialize_cover/ formal/stream_alu_mul_pulse/ formal/stream_alu_mul_pulse_induction/ formal/stream_alu_mul_pulse_cover/ +formal/lsc1u_protocol_bmc/ +formal/lsc1u_protocol_cover/ +test/results.xml +test/sim_build/ +.venv/ openlane/ reports/ tools/blake3_reference/target/ diff --git a/Makefile b/Makefile index f1e6432..bd7a42b 100644 --- a/Makefile +++ b/Makefile @@ -1,6 +1,6 @@ PYTHON ?= python3 -.PHONY: check python conformance-check conformance-differential scalar-differential m2-differential host-export host-comparison design-space exact-xor interface-check consistency checksum-check smoke placeholders fpga-boundary fpga-harness fpga-detect fpga-preflight mincore-state-count sim lean formal clean package checksums +.PHONY: check python conformance-check conformance-differential scalar-differential m2-differential host-export host-comparison design-space exact-xor interface-check consistency checksum-check smoke placeholders fpga-boundary fpga-harness fpga-detect fpga-preflight mincore-state-count sim lean formal formal-mutations clean package checksums HOST_SOURCE ?= host/fixtures/assert_set_xor_mul.zkdsl HOST_ARTIFACT ?= host/fixtures/assert_set_xor_mul.program.json @@ -80,6 +80,11 @@ lean: formal: cd formal && sby -f gf8_mul.sby + cd formal && sby -f lsc1u_protocol.sby + cd formal && sby -f lsc1u_reachability.sby + +formal-mutations: + $(PYTHON) formal/check_mutations.py clean: $(MAKE) -C test clean diff --git a/README.md b/README.md index 67f2b95..9a4526b 100644 --- a/README.md +++ b/README.md @@ -28,6 +28,13 @@ the [proof-boundary matrix](docs/PROOF_BOUNDARIES.md), Frozen leanVM-b evidence remains tied to `c308034ab78619b39a59d26f3dc60e7df5b52649` and is never relabeled. +> [!IMPORTANT] +> **LSC-1µ (LSC-1 Micro) is the deliberately reduced Tiny Tapeout +> profile/sub-core of LSC-1. It is not “LSC-1/2”, LSC-2, or a second-generation +> architecture.** ASCII identifiers use `LSC-1u` / `lsc1u`. Full LSC-1 remains +> unchanged for FPGA and future larger ASIC targets. See the +> [LSC-1µ architecture contract](docs/LSC1U_ARCHITECTURE.md). + ## Layout - `asic_core/`: exact Tiny Tapeout LSC-1 RTL boundary. @@ -41,6 +48,7 @@ Frozen leanVM-b evidence remains tied to frozen-upstream Rust differential adapter. - `planning/`: machine-readable milestones and file-lane ownership. - `src/`: retained compatibility/historical MinCore and M2 sources. +- `src/lsc1u_core.sv`: profile-specific streamed LSC-1µ arithmetic kernel. Run `make check`, `make sim`, `make lean`, and `make formal` where the corresponding tools are installed. `make consistency` rejects stale active diff --git a/SHA256SUMS b/SHA256SUMS index b3f922e..51d679a 100644 --- a/SHA256SUMS +++ b/SHA256SUMS @@ -1,9 +1,11 @@ -3ab4c0298695ac927493f923d3d42015a0d413900c2b0102d10d42fc85ecf766 ./.github/workflows/ci.yml -53c8efe9491c0fb3fde6db8e79d7fed66b8d9593d92db360fb95d2adb2ed56a4 ./.gitignore +2119773e56595054a25e658cfa04cf2acd919e831db4f27cc940f862be162703 ./.github/workflows/ci.yml +5e6a29a5b46af46a1d8ebb9cb9ed4b4042d492b86c752e7aaa845dc73c164c2f ./.github/workflows/gds.yaml +dc4fd27671dc6184c8106cac4193bada03706186206784f4cd872ca183592494 ./.github/workflows/tt-test.yaml +160fb469e2232fac0b9e620106c3ca72c8fadbb34f75892f5186bc3b5a798883 ./.gitignore cfc7749b96f63bd31c3c42b5c471bf756814053e847c10f3eb003417bc523d30 ./LICENSE 6bdbfe37959e0283134042372101a8a446432eb2516e085bf7850a712720c3c5 ./MANIFEST.md -46eac72b525297a0c233bc624faa6cbcbf5e5cf106520854a765e151b6c9822a ./Makefile -5ad7fec74f48ad429f8f66411a292f75f8be9e80760071c6069d5534c43aae83 ./README.md +951f2caca90edf123f701c719b0745d08b450f63378c78d4a88456315179b493 ./Makefile +30fdeb94f91b6b8b57a05ffec53239284ec23366508bd0a5d59430cdde824d4d ./README.md de4c0f6adf6ff1356bf9d7599ab52aef93a00b50c5a77c727ec0ce036ff2d1a2 ./RESULTS.md baa38ad5792511470f4cc9d2344d46f0c7af8a365d5b5e178dca88634b288bff ./VALIDATION.txt 56f3315873ddf849b851b0fb106e9eeec7160c33d15914c6157d7fe13065b6b5 ./VERSION @@ -29,6 +31,7 @@ ac44a1838e7da255ed93835cc0de01e1751efc05f78cf9f8b8145cc963d6836a ./docs/DECISIO 5ecf1ccdc8eb9562aaee69502fab30727351290892df2483e29680149eada14f ./docs/FULL_CORE.md b989d03d5e6c7dd3c1c11bf40277da8d700463601f23c8c51787f8ac371bc596 ./docs/FULL_CORE_PROTOCOL.md 42e5b0f0b0f98d2c7c89cbc5db737b1d1f2dd02685f4f07b98ea709a7f9e7690 ./docs/HOST_RUNTIME.md +fdebab4c908e5b84d41cd83cb880e23fa68cbf14f556115f0ba19b0bad377934 ./docs/LSC1U_ARCHITECTURE.md 59832e723e7c3e52b1e23ce70fb30760b6221b5e135c54ee5556775b7cf792f3 ./docs/LSC1_PROTOCOL.md 549ecdb6797df667096e3081f26357ff3aa33de323b65aae7445f77902d017a9 ./docs/LSC1_TRANSACTION_PROTOCOL.md c41da7c4e22cc809e471da2bfcce176505db234c3b48e9c01ff20b8bcaef4b29 ./docs/M0_MANAGER.md @@ -43,8 +46,9 @@ b81b89574ed84c67b64ae7b56001bf9d03b9d66be2bed7977d8adc715481eafb ./docs/PROTOCO 6ec7c4c80628391da706725be1a2361ae8eb2ee014fb4cde6dae31c53f13e9f0 ./docs/SEMANTIC_DIFFERENCES.md 02e8a5b52b341390f008ff8bc62f5d2d982b23adb8b26cb73ef3b07dddeed807 ./docs/SOURCE_AUDIT.md 63a4e673f49e169d587cb2302547cc251add4531c62908a38dadc169eaa312d3 ./docs/STATUS.md -9c2582c40fbd9a4e2b163abed784f5a6c82b2cb3136c37a4123a0ba6584f6136 ./docs/TAPEOUT.md +12d791e2dfa543d0b2295fd2c0c388596c1a5b8f2dcbe649ba33abedcc19d82e ./docs/TAPEOUT.md 0d976224f3f8c1198e8f0c51c0f4d022bd7c6f3dfcd36653f6d82bdfe2ae36c4 ./docs/THEOREM_INVENTORY.md +67a886e53f467b63e24b850ea3ebf4f6548dd9bdf76102fb57ad2002eaf9273c ./docs/TINY_TAPEOUT_TTSKY26C.md e61e74c84bce2ec92ef18520eb134299f9341e63d3ec43cdbe0ef4879d22ba37 ./docs/ULX3S_SMOKE_AND_UART.md a08743f1a3cf4af68683cdaac5b00ca624ac875dbeef9f78614bda7297579df8 ./docs/USE_CASES.md 20aa56b3f69c28c9639e9bd16b8239f0ef511d8fded9340185814b3257e25f01 ./docs/VALIDATION.md @@ -53,14 +57,21 @@ c8dbcf0008931bfd0d6a27c00425480de54d322dd27367ae83f54f93e3382b8c ./docs/semanti 3e896ee33e3804876f6e169c872746146c1b3d773811683616986a4148b9f785 ./docs/semantics/reference/oracle.py c49a013eb503060394007d07395e625024d7c1ff0e9b177bc71e691e1a4efec8 ./docs/semantics/reference/vectors.json 961d9f2f85fe6a6e2a5f586412e03759cb94a80683959e7f0271f37f200a4f1d ./docs/upstream-clarifications/README.md -e563e1a3b9189f28388b5335b0be480856200a4e196de6f61e90b8e7ece0b5e1 ./formal/README.md -d99deb35f0ccb83779670acf8dcdece29cfa502dda4bed6d86cc84dc8f5fb836 ./formal/gf128_serialize.sby +dcacd1be08c71bc51b462f3b434a056fd1294c066b43057fcac00b5c0c0c87e5 ./formal/README.md +1486cd0794137a682e6819faaf675939378b52327ec519e2cb27a56a0d120548 ./formal/check_mutations.py +2750eec4e2ff35adda6474dda1ddea18bf84be7e59e7db9d1e42e70e7a595d40 ./formal/gf128_mul_boundary_formal.sv +45bc083098d91a1e9064acb93f52fad4a789c8d38071fdfbe3e9d6096683f431 ./formal/gf128_mul_reachability_formal.sv +e1dd15bab27d5835a88bc7054b1f457e874256cd7449d02e52f44611870563c3 ./formal/gf128_serialize.sby 9a069838244bd75c66ab3930eb944c3677ae83242f9b2cbd9866a0d6d1db3198 ./formal/gf128_serialize_formal.sv -262182a8a42eacdac94a70931e2b19e57f1c56caaa492947c30d41051612028f ./formal/gf8_mul.sby +e098dda96308bf191d46ad58c8c6b9642372a6357e581270c7535bf75966e6de ./formal/gf8_mul.sby 2daea1b47c29dfac6dee57c423816c6f64249029ee1d5d5faf895bebd982765c ./formal/gf8_mul_bounded.ys 15abdc4c23f94b7389e25487e4c4d35a13ed1565882cbe449629bcbc6a488419 ./formal/gf8_mul_bounded_boolector.sby 531723ced686badb599022ea068d4b94f1d7e00f83ed3d7b86a9f91cc59448f2 ./formal/gf8_mul_depth22_z3.sby 25a0d4fe96e4bcd910ebac0ba76be01f8924aedfa1f7e83588610f1a758baf4f ./formal/gf8_mul_formal.sv +17b0139bcce1f71fdf5d64a6ac5065168b84aabbec093ae7d21e0dcb70496946 ./formal/lsc1u_protocol.sby +86fb8eeb25a88369a839cc590270cd958f03138a0835d0bb2139c4d759a8371f ./formal/lsc1u_protocol_formal.sv +c0847d7e066bf0e400d294fbaabb49717dbbb97efc5033daed2c9d9d1a18673c ./formal/lsc1u_reachability.sby +a73a0e8fb66e95d9df074bb7270f74c0b6e2136502152e7a0300960e7bd74dba ./formal/lsc1u_reachability_formal.sv 1e6b80dd959472d00411116899097fb37c930651efe6290fda93a8f4ae5ae97e ./formal/stream_alu_mul_pulse.sby b61a1ea32d6b114093dd2679fd4fb3315dbfbb9829b8e4f739c0177f66ff1bc1 ./formal/stream_alu_mul_pulse_formal.sv 53da30df5dd375567994d2e071664456f0c90d420710817fbbb4b53d894b668a ./fpga/ulx3s/Makefile @@ -81,7 +92,7 @@ dad7d78465d3b8f339d22d79c0823e52dc587fba26272b4f6fd7ce6ed1de6201 ./fpga_harness 5afe24acc0e398a66591f66ef62fb63ca300c2f925f9de828547e7e9ea8b302e ./fpga_harness/INVENTORY.md 17cbb54c9085c6dde96caf6bf8294444339d6878d65d9aa1f5cb193705e5f2e3 ./fpga_harness/README.md a538a3b5e64df095b867eb23f77953be4ea021a5d755f45f13a7b9a8ed8e7ccb ./fpga_harness/board_detect.py -f00b4c8c96b74b20c75ebc0cd3cc042def53f39d9cf1d963435e9b2e8f96e176 ./fpga_harness/boundary_check.py +00fa44f3e6a43bc6e833031b50dcc5f228472d6ad336951448bcd8b4a924a61f ./fpga_harness/boundary_check.py ac042826f976c6e04c668613676b006743f487a463e2cd6a2ca14a5f31571502 ./fpga_harness/fixtures/ulx3s_full_visibility.json 15eafd1c269122e92939f4bded3c778b802e15c01d26001cc20a09b6d2a0fbe0 ./fpga_harness/hardware_preflight.py 7571676d26daf04b94b9fadbdbc9740568ea92439ae0830f41a7567fdbd002a7 ./fpga_harness/host/__init__.py @@ -110,7 +121,7 @@ c22e2dd6edcd014dd803fd1ea630ae063aeee86e192afd6c34b4ac81efa73daa ./host/lean_co 809335481a0314cc5231d26931bfdef14343cdae5fdf6025576ea1ab17dcac89 ./host/memory.py 451f3d686ce47b16d81de2f85d36a52231c99a1b47c261475c0cb4134a09d777 ./host/protocol.py f3b64010406928c48e879ad0ec9a539acec43971570a8a5b4ee25024a4b52502 ./host/runtime.py -effcad52a728f7c1cc4b463ea8d7bc6cc6350ddb6daf836f4adc601f714485ab ./info.yaml +f1194bbf4d72e9f2a1a0c4dffb6d0137fbd6eca56fb1cd22246ab6c74546336e ./info.yaml 68a4209dcbdcc663454d02012642fa7b5a3476a13e363982fc9236e89c27a6b7 ./lean/LeanVMBMinCore.lean c09c6cf1a82598ec2c0e5f6ecf58852c8c27554f7036f36baadf027067a55f4e ./lean/LeanVMBMinCore/Address.lean 70ce5c26e2964f9c095505c2a621e5bdc08a9379656048ef5cc6d350d9a0bf31 ./lean/LeanVMBMinCore/ByteSerialization.lean @@ -308,6 +319,7 @@ e3329b92c1baf92fa161eb36a067e2ccbe73342fe8e419c315fbadfef9729b7d ./results/ulx3 2ce193a38f1a8c96ec1cbfe2c8b7555d025944cb450859c3e09dd2cbab66a03c ./sim/__init__.py 56f95ab49ce35604c5b30cd95d142a4d630b2d503af5398b1f975ef84492b48c ./sim/cycle_model.py 3ebec652b76c20903fde598d748dbaff596cbc3f962f80ca23f30b31e1327da5 ./sim/lsc1_transaction.py +c9ab7832b0691e2221ad73dc40a581023c28cd6e7fbfe2406ae491c77cfafd0c ./sim/lsc1u_model.py 12dd1aca968efeafb9ffa7015f849607c96fb6e14ad2aa8f65938dd254ef6f49 ./sim/model.py dee5dc820b96f24d4dbd752b17aaad3c8e025d519c043dfd1ab7c46be5600245 ./sim/packet_executor_model.py 659496fd9f21edafb7c4c12500d9b623bd0ea063808dc9494053ad923102dc31 ./sim/protocol_contract.py @@ -319,25 +331,34 @@ a2fda9c21da5f3301de411060ffbb644c08c4c5e4c103e036b3834e2922ce10a ./sim/test_cyc 002325ca4bcceb7b5ec19e8b279df399661ac368b118eb160d97a6a450fe74e7 ./sim/test_host_runtime.py f1ab500117ae9d7a20a9258a32dbc7271b4d0ec5f57d3fc058ff426ba2289a40 ./sim/test_lsc1_protocol_doc.py 2c19d774213f293a361de949f7cecc99b35111cc9afe5da73bac924d02b2747d ./sim/test_lsc1_transaction.py +eeb0ad5bc4246bc3d1163393c6224bc0c045812157742031d173124d7d429299 ./sim/test_lsc1u_model.py 3e8c789984dbc6b6150881f9aa823aaaef80e4e8b90eb329e9e9e351bfbe9b06 ./sim/test_model.py b6f8a2af3bdba662f41be970f3a43ed6e5a9f4ec0cb69a11b2087b2acfa8b691 ./sim/test_packet_executor_model.py cfad76ffba1453cc8c7f76dd688d55201aa4f9b83fbd726ab77b72d201e0a62a ./sim/test_packet_frontend_rtl_differential.py c128acb44fa334177d240255f997d4e245d6a996db5938d65deca48962ebce79 ./sim/test_protocol_contract.py 8486656729b8978f8059189845dff97dad929befde94cb3cb89ad9febf08753b ./sim/test_scalar_step_oracle.py +40ea3446c5885880a4da0a59b1a2553188f2e8613f2008f843abd5273f86f544 ./src/config.json d8e83531981677f629877cbeff643e07e169f8f6e8cf3ecd7c1b0c417a79b614 ./src/gf128_mul_bitstream.sv 4aa363edd4a6b2797191599d838f3d5f81cc97aa5fc8d88f2f0050420ccf6396 ./src/gf2n_mul_bitstream.sv f3e038032b2f1c76b176651dd79b266976091f1215b7e617c194888e387ab5e5 ./src/leanvm_b_m2_scalar_controller.sv bf844b461def08fbf5b69093f95f792fd9302b26098351d192e32c76583f001b ./src/leanvm_b_stream_alu.sv +0fb39cd775beb6a76dd4ad30728937f6eabe35ee951e939f51d8d80456793087 ./src/lsc1u_core.sv e97452e6444238c80a86811f86d892a0db6e79e498d00afc638387f8656ef28c ./src/tt_um_leanvm_b_mincore.sv -a3574d9d454d7b7580d2dcdc2801013a7648c48358a3f4a90a5c876ae9791331 ./src/user_config.tcl -69cd41bda612b601228752f516472df0f3be356de2f327ce4bbaaccb588edcf7 ./test/Makefile +bd60c7c4140ad69af8fa6da8a02e5eb3be7224a6aa2d70d3c6762e3685222102 ./src/tt_um_lfglabs_lean_silicon_lsc1.sv +595b51e8411023c614163030d621dcb906d9152108874655759d8a9a0e0cdc03 ./src/tt_um_lfglabs_lsc1u.sv +a9e12c7785940b058ea8976694b79d186a82cf3a111215cd6a4dd259c029c2ec ./src/user_config.tcl +56b41ad9df61282e60ec313ba69cd4c89d5bf9f8802a8c7026eca7f748ed2b4e ./test/Makefile +258e92c9b01b56b6f1443e18b6b478af5e510ecda337a253155499951712d7af ./test/Makefile.tt 89275e550ed74ce4b6fd8dc55c7fbf92b95ff5c26cb4f5a9315e4ac1c20a0192 ./test/packet_frontend/Makefile da38796aaa0eb9785e858d9e14bdcf246790410c0b79baa349ff8afa3d14b5f4 ./test/packet_frontend/tb_lsc1_packet_frontend.sv f1bf4caf7438081d289ea48ebfcbed8f278866a664636dc810ea5e2c1b4410c3 ./test/packet_frontend/tb_lsc1_packet_vector.sv +4273151bc1544b57436ccd1af30e6428beb0291e4f9fba3307db8115ef53f60d ./test/requirements.txt d0c03fb87fe5f08fbec435d485e4dd14c96d164e90b0e8b0ed8980cf27e8c077 ./test/tb_m2_scalar_controller.sv 2ea0bf23432e7c9471b09d7dac47b1b548f37d746a8cdf1fc9bd8128cd2a8018 ./test/tb_packet_uart_bridge.sv b78b938f396ae20d1fdccde99281430778a879808e60a35788b6fe044151329c ./test/tb_stream_alu.sv 1cdfef46a813dd43f5700b5e3ed7ec0bfb07e07403c82f8ac8fa4fb4dfbd0d55 ./test/tb_uart_bridge.sv +82e3588552877cf87b22f4eb269e597d75adc0929efd01e221d45375ec28984d ./test/test_tt.py +d571f9ffc49ce4232c671d2535fa4862a4800134254230ca29daae74130147a9 ./test/tt_tb.sv e401ecd06a20a3f1e54de6e47ff6e12f61064bd2b9278517fe3d0db97933bd8a ./tools/atomic_publish.py 7894f75175f62edfd1ed33639a23d736ad6e57ddd9182e040f556502bff21a52 ./tools/blake3_reference/Cargo.lock e28e67bc3fd6dee898130648c74691ca7b8e61d1fccfa75c52d87d52fc8d9c3f ./tools/blake3_reference/Cargo.toml @@ -351,11 +372,11 @@ a1fbbcbe225a1e2edb2456f92825e7b6853f224e8d0379aa4454d298c2419919 ./tools/frozen 002cac3d59f29613e237142d4dedc33d25bac1fc11b45bec65a402c528507dc0 ./tools/generate_checksums.py 0cb6c11945cd152db661b39e7116af8cc53ed4ab02a3cd33b11938069a1ee72a ./tools/generate_conformance_corpus.py 35d18cfd8627ecd5441d7084b2c47f332320d96acff285aa557daf53a813647a ./tools/host_upstream_comparison.py -0505e646089ff7b98b528140c596a2c93a6a9238013296111f39987def68e1f5 ./tools/interface_consistency.py +37fc25a825fca61c4a2fe67ed1ccdf3bbd048ed8f02c806efd54319cc96e67b2 ./tools/interface_consistency.py 87bf0131d197add11cab19ba34e9278a16dddcc066e254ca77b3c28d46b9da4b ./tools/lean_compiler_export.py 13cda9f3b47fda14a1ea23b3e210212eacd7250ea15ffd1e1ac638ea0d5bff3a ./tools/m2_rtl_differential.py 737518912d916251885645517f2d5cabf3c786b47c71cb9f725cf3ae2c985326 ./tools/portable_build_support.py -af28d238b411fcc075bb00b09a204ed1a98c4b4c36479ab5aa6ca611928efba0 ./tools/repo_consistency.py +774f5d1a0041034cf769fcf504d91a316849ea8eb4b7843d6e54f3b830d14658 ./tools/repo_consistency.py d39b590b15a494a1e62ff7605ca3b8c8ffec122e0f10f6dce7f997fcecceef1b ./tools/rtl_state_count.py a2b4b3a985df1ecde148745dcc94684c77364cf9a4fa22735f2f4754aa0489db ./tools/source_provenance.py 77760424b9ccaea9dfca5b3ac0412cce74db801bf583f4b7d32eb6d9b80b255d ./tools/sv_smoke_check.py diff --git a/docs/LSC1U_ARCHITECTURE.md b/docs/LSC1U_ARCHITECTURE.md new file mode 100644 index 0000000..62a1453 --- /dev/null +++ b/docs/LSC1U_ARCHITECTURE.md @@ -0,0 +1,69 @@ +# LSC-1µ (LSC-1 Micro) architecture contract + +> **LSC-1µ is a deliberately reduced Tiny Tapeout profile/sub-core of LSC-1.** +> It is not “LSC-1/2”, not LSC-2, and not a second-generation architecture. +> Full LSC-1 remains unchanged for FPGA and future larger ASIC targets. +> ASCII contexts use `LSC-1u` and `lsc1u`. + +## Retained semantic boundary + +LSC-1µ accepts fixed-width byte-streamed micro-operations: + +| Opcode | Operation | Accepted payload | Response | +| --- | --- | --- | --- | +| `0x01` | GF(2¹²⁸) XOR | `A0,B0,...,A15,B15` | `A XOR B`, 16 bytes | +| `0x02` | GF(2¹²⁸) MUL | `A0..A15,B0..B15` | `A × B`, 16 bytes | +| `0x03` | SET | `V0..V15` | `V`, 16 bytes | + +All retained values use the exact LSC-1 convention: byte 0 and bit 0 are +least-significant; multiplication is in GF(2¹²⁸) modulo +`x^128 + x^7 + x^2 + x + 1` (low reduction constant `0x87`). SET is an exact +copy and XOR is bitwise. There is no weakened or alternative arithmetic. + +An unsupported opcode produces one `0xe0` response byte and asserts `FAULT` +until that byte is accepted or a new supported command is accepted. + +## Explicit exclusions and host responsibilities + +LSC-1µ does **not** implement LSC-1 packet framing, packet CRC, transaction +orchestration, instruction fetch or memory, DEREF/JUMP resolution, the BLAKE3 +service, witnesses, or commit tracking. It never claims that an arithmetic +response represents any of those omitted behaviors. The host must validate and +frame packets, check CRCs, resolve control/memory effects, call BLAKE3, manage +witnesses/commits, and decompose authorized scalar work into these micro-ops. +The canonical `asic_core/` full LSC-1 implementation is unchanged. + +## Tiny Tapeout pin protocol + +`ui_in[7:0]` is RX data and `uo_out[7:0]` is TX data. Bidirectional pins are: + +| Pin | Direction | Meaning | +| --- | --- | --- | +| `uio[0]` | input | `RX_VALID` | +| `uio[1]` | output | `RX_READY` | +| `uio[2]` | output | `TX_VALID` | +| `uio[3]` | input | `TX_READY` | +| `uio[4]` | output | `BUSY` | +| `uio[5]` | output | `FAULT` | +| `uio[6]` | reserved input | ignored | +| `uio[7]` | output | one-cycle `DONE_PULSE` | + +A byte is accepted only on a rising edge with both VALID and READY high. +Payload width is determined solely by the accepted opcode; there is no length +field, delimiter, CRC, or full-packet buffer. The producer must hold RX data +stable while stalled. TX data remains stable while `TX_VALID && !TX_READY`. +Exactly one `DONE_PULSE` is emitted when the final response byte is accepted. + +`rst_n=0` synchronously cancels partial work, clears outputs/fault, and returns +to command acceptance. When `ena=0`, all outputs and output-enables are zero, +no transfer can be accepted, and internal state is frozen. Therefore +deselect/reselect resumes the same partial operation without duplicating it. + +## Physical inclusion rule for MUL + +The real 1×1 ttsky26c attempt mapped to 1,616 cells / 17,583.1136 µm² and +stopped at 128.237% global-placement utilization. Local hierarchy attributes +1,027 of 1,433 generic cells and 256 of 283 flops to MUL. The smallest +follow-up is therefore 1×2. MUL remains only if real placement and routing +succeeds; if it still prevents routing it will be removed, and SET/XOR +semantics will not be altered to make room. diff --git a/docs/TAPEOUT.md b/docs/TAPEOUT.md index c01931b..8d7d8f7 100644 --- a/docs/TAPEOUT.md +++ b/docs/TAPEOUT.md @@ -1,11 +1,9 @@ # Tiny Tapeout target -The target top is `lean_silicon_lsc1` in `asic_core/rtl`, listed by -`info.yaml`. It has only the standard Tiny Tapeout `ui_in[7:0]`, -`uo_out[7:0]`, and `uio[7:0]` interface. uio transports byte ready/valid, -busy/fault, abort, and done as specified in [LSC1_PROTOCOL](LSC1_PROTOCOL.md). +The ttsky26c integration top is `tt_um_lfglabs_lean_silicon_lsc1` in `src/`. +It is a thin wrapper around the unchanged `lean_silicon_lsc1` boundary in +`asic_core/rtl`. See [TINY_TAPEOUT_TTSKY26C](TINY_TAPEOUT_TTSKY26C.md) for the +complete pin map, workflow, source boundary, and limitations. -Use the official flow only after the v1 packet executor is complete and -differentially validated. No LSC-1 PPA/tapeout-fit result exists yet. The -ULX3S is a pin-accurate debug harness; it must not introduce a wide internal -ASIC bypass. +No LSC-1 PPA or routed tile-fit result exists yet. The ULX3S remains a separate +pin-accurate debug harness and is not included in the Tiny Tapeout source list. diff --git a/docs/TINY_TAPEOUT_TTSKY26C.md b/docs/TINY_TAPEOUT_TTSKY26C.md new file mode 100644 index 0000000..56f2357 --- /dev/null +++ b/docs/TINY_TAPEOUT_TTSKY26C.md @@ -0,0 +1,53 @@ +# Tiny Tapeout ttsky26c: LSC-1µ + +> **LSC-1µ (LSC-1 Micro) is a reduced Tiny Tapeout profile/sub-core of +> LSC-1—not “LSC-1/2”, LSC-2, or a second-generation architecture.** ASCII +> filenames, modules, identifiers, and URLs use `LSC-1u` / `lsc1u`. + +The normative retained/excluded boundary and pin protocol are in +[LSC1U_ARCHITECTURE.md](LSC1U_ARCHITECTURE.md). Full LSC-1 in `asic_core/` +remains unchanged for FPGA and future larger ASIC targets. Tiny Tapeout builds +the thin `tt_um_lfglabs_lsc1u` top and profile-specific `lsc1u_core`. + +## Evidence-driven reduction + +The previous full-LSC-1 canary at commit +`ba954bcd0e6dbf101eba119d3234a80b12d9113e` used the maximum 8×4 macro. Yosys +mapped 32,551 cells with total standard-cell area 367,825.2736 µm², including +5,474 flops occupying 116,434.1696 µm². LibreLane then stopped with +`[DPL-0036] Detailed placement failed`; precheck and gate-level test were +skipped. That is a physical failure, not merely an RTL estimate. + +The initial LSC-1µ 1×1 candidate synthesized in the real ttsky26c flow to +1,616 mapped Sky130 cells and 17,583.1136 µm², including 283 flops occupying +6,019.5232 µm². Its 16,493.3 µm² core area was too small: floorplan instance +utilization was 106.607%, and global placement reported 128.237% after its +pin-density adjustment (`GPL-0301`). Precheck and gate-level test were skipped. + +The preceding local hierarchy synthesized to 1,433 generic cells. It attributed +1,027 cells and 256 flops to the serial multiplier; the wrapper plus +protocol/SET/XOR control used 406 cells and 27 flops. Since the mapped 1×1 +design is only 28.237 percentage points over the global-placement limit, 1×2 is +the smallest evidence-based follow-up. MUL remains for that attempt. If 1×2 +still cannot route, the next candidate removes the measured multiplier block +while leaving SET/XOR semantics intact. + +The first 1×2 run completed GDS and passed precheck with MUL retained. Its +gate-level job stopped during testbench elaboration because Icarus 13 requires +the bidirectional `VPWR`/`VGND` ports to connect to nets rather than literals; +this is a testbench integration defect, not a circuit mismatch. The wrapper +now uses `supply1`/`supply0` nets for that check. The optional viewer rendered +and uploaded its artifact but could not deploy it because GitHub Pages is not +enabled (HTTP 404); that repository setting is unrelated to physical signoff. +The subsequent GL run elaborated but showed that the test helper's 1 ps +post-edge sample preceded the netlist's configured 1 ns unit delays. The common +sample guard is now 2 ns, still safely within the 40 ns clock period. + +## Flow and claim boundary + +The workflow pins `TinyTapeout/tt-gds-action` to +`30d38a7dfc6fda561d452b196fc822af0332ec23`. Local RTL simulation, oracle +differential tests, lint, synthesis, and formal checks do not establish a +tapeout result. A physical success claim requires the real `gds`, `precheck`, +and `gl_test` jobs to pass and their area, utilization, timing, and routing +reports to be inspected. diff --git a/formal/README.md b/formal/README.md index f99def7..d023797 100644 --- a/formal/README.md +++ b/formal/README.md @@ -9,6 +9,38 @@ them proves the full LSC-1 controller or ISA correspondence. See | `gf8_mul.sby` | GF(2^8) product of the generic multiplier at WIDTH=8 | bounded BMC | | `gf128_serialize.sby` | WIDTH=128 16-beat little-endian byte load and result shift-out ordering | BMC + k-induction + cover | | `stream_alu_mul_pulse.sby` | `mul_a_valid`/`mul_bit_valid`/`mul_result_shift` are mutually exclusive in the shipped `leanvm_b_stream_alu` FSM | k-induction + cover | +| `lsc1u_protocol.sby` | LSC-1u clamp/reset/stall/completion/framing plus retained XOR/SET bytes | unbounded PDR | +| `lsc1u_reachability.sby` | Independent completion witnesses for XOR, MUL, SET, and fault response | bounded cover per opcode | + +## LSC-1u retained boundary + +`lsc1u_protocol.sby` deliberately does not elaborate the concrete 256-bit +multiplier state. It links `lsc1u_core` against +`gf128_mul_boundary_formal.sv`, whose result is unconstrained. This is a +conservative over-approximation for these properties: the core never branches +on the result, MUL data arithmetic is not asserted here, and every concrete +multiplier output is among the values considered by the boundary model. +Concrete arithmetic and serialization remain checked by `gf8_mul.sby` and +`gf128_serialize.sby`. + +The safety run uses ABC PDR and proves all ten assertions for unbounded +reachable execution. Reachability is a separate four-task config so a deep +MUL witness (completion at depth 178) cannot force every safety property +through the same incremental SMT-BMC. The reachability harness drives a legal, +always-ready retained-boundary transaction; its constant multiplier result is +only a witness choice because control is result-independent. + +Run: + +```sh +sby -f lsc1u_protocol.sby +sby -f lsc1u_reachability.sby +python3 check_mutations.py +``` + +`check_mutations.py` works only in temporary copies. It requires terminal +counterexamples for broken stall stability, enable clamping, XOR data, SET +data, generic multiplier arithmetic, and WIDTH=128 result serialization. ## GF(2^8) product check @@ -137,8 +169,8 @@ the ALU's opcode decode, its result values, or the full controller. ## Non-vacuity -All three new properties were mutation-tested; each mutation was reverted after -the run and none is present in the tree: +The earlier properties were mutation-tested as follows; each mutation was +reverted after the run and none is present in the tree: | Mutation | Expected | Observed | |---|---|---| diff --git a/formal/check_mutations.py b/formal/check_mutations.py new file mode 100644 index 0000000..70d8552 --- /dev/null +++ b/formal/check_mutations.py @@ -0,0 +1,105 @@ +#!/usr/bin/env python3 +"""Require retained LSC-1u formal checks to reject representative RTL faults.""" + +from __future__ import annotations + +import shutil +import subprocess +import tempfile +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] + +MUTATIONS = [ + ( + "stall_stability", + "src/lsc1u_core.sv", + "assign tx_data = out_byte;", + "assign tx_data = out_byte ^ {8{!tx_ready}};", + ["lsc1u_protocol.sby"], + ), + ( + "enable_clamp", + "src/lsc1u_core.sv", + "assign tx_valid = ena && out_valid;", + "assign tx_valid = out_valid;", + ["lsc1u_protocol.sby"], + ), + ( + "xor_result", + "src/lsc1u_core.sv", + "out_byte <= saved_byte ^ rx_data;", + "out_byte <= saved_byte + rx_data;", + ["lsc1u_protocol.sby"], + ), + ( + "set_result", + "src/lsc1u_core.sv", + "out_byte <= rx_data;\n out_valid <= 1'b1;", + "out_byte <= rx_data ^ 8'h01;\n out_valid <= 1'b1;", + ["lsc1u_protocol.sby"], + ), + ( + "mul_arithmetic", + "asic_core/rtl/gf2n_mul_bitstream.sv", + "wire [WIDTH-1:0] accumulator_next = accumulator ^ selected;", + "wire [WIDTH-1:0] accumulator_next = accumulator | selected;", + ["gf8_mul.sby"], + ), + ( + "mul_serialization", + "asic_core/rtl/gf2n_mul_bitstream.sv", + "assign result_byte = accumulator[BYTE_BITS-1:0];", + "assign result_byte = accumulator[WIDTH-1 -: BYTE_BITS];", + ["gf128_serialize.sby"], + ), +] + + +def main() -> int: + sby = shutil.which("sby") + if not sby: + raise SystemExit("sby is required") + + failures: list[str] = [] + for name, relative, old, new, configs in MUTATIONS: + with tempfile.TemporaryDirectory(prefix=f"lsc1u-{name}-") as raw: + work = Path(raw) + shutil.copytree(ROOT / "formal", work / "formal") + shutil.copytree(ROOT / "src", work / "src") + shutil.copytree(ROOT / "asic_core", work / "asic_core") + target = work / relative + text = target.read_text() + if text.count(old) != 1: + failures.append(f"{name}: mutation anchor count was {text.count(old)}") + continue + target.write_text(text.replace(old, new)) + + for config in configs: + result = subprocess.run( + [sby, "-f", config], + cwd=work / "formal", + text=True, + stdout=subprocess.PIPE, + stderr=subprocess.STDOUT, + timeout=180, + ) + output = result.stdout + rejected = result.returncode != 0 and "DONE (FAIL" in output + print( + f"{name}: config={config} exit={result.returncode} " + f"mutation_rejected={str(rejected).lower()}" + ) + if not rejected: + print(output[-4000:]) + failures.append(f"{name}: {config} did not terminal-FAIL") + + if failures: + for failure in failures: + print(f"ERROR: {failure}") + return 1 + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/formal/gf128_mul_boundary_formal.sv b/formal/gf128_mul_boundary_formal.sv new file mode 100644 index 0000000..61a05fb --- /dev/null +++ b/formal/gf128_mul_boundary_formal.sv @@ -0,0 +1,29 @@ +/* + * Conservative formal boundary for lsc1u_core protocol proofs. + * + * The concrete GF(2^128) implementation is proved separately by + * gf128_serialize.sby and the exhaustive generic-arithmetic check in + * gf8_mul.sby. None of the LSC-1u control/framing assertions depends on the + * multiplier result value, so leaving it unconstrained removes irrelevant + * 256-bit datapath state while considering strictly more output behaviours. + */ +`default_nettype none + +module gf128_mul_bitstream ( + input wire clk, + input wire rst_n, + input wire abort, + input wire a_valid, + input wire [7:0] a_byte, + input wire a_last, + input wire bit_valid, + input wire bit_value, + input wire bit_last, + input wire result_shift, + output wire [7:0] result_byte +); + (* anyseq *) wire [7:0] unconstrained_result; + assign result_byte = unconstrained_result; +endmodule + +`default_nettype wire diff --git a/formal/gf128_mul_reachability_formal.sv b/formal/gf128_mul_reachability_formal.sv new file mode 100644 index 0000000..fbbf726 --- /dev/null +++ b/formal/gf128_mul_reachability_formal.sv @@ -0,0 +1,14 @@ +`default_nettype none + +// A concrete multiplier-result witness is sufficient for control reachability: +// lsc1u_core never branches on result_byte. +module gf128_mul_bitstream ( + input wire clk, rst_n, abort, a_valid, a_last, + input wire [7:0] a_byte, + input wire bit_valid, bit_value, bit_last, result_shift, + output wire [7:0] result_byte +); + assign result_byte = 8'h00; +endmodule + +`default_nettype wire diff --git a/formal/gf128_serialize.sby b/formal/gf128_serialize.sby index 303a9d1..e89c88c 100644 --- a/formal/gf128_serialize.sby +++ b/formal/gf128_serialize.sby @@ -14,6 +14,7 @@ cover: mode cover cover: depth 80 multiclock on timeout 900 +vcd off [engines] bmc: smtbmc yices diff --git a/formal/gf8_mul.sby b/formal/gf8_mul.sby index c83fecc..0922da6 100644 --- a/formal/gf8_mul.sby +++ b/formal/gf8_mul.sby @@ -3,6 +3,7 @@ mode bmc depth 32 multiclock on timeout 45 +vcd off [engines] abc bmc3 diff --git a/formal/lsc1u_protocol.sby b/formal/lsc1u_protocol.sby new file mode 100644 index 0000000..ed85f36 --- /dev/null +++ b/formal/lsc1u_protocol.sby @@ -0,0 +1,26 @@ +[tasks] +protocol + +[options] +protocol: mode prove +protocol: depth 32 +timeout 300 +vcd off + +[engines] +protocol: abc pdr + +[script] +read -formal -sv gf128_mul_boundary_formal.sv +read -formal -sv lsc1u_core.sv +read -formal -sv lsc1u_protocol_formal.sv +# Protocol and retained-boundary properties do not depend on the multiplier's +# internal arithmetic state. Replace only that independently-proved boundary +# with an unconstrained output: this is a conservative over-approximation, not +# an assumption about its result. +prep -top lsc1u_protocol_formal + +[files] +gf128_mul_boundary_formal.sv +../src/lsc1u_core.sv +lsc1u_protocol_formal.sv diff --git a/formal/lsc1u_protocol_formal.sv b/formal/lsc1u_protocol_formal.sv new file mode 100644 index 0000000..c23fe7f --- /dev/null +++ b/formal/lsc1u_protocol_formal.sv @@ -0,0 +1,115 @@ +`default_nettype none + +module lsc1u_protocol_formal; + (* gclk *) reg clk; + (* anyseq *) reg rst_n; + (* anyseq *) reg ena; + (* anyseq *) reg [7:0] rx_data; + (* anyseq *) reg rx_valid; + (* anyseq *) reg tx_ready; + wire rx_ready, tx_valid, busy, fault, done_pulse; + wire [7:0] tx_data; + + lsc1u_core dut ( + .clk(clk), .rst_n(rst_n), .ena(ena), + .rx_data(rx_data), .rx_valid(rx_valid), .rx_ready(rx_ready), + .tx_data(tx_data), .tx_valid(tx_valid), .tx_ready(tx_ready), + .busy(busy), .fault(fault), .done_pulse(done_pulse) + ); + + reg past_valid = 1'b0; + reg txn_active; + reg txn_completed; + reg [127:0] expected; + reg [4:0] expected_count; + reg [4:0] output_count; + reg [7:0] xor_a; + reg [1:0] op; + reg [5:0] payload_count; + + always @(posedge clk) begin + past_valid <= 1'b1; + if (!past_valid) + assume(!rst_n); + + if (!rst_n) begin + txn_active <= 0; + txn_completed <= 0; + expected_count <= 0; + output_count <= 0; + expected <= 0; + xor_a <= 0; + op <= 0; + payload_count <= 0; + end else begin + if (rx_valid && rx_ready) begin + if (!busy) begin + txn_active <= 1; + txn_completed <= 0; + output_count <= 0; + expected_count <= 0; + payload_count <= 0; + if (rx_data == 8'h01) op <= 1; + else if (rx_data == 8'h02) op <= 2; + else if (rx_data == 8'h03) op <= 3; + else begin + expected[7:0] <= 8'he0; + expected_count <= 1; + op <= 0; + end + end else if (op == 1) begin + payload_count <= payload_count + 1'b1; + if (!payload_count[0]) + xor_a <= rx_data; + else begin + expected[output_count[3:0] * 8 +: 8] <= xor_a ^ rx_data; + expected_count <= output_count + 1'b1; + end + end else if (op == 3) begin + payload_count <= payload_count + 1'b1; + expected[output_count[3:0] * 8 +: 8] <= rx_data; + expected_count <= output_count + 1'b1; + end else if (op == 2) begin + payload_count <= payload_count + 1'b1; + if (payload_count == 31) + expected_count <= 16; + end + end + if (tx_valid && tx_ready) begin + assert(output_count < expected_count); + // SET/XOR are checked byte-for-byte here. MUL arithmetic is + // exhaustively proved at the reused serial block boundary by + // gf128_serialize.sby; this harness proves its 16-byte + // streamed framing and exactly-one-completion behavior. + if (op != 2) + assert(tx_data == expected[output_count[3:0] * 8 +: 8]); + output_count <= output_count + 1'b1; + end + if (done_pulse && !(rx_valid && rx_ready && !busy)) + txn_completed <= 1'b1; + end + + if (past_valid && $past(rst_n)) begin + if (ena && $past(tx_valid && !tx_ready && ena && rst_n)) begin + assert(tx_valid); + assert(tx_data == $past(tx_data)); + end + if (!$past(ena) && ena && rst_n) + assert(!done_pulse); + if ($past(!ena) && !ena) begin + assert(!rx_ready && !tx_valid && !busy && !fault && !done_pulse); + end + if ($past(!rst_n)) begin + assert(!tx_valid && !done_pulse && !busy && !fault); + end + assert(!tx_valid || txn_active); + if (done_pulse) + assert($past(tx_valid && tx_ready && ena)); + if (txn_completed) + assert(!done_pulse); + end + + end +endmodule + +`default_nettype wire diff --git a/formal/lsc1u_reachability.sby b/formal/lsc1u_reachability.sby new file mode 100644 index 0000000..bca629f --- /dev/null +++ b/formal/lsc1u_reachability.sby @@ -0,0 +1,34 @@ +[tasks] +xor +mul +set +fault + +[options] +xor: mode cover +xor: depth 60 +mul: mode cover +mul: depth 200 +set: mode cover +set: depth 45 +fault: mode cover +fault: depth 8 +timeout 120 + +[engines] +btor btormc + +[script] +read -formal -sv gf128_mul_reachability_formal.sv +read -formal -sv lsc1u_core.sv +read -formal -sv lsc1u_reachability_formal.sv +xor: chparam -set SELECTED_OP 0 lsc1u_reachability_formal +mul: chparam -set SELECTED_OP 1 lsc1u_reachability_formal +set: chparam -set SELECTED_OP 2 lsc1u_reachability_formal +fault: chparam -set SELECTED_OP 3 lsc1u_reachability_formal +prep -top lsc1u_reachability_formal + +[files] +gf128_mul_reachability_formal.sv +../src/lsc1u_core.sv +lsc1u_reachability_formal.sv diff --git a/formal/lsc1u_reachability_formal.sv b/formal/lsc1u_reachability_formal.sv new file mode 100644 index 0000000..faa7c86 --- /dev/null +++ b/formal/lsc1u_reachability_formal.sv @@ -0,0 +1,34 @@ +`default_nettype none + +module lsc1u_reachability_formal #( + parameter [1:0] SELECTED_OP = 0 +); + (* gclk *) reg clk; + reg rst_n = 1'b0; + reg started = 1'b0; + wire [1:0] selected_op = SELECTED_OP; + + wire [7:0] command = + selected_op == 0 ? 8'h01 : + selected_op == 1 ? 8'h02 : + selected_op == 2 ? 8'h03 : 8'hff; + wire rx_ready, tx_valid, done_pulse; + wire [7:0] tx_data; + + lsc1u_core dut ( + .clk(clk), .rst_n(rst_n), .ena(1'b1), + .rx_data(started ? 8'h01 : command), + .rx_valid(1'b1), .rx_ready(rx_ready), + .tx_data(tx_data), .tx_valid(tx_valid), .tx_ready(1'b1), + .busy(), .fault(), .done_pulse(done_pulse) + ); + + always @(posedge clk) begin + rst_n <= 1'b1; + if (rst_n && rx_ready) + started <= 1'b1; + cover(done_pulse); + end +endmodule + +`default_nettype wire diff --git a/fpga_harness/boundary_check.py b/fpga_harness/boundary_check.py index 67cb2eb..377e1ed 100644 --- a/fpga_harness/boundary_check.py +++ b/fpga_harness/boundary_check.py @@ -6,8 +6,9 @@ wider than the pin interface (a wide bypass), and an ASIC top that drives a pin the direction mask declares an input. -Role names come from ``info.yaml`` and ``docs/LSC1_PROTOCOL.md``, which belong -to other lanes. This checker only reads them. It hard-fails on objective, +Role names for full LSC-1 come from ``docs/LSC1_PROTOCOL.md``. Tiny Tapeout's +``info.yaml`` may describe the deliberately reduced LSC-1u profile instead. +This checker hard-fails on objective, structural violations and reports unrecognised driven signals as observations, so that renaming an internal RTL signal in another lane cannot turn this into a false tripwire. @@ -76,6 +77,10 @@ def _is_abbreviation(first: str, second: str) -> bool: def _uio_roles_from_info() -> dict[int, str]: info = yaml.safe_load(INFO_YAML.read_text()) + if info["project"]["top_module"] == "tt_um_lfglabs_lsc1u": + # The FPGA harness remains full LSC-1; do not compare it to the + # profile-specific reserved LSC-1u input pin. + return _uio_roles_from_protocol() roles: dict[int, str] = {} for key, value in info["pinout"].items(): match = re.fullmatch(r"uio\[(\d)\]", str(key)) diff --git a/info.yaml b/info.yaml index b316fc9..29fa8e8 100644 --- a/info.yaml +++ b/info.yaml @@ -1,42 +1,39 @@ # Tiny Tapeout project information project: - title: "leanSilicon LSC-1" - author: "Thomas" + title: "leanSilicon LSC-1 Micro arithmetic kernel" + author: "LFG Labs" discord: "" - description: "Verification-in-progress physical scalar coprocessor for leanVM-b." + description: "LSC-1 Micro (LSC-1u): reduced Tiny Tapeout arithmetic sub-core of LSC-1, not LSC-2." language: "SystemVerilog" clock_hz: 25000000 - tiles: "2x2" - top_module: "lean_silicon_lsc1" + # 1x1 measured 128.237% GPL utilization; 1x2 is the smallest evidence-based + # follow-up that can retain the serial multiplier. + tiles: "1x2" + top_module: "tt_um_lfglabs_lsc1u" source_files: - - "asic_core/rtl/gf2n_mul_bitstream.sv" - - "asic_core/rtl/gf128_mul_bitstream.sv" - - "asic_core/rtl/leanvm_b_stream_alu.sv" - - "asic_core/rtl/lsc1_stream_adapter.sv" - - "asic_core/rtl/lsc1_packet_rx.sv" - - "asic_core/rtl/lsc1_packet_tx.sv" - - "asic_core/rtl/lsc1_packet_frontend.sv" - - "asic_core/rtl/lsc1_field_encoder.sv" - - "asic_core/rtl/lean_silicon_lsc1.sv" + - "tt_um_lfglabs_lsc1u.sv" + - "lsc1u_core.sv" + - "../asic_core/rtl/gf2n_mul_bitstream.sv" + - "../asic_core/rtl/gf128_mul_bitstream.sv" pinout: - ui[0]: "RX_DATA[0]" - ui[1]: "RX_DATA[1]" - ui[2]: "RX_DATA[2]" - ui[3]: "RX_DATA[3]" - ui[4]: "RX_DATA[4]" - ui[5]: "RX_DATA[5]" - ui[6]: "RX_DATA[6]" - ui[7]: "RX_DATA[7]" + ui[0]: "REQUEST_BYTE[0]" + ui[1]: "REQUEST_BYTE[1]" + ui[2]: "REQUEST_BYTE[2]" + ui[3]: "REQUEST_BYTE[3]" + ui[4]: "REQUEST_BYTE[4]" + ui[5]: "REQUEST_BYTE[5]" + ui[6]: "REQUEST_BYTE[6]" + ui[7]: "REQUEST_BYTE[7]" - uo[0]: "TX_DATA[0]" - uo[1]: "TX_DATA[1]" - uo[2]: "TX_DATA[2]" - uo[3]: "TX_DATA[3]" - uo[4]: "TX_DATA[4]" - uo[5]: "TX_DATA[5]" - uo[6]: "TX_DATA[6]" - uo[7]: "TX_DATA[7]" + uo[0]: "RESPONSE_BYTE[0]" + uo[1]: "RESPONSE_BYTE[1]" + uo[2]: "RESPONSE_BYTE[2]" + uo[3]: "RESPONSE_BYTE[3]" + uo[4]: "RESPONSE_BYTE[4]" + uo[5]: "RESPONSE_BYTE[5]" + uo[6]: "RESPONSE_BYTE[6]" + uo[7]: "RESPONSE_BYTE[7]" uio[0]: "RX_VALID" uio[1]: "RX_READY" @@ -44,7 +41,7 @@ pinout: uio[3]: "TX_READY" uio[4]: "BUSY" uio[5]: "FAULT" - uio[6]: "ABORT" + uio[6]: "RESERVED" uio[7]: "DONE_PULSE" yaml_version: 6 diff --git a/sim/lsc1u_model.py b/sim/lsc1u_model.py new file mode 100644 index 0000000..b21999c --- /dev/null +++ b/sim/lsc1u_model.py @@ -0,0 +1,27 @@ +"""Executable oracle for the fixed-width LSC-1u arithmetic boundary.""" + +WIDTH = 128 +MASK = (1 << WIDTH) - 1 + + +def gf128_mul(a: int, b: int) -> int: + """LSC-1 GF(2^128), little-endian polynomial basis, modulus low 0x87.""" + result = 0 + for _ in range(WIDTH): + if b & 1: + result ^= a + b >>= 1 + a = ((a << 1) & MASK) ^ (0x87 if (a >> 127) else 0) + return result + + +def execute(opcode: int, payload: bytes) -> bytes: + if opcode == 0x03 and len(payload) == 16: + return payload + if opcode == 0x01 and len(payload) == 32: + return bytes(payload[i] ^ payload[i + 1] for i in range(0, 32, 2)) + if opcode == 0x02 and len(payload) == 32: + a = int.from_bytes(payload[:16], "little") + b = int.from_bytes(payload[16:], "little") + return gf128_mul(a, b).to_bytes(16, "little") + raise ValueError("unsupported opcode or wrong fixed payload width") diff --git a/sim/test_lsc1u_model.py b/sim/test_lsc1u_model.py new file mode 100644 index 0000000..f81e529 --- /dev/null +++ b/sim/test_lsc1u_model.py @@ -0,0 +1,34 @@ +import random +import unittest + +from lsc1u_model import execute, gf128_mul +from scalar_step_oracle import multiply as full_lsc1_mul + + +class LSC1uOracleTests(unittest.TestCase): + def test_retained_boundary_matches_full_lsc1_oracle(self): + rng = random.Random(0x1C51) + for _ in range(500): + a = rng.getrandbits(128) + b = rng.getrandbits(128) + self.assertEqual(gf128_mul(a, b), full_lsc1_mul(a, b)) + ab = a.to_bytes(16, "little") + b.to_bytes(16, "little") + interleaved = b"".join( + bytes(pair) for pair in zip(ab[:16], ab[16:]) + ) + self.assertEqual( + execute(0x01, interleaved), + (a ^ b).to_bytes(16, "little"), + ) + self.assertEqual(execute(0x02, ab), + full_lsc1_mul(a, b).to_bytes(16, "little")) + self.assertEqual(execute(0x03, ab[:16]), ab[:16]) + + def test_fixed_framing_is_enforced(self): + for opcode in (0x01, 0x02, 0x03, 0x04): + with self.assertRaises(ValueError): + execute(opcode, b"") + + +if __name__ == "__main__": + unittest.main() diff --git a/src/config.json b/src/config.json new file mode 100644 index 0000000..3eb0b2a --- /dev/null +++ b/src/config.json @@ -0,0 +1,26 @@ +{ + "//": "Tiny Tapeout ttsky26c/LibreLane configuration; physical results remain CI-authoritative.", + "PL_TARGET_DENSITY_PCT": 60, + "CLOCK_PERIOD": 40, + "PL_RESIZER_HOLD_SLACK_MARGIN": 0.1, + "GRT_RESIZER_HOLD_SLACK_MARGIN": 0.05, + "RUN_LINTER": 1, + "LINTER_INCLUDE_PDK_MODELS": 1, + "CLOCK_PORT": "clk", + "RUN_KLAYOUT_XOR": 0, + "RUN_KLAYOUT_DRC": 0, + "DESIGN_REPAIR_BUFFER_OUTPUT_PORTS": 0, + "TOP_MARGIN_MULT": 1, + "BOTTOM_MARGIN_MULT": 1, + "LEFT_MARGIN_MULT": 6, + "RIGHT_MARGIN_MULT": 6, + "FP_SIZING": "absolute", + "GRT_ALLOW_CONGESTION": 1, + "FP_IO_HLENGTH": 2, + "FP_IO_VLENGTH": 2, + "FP_PDN_VPITCH": 38.87, + "RUN_CTS": 1, + "FP_PDN_MULTILAYER": 0, + "MAGIC_DEF_LABELS": 0, + "MAGIC_WRITE_LEF_PINONLY": 1 +} diff --git a/src/lsc1u_core.sv b/src/lsc1u_core.sv new file mode 100644 index 0000000..0faadc8 --- /dev/null +++ b/src/lsc1u_core.sv @@ -0,0 +1,195 @@ +/* + * LSC-1u: Tiny Tapeout streamed arithmetic/checking sub-core of LSC-1. + * + * This is deliberately not the full packet interface. Each accepted command + * has a fixed payload and response width: + * 0x01 XOR: A0,B0,...,A15,B15 -> R0..R15 + * 0x02 MUL: A0..A15,B0..B15 -> R0..R15 + * 0x03 SET: V0..V15 -> V0..V15 + * Bytes and polynomial coefficients are least-significant first. + */ +`default_nettype none + +module lsc1u_core ( + input wire clk, + input wire rst_n, + input wire ena, + input wire [7:0] rx_data, + input wire rx_valid, + output wire rx_ready, + output wire [7:0] tx_data, + output wire tx_valid, + input wire tx_ready, + output wire busy, + output wire fault, + output wire done_pulse +); + localparam [7:0] CMD_XOR = 8'h01; + localparam [7:0] CMD_MUL = 8'h02; + localparam [7:0] CMD_SET = 8'h03; + + localparam [3:0] IDLE = 4'd0; + localparam [3:0] XOR_A = 4'd1; + localparam [3:0] XOR_B = 4'd2; + localparam [3:0] SET_RX = 4'd3; + localparam [3:0] MUL_A = 4'd4; + localparam [3:0] MUL_B = 4'd5; + localparam [3:0] MUL_BITS = 4'd6; + localparam [3:0] MUL_TX = 4'd7; + + reg [3:0] state; + reg [3:0] byte_index; + reg [7:0] saved_byte; + reg [7:0] out_byte; + reg out_valid; + reg fault_reg; + reg done_reg; + + wire mul_a_valid = ena && rx_valid && rx_ready && (state == MUL_A); + wire mul_bit_valid = + ena && (((state == MUL_B) && rx_valid && rx_ready) || + (state == MUL_BITS)); + wire mul_bit_value = + (state == MUL_B) ? rx_data[0] : saved_byte[0]; + wire mul_tail_last = (saved_byte[7:1] == 7'b0000001); + wire mul_bit_last = + (state == MUL_BITS) && (byte_index == 4'd15) && mul_tail_last; + wire mul_result_shift = + ena && (state == MUL_TX) && !out_valid; + wire [7:0] mul_result_byte; + + gf128_mul_bitstream multiplier ( + .clk(clk), + .rst_n(rst_n), + .abort(1'b0), + .a_valid(mul_a_valid), + .a_byte(rx_data), + .a_last(byte_index == 4'd15), + .bit_valid(mul_bit_valid), + .bit_value(mul_bit_value), + .bit_last(mul_bit_last), + .result_shift(mul_result_shift), + .result_byte(mul_result_byte) + ); + + assign rx_ready = ena && !out_valid && + ((state == IDLE) || (state == XOR_A) || (state == XOR_B) || + (state == SET_RX) || (state == MUL_A) || (state == MUL_B)); + assign tx_data = out_byte; + assign tx_valid = ena && out_valid; + assign busy = ena && ((state != IDLE) || out_valid); + assign fault = ena && fault_reg; + assign done_pulse = ena && rst_n && done_reg; + + wire rx_fire = rx_valid && rx_ready; + wire tx_fire = tx_valid && tx_ready; + + always @(posedge clk) begin + if (!rst_n) begin + state <= IDLE; + byte_index <= 4'd0; + saved_byte <= 8'd0; + out_byte <= 8'd0; + out_valid <= 1'b0; + fault_reg <= 1'b0; + done_reg <= 1'b0; + end else if (!ena) begin + done_reg <= 1'b0; + end else begin + done_reg <= 1'b0; + + if (tx_fire) + out_valid <= 1'b0; + + case (state) + IDLE: begin + byte_index <= 4'd0; + if (rx_fire) begin + fault_reg <= 1'b0; + case (rx_data) + CMD_XOR: state <= XOR_A; + CMD_MUL: state <= MUL_A; + CMD_SET: state <= SET_RX; + default: begin + out_byte <= 8'he0; + out_valid <= 1'b1; + fault_reg <= 1'b1; + end + endcase + end + if (tx_fire) begin + done_reg <= 1'b1; + fault_reg <= 1'b0; + end + end + + XOR_A: if (rx_fire) begin + saved_byte <= rx_data; + state <= XOR_B; + end + + XOR_B: if (rx_fire) begin + out_byte <= saved_byte ^ rx_data; + out_valid <= 1'b1; + state <= XOR_A; + end + + SET_RX: if (rx_fire) begin + out_byte <= rx_data; + out_valid <= 1'b1; + end + + MUL_A: if (rx_fire) begin + if (byte_index == 4'd15) begin + byte_index <= 4'd0; + state <= MUL_B; + end else begin + byte_index <= byte_index + 1'b1; + end + end + + MUL_B: if (rx_fire) begin + saved_byte <= {1'b1, rx_data[7:1]}; + state <= MUL_BITS; + end + + MUL_BITS: begin + if (mul_tail_last) begin + if (byte_index == 4'd15) begin + byte_index <= 4'd0; + state <= MUL_TX; + end else begin + byte_index <= byte_index + 1'b1; + state <= MUL_B; + end + end else begin + saved_byte <= saved_byte >> 1; + end + end + + MUL_TX: if (!out_valid) begin + out_byte <= mul_result_byte; + out_valid <= 1'b1; + end + + default: begin + state <= IDLE; + fault_reg <= 1'b1; + end + endcase + + if (tx_fire && (state != IDLE)) begin + if (byte_index == 4'd15) begin + byte_index <= 4'd0; + state <= IDLE; + done_reg <= 1'b1; + end else if ((state == XOR_A) || (state == SET_RX) || + (state == MUL_TX)) begin + byte_index <= byte_index + 1'b1; + end + end + end + end +endmodule + +`default_nettype wire diff --git a/src/tt_um_lfglabs_lean_silicon_lsc1.sv b/src/tt_um_lfglabs_lean_silicon_lsc1.sv new file mode 100644 index 0000000..3fba2c1 --- /dev/null +++ b/src/tt_um_lfglabs_lean_silicon_lsc1.sv @@ -0,0 +1,56 @@ +/* + * Tiny Tapeout integration wrapper for the canonical LSC-1 ASIC boundary. + * SPDX-License-Identifier: Apache-2.0 + */ +`default_nettype none + +module tt_um_lfglabs_lean_silicon_lsc1 ( + input wire [7:0] ui_in, + output wire [7:0] uo_out, + input wire [7:0] uio_in, + output wire [7:0] uio_out, + output wire [7:0] uio_oe, + input wire ena, + input wire clk, + input wire rst_n +); + wire [7:0] core_uo_out; + wire [7:0] core_uio_out; + wire [7:0] core_uio_oe; + + // Do not present handshakes or ABORT to the core while this TT project is + // deselected. Reserved input positions remain explicit and deterministic. + wire [7:0] core_uio_in = { + 1'b0, // [7] output at the core boundary + uio_in[6] & ena, // [6] ABORT + 1'b0, // [5] output at the core boundary + 1'b0, // [4] output at the core boundary + uio_in[3] & ena, // [3] RESPONSE_READY + 1'b0, // [2] output at the core boundary + 1'b0, // [1] output at the core boundary + uio_in[0] & ena // [0] REQUEST_VALID + }; + + lean_silicon_lsc1 core ( + .ui_in (ui_in), + .uo_out (core_uo_out), + .uio_in (core_uio_in), + .uio_out (core_uio_out), + .uio_oe (core_uio_oe), + .ena (ena), + .clk (clk), + .rst_n (rst_n) + ); + + // A deselected project never drives the shared bidirectional pins and + // presents zero on dedicated outputs. Every output is assigned. + assign uo_out = ena ? core_uo_out : 8'b0; + assign uio_out = ena ? core_uio_out : 8'b0; + assign uio_oe = ena ? core_uio_oe : 8'b0; + + // Input-only uio positions are intentionally ignored on the output side. + wire _unused = &{uio_in[7], uio_in[5], uio_in[4], + uio_in[2], uio_in[1], 1'b0}; +endmodule + +`default_nettype wire diff --git a/src/tt_um_lfglabs_lsc1u.sv b/src/tt_um_lfglabs_lsc1u.sv new file mode 100644 index 0000000..18f06ad --- /dev/null +++ b/src/tt_um_lfglabs_lsc1u.sv @@ -0,0 +1,38 @@ +/* Tiny Tapeout pin wrapper for LSC-1u (LSC-1 Micro). */ +`default_nettype none + +module tt_um_lfglabs_lsc1u ( + input wire [7:0] ui_in, + output wire [7:0] uo_out, + input wire [7:0] uio_in, + output wire [7:0] uio_out, + output wire [7:0] uio_oe, + input wire ena, + input wire clk, + input wire rst_n +); + wire rx_ready; + wire tx_valid; + wire busy; + wire fault; + wire done_pulse; + wire [7:0] tx_data; + + lsc1u_core core ( + .clk(clk), .rst_n(rst_n), .ena(ena), + .rx_data(ui_in), .rx_valid(uio_in[0]), + .rx_ready(rx_ready), + .tx_data(tx_data), .tx_valid(tx_valid), .tx_ready(uio_in[3]), + .busy(busy), .fault(fault), .done_pulse(done_pulse) + ); + + assign uo_out = ena ? tx_data : 8'd0; + assign uio_out = ena ? + {done_pulse, 1'b0, fault, busy, 1'b0, tx_valid, rx_ready, 1'b0} : + 8'd0; + assign uio_oe = ena ? 8'b10110110 : 8'd0; + + wire _unused = &{uio_in[7:4], uio_in[2:1], 1'b0}; +endmodule + +`default_nettype wire diff --git a/src/user_config.tcl b/src/user_config.tcl index be36fe7..8b9101d 100644 --- a/src/user_config.tcl +++ b/src/user_config.tcl @@ -1,8 +1,8 @@ -set ::env(DESIGN_NAME) tt_um_leanvm_b_mincore +set ::env(DESIGN_NAME) tt_um_lfglabs_lsc1u set ::env(VERILOG_FILES) "\ - $::env(DESIGN_DIR)/gf2n_mul_bitstream.sv \ - $::env(DESIGN_DIR)/gf128_mul_bitstream.sv \ - $::env(DESIGN_DIR)/leanvm_b_stream_alu.sv \ - $::env(DESIGN_DIR)/tt_um_leanvm_b_mincore.sv" + $::env(DESIGN_DIR)/../asic_core/rtl/gf2n_mul_bitstream.sv \ + $::env(DESIGN_DIR)/../asic_core/rtl/gf128_mul_bitstream.sv \ + $::env(DESIGN_DIR)/lsc1u_core.sv \ + $::env(DESIGN_DIR)/tt_um_lfglabs_lsc1u.sv" set ::env(CLOCK_PORT) "clk" set ::env(CLOCK_PERIOD) "40" diff --git a/test/Makefile b/test/Makefile index 8819bd3..3f2b515 100644 --- a/test/Makefile +++ b/test/Makefile @@ -1,4 +1,5 @@ PYTHON ?= python3 +.DEFAULT_GOAL := tt-test PROJECT_SOURCES = \ ../asic_core/rtl/gf2n_mul_bitstream.sv \ @@ -17,7 +18,12 @@ BRIDGE_SOURCES = \ ../fpga/ulx3s/uart_tx.sv \ ../fpga/ulx3s/uart_bridge.sv -.PHONY: sim stream-alu uart-bridge packet-uart-bridge packet-frontend-sim packet-frontend-mutation packet-rtl-differential clean +.PHONY: tt-test sim stream-alu uart-bridge packet-uart-bridge packet-frontend-sim packet-frontend-mutation packet-rtl-differential clean + +# Default target used by TinyTapeout/tt-gds-action/gl_test@ttsky26c. +# The legacy repository regression remains available explicitly as `make sim`. +tt-test: + $(MAKE) -f Makefile.tt sim: stream-alu uart-bridge packet-uart-bridge packet-frontend-sim packet-frontend-mutation packet-rtl-differential @@ -43,5 +49,6 @@ packet-rtl-differential: cd .. && $(PYTHON) -m unittest sim.test_packet_frontend_rtl_differential -v clean: + $(MAKE) -f Makefile.tt clean rm -f tb_stream_alu.vvp tb_uart_bridge.vvp tb_packet_uart_bridge.vvp $(MAKE) -C packet_frontend clean diff --git a/test/Makefile.tt b/test/Makefile.tt new file mode 100644 index 0000000..cfb25dd --- /dev/null +++ b/test/Makefile.tt @@ -0,0 +1,28 @@ +SIM ?= icarus +TOPLEVEL_LANG ?= verilog +ROOT := $(abspath ..) +ASIC := $(ROOT)/asic_core/rtl + +PROJECT_SOURCES := \ + $(ROOT)/src/tt_um_lfglabs_lsc1u.sv \ + $(ROOT)/src/lsc1u_core.sv \ + $(ASIC)/gf2n_mul_bitstream.sv \ + $(ASIC)/gf128_mul_bitstream.sv + +ifeq ($(GATES),yes) +SIM_BUILD := sim_build/tt_gl +COMPILE_ARGS += -DGL_TEST -DFUNCTIONAL -DUSE_POWER_PINS -DSIM -DUNIT_DELAY=\#1 +VERILOG_SOURCES += $(PDK_ROOT)/sky130A/libs.ref/sky130_fd_sc_hd/verilog/primitives.v +VERILOG_SOURCES += $(PDK_ROOT)/sky130A/libs.ref/sky130_fd_sc_hd/verilog/sky130_fd_sc_hd.v +VERILOG_SOURCES += $(CURDIR)/gate_level_netlist.v +else +SIM_BUILD := sim_build/tt_rtl +COMPILE_ARGS += -g2012 -Wall +VERILOG_SOURCES += $(PROJECT_SOURCES) +endif + +VERILOG_SOURCES += $(CURDIR)/tt_tb.sv +TOPLEVEL := tt_tb +COCOTB_TEST_MODULES := test_tt + +include $(shell cocotb-config --makefiles)/Makefile.sim diff --git a/test/requirements.txt b/test/requirements.txt new file mode 100644 index 0000000..e316b1d --- /dev/null +++ b/test/requirements.txt @@ -0,0 +1,2 @@ +pytest==8.4.2 +cocotb==2.0.1 diff --git a/test/test_tt.py b/test/test_tt.py new file mode 100644 index 0000000..d56b461 --- /dev/null +++ b/test/test_tt.py @@ -0,0 +1,186 @@ +# SPDX-License-Identifier: Apache-2.0 +import random + +import cocotb +from cocotb.triggers import ReadOnly, RisingEdge, Timer + + +RX_VALID = 1 << 0 +RX_READY = 1 << 1 +TX_VALID = 1 << 2 +TX_READY = 1 << 3 +BUSY = 1 << 4 +FAULT = 1 << 5 +DONE = 1 << 7 +OUTPUT_ENABLES = 0b10110110 + + +async def tick(dut, count=1): + for _ in range(count): + await RisingEdge(dut.clk) + await ReadOnly() + # The GL build uses UNIT_DELAY=#1 (1 ns); sample after it settles while + # staying far inside the 40 ns clock period. RTL also uses this path. + await Timer(2, unit="ns") + + +def bit(dut, mask): + return bool(int(dut.uio_out.value) & mask) + + +async def reset(dut): + dut.ui_in.value = 0 + dut.uio_in.value = 0 + dut.ena.value = 1 + dut.rst_n.value = 0 + await tick(dut, 3) + dut.rst_n.value = 1 + await tick(dut) + assert bit(dut, RX_READY) + + +async def send(dut, byte, stall=0): + dut.ui_in.value = byte + dut.uio_in.value = 0 + for _ in range(stall): + await tick(dut) + dut.uio_in.value = RX_VALID + waits = 0 + while not bit(dut, RX_READY): + await tick(dut) + waits += 1 + assert waits < 400, ( + f"RX_READY timeout sending 0x{byte:02x}; " + f"state={int(dut.dut.core.state.value)} " + f"index={int(dut.dut.core.byte_index.value)} " + f"saved=0x{int(dut.dut.core.saved_byte.value):02x}" + ) + await tick(dut) + dut.uio_in.value = 0 + + +async def receive(dut, stall=0): + waits = 0 + while not bit(dut, TX_VALID): + await tick(dut) + waits += 1 + assert waits < 400, "TX_VALID timeout" + held = int(dut.uo_out.value) + for _ in range(stall): + assert bit(dut, TX_VALID) + assert int(dut.uo_out.value) == held + await tick(dut) + dut.uio_in.value = TX_READY + value = int(dut.uo_out.value) + await tick(dut) + done = bit(dut, DONE) + dut.uio_in.value = 0 + return value, done + + +async def transact(dut, opcode, payload, expected, rng): + await send(dut, opcode) + assert bit(dut, BUSY) + output = [] + done_count = 0 + for byte in payload: + await send(dut, byte, rng.randrange(3)) + if bit(dut, TX_VALID): + value, done = await receive(dut, rng.randrange(5)) + output.append(value) + done_count += done + while len(output) < len(expected): + value, done = await receive(dut, rng.randrange(5)) + output.append(value) + done_count += done + assert bytes(output) == expected + assert done_count == 1 + await tick(dut) + assert not bit(dut, DONE) + assert not bit(dut, BUSY) + + +def gf128_mul(a, b): + product = 0 + for _ in range(128): + if b & 1: + product ^= a + b >>= 1 + a = ((a << 1) & ((1 << 128) - 1)) ^ (0x87 if a >> 127 else 0) + return product + + +@cocotb.test() +async def lsc1u_all_retained_operations(dut): + rng = random.Random(0x1C51) + await reset(dut) + for _ in range(8): + a = bytes(rng.getrandbits(8) for _ in range(16)) + b = bytes(rng.getrandbits(8) for _ in range(16)) + xor_payload = b"".join(bytes((x, y)) for x, y in zip(a, b)) + await transact(dut, 0x01, xor_payload, + bytes(x ^ y for x, y in zip(a, b)), rng) + await transact(dut, 0x03, a, a, rng) + product = gf128_mul(int.from_bytes(a, "little"), + int.from_bytes(b, "little")) + await transact(dut, 0x02, a + b, + product.to_bytes(16, "little"), rng) + + +@cocotb.test() +async def lsc1u_reset_ena_framing_and_backpressure(dut): + await reset(dut) + + # A payload byte without an accepted opcode is itself an unsupported opcode. + await send(dut, 0x44) + value, done = await receive(dut, 3) + assert (value, done) == (0xE0, True) + assert not bit(dut, FAULT) + + # Freeze a partial XOR while deselected; no pin is driven and no byte fires. + await send(dut, 0x01) + await send(dut, 0xA5) + dut.ui_in.value = 0x5A + dut.uio_in.value = RX_VALID | TX_READY + dut.ena.value = 0 + await tick(dut, 4) + assert int(dut.uo_out.value) == 0 + assert int(dut.uio_out.value) == 0 + assert int(dut.uio_oe.value) == 0 + dut.ena.value = 1 + await tick(dut) + assert int(dut.uio_oe.value) == OUTPUT_ENABLES + dut.uio_in.value = 0 + value, done = await receive(dut, 4) + assert value == 0xFF and not done + + # Reset cancels the remaining fixed-width frame and exposes command ready. + dut.rst_n.value = 0 + dut.uio_in.value = RX_VALID | TX_READY + await tick(dut) + assert not bit(dut, TX_VALID | DONE | BUSY | FAULT) + dut.rst_n.value = 1 + dut.uio_in.value = 0 + await tick(dut) + assert bit(dut, RX_READY) + + # Output stability under a long stall is mutation-sensitive. + await send(dut, 0x03) + await send(dut, 0xC3) + assert bit(dut, TX_VALID) + for value in (0x00, 0xFF, 0x5A, 0x81): + dut.ui_in.value = value + await tick(dut) + assert bit(dut, TX_VALID) + assert int(dut.uo_out.value) == 0xC3 + + +@cocotb.test() +async def lsc1u_little_endian_polynomial_vectors(dut): + await reset(dut) + rng = random.Random(1) + one = (1).to_bytes(16, "little") + top = (1 << 127).to_bytes(16, "little") + two = (2).to_bytes(16, "little") + await transact(dut, 0x02, one + top, top, rng) + await transact(dut, 0x02, top + two, (0x87).to_bytes(16, "little"), rng) diff --git a/test/tt_tb.sv b/test/tt_tb.sv new file mode 100644 index 0000000..6c96a07 --- /dev/null +++ b/test/tt_tb.sv @@ -0,0 +1,34 @@ +`default_nettype none +`timescale 1ns/1ps + +module tt_tb; + reg clk = 0; + reg rst_n = 0; + reg ena = 0; + reg [7:0] ui_in = 0; + reg [7:0] uio_in = 0; + wire [7:0] uo_out; + wire [7:0] uio_out; + wire [7:0] uio_oe; + supply1 VPWR; + supply0 VGND; + + always #20 clk = ~clk; + +`ifdef GL_TEST + tt_um_lfglabs_lsc1u dut ( + .VPWR(VPWR), .VGND(VGND), + .ui_in(ui_in), .uo_out(uo_out), + .uio_in(uio_in), .uio_out(uio_out), .uio_oe(uio_oe), + .ena(ena), .clk(clk), .rst_n(rst_n) + ); +`else + tt_um_lfglabs_lsc1u dut ( + .ui_in(ui_in), .uo_out(uo_out), + .uio_in(uio_in), .uio_out(uio_out), .uio_oe(uio_oe), + .ena(ena), .clk(clk), .rst_n(rst_n) + ); +`endif +endmodule + +`default_nettype wire diff --git a/tools/interface_consistency.py b/tools/interface_consistency.py index f157b38..f0583d4 100644 --- a/tools/interface_consistency.py +++ b/tools/interface_consistency.py @@ -11,7 +11,8 @@ ROOT = Path(__file__).resolve().parents[1] RTL = (ROOT / "asic_core" / "rtl" / "leanvm_b_stream_alu.sv").read_text() PYMODEL = (ROOT / "sim" / "model.py").read_text() -WRAPPER = (ROOT / "asic_core" / "rtl" / "lean_silicon_lsc1.sv").read_text() +ASIC_TOP = (ROOT / "asic_core" / "rtl" / "lean_silicon_lsc1.sv").read_text() +TT_WRAPPER = (ROOT / "src" / "tt_um_lfglabs_lsc1u.sv").read_text() INFO = yaml.safe_load((ROOT / "info.yaml").read_text()) EXPECTED = { @@ -57,23 +58,20 @@ def main() -> None: project = INFO["project"] top = project["top_module"] - if not re.search(rf"\bmodule\s+{re.escape(top)}\b", WRAPPER): + if not re.search(rf"\bmodule\s+{re.escape(top)}\b", TT_WRAPPER): raise SystemExit(f"info.yaml top module {top!r} is not present in wrapper") + if not re.search(r"\bmodule\s+lean_silicon_lsc1\b", ASIC_TOP): + raise SystemExit("canonical LSC-1 ASIC boundary is missing") if project["clock_hz"] != 25_000_000: raise SystemExit("unexpected clock_hz") for source in project["source_files"]: - if not (ROOT / source).is_file(): + if not (ROOT / "src" / source).is_file(): raise SystemExit(f"missing Tiny Tapeout source file: {source}") required_sources = { - "asic_core/rtl/gf2n_mul_bitstream.sv", - "asic_core/rtl/gf128_mul_bitstream.sv", - "asic_core/rtl/leanvm_b_stream_alu.sv", - "asic_core/rtl/lsc1_stream_adapter.sv", - "asic_core/rtl/lsc1_field_encoder.sv", - "asic_core/rtl/lsc1_packet_rx.sv", - "asic_core/rtl/lsc1_packet_tx.sv", - "asic_core/rtl/lsc1_packet_frontend.sv", - "asic_core/rtl/lean_silicon_lsc1.sv", + "tt_um_lfglabs_lsc1u.sv", + "lsc1u_core.sv", + "../asic_core/rtl/gf2n_mul_bitstream.sv", + "../asic_core/rtl/gf128_mul_bitstream.sv", } configured_sources = set(project["source_files"]) if configured_sources != required_sources: diff --git a/tools/repo_consistency.py b/tools/repo_consistency.py index a4f95be..fff145e 100644 --- a/tools/repo_consistency.py +++ b/tools/repo_consistency.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""Reject stale active integration names and verify LSC-1 declared sources.""" +"""Verify the LSC-1u TT profile and the unchanged full LSC-1 source boundary.""" from pathlib import Path import re import yaml @@ -18,15 +18,19 @@ def files(): def main(): info = yaml.safe_load((ROOT / "info.yaml").read_text()) - if info["project"]["top_module"] != "lean_silicon_lsc1": - raise SystemExit("info.yaml must name lean_silicon_lsc1") + if info["project"]["top_module"] != "tt_um_lfglabs_lsc1u": + raise SystemExit("info.yaml must name tt_um_lfglabs_lsc1u") for source in info["project"]["source_files"]: - path = ROOT / source + path = ROOT / "src" / source if not path.is_file(): raise SystemExit(f"missing declared ASIC source: {source}") + wrapper = ROOT / "src/tt_um_lfglabs_lsc1u.sv" + if not re.search(r"module\s+tt_um_lfglabs_lsc1u\b", + wrapper.read_text()): + raise SystemExit("LSC-1u Tiny Tapeout integration wrapper missing") top = ROOT / "asic_core/rtl/lean_silicon_lsc1.sv" if not re.search(r"module\s+lean_silicon_lsc1\b", top.read_text()): - raise SystemExit("LSC-1 Tiny Tapeout top missing") + raise SystemExit("full LSC-1 ASIC top missing") for path in files(): if OLD_TOP in path.read_text(errors="ignore"): raise SystemExit(f"stale active top name in {path.relative_to(ROOT)}") @@ -34,7 +38,7 @@ def main(): for required in ("version=1", "seed-0", "0xa1", "0x5a"): if required not in protocol: raise SystemExit(f"packet protocol marker missing: {required}") - print("LSC-1 repository consistency: OK") + print("LSC-1u TT profile and full LSC-1 source boundary: OK") if __name__ == "__main__": main()