diff options
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 98 |
1 files changed, 63 insertions, 35 deletions
@@ -7,10 +7,13 @@ else ifeq ($(ARCH),64) override ARCH := RV64 endif +# Currently, we only have F with RV32, and both F and D with RV64. ifeq ($(ARCH),RV32) SAIL_XLEN := riscv_xlen32.sail + SAIL_FLEN := riscv_flen_F.sail else ifeq ($(ARCH),RV64) SAIL_XLEN := riscv_xlen64.sail + SAIL_FLEN := riscv_flen_D.sail else $(error '$(ARCH)' is not a valid architecture, must be one of: RV32, RV64) endif @@ -18,6 +21,11 @@ endif # Instruction sources, depending on target SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail SAIL_DEFAULT_INST = riscv_insts_base.sail riscv_insts_aext.sail riscv_insts_cext.sail riscv_insts_mext.sail riscv_insts_zicsr.sail riscv_insts_next.sail +SAIL_DEFAULT_INST += riscv_softfloat_interface.sail riscv_insts_fext.sail +ifeq ($(ARCH),RV64) +SAIL_DEFAULT_INST +=riscv_insts_dext.sail +endif + SAIL_SEQ_INST = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail @@ -30,6 +38,7 @@ SAIL_SYS_SRCS += riscv_next_regs.sail SAIL_SYS_SRCS += riscv_sys_exceptions.sail # default basic helpers for exception handling SAIL_SYS_SRCS += riscv_sync_exception.sail # define the exception structure used in the model SAIL_SYS_SRCS += riscv_next_control.sail # helpers for the 'N' extension +SAIL_SYS_SRCS += riscv_fdext_regs.sail riscv_fdext_control.sail SAIL_SYS_SRCS += riscv_csr_ext.sail # access to CSR extensions SAIL_SYS_SRCS += riscv_sys_control.sail # general exception handling @@ -44,17 +53,18 @@ SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS) endif # Non-instruction sources -PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) prelude_mem_metadata.sail prelude_mem.sail +PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) $(SAIL_FLEN) prelude_mem_metadata.sail prelude_mem.sail -SAIL_REGS_SRCS = riscv_reg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail +SAIL_REGS_SRCS = riscv_reg_type.sail riscv_freg_type.sail riscv_regs.sail riscv_pc_access.sail riscv_sys_regs.sail SAIL_REGS_SRCS += riscv_pmp_regs.sail riscv_pmp_control.sail SAIL_REGS_SRCS += riscv_ext_regs.sail $(SAIL_CHECK_SRCS) SAIL_ARCH_SRCS = $(PRELUDE) -SAIL_ARCH_SRCS += riscv_types_ext.sail riscv_types.sail +SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail SAIL_ARCH_SRCS += riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail SAIL_ARCH_SRCS += riscv_mem.sail $(SAIL_VM_SRCS) -SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) +SAIL_ARCH_RVFI_SRCS = $(PRELUDE) rvfi_dii.sail riscv_types_common.sail riscv_types_ext.sail riscv_types.sail riscv_vmem_types.sail $(SAIL_REGS_SRCS) $(SAIL_SYS_SRCS) riscv_platform.sail riscv_mem.sail $(SAIL_VM_SRCS) + SAIL_STEP_SRCS = riscv_step_common.sail riscv_step_ext.sail riscv_decode_ext.sail riscv_fetch.sail riscv_step.sail RVFI_STEP_SRCS = riscv_step_common.sail riscv_step_rvfi.sail riscv_decode_ext.sail riscv_fetch_rvfi.sail riscv_step.sail @@ -74,7 +84,7 @@ SAIL_RMEM_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_RMEM_INST_SRCS) $(S SAIL_RVFI_SRCS = $(addprefix model/,$(SAIL_ARCH_RVFI_SRCS) $(SAIL_SEQ_INST_SRCS) $(RVFI_STEP_SRCS)) SAIL_COQ_SRCS = $(addprefix model/,$(SAIL_ARCH_SRCS) $(SAIL_SEQ_INST_SRCS) $(SAIL_OTHER_COQ_SRCS)) -PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml riscv_ocaml_sim.ml) +PLATFORM_OCAML_SRCS = $(addprefix ocaml_emulator/,platform.ml platform_impl.ml softfloat.ml riscv_ocaml_sim.ml) SAIL_FLAGS += -dno_cast @@ -99,8 +109,8 @@ BBV_DIR?=../bbv C_WARNINGS ?= #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function -C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h) -C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_sim.c) +C_INCS = $(addprefix c_emulator/,riscv_prelude.h riscv_platform_impl.h riscv_platform.h riscv_softfloat.h) +C_SRCS = $(addprefix c_emulator/,riscv_prelude.c riscv_platform_impl.c riscv_platform.c riscv_softfloat.c riscv_sim.c) C_INCS += $(addprefix c_emulator/gdb_remote/,gdb_utils.h gdb_arch.h gdb_rsp.h) C_SRCS += $(addprefix c_emulator/gdb_remote/,gdb_utils.c gdb_arch_riscv.c gdb_rsp.c) @@ -108,8 +118,15 @@ C_SRCS += $(addprefix c_emulator/gdb_remote/,gdb_utils.c gdb_arch_riscv.c gdb_rs C_SYS_INCLUDES = -I /opt/local/include C_SYS_LIBDIRS = -L /opt/local/lib -C_FLAGS = $(C_SYS_INCLUDES) -I $(SAIL_LIB_DIR) -I c_emulator -C_LIBS = $(C_SYS_LIBDIRS) -lgmp -lz +SOFTFLOAT_DIR = c_emulator/SoftFloat-3e +SOFTFLOAT_INCDIR = $(SOFTFLOAT_DIR)/source/include +SOFTFLOAT_LIBDIR = $(SOFTFLOAT_DIR)/build/Linux-RISCV-GCC +SOFTFLOAT_FLAGS = -I $(SOFTFLOAT_INCDIR) +SOFTFLOAT_LIBS = $(SOFTFLOAT_LIBDIR)/softfloat.a +SOFTFLOAT_SPECIALIZE_TYPE = RISCV + +C_FLAGS = $(C_SYS_INCLUDES) -I $(SAIL_LIB_DIR) -I c_emulator $(SOFTFLOAT_FLAGS) +C_LIBS = $(C_SYS_LIBDIRS) -lgmp -lz $(SOFTFLOAT_LIBS) # The C simulator can be built to be linked against Spike for tandem-verification. # This needs the C bindings to Spike from https://github.com/SRI-CSL/l3riscv @@ -131,16 +148,19 @@ else C_FLAGS += -O3 -flto endif +RISCV_EXTRAS_LEM_FILES = riscv_extras.lem mem_metadata.lem riscv_extras_fdext.lem # Feature detect if we are on the latest development version of Sail # and use an updated lem file if so. This is just until the opam # version catches up with changes to the barrier type. SAIL_LATEST := $(shell $(SAIL) -have_feature FEATURE_UNION_BARRIER 1>&2 2> /dev/null; echo $$?) ifeq ($(SAIL_LATEST),0) -RISCV_EXTRAS_LEM = 0.11/riscv_extras.lem +RISCV_EXTRAS_LEM = $(addprefix handwritten_support/0.11/,$(RISCV_EXTRAS_LEM_FILES)) else -RISCV_EXTRAS_LEM = riscv_extras.lem +RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES)) endif +.PHONY: + all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH) riscv_isa riscv_coq riscv_hol riscv_rmem .PHONY: all @@ -193,7 +213,7 @@ gcovr: generated_definitions/ocaml/riscv_duopod_ocaml: $(PRELUDE_SRCS) model/riscv_duopod.sail mkdir -p generated_definitions/ocaml - $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml_build_dir generated_definitions/ocaml -o riscv_duopod_ocaml $^ + $(SAIL) $(SAIL_FLAGS) -ocaml -ocaml_build_dir generated_definitions/ocaml -o riscv_duopod_ocaml model/riscv_duopod.sail ocaml_emulator/tracecmp: ocaml_emulator/tracecmp.ml ocamlfind ocamlopt -annot -linkpkg -package unix $^ -o $@ @@ -202,15 +222,24 @@ generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_SRCS) model/main.sail Make mkdir -p generated_definitions/c $(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_SRCS) model/main.sail -o $(basename $@) -c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) Makefile +$(SOFTFLOAT_LIBS): + $(MAKE) SPECIALIZE_TYPE=$(SOFTFLOAT_SPECIALIZE_TYPE) -C $(SOFTFLOAT_LIBDIR) + +# convenience target +.PHONY: csim +csim: c_emulator/riscv_sim_$(ARCH) +.PHONY: rvfi +rvfi: c_emulator/riscv_rvfi_$(ARCH) + +c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile gcc -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ -generated_definitions/c/riscv_rvfi_model.c: $(SAIL_RVFI_SRCS) model/main.sail Makefile +generated_definitions/c/riscv_rvfi_model_$(ARCH).c: $(SAIL_RVFI_SRCS) model/main.sail Makefile mkdir -p generated_definitions/c - $(SAIL) $(SAIL_FLAGS) -O -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@) + $(SAIL) $(SAIL_FLAGS) -O -Oconstant_fold -memo_z3 -c -c_include riscv_prelude.h -c_include riscv_platform.h -c_no_main $(SAIL_RVFI_SRCS) model/main.sail -o $(basename $@) sed -i -e '/^[[:space:]]*$$/d' $@ -c_emulator/riscv_rvfi: generated_definitions/c/riscv_rvfi_model.c $(C_INCS) $(C_SRCS) Makefile +c_emulator/riscv_rvfi_$(ARCH): generated_definitions/c/riscv_rvfi_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS) Makefile gcc -g $(C_WARNINGS) $(C_FLAGS) $< -DRVFI_DII $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@ latex: $(SAIL_SRCS) Makefile @@ -223,10 +252,11 @@ generated_definitions/isabelle/$(ARCH)/ROOT: handwritten_support/ROOT generated_definitions/lem/riscv_duopod.lem: $(PRELUDE_SRCS) model/riscv_duopod.sail mkdir -p generated_definitions/lem - $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -isa_output_dir generated_definitions/isabelle -lem_mwords -lem_lib Riscv_extras -o riscv_duopod $^ -generated_definitions/isabelle/Riscv_duopod.thy: generated_definitions/isabelle/ROOT generated_definitions/lem/riscv_duopod.lem handwritten_support/$(RISCV_EXTRAS_LEM) + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem -isa_output_dir generated_definitions/isabelle -lem_mwords -lem_lib Riscv_extras -lem_lib Mem_metadata -o riscv_duopod model/riscv_duopod.sail + +generated_definitions/isabelle/Riscv_duopod.thy: generated_definitions/isabelle/RV64/ROOT generated_definitions/lem/riscv_duopod.lem $(RISCV_EXTRAS_LEM) lem -isa -outdir generated_definitions/isabelle -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - handwritten_support/$(RISCV_EXTRAS_LEM) \ + $(RISCV_EXTRAS_LEM) \ generated_definitions/lem/riscv_duopod_types.lem \ generated_definitions/lem/riscv_duopod.lem @@ -246,30 +276,26 @@ endif generated_definitions/lem/$(ARCH)/riscv.lem: $(SAIL_SRCS) Makefile mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras $(SAIL_SRCS) - echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem - -generated_definitions/lem/$(ARCH)/riscv_sequential.lem: $(SAIL_SRCS) Makefile - mkdir -p generated_definitions/lem/$(ARCH) generated_definitions/isabelle/$(ARCH) - $(SAIL_DIR)/sail -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -lem_sequential -o riscv_sequential -lem_mwords -lem_lib Riscv_extras_sequential $(SAIL_SRCS) + $(SAIL) $(SAIL_FLAGS) -lem -lem_output_dir generated_definitions/lem/$(ARCH) -isa_output_dir generated_definitions/isabelle/$(ARCH) -o riscv -lem_mwords -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata $(SAIL_SRCS) echo "declare {isabelle} rename field sync_exception_ext = sync_exception_ext_exception" >> generated_definitions/lem/$(ARCH)/riscv_types.lem -generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) Makefile +generated_definitions/isabelle/$(ARCH)/Riscv.thy: generated_definitions/isabelle/$(ARCH)/ROOT generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) Makefile lem -isa -outdir generated_definitions/isabelle/$(ARCH) -lib Sail=$(SAIL_SRC_DIR)/lem_interp -lib Sail=$(SAIL_SRC_DIR)/gen_lib \ - handwritten_support/$(RISCV_EXTRAS_LEM) \ + $(RISCV_EXTRAS_LEM) \ generated_definitions/lem/$(ARCH)/riscv_types.lem \ generated_definitions/lem/$(ARCH)/riscv.lem sed -i 's/datatype ast/datatype (plugins only: size) ast/' generated_definitions/isabelle/$(ARCH)/Riscv_types.thy sed -i "s/record( 'asidlen, 'valen, 'palen, 'ptelen) TLB_Entry/record (overloaded) ( 'asidlen, 'valen, 'palen, 'ptelen) TLB_Entry/" generated_definitions/isabelle/$(ARCH)/Riscv_types.thy + sed -i "s/by pat_completeness auto/by pat_completeness (auto intro!: let_cong bind_cong MemoryOpResult.case_cong)/" generated_definitions/isabelle/$(ARCH)/Riscv.thy generated_definitions/hol4/$(ARCH)/Holmakefile: handwritten_support/Holmakefile mkdir -p generated_definitions/hol4/$(ARCH) cp handwritten_support/Holmakefile generated_definitions/hol4/$(ARCH) -generated_definitions/hol4/$(ARCH)/riscvScript.sml: generated_definitions/hol4/$(ARCH)/Holmakefile generated_definitions/lem/$(ARCH)/riscv.lem handwritten_support/$(RISCV_EXTRAS_LEM) +generated_definitions/hol4/$(ARCH)/riscvScript.sml: generated_definitions/hol4/$(ARCH)/Holmakefile generated_definitions/lem/$(ARCH)/riscv.lem $(RISCV_EXTRAS_LEM) lem -hol -outdir generated_definitions/hol4/$(ARCH) -lib $(SAIL_LIB_DIR)/hol -i $(SAIL_LIB_DIR)/hol/sail2_prompt_monad.lem -i $(SAIL_LIB_DIR)/hol/sail2_prompt.lem \ -lib $(SAIL_DIR)/src/lem_interp -lib $(SAIL_DIR)/src/gen_lib \ - handwritten_support/$(RISCV_EXTRAS_LEM) \ + $(RISCV_EXTRAS_LEM) \ generated_definitions/lem/$(ARCH)/riscv_types.lem \ generated_definitions/lem/$(ARCH)/riscv.lem @@ -294,10 +320,10 @@ riscv_coq_build: generated_definitions/coq/$(ARCH)/riscv.vo $(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile mkdir -p generated_definitions/coq/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS) + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib riscv_extras -coq_lib mem_metadata $(SAIL_COQ_SRCS) $(addprefix generated_definitions/coq/$(ARCH)/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) model/riscv_duopod.sail model/riscv_termination_duo.sail mkdir -p generated_definitions/coq/$(ARCH) - $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv_duopod -coq_lib riscv_extras $^ + $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv_duopod -coq_lib riscv_extras -coq_lib mem_metadata $^ %.vo: %.v ifeq ($(wildcard $(BBV_DIR)/theories),) @@ -308,8 +334,8 @@ ifeq ($(wildcard $(SAIL_LIB_DIR)/coq),) endif coqc $(COQ_LIBS) $< -generated_definitions/coq/$(ARCH)/riscv.vo: generated_definitions/coq/$(ARCH)/riscv_types.vo handwritten_support/riscv_extras.vo -generated_definitions/coq/$(ARCH)/riscv_duopod.vo: generated_definitions/coq/$(ARCH)/riscv_duopod_types.vo handwritten_support/riscv_extras.vo +generated_definitions/coq/$(ARCH)/riscv.vo: generated_definitions/coq/$(ARCH)/riscv_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo +generated_definitions/coq/$(ARCH)/riscv_duopod.vo: generated_definitions/coq/$(ARCH)/riscv_duopod_types.vo handwritten_support/riscv_extras.vo handwritten_support/mem_metadata.vo echo_rmem_srcs: echo $(SAIL_RMEM_SRCS) @@ -319,7 +345,7 @@ riscv_rmem: generated_definitions/for-rmem/riscv_toFromInterp2.ml riscv_rmem: generated_definitions/for-rmem/riscv.defs .PHONY: riscv_rmem -generated_definitions/for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extras +generated_definitions/for-rmem/riscv.lem: SAIL_FLAGS += -lem_lib Riscv_extras -lem_lib Riscv_extras_fdext -lem_lib Mem_metadata generated_definitions/for-rmem/riscv.lem: $(SAIL_RMEM_SRCS) mkdir -p $(dir $@) # We do not need the isabelle .thy files, but sail always generates them @@ -363,10 +389,12 @@ clean: -rm -rf generated_definitions/ocaml/* generated_definitions/c/* generated_definitions/latex/* -rm -rf generated_definitions/lem/* generated_definitions/isabelle/* generated_definitions/hol4/* generated_definitions/coq/* -rm -rf generated_definitions/for-rmem/* - -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi + -$(MAKE) -C $(SOFTFLOAT_LIBDIR) clean + -rm -f c_emulator/riscv_sim_RV32 c_emulator/riscv_sim_RV64 c_emulator/riscv_rvfi_RV32 c_emulator/riscv_rvfi_RV64 -rm -rf ocaml_emulator/_sbuild ocaml_emulator/_build ocaml_emulator/riscv_ocaml_sim_RV32 ocaml_emulator/riscv_ocaml_sim_RV64 ocaml_emulator/tracecmp -rm -f *.gcno *.gcda -rm -f z3_problems -Holmake cleanAll -rm -f handwritten_support/riscv_extras.vo handwritten_support/riscv_extras.glob handwritten_support/.riscv_extras.aux + -rm -f handwritten_support/mem_metadata.vo handwritten_support/mem_metadata.glob handwritten_support/.mem_metadata.aux ocamlbuild -clean |