diff --git a/.github/workflows/gft-verilog-kat.yml b/.github/workflows/gft-verilog-kat.yml new file mode 100644 index 00000000..8d3b76ff --- /dev/null +++ b/.github/workflows/gft-verilog-kat.yml @@ -0,0 +1,63 @@ +name: gft-verilog-kat +on: + push: + branches: [main] + pull_request: + paths: + - "specs/tri_gft_add.t27" + - "specs/tri_gft_sub.t27" + - "specs/tri_gft_ladder.t27" + - ".github/workflows/gft-verilog-kat.yml" + +# Execute the GF-T specs' own test blocks IN SIMULATED HARDWARE: t27c +# icarus-simulate generates a self-checking Verilog testbench from the spec +# and runs it under Icarus Verilog. This is the gen-verilog leg of the ring's +# verification -- the same spec that drives the Rust verifier and the +# synthesizable silicon now has its assertions executed on the Verilog path +# too, so a codegen or spec regression on the hardware side cannot land +# silently. Requires t27c >= gHashTag/t27#1885 (assert lowering). +# +# tri_gft_arith is EXCLUDED: its GF-T32 u64-helper tests fail in simulation +# due to a pre-existing u64 width-truncation bug in gen-verilog +# (gHashTag/t27#1886); add it back when that is fixed upstream. + +jobs: + icarus-kat: + name: GF-T spec KATs under Icarus Verilog + runs-on: ubuntu-latest + steps: + - name: Checkout tri-net + uses: actions/checkout@v4 + with: + path: tri-net + + - name: Checkout t27 (SSOT compiler source) + uses: actions/checkout@v4 + with: + repository: gHashTag/t27 + ref: master + path: t27 + + - name: Install Icarus Verilog + run: sudo apt-get update && sudo apt-get install -y iverilog + + - name: Install stable Rust toolchain + uses: dtolnay/rust-toolchain@stable + + - name: Build t27c (release) + working-directory: t27 + run: cargo build --release --manifest-path bootstrap/Cargo.toml --bin t27c + + - name: Simulate GF-T spec testbenches + working-directory: tri-net + run: | + T27C=../t27/target/release/t27c + STATUS=0 + for spec in tri_gft_add tri_gft_sub tri_gft_ladder; do + echo "== ${spec}" + if ! $T27C icarus-simulate specs/${spec}.t27; then + echo "::error file=specs/${spec}.t27::icarus-simulate failed for specs/${spec}.t27" + STATUS=1 + fi + done + exit $STATUS