RISC-V: more tidying up of the Spike interface.

2 files changed, 22 insertions, 23 deletions

diff --git a/riscv/Makefile b/riscv/Makefile
index a49ba6e3..ae86adbe 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -17,21 +17,21 @@ SAIL_DIR ?= $(realpath ..)
 SAIL ?= $(SAIL_DIR)/sail
 C_WARNINGS ?=
 #-Wall -Wextra -Wno-unused-label -Wno-unused-parameter -Wno-unused-but-set-variable -Wno-unused-function
-C_FLAGS = -I ../lib
 C_INCS = riscv_prelude.h riscv_platform_impl.h riscv_platform.h
 C_SRCS = riscv_prelude.c riscv_platform_impl.c riscv_platform.c
 
-ENABLE_SPIKE = 0
-TV_SPIKE_DIR = /home/mundkur/src/hw/l3/l3riscv
-SPIKE_FLAGS = -I $(TV_SPIKE_DIR)/src/cpp
-SPIKE_LIBS  = -L $(TV_SPIKE_DIR) -ltv_spike -Wl,-rpath=$(TV_SPIKE_DIR)
-SPIKE_LIBS += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib
-
-C_LIBS = -lgmp -lz
-
-ifeq ($(ENABLE_SPIKE),1)
-C_FLAGS += $(SPIKE_FLAGS)
-C_LIBS  += $(SPIKE_LIBS)
+C_FLAGS = -I ../lib
+C_LIBS  = -lgmp -lz
+
+# 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
+# TV_SPIKE_DIR in the environment should point to the top-level dir of the L3
+# RISC-V, containing the built C bindings to Spike.
+# RISCV should be defined if TV_SPIKE_DIR is.
+ifneq (,$(TV_SPIKE_DIR))
+C_FLAGS += -I $(TV_SPIKE_DIR)/src/cpp -DENABLE_SPIKE
+C_LIBS  += -L $(TV_SPIKE_DIR) -ltv_spike -Wl,-rpath=$(TV_SPIKE_DIR)
+C_LIBS  += -L $(RISCV)/lib -lfesvr -lriscv -Wl,-rpath=$(RISCV)/lib
 endif
 
 export SAIL_DIR
diff --git a/riscv/riscv_sim.c b/riscv/riscv_sim.c
index 038c44b6..d86a197d 100644
--- a/riscv/riscv_sim.c
+++ b/riscv/riscv_sim.c
@@ -17,8 +17,7 @@
 #include "riscv_platform_impl.h"
 #include "riscv_sail.h"
 
-//#define SPIKE 1
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
 #include "tv_spike_intf.h"
 #else
 struct tv_spike_t;
@@ -95,7 +94,7 @@ static void print_usage(const char *argv0, int ec)
 
 static void dump_dts(void)
 {
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
   size_t dts_len = 0;
   struct tv_spike_t *s = tv_init("RV64IMAC", rv_ram_size, 0);
   tv_get_dts(s, NULL, &dts_len);
@@ -229,7 +228,7 @@ uint64_t load_sail(char *f)
 
 void init_spike(const char *f, uint64_t entry, uint64_t ram_size)
 {
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
   bool mismatch = false;
   s = tv_init("RV64IMAC", ram_size, 1);
   if (tv_is_dirty_enabled(s) != rv_enable_dirty_update) {
@@ -281,7 +280,7 @@ void init_spike(const char *f, uint64_t entry, uint64_t ram_size)
 
 void tick_spike()
 {
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
   tv_tick_clock(s);
   tv_step_io(s);
 #endif
@@ -313,7 +312,7 @@ void init_sail_reset_vector(uint64_t entry)
       write_mem(addr++, dtb[i]);
   }
 
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
   if (dtb && dtb_len) {
     // Ensure that Spike's DTB matches the one provided.
     bool matched = dtb_len == spike_dtb_len;
@@ -370,7 +369,7 @@ void init_sail(uint64_t elf_entry)
 int init_check(struct tv_spike_t *s)
 {
   int passed = 1;
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
   passed &= tv_check_csr(s, CSR_MISA, zmisa.zMisa_chunk_0);
 #endif
   return passed;
@@ -379,7 +378,7 @@ int init_check(struct tv_spike_t *s)
 void finish(int ec)
 {
   model_fini();
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
   tv_free(s);
 #endif
   exit(ec);
@@ -389,7 +388,7 @@ int compare_states(struct tv_spike_t *s)
 {
   int passed = 1;
 
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
 #define TV_CHECK(reg, spike_reg, sail_reg)   \
   passed &= tv_check_ ## reg(s, spike_reg, sail_reg);
 
@@ -542,7 +541,7 @@ void run_sail(void)
       insn_cnt++;
     }
 
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
     { /* run a Spike step */
       tv_step(s);
       spike_done = tv_is_done(s);
@@ -595,7 +594,7 @@ void run_sail(void)
 
 void init_logs()
 {
-#ifdef SPIKE
+#ifdef ENABLE_SPIKE
   // The Spike interface uses stdout for terminal output, and stderr for logs.
   // Do the same here.
   if (dup2(1, 2) < 0) {