Added support and instructions for using the C and OCaml simulators …

…from the Sail RISC-V formal model as targets.

        * added subdirectories riscv-target/sail-riscv-c and riscv-target/sail-riscv-ocaml
        * updated README.md and doc/README.adoc

ChangeLog

@@ -1,3 +1,8 @@
+2019-05-23 Prashanth Mundkur <prashanth.mundkur@gmail.com>
+    * Added support and instructions for using the C and OCaml simulators from the Sail RISC-V formal model as targets.
+	* added subdirectories riscv-target/sail-riscv-c and riscv-target/sail-riscv-ocaml
+	* updated README.md and doc/README.adoc
+
 2019-04-05 Allen Baum <allen.baum@esperantotech.com>
     * spec/TestFormatSpec.adoc:  Adding details, minor corrections, ToBeDiscussed
       items and clarifications to the specification of the future compliance test

README.md

@@ -40,7 +40,7 @@ The only setup required is to define where the toolchain is found, and where the
 For the toolchain, the binaries must be in the search path and the compiler prefix is defined on the make line. The default value for this is
 
     RISCV_PREFIX ?= riscv64-unknown-elf-
-    
+
 The path to the RUN_TARGET is defined within the riscv-target Makefile.include.
 
 To run the rv32i test suite on riscvOVPsim
@@ -52,3 +52,23 @@ To run the rv32i test suite on riscvOVPsim
 As we create the RISCV.org compliance test suite, the Imperas developed _riscvOVPsim_ compliance simulator is included as part of this GitHub repository. For more information please contact info@ovpworld.org or info@imperas.com.
 
 For more information on riscvOVPsim look here: [riscv-ovpsim/README.md](riscv-ovpsim/README.md) and here: [riscv-ovpsim/doc/riscvOVPsim_User_Guide.pdf](riscv-ovpsim/doc/riscvOVPsim_User_Guide.pdf).
+
+### Using the simulators from the Sail RISC-V formal model
+
+The [Sail RISC-V formal model](https://github.com/rems-project/sail-riscv) generates two
+simulators, in C and OCaml.  They can be used as test targets for this compliance suite.
+
+For this purpose, the Sail model needs to be checked out and built on
+the machine running the compliance suite.  Follow the build
+instructions described the README for building the RV32 and RV64
+models.  Once built, please add `$SAIL_RISCV/c_emulator` and
+`$SAIL_RISCV/ocaml_emulator` to your path, where $SAIL_RISCV is the
+top-level directory containing the model.
+
+To test the compliance of the C simulator for the current RV32 and RV64 tests, use
+
+    make RISCV_TARGET=sail-riscv-c all_variant
+
+while the corresponding command for the OCaml simulator is
+
+    make RISCV_TARGET=sail-riscv-ocaml all_variant

doc/README.adoc

@@ -121,6 +121,10 @@ Jeremy Bennett, Mary Bennett, Simon Davidmann, Neel Gala, Radek Hajek, Lee Moore
 [cols="<1,<2,<3,<4",options="header,pagewidth",]
 |================================================================================
 | _Revision_ | _Date_            | _Author_ | _Modification_
+| 1.15 Draft | 14 March 2019     |
+Prashanth Mundkur |
+
+Added support and instructions for using the C and OCaml simulators from the Sail RISC-V formal model as targets.
 | 1.14 Draft  | 21 February 2019      |
 Deborah Soung |
 

riscv-target/sail-riscv-c/compliance_io.h

@@ -0,0 +1,36 @@
+// RISC-V Compliance IO Test Header File
+
+/*
+ * Copyright (c) 2005-2018 Imperas Software Ltd., www.imperas.com
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ *   http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND,
+ * either express or implied.
+ *
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *
+ */
+
+#ifndef _COMPLIANCE_IO_H
+#define _COMPLIANCE_IO_H
+
+//-----------------------------------------------------------------------
+// RV IO Macros (Non functional)
+//-----------------------------------------------------------------------
+
+#define RVTEST_IO_INIT
+#define RVTEST_IO_WRITE_STR(_SP, _STR)
+#define RVTEST_IO_CHECK()
+#define RVTEST_IO_ASSERT_GPR_EQ(_SP, _R, _I)
+#define RVTEST_IO_ASSERT_SFPR_EQ(_F, _R, _I)
+#define RVTEST_IO_ASSERT_DFPR_EQ(_D, _R, _I)
+
+#endif // _COMPLIANCE_IO_H

riscv-target/sail-riscv-c/compliance_test.h

@@ -0,0 +1,34 @@
+// RISC-V Compliance Test Header File
+// Copyright (c) 2017, Codasip Ltd. All Rights Reserved.
+// See LICENSE for license details.
+//
+// Description: Common header file for RV32I tests
+
+#ifndef _COMPLIANCE_TEST_H
+#define _COMPLIANCE_TEST_H
+
+#include "riscv_test.h"
+
+//-----------------------------------------------------------------------
+// RV Compliance Macros
+//-----------------------------------------------------------------------
+
+#define RV_COMPLIANCE_HALT                                                    \
+        RVTEST_PASS                                                           \
+
+#define RV_COMPLIANCE_RV32M                                                   \
+        RVTEST_RV32M                                                          \
+
+#define RV_COMPLIANCE_CODE_BEGIN                                              \
+        RVTEST_CODE_BEGIN                                                     \
+
+#define RV_COMPLIANCE_CODE_END                                                \
+        RVTEST_CODE_END                                                       \
+
+#define RV_COMPLIANCE_DATA_BEGIN                                              \
+        RVTEST_DATA_BEGIN                                                     \
+
+#define RV_COMPLIANCE_DATA_END                                                \
+        RVTEST_DATA_END                                                       \
+
+#endif

riscv-target/sail-riscv-c/device/rv32i/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV32
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv32-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv32im/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV32
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv32-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv32imc/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV32
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv32-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv32mi/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV32
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv32-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv32si/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV32
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv32-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv32ua/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV32
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv32-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv32uc/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV32
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv32-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv32ui/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV32
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv32-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv64i/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV64
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv64-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump

riscv-target/sail-riscv-c/device/rv64im/Makefile.include

@@ -0,0 +1,24 @@
+TARGET_SIM ?= riscv_sim_RV64
+ifeq ($(shell command -v $(TARGET_SIM) 2> /dev/null),)
+    $(error Target simulator executable '$(TARGET_SIM)` not found)
+endif
+
+RUN_TARGET=\
+    $(TARGET_SIM) \
+        --test-signature=$(work_dir_isa)/$(*).signature.output \
+        $(work_dir_isa)/$< 2> $(work_dir_isa)/$@ 1>&2
+
+
+RISCV_PREFIX   ?= riscv64-unknown-elf-
+RISCV_GCC      ?= $(RISCV_PREFIX)gcc
+RISCV_OBJDUMP  ?= $(RISCV_PREFIX)objdump
+RISCV_GCC_OPTS ?= -static -mcmodel=medany -fvisibility=hidden -nostdlib -nostartfiles
+
+COMPILE_TARGET=\
+	$$(RISCV_GCC) $(2) $$(RISCV_GCC_OPTS) \
+		-I$(ROOTDIR)/riscv-test-env/ \
+		-I$(ROOTDIR)/riscv-test-env/p/ \
+		-I$(TARGETDIR)/$(RISCV_TARGET)/ \
+		-T$(ROOTDIR)/riscv-test-env/p/link.ld $$< \
+		-o $(work_dir_isa)/$$@; \
+	$$(RISCV_OBJDUMP) -D $(work_dir_isa)/$$@ > $(work_dir_isa)/$$@.objdump