SHD-FormalVerificationLab/Makefile at main · MATCHA-MIT/SHD-FormalVerificationLab · GitHub

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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
PWD := $(shell pwd)
PYTHON := $(shell which python)

TOY := 0
ifneq ($(TOY),0)
DUV := toy
INCLUDES :=
ENTRY := toy
else
DUV := cpu
INCLUDES := -I$(DUV)/spec -I$(DUV)/core_to_verify -I$(DUV)/core_to_verify/core -I$(DUV)/core_to_verify/interfaces
ENTRY ?= miter
endif
SRCS := $(shell find $(DUV) -type f -name '*.sv')
SRCS += $(PWD)/entry/$(ENTRY).sv

DEST ?= $(PWD)/build
VERILOG_DUMP := $(DEST)/top.dump.v
CEX_DUMP := $(DEST)/cex.txt
CEX_CERT := $(DEST)/cert.txt
INV_DUMP := $(DEST)/invariants.txt
CEX_VCD  := $(DEST)/cex.vcd

sv2aig_FLAG := --top-module top --dump --vmap --dst $(DEST) $(INCLUDES)

RIC3_DIR := $(PWD)/rIC3
RIC3_TMP_DIR := /tmp/rIC3-$(shell whoami)
RIC3 := $(RIC3_DIR)/target/release/rIC3
RIC3_FLAG := --model-map $(DEST)/top.map $(DEST)/top.aig $(CEX_CERT) --inv-dump $(INV_DUMP) --cex-dump $(CEX_DUMP)
BMC_K := 5

$(DEST):
	mkdir -p $(DEST)

ric3:
	cd $(RIC3_DIR) && git submodule update --init && cargo build --release

aiger: $(DEST)
	$(PYTHON) -m scripts.sv2aig $(sv2aig_FLAG) $(SRCS)

bmc: $(DEST)
	mkdir -p $(RIC3_TMP_DIR)
	RIC3_TMP_DIR=$(RIC3_TMP_DIR) $(RIC3) --engine=bmc --bmc-max-k $(BMC_K) $(RIC3_FLAG) 2>&1 | tee $(DEST)/run.txt

umc: $(DEST)
	mkdir -p $(RIC3_TMP_DIR)
	RIC3_TMP_DIR=$(RIC3_TMP_DIR) $(RIC3) --engine=ic3 $(RIC3_FLAG) 2>&1 | tee $(DEST)/run.txt

scripts/zeroall.vpi: scripts/zeroall.c
	cd scripts; iverilog-vpi zeroall.c

cex: scripts/zeroall.vpi
	mkdir -p $(DEST)/simulate
	python scripts/cex2tb.py $(VERILOG_DUMP) $(DEST)/top.map $(CEX_CERT) $(CEX_VCD) --certificate > $(DEST)/simulate/cex_tb.sv
	iverilog -g2012 -gassertions $(DEST)/simulate/cex_tb.sv $(VERILOG_DUMP) -o $(DEST)/simulate/cex_tb.out
	vvp -M $(PWD)/scripts -m zeroall $(DEST)/simulate/cex_tb.out

VERILATOR := verilator
VERILATOR_FLAGS := --cc --exe --build --trace -Wall -Wno-fatal -Wno-UNOPTFLAT $(INCLUDES) -CFLAGS "-std=c++20"
VERILATOR_TOP := $(PWD)/entry/$(ENTRY).cpp
VERILATOR_OUT := $(DEST)/Vtop-$(ENTRY)
ASM ?= testcase.s
IMEM_ASM := $(PWD)/simulation/$(ASM)
IMEM_BIN := $(DEST)/imem.bin
CYCLES ?= 5
PRIV_INIT ?= 3  # Machine mode

verilator: $(DEST) # do not use $(VERILATOR_OUT), to force rebuild, since sharing obj_dir may cause problems
	$(VERILATOR) $(VERILATOR_FLAGS) --Mdir $(DEST)/obj_dir --top-module top $(SRCS) $(VERILATOR_TOP)
	cp $(DEST)/obj_dir/Vtop $(VERILATOR_OUT)

$(IMEM_BIN): $(DEST) $(IMEM_ASM)
	sh $(PWD)/scripts/compile_testcase.sh $(IMEM_ASM) $(IMEM_BIN)

sim: verilator $(IMEM_BIN)
	$(VERILATOR_OUT) --imem $(IMEM_BIN) --vcd $(DEST)/sim-$(ENTRY).vcd --cycles $(CYCLES) --priv $(PRIV_INIT)

clean:
	rm -rf $(DEST)

.PHONY: ric3 verilator sim clean