Skip to content
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
63 changes: 63 additions & 0 deletions .github/workflows/gft-verilog-kat.yml
Original file line number Diff line number Diff line change
@@ -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
Loading