blob: 0be4eaebffd3bf2514677ba1ae6279a8bd4fbed4 (
plain)
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
|
SRCS = riscv_reg_type.sail riscv_regs.sail
SAIL_DIR:=$(shell opam config var sail:share)
SAIL:=sail
SAIL_LIB_DIR:=$(SAIL_DIR)/lib
export SAIL_LIB_DIR
SAIL_SRC_DIR:=$(SAIL_DIR)/src
EXPLICIT_COQ_BBV = $(shell if opam config var coq-bbv:share >/dev/null 2>/dev/null; then echo no; else echo yes; fi)
COQ_LIBS += -Q $(BBV_DIR)/src/bbv bbv
COQ_LIBS += -Q $(SAIL_LIB_DIR)/coq Sail
COQ_LIBS = -R generated_definitions/coq/$(ARCH) '' -R generated_definitions/coq '' -R handwritten_support ''
riscv_coq: $(addprefix build/,riscv.v riscv_types.v)
riscv_coq_build: build/riscv.vo
.PHONY: riscv_coq riscv_coq_build
# %.vo: %.v
# coqc $(COQ_LIBS) $<
$(addprefix build/,riscv.v riscv_types.v): $(SRCS) Makefile
mkdir -p build
$(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir build/ -o riscv $(SRCS)
# $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir build/ -o riscv -coq_lib riscv_extras -coq_lib mem_metadata $(SRCS)
# build/riscv.vo: build/riscv_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo
default:riscv_coq
|
