diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..0be4eae --- /dev/null +++ b/Makefile @@ -0,0 +1,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 |