October 2026 main drop: mirror from GitHub

0ba037b verified 16 days ago

2.93 kB

# bit-string-accelerator: build and verification entry points.
#
#   make test      everything below (what CI runs)
#   make lint      verilator -Wall on rtl/bit_accelerator.sv
#   make sim       self-checking testbench under Icarus and Verilator
#   make formal    Why3 proofs in formal/ (every goal must be proved by Z3)
#   make spice     ngspice timing model, fails if the delay is not measured
#   make accel     the bit_accelerator/ v2 design (lint, sim, formal)
#   make gpu       the Rust OpenCL crate in gpu/ (fmt, clippy, tests)
#   make fpga      FPGA wrapper: lint, UART testbench, host co-simulation, bitstreams
#   make fpga-gl   FPGA wrapper on post-synthesis netlists (slow, ~10 min)
#   make asic      sky130 synthesis + proof that the netlist equals the RTL
#   make pcie      parallel engine + PCIe core: lint, equivalence vs the reference core
#   make tapeout   Tiny Tapeout project: sources in sync, RTL test at both divisors

IVERILOG    ?= iverilog
VVP         ?= vvp
VERILATOR   ?= verilator
NGSPICE     ?= ngspice
WHY3_PROVER ?= z3
WHY3_TIME   ?= 30
BUILD       ?= build
SEED        ?= 1
OPS         ?= 2000

RTL     := rtl/bit_accelerator.sv
TB      := verification/tb_bit_accelerator.sv
FORMAL  := formal/bit_address.mlw formal/bit_extract.mlw formal/lane_map.mlw
PROVE   := bit_accelerator/scripts/prove.sh

.PHONY: all test lint sim sim-icarus sim-verilator formal spice accel gpu fpga fpga-gl asic pcie tapeout clean
.DEFAULT_GOAL := test

all test: lint sim formal spice accel gpu fpga asic pcie tapeout

lint:
	$(VERILATOR) --lint-only -Wall $(RTL)

sim: sim-icarus sim-verilator

sim-icarus:
	mkdir -p $(BUILD)
	$(IVERILOG) -g2012 -o $(BUILD)/tb.vvp $(RTL) $(TB)
	$(VVP) -n $(BUILD)/tb.vvp +seed=$(SEED) +ops=$(OPS)

sim-verilator:
	mkdir -p $(BUILD)/verilator
	$(VERILATOR) --binary --timing --timescale 1ns/1ps -Wno-fatal -Wno-lint --top-module tb_bit_accelerator \
	  -Mdir $(BUILD)/verilator $(RTL) $(TB) >/dev/null
	$(BUILD)/verilator/Vtb_bit_accelerator +seed=$(SEED) +ops=$(OPS)

formal:
	$(PROVE) -P $(WHY3_PROVER) -t $(WHY3_TIME) $(FORMAL)

spice:
	mkdir -p $(BUILD)
	$(NGSPICE) -b spice/bit_extract.sp > $(BUILD)/spice.log 2>&1
	@grep -E '^tpd *= *[0-9.e+-]+' $(BUILD)/spice.log || { cat $(BUILD)/spice.log; echo "tpd not measured"; exit 1; }

accel:
	$(MAKE) -C bit_accelerator test

gpu:
	cd gpu && cargo fmt --check
	cd gpu && cargo clippy --all-targets -- -D warnings
	# Serial: PoCL 5.0 can abort when several contexts are released concurrently.
	cd gpu && RUST_TEST_THREADS=1 cargo test

fpga:
	$(MAKE) -C fpga lint sim cosim icebreaker ulx3s

fpga-gl:
	$(MAKE) -C fpga gl-sim

asic:
	$(MAKE) -C asic all

pcie:
	$(MAKE) -C pcie lint sim sim-verilator

tapeout:
	$(MAKE) -C tapeout check-sync test

clean:
	rm -rf $(BUILD) simv
	$(MAKE) -C bit_accelerator clean
	$(MAKE) -C fpga clean
	$(MAKE) -C asic clean
	$(MAKE) -C pcie clean
	$(MAKE) -C tapeout clean
	cd gpu && cargo clean

	# bit-string-accelerator: build and verification entry points.
	#
	# make test everything below (what CI runs)
	# make lint verilator -Wall on rtl/bit_accelerator.sv
	# make sim self-checking testbench under Icarus and Verilator
	# make formal Why3 proofs in formal/ (every goal must be proved by Z3)
	# make spice ngspice timing model, fails if the delay is not measured
	# make accel the bit_accelerator/ v2 design (lint, sim, formal)
	# make gpu the Rust OpenCL crate in gpu/ (fmt, clippy, tests)
	# make fpga FPGA wrapper: lint, UART testbench, host co-simulation, bitstreams
	# make fpga-gl FPGA wrapper on post-synthesis netlists (slow, ~10 min)
	# make asic sky130 synthesis + proof that the netlist equals the RTL
	# make pcie parallel engine + PCIe core: lint, equivalence vs the reference core
	# make tapeout Tiny Tapeout project: sources in sync, RTL test at both divisors

	IVERILOG ?= iverilog
	VVP ?= vvp
	VERILATOR ?= verilator
	NGSPICE ?= ngspice
	WHY3_PROVER ?= z3
	WHY3_TIME ?= 30
	BUILD ?= build
	SEED ?= 1
	OPS ?= 2000

	RTL := rtl/bit_accelerator.sv
	TB := verification/tb_bit_accelerator.sv
	FORMAL := formal/bit_address.mlw formal/bit_extract.mlw formal/lane_map.mlw
	PROVE := bit_accelerator/scripts/prove.sh

	.PHONY: all test lint sim sim-icarus sim-verilator formal spice accel gpu fpga fpga-gl asic pcie tapeout clean
	.DEFAULT_GOAL := test

	all test: lint sim formal spice accel gpu fpga asic pcie tapeout

	lint:
	$(VERILATOR) --lint-only -Wall $(RTL)

	sim: sim-icarus sim-verilator

	sim-icarus:
	mkdir -p $(BUILD)
	$(IVERILOG) -g2012 -o $(BUILD)/tb.vvp $(RTL) $(TB)
	$(VVP) -n $(BUILD)/tb.vvp +seed=$(SEED) +ops=$(OPS)

	sim-verilator:
	mkdir -p $(BUILD)/verilator
	$(VERILATOR) --binary --timing --timescale 1ns/1ps -Wno-fatal -Wno-lint --top-module tb_bit_accelerator \
	-Mdir $(BUILD)/verilator $(RTL) $(TB) >/dev/null
	$(BUILD)/verilator/Vtb_bit_accelerator +seed=$(SEED) +ops=$(OPS)

	formal:
	$(PROVE) -P $(WHY3_PROVER) -t $(WHY3_TIME) $(FORMAL)

	spice:
	mkdir -p $(BUILD)
	$(NGSPICE) -b spice/bit_extract.sp > $(BUILD)/spice.log 2>&1
	@grep -E '^tpd = [0-9.e+-]+' $(BUILD)/spice.log \|\| { cat $(BUILD)/spice.log; echo "tpd not measured"; exit 1; }

	accel:
	$(MAKE) -C bit_accelerator test

	gpu:
	cd gpu && cargo fmt --check
	cd gpu && cargo clippy --all-targets -- -D warnings
	# Serial: PoCL 5.0 can abort when several contexts are released concurrently.
	cd gpu && RUST_TEST_THREADS=1 cargo test

	fpga:
	$(MAKE) -C fpga lint sim cosim icebreaker ulx3s

	fpga-gl:
	$(MAKE) -C fpga gl-sim

	asic:
	$(MAKE) -C asic all

	pcie:
	$(MAKE) -C pcie lint sim sim-verilator

	tapeout:
	$(MAKE) -C tapeout check-sync test

	clean:
	rm -rf $(BUILD) simv
	$(MAKE) -C bit_accelerator clean
	$(MAKE) -C fpga clean
	$(MAKE) -C asic clean
	$(MAKE) -C pcie clean
	$(MAKE) -C tapeout clean
	cd gpu && cargo clean