Rebase

Makefile

@@ -203,6 +203,19 @@ RISCV_EXTRAS_LEM = $(addprefix handwritten_support/,$(RISCV_EXTRAS_LEM_FILES))
 all: ocaml_emulator/riscv_ocaml_sim_$(ARCH) c_emulator/riscv_sim_$(ARCH)
 .PHONY: all
 
+json: $(SAIL_SRCS) model/main.sail Makefile
+	@sail -json $(SAIL_FLAGS) $(SAIL_SRCS)
+
+.PHONY: check-json
+check-json:
+	sail -json $(SAIL_FLAGS) $(SAIL_SRCS) | python3 -c "import json; import sys; j=json.load(sys.stdin)"
+
+output: $(SAIL_SRCS) model/main.sail Makefile
+	sail -output-sail $(SAIL_FLAGS) $(SAIL_SRCS)
+
+decode: $(SAIL_SRCS) model/main.sail Makefile
+	sail -plugin $(HOME)/projects/Sail/riscvdecode/riscv_decode.cmxs -riscv_decode $(SAIL_FLAGS) $(SAIL_SRCS)
+
 # the following ensures empty sail-generated .c files don't hang around and
 # break future builds if sail exits badly
 .DELETE_ON_ERROR: generated_definitions/c/%.c

README.md

@@ -347,6 +347,10 @@ There is also (as yet unmerged) support for [integration with riscv-config](http
 For booting operating system images, see the information under the
 [os-boot/](os-boot/) subdirectory.
 
+### How to use the out-of-tree JSON backend to generate JSON from Sail
+
+For details, see [JSON.md](doc/JSON.md).
+
 ### Using development versions of Sail
 
 Rarely, the version of Sail packaged in opam may not meet your needs. This could happen if you need a bug fix or new feature not yet in the released Sail version, or you are actively working on Sail. In this case you can tell the `sail-riscv` `Makefile` to use a local copy of Sail by setting `SAIL_DIR` to the root of a checkout of the Sail repo when you invoke `make`. Alternatively, you can use `opam pin` to install Sail from a local checkout of the Sail repo as described in the Sail installation instructions.

doc/JSON.md

@@ -0,0 +1,18 @@
+STEPS TO BUILD AND COMPILE THE PROJECT
+=======================================
+
+After Installing the prerequisites
+
+1.  We first need to build the sail parser.
+    1. Find a directory to clone this repository, and make that directory your current working directory.
+    2. `git clone https://github.com/ThinkOpenly/sail`
+    3. `cd sail`
+    4. `make`
+
+2.  Then, set up the environment for building in the RISC-V Sail repository:
+    1. `eval $(opam env)`
+    2. `export PATH=<path-to-sail-repository>:$PATH`
+
+3.  Clone this sail-riscv repository.
+
+4.  Within that clone : `make json`

model/riscv_fdext_control.sail

@@ -17,9 +17,9 @@
 
 /* val clause ext_is_CSR_defined : (csreg, Privilege) -> bool */
 
-function clause ext_is_CSR_defined (0x001, _) = haveFExt() | haveZfinx()
-function clause ext_is_CSR_defined (0x002, _) = haveFExt() | haveZfinx()
-function clause ext_is_CSR_defined (0x003, _) = haveFExt() | haveZfinx()
+function clause ext_is_CSR_defined (0x001, _) = extension("F") | extension("Zfinx")
+function clause ext_is_CSR_defined (0x002, _) = extension("F") | extension("Zfinx")
+function clause ext_is_CSR_defined (0x003, _) = extension("F") | extension("Zfinx")
 
 function clause ext_read_CSR (0x001) = Some(zero_extend(fcsr[FFLAGS]))
 function clause ext_read_CSR (0x002) = Some(zero_extend(fcsr[FRM]))

model/riscv_fetch.sail

@@ -19,7 +19,7 @@ function fetch() -> FetchResult =
   match ext_fetch_check_pc(PC, PC) {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC())))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extension("C"))))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _)     => F_Error(e, PC),

model/riscv_fetch_rvfi.sail

@@ -17,7 +17,7 @@ function fetch() -> FetchResult = {
     Ext_FetchAddr_Error(e)   => F_Ext_Error(e),
     Ext_FetchAddr_OK(use_pc) => {
       /* then check PC alignment */
-      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(haveRVC())))
+      if   (use_pc[0] != bitzero | (use_pc[1] != bitzero & not(extension("C"))))
       then F_Error(E_Fetch_Addr_Align(), PC)
       else match translateAddr(use_pc, Execute()) {
         TR_Failure(e, _) => F_Error(e, PC),

model/riscv_insts_aext.sail

@@ -43,8 +43,8 @@ function amo_width_valid(size : word_width) -> bool = {
 /* ****************************************************************** */
 union clause ast = LOADRES : (bool, bool, regidx, word_width, regidx)
 
-mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)                                                if haveZalrsc() & amo_width_valid(size)
-  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & amo_width_valid(size)
+mapping clause encdec = LOADRES(aq, rl, rs1, size, rd)                                                if extension("Zalrsc") & amo_width_valid(size)
+  <-> 0b00010 @ bool_bits(aq) @ bool_bits(rl) @ 0b00000 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zalrsc") & amo_width_valid(size)
 
 
 /* We could set load-reservations on physical or virtual addresses.
@@ -88,8 +88,8 @@ mapping clause assembly = LOADRES(aq, rl, rs1, size, rd)
 /* ****************************************************************** */
 union clause ast = STORECON : (bool, bool, regidx, regidx, word_width, regidx)
 
-mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)                                      if haveZalrsc() & amo_width_valid(size)
-  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZalrsc() & amo_width_valid(size)
+mapping clause encdec = STORECON(aq, rl, rs2, rs1, size, rd)                                      if extension("Zalrsc") & amo_width_valid(size)
+  <-> 0b00011 @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zalrsc") & amo_width_valid(size)
 
 /* NOTE: Currently, we only EA if address translation is successful. This may need revisiting. */
 function clause execute (STORECON(aq, rl, rs2, rs1, width, rd)) = {
@@ -163,8 +163,8 @@ mapping encdec_amoop : amoop <-> bits(5) = {
   AMOMAXU <-> 0b11100
 }
 
-mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)                                                if haveZaamo() & amo_width_valid(size)
-  <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if haveZaamo() & amo_width_valid(size)
+mapping clause encdec = AMO(op, aq, rl, rs2, rs1, size, rd)                                                if extension("Zaamo") & amo_width_valid(size)
+  <-> encdec_amoop(op) @ bool_bits(aq) @ bool_bits(rl) @ rs2 @ rs1 @ 0b0 @ size_enc(size) @ rd @ 0b0101111 if extension("Zaamo") & amo_width_valid(size)
 
 /* NOTE: Currently, we only EA if address translation is successful.
    This may need revisiting. */