File size: 1,816 Bytes
a8baeed | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 | # bit_accelerator build and verification.
#
# The verified design is bit_accelerator_v2 (rtl/bit_accelerator_v2.sv).
# The v1 sources (bit_accelerator.sv and its submodules) are kept for reference
# only and are not built: v1 multiply-drives result_valid/result_bit and its
# testbench does not compile. See README.md, "Design versions".
VERILATOR ?= verilator
IVERILOG ?= iverilog
VVP ?= vvp
WHY3_PROVER ?= z3
WHY3_TIME ?= 30
BUILD ?= build
V2_RTL := rtl/bit_accelerator_v2.sv
V2_TB := testbenches/tb_bit_accelerator_v2.sv
FORMAL := formal/bit_addressing.mlw formal/bit_addressing_proofs.mlw
.PHONY: help all test lint sim sim-verilator sim-icarus formal formal-cvc4 clean
.DEFAULT_GOAL := help
all test: lint sim formal
lint:
$(VERILATOR) --lint-only -Wall $(V2_RTL)
sim: sim-verilator sim-icarus
sim-verilator:
OUT=$(abspath $(BUILD))/verilator ./run_v2_sim.sh
sim-icarus:
mkdir -p $(BUILD)
$(IVERILOG) -g2012 -o $(BUILD)/tb_v2.vvp $(V2_RTL) $(V2_TB)
$(VVP) -n $(BUILD)/tb_v2.vvp
formal:
./scripts/prove.sh -P $(WHY3_PROVER) -t $(WHY3_TIME) -L formal $(FORMAL)
# Cross-check with CVC4. Informational: CVC4 does not discharge every goal
# within the time limit, Z3 does.
formal-cvc4:
-./scripts/prove.sh -P cvc4 -t $(WHY3_TIME) -L formal $(FORMAL)
clean:
rm -rf $(BUILD) obj_dir
help:
@echo "make test lint + both simulators + Why3 proofs"
@echo "make lint verilator -Wall on the v2 RTL"
@echo "make sim v2 testbench under Verilator and Icarus"
@echo "make formal prove formal/*.mlw with $(WHY3_PROVER) (every goal must be Valid)"
@echo "make formal-cvc4 informational CVC4 cross-check"
@echo "make clean remove $(BUILD)/"
@echo "Needs: verilator >= 5, iverilog >= 12, why3 >= 1.6 with z3 (why3 config detect)"
|