Modularise the specification

Makefile.new

@@ -0,0 +1,98 @@
+ARCH ?= RV64
+
+ifeq ($(ARCH),32)
+  override ARCH := RV32
+else ifeq ($(ARCH),64)
+  override ARCH := RV64
+endif
+
+# ##############################################################################
+# Sail setup
+# ##############################################################################
+
+SAIL_PROJECT ?= model/riscv.sail_project
+
+ifneq ($(SAIL_DIR),)
+# Can use sail repo directory as the value SAIL_DIR
+SAIL:=$(SAIL_DIR)/sail
+export SAIL_DIR
+else
+# Use sail from opam package
+SAIL_DIR:=$(shell opam var sail:share)
+SAIL:=sail
+endif
+
+SAIL_LIB_DIR:=$(SAIL_DIR)/lib
+
+SAIL_FLAGS += --require-version 0.18
+SAIL_FLAGS += --memo-z3
+
+# Use all available extensions by default
+EXTENSIONS ?= --all-modules
+
+SAIL_PROJECT_FLAGS := --project $(SAIL_PROJECT) --variable ARCH=$(ARCH)
+SAIL_SRCS := $(shell $(SAIL) $(SAIL_PROJECT_FLAGS) --list-files --all-modules)
+
+SAIL_BUILD := $(SAIL) $(SAIL_PROJECT_FLAGS)
+SAIL_DEPS := $(SAIL_PROJECT) $(SAIL_SRCS)
+
+# ##############################################################################
+# Default target
+# ##############################################################################
+
+.PHONY: all help
+
+all: help
+
+help:
+	@cat help-make
+
+# ##############################################################################
+# Sail C simulator
+# ##############################################################################
+
+# The following ensures empty sail-generated .c files don't hang around and
+# break future builds if sail exits badly
+.DELETE_ON_ERROR: generated_defintions/c/%.c
+
+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
+
+$(SOFTFLOAT_LIBS):
+	$(MAKE) SPECIALIZE_TYPE=$(SOFTFLOAT_SPECIALIZE_TYPE) -C $(SOFTFLOAT_LIBDIR)
+
+SAIL_C_FLAGS = --c-no-main \
+        --c-include riscv_prelude.h \
+	--c-include riscv_platform.h \
+        --c-preserve _set_Misa_C \
+	-O \
+	--Oconstant-fold
+
+generated_definitions/c/riscv_model_$(ARCH).c: $(SAIL_DEPS)
+	mkdir -p generated_defintions/c
+	$(SAIL_BUILD) $(SAIL_FLAGS) $(EXTENSIONS) -c $(SAIL_C_FLAGS) -o $(basename $@)
+
+GMP_FLAGS = $(shell pkg-config --cflags gmp)
+# N.B. GMP does not have pkg-config metadata on Ubuntu 18.04 so default to -lgmp
+GMP_LIBS = $(shell pkg-config --libs gmp || echo -lgmp)
+ZLIB_FLAGS = $(shell pkg-config --cflags zlib)
+ZLIB_LIBS = $(shell pkg-config --libs zlib)
+
+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 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_FLAGS = -I $(SAIL_LIB_DIR) -I c_emulator $(GMP_FLAGS) $(ZLIB_FLAGS) $(SOFTFLOAT_FLAGS)
+C_LIBS  = $(GMP_LIBS) $(ZLIB_LIBS) $(SOFTFLOAT_LIBS)
+
+c_emulator/riscv_sim_$(ARCH): generated_definitions/c/riscv_model_$(ARCH).c $(C_INCS) $(C_SRCS) $(SOFTFLOAT_LIBS)
+	gcc -g $(C_WARNINGS) $(C_FLAGS) $< $(C_SRCS) $(SAIL_LIB_DIR)/*.c $(C_LIBS) -o $@
+
+# Convenience target
+.PHONY: csim
+csim: c_emulator/riscv_sim_$(ARCH)

help-make

@@ -0,0 +1,7 @@
+This Makefile can be used to build several targets, you should choose
+one explicitly, for example:
+
+- 'make csim' to build the C simulator
+
+The variable ARCH controls whether the model is built in RV32 or RV64
+mode. By default it is set to RV64.

model/riscv.sail_project

@@ -0,0 +1,254 @@
+variable ARCH = "RV32"
+
+riscv_core {
+  files
+    prelude.sail,
+    if $ARCH == "RV32" then
+      riscv_xlen32.sail
+    else if $ARCH == "RV64" then
+      riscv_xlen64.sail
+    else
+      error("ARCH variable must be either RV32 or RV64"),
+    riscv_xlen.sail,
+    riscv_flen_D.sail,
+    riscv_vlen.sail,
+    prelude_mem_metadata.sail,
+    prelude_mem.sail,
+    riscv_types_common.sail,
+    riscv_types_ext.sail,
+    riscv_types.sail,
+    riscv_vmem_types.sail,
+    riscv_reg_type.sail,
+    riscv_regs.sail,
+    riscv_pc_access.sail,
+    riscv_sys_regs.sail,
+    riscv_ext_regs.sail,
+    riscv_addr_checks_common.sail,
+    riscv_addr_checks.sail,
+    riscv_misa_ext.sail,
+    riscv_csr_begin.sail,
+}
+
+riscv_exceptions {
+  requires riscv_core, N_regs
+
+  files
+    riscv_sys_exceptions.sail,
+    riscv_sync_exception.sail,
+}
+
+pmp {
+  requires riscv_core
+
+  files
+    riscv_pmp_regs.sail,
+    riscv_pmp_control.sail,
+}
+
+riscv {
+  requires riscv_core, riscv_exceptions, pmp, N_regs, V_core
+
+  files
+    riscv_sys_control.sail,
+    riscv_platform.sail,
+    riscv_mem.sail,
+    riscv_vmem_common.sail,
+    riscv_vmem_pte.sail,
+    riscv_vmem_ptw.sail,
+    riscv_vmem_tlb.sail,
+    riscv_vmem.sail,
+    riscv_insts_begin.sail,
+}
+
+extensions {
+  I {
+    requires riscv_core, riscv_exceptions, riscv
+
+    files
+      riscv_insts_base.sail,
+      riscv_jalr_seq.sail
+  }
+
+  N {
+    N_regs {
+      requires riscv_core
+      files riscv_next_regs.sail
+    }
+    N_control {
+      requires riscv_core, riscv_exceptions, riscv, N_regs
+      files riscv_next_control.sail
+    }
+    N_instructions {
+      requires riscv_core, riscv_exceptions, riscv, N_regs, N_control
+      files riscv_insts_next.sail,
+    }
+  }
+
+  A {
+    requires riscv_core, riscv_exceptions, riscv, I
+    files riscv_insts_aext.sail
+  }
+
+  M {
+    requires riscv_core, riscv
+    files riscv_insts_mext.sail
+  }
+
+  // RISC-V Bit manipulation extensions
+  B {
+    requires riscv_core, riscv
+
+    Zba {
+      files riscv_insts_zba.sail
+    }
+    Zbb {
+      files riscv_insts_zbb.sail
+    }
+    Zbc {
+      files riscv_insts_zbc.sail
+    }
+    Zbs {
+      files riscv_insts_zbs.sail
+    }
+  }
+
+  // Compressed instructions
+  C {
+    Zca {
+      requires riscv_core, riscv_exceptions, riscv, I
+      files riscv_insts_zca.sail
+    }
+    Zcb {
+      requires riscv_core, riscv_exceptions, riscv, I, B, M
+      files riscv_insts_zcb.sail
+    }
+  }
+
+  // Floating point (F and D extensions)
+  FD {
+    requires riscv_core
+
+    FD_core {
+      before riscv
+      files
+        riscv_softfloat_interface.sail,
+        riscv_freg_type.sail,
+        riscv_fdext_regs.sail,
+        riscv_fdext_control.sail,
+    }
+
+    FD_instructions {
+      requires riscv, I, FD_core
+      files
+        riscv_insts_fext.sail,
+        riscv_insts_zcf.sail,
+        riscv_insts_dext.sail,
+        riscv_insts_zcd.sail,
+        riscv_insts_zfh.sail,
+        riscv_insts_zfa.sail,
+    }
+  }
+
+  // RISC-V vector extension
+  V {
+    requires riscv_core
+
+    V_core {
+      files
+        riscv_vreg_type.sail,
+        riscv_vext_regs.sail,
+        riscv_vext_control.sail,
+    }
+
+    V_instructions {
+      requires riscv, I, FD, V_core
+      files
+        riscv_insts_vext_utils.sail,
+        riscv_insts_vext_fp_utils.sail,
+        riscv_insts_vext_vset.sail,
+        riscv_insts_vext_arith.sail,
+        riscv_insts_vext_fp.sail,
+        riscv_insts_vext_mem.sail,
+        riscv_insts_vext_mask.sail,
+        riscv_insts_vext_vm.sail,
+        riscv_insts_vext_fp_vm.sail,
+        riscv_insts_vext_red.sail,
+        riscv_insts_vext_fp_red.sail,
+     }
+  }
+
+  // RISC-V Cryptography Extension
+  K {
+    requires riscv_core
+
+    K_core {
+      files riscv_types_kext.sail
+    }
+    Zkn {
+      requires riscv, K_core
+      files riscv_insts_zkn.sail
+    }
+    Zks {
+      requires riscv, K_core
+      files riscv_insts_zks.sail
+    }
+    Zbkb {
+      requires riscv
+      files riscv_insts_zbkb.sail
+    }
+    Zbkx {
+      requires riscv
+      files riscv_insts_zbkx.sail
+    }
+  }
+
+  // Control and Status Register (CSR) Instructions
+  Zicsr {
+    requires riscv_core, riscv, riscv_exceptions, pmp, V_core
+    files riscv_insts_zicsr.sail
+  }
+
+  Svinval {
+    requires riscv_core, riscv, I
+    files riscv_insts_svinval.sail
+  }
+
+  Zicond {
+    requires riscv_core, riscv
+    files riscv_insts_zicond.sail
+  }
+
+  Zicbom {
+    requires riscv_core, riscv
+    files riscv_insts_zicbom.sail
+  }
+
+  Zicboz {
+    requires riscv_core, riscv
+    files riscv_insts_zicboz.sail
+  }
+}
+
+hints {
+  after extensions
+
+  requires riscv_core, riscv, I
+
+  files riscv_insts_hints.sail
+}
+
+riscv_postlude {
+  after extensions, hints
+
+  requires riscv_core, riscv
+
+  files
+    riscv_insts_end.sail,
+    riscv_csr_end.sail,
+    riscv_step_common.sail,
+    riscv_step_ext.sail,
+    riscv_decode_ext.sail,
+    riscv_fetch.sail,
+    riscv_step.sail,
+    main.sail
+}