These updates introduce support for the RISC-V Vector Extension.

It is a combination of 16 commits.

V extension general framework and configuration setting instructions (#191)

* V extension general framework and configuration setting instructions

* Update model/riscv_insts_vext_utils.sail

fix a typo

Co-authored-by: Nicolas Brunie <[email protected]>
Signed-off-by: BrighterW <[email protected]>

* Update model/riscv_insts_vext_vset.sail

* Revisions after Nov 22 meeting

* Update effect matching for functions in riscv_vlen.sail

* Fix code formatting issues

* Update model/riscv_insts_vext_utils.sail

Co-authored-by: Jessica Clarke <[email protected]>
Signed-off-by: Xinlai Wan <[email protected]>

* Fix coding style issues

* Update vset instructions

Signed-off-by: BrighterW <[email protected]>
Signed-off-by: Xinlai Wan <[email protected]>
Co-authored-by: Nicolas Brunie <[email protected]>
Co-authored-by: Jessica Clarke <[email protected]>

Vector load / store instructions (#198)

* Add vector load / store instructions

* Modify the implementation of SEW, LMUL, VLEN and avoid real numbers in the code

* Update vstart setting in vector load / store instructions

* Remove unnecessary assert statements in vector instructions

* Fix bugs in vleff instructions and revise coding styles

* Add guards for vector encdec clauses, Avoid redundant memory access after vector load/store failure

Vector integer/fixed-point arithmetic & mask instructions (#227)

* Add vector arithmetic & mask instructions

* Update vector EEW and EMUL checking function

* Add vector instruction illegal check functions

* Adjust code formatting for vector instruction illegal check functions

Merge approved by team at tech-golden-model meeting on 2023-03-14.

Vector floating-point instructions (#232)

* Add vector floating-point instructions

* Update vector floating-point conversion instructions

* Update copyright headers for vector extension code

---------

Co-authored-by: xwan <[email protected]>

Vector reduction and mask instructions (#259)

* Add vector mask and reduction instructions

* Fix register overlap check in vector mask instructions

---------

Co-authored-by: xwan <[email protected]>

update vector CSR vtype.vill setting and judgement

Summarize patterns of vector illegal instruction check

Fix issues in vector load/store and reduction operations

Clean up the V extension code and vector floating-point functions

Clean up the softfloat makefiles

Rename EXTZ and EXTS in the V extension code

Fix an issue in the V extension code for clang-format check

Fix NaN boxing issue and add notes for RVV configuration TODOs

Add default VLEN value and set vlenb CSR

Add constraints for vector variable initialization

Add mstatus.VS setting code for vector extension

Makefile

@@ -16,6 +16,7 @@ else
 endif
 
 SAIL_FLEN := riscv_flen_D.sail
+SAIL_VLEN := riscv_vlen.sail
 
 # Instruction sources, depending on target
 SAIL_CHECK_SRCS = riscv_addr_checks_common.sail riscv_addr_checks.sail riscv_misa_ext.sail
@@ -41,6 +42,15 @@ SAIL_DEFAULT_INST += riscv_insts_zbkx.sail
 
 SAIL_DEFAULT_INST += riscv_insts_zicond.sail
 
+SAIL_DEFAULT_INST += riscv_insts_vext_utils.sail
+SAIL_DEFAULT_INST += riscv_insts_vext_vset.sail
+SAIL_DEFAULT_INST += riscv_insts_vext_arith.sail
+SAIL_DEFAULT_INST += riscv_insts_vext_fp.sail
+SAIL_DEFAULT_INST += riscv_insts_vext_mem.sail
+SAIL_DEFAULT_INST += riscv_insts_vext_mask.sail
+SAIL_DEFAULT_INST += riscv_insts_vext_vm.sail
+SAIL_DEFAULT_INST += riscv_insts_vext_red.sail
+
 SAIL_SEQ_INST  = $(SAIL_DEFAULT_INST) riscv_jalr_seq.sail
 SAIL_RMEM_INST = $(SAIL_DEFAULT_INST) riscv_jalr_rmem.sail riscv_insts_rmem.sail
 
@@ -49,6 +59,7 @@ SAIL_RMEM_INST_SRCS = riscv_insts_begin.sail $(SAIL_RMEM_INST) riscv_insts_end.s
 
 # System and platform sources
 SAIL_SYS_SRCS =  riscv_csr_map.sail
+SAIL_SYS_SRCS += riscv_vext_control.sail    # helpers for the 'V' extension
 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
@@ -68,11 +79,12 @@ SAIL_VM_SRCS += $(SAIL_RV64_VM_SRCS)
 endif
 
 # Non-instruction sources
-PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) $(SAIL_FLEN) prelude_mem_metadata.sail prelude_mem.sail
+PRELUDE = prelude.sail prelude_mapping.sail $(SAIL_XLEN) $(SAIL_FLEN) $(SAIL_VLEN) prelude_mem_metadata.sail prelude_mem.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_REGS_SRCS += riscv_vreg_type.sail riscv_vext_regs.sail
 
 SAIL_ARCH_SRCS = $(PRELUDE)
 SAIL_ARCH_SRCS += riscv_types_common.sail riscv_types_ext.sail riscv_types.sail

c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC/Makefile

@@ -38,6 +38,7 @@ SOURCE_DIR ?= ../../source
 SPECIALIZE_TYPE ?= RISCV
 
 SOFTFLOAT_OPTS ?= \
+  -DSOFTFLOAT_ROUND_ODD
 
 
 DELETE = rm -f

c_emulator/riscv_platform.c

@@ -37,6 +37,11 @@ bool sys_enable_zfinx(unit u)
   return rv_enable_zfinx;
 }
 
+bool sys_enable_vext(unit u)
+{
+  return rv_enable_vext;
+}
+
 bool sys_enable_writable_misa(unit u)
 {
   return rv_enable_writable_misa;

c_emulator/riscv_platform.h

@@ -6,6 +6,7 @@ bool sys_enable_next(unit);
 bool sys_enable_fdext(unit);
 bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);
+bool sys_enable_vext(unit);
 
 bool plat_enable_dirty_update(unit);
 bool plat_enable_misaligned_access(unit);

c_emulator/riscv_platform_impl.c

@@ -9,6 +9,7 @@ bool rv_enable_rvc = true;
 bool rv_enable_next = false;
 bool rv_enable_writable_misa = true;
 bool rv_enable_fdext = true;
+bool rv_enable_vext = true;
 
 bool rv_enable_dirty_update = false;
 bool rv_enable_misaligned = false;

c_emulator/riscv_platform_impl.h

@@ -12,6 +12,7 @@ extern bool rv_enable_zfinx;
 extern bool rv_enable_rvc;
 extern bool rv_enable_next;
 extern bool rv_enable_fdext;
+extern bool rv_enable_vext;
 extern bool rv_enable_writable_misa;
 extern bool rv_enable_dirty_update;
 extern bool rv_enable_misaligned;

c_emulator/riscv_sim.c

@@ -231,6 +231,7 @@ char *process_args(int argc, char **argv)
                     "N"
                     "I"
                     "F"
+                    "W"
                     "i"
                     "s"
                     "p"
@@ -285,6 +286,10 @@ char *process_args(int argc, char **argv)
       fprintf(stderr, "disabling floating point (F and D extensions).\n");
       rv_enable_fdext = false;
       break;
+    case 'W':
+      fprintf(stderr, "disabling RVV vector instructions.\n");
+      rv_enable_vext = false;
+      break;
     case 'i':
       fprintf(stderr, "enabling storing illegal instruction bits in mtval.\n");
       rv_mtval_has_illegal_inst_bits = true;

handwritten_support/riscv_extras_fdext.lem

@@ -234,6 +234,9 @@ let softfloat_f64_to_f32 _ _ = ()
 val softfloat_f16_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
 let softfloat_f16_lt _ _ = ()
 
+val softfloat_f16_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f16_lt_quiet _ _ = ()
+
 val softfloat_f16_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
 let softfloat_f16_le _ _ = ()
 
@@ -243,6 +246,9 @@ let softfloat_f16_eq _ _ = ()
 val softfloat_f32_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
 let softfloat_f32_lt _ _ = ()
 
+val softfloat_f32_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f32_lt_quiet _ _ = ()
+
 val softfloat_f32_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
 let softfloat_f32_le _ _ = ()
 
@@ -252,6 +258,9 @@ let softfloat_f32_eq _ _ = ()
 val softfloat_f64_lt : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
 let softfloat_f64_lt _ _ = ()
 
+val softfloat_f64_lt_quiet : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
+let softfloat_f64_lt_quiet _ _ = ()
+
 val softfloat_f64_le : forall 's. Size 's => bitvector 's -> bitvector 's -> unit
 let softfloat_f64_le _ _ = ()
 

model/prelude.sail

@@ -200,8 +200,11 @@ overload zeros = {zeros_implicit}
 val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
 function ones (n) = sail_ones (n)
 
+val bool_to_bit : bool -> bit
+function bool_to_bit x = if x then bitone else bitzero
+
 val bool_to_bits : bool -> bits(1)
-function bool_to_bits x = if x then 0b1 else 0b0
+function bool_to_bits x = [bool_to_bit(x)]
 
 val bit_to_bool : bit -> bool
 function bit_to_bool b = match b {
@@ -329,3 +332,26 @@ val def_spc_backwards : string -> unit
 function def_spc_backwards s = ()
 val def_spc_matches_prefix : string -> option((unit, nat))
 function def_spc_matches_prefix s = opt_spc_matches_prefix(s)
+
+val "print_int" : (string, int) -> unit
+
+overload operator / = {quot_round_zero}
+overload operator * = {mult_atom, mult_int}
+
+/* helper for vector extension
+ * 1. EEW between 8 and 64
+ * 2. EMUL in vmv<nr>r.v instructions between 1 and 8
+ */
+val log2 : forall 'n, 'n in {1, 2, 4, 8, 16, 32, 64}. int('n) -> int
+function log2(n) = {
+  let result : int = match n {
+    1    => 0,
+    2    => 1,
+    4    => 2,
+    8    => 3,
+    16   => 4,
+    32   => 5,
+    64   => 6
+  };
+  result
+}

model/riscv_csr_map.sail

@@ -165,6 +165,14 @@ mapping clause csr_name_map = 0x7a0  <-> "tselect"
 mapping clause csr_name_map = 0x7a1  <-> "tdata1"
 mapping clause csr_name_map = 0x7a2  <-> "tdata2"
 mapping clause csr_name_map = 0x7a3  <-> "tdata3"
+/* vector csrs */
+mapping clause csr_name_map = 0x008  <-> "vstart"
+mapping clause csr_name_map = 0x009  <-> "vxsat"
+mapping clause csr_name_map = 0x00A  <-> "vxrm"
+mapping clause csr_name_map = 0x00F  <-> "vcsr"
+mapping clause csr_name_map = 0xC20  <-> "vl"
+mapping clause csr_name_map = 0xC21  <-> "vtype"
+mapping clause csr_name_map = 0xC22  <-> "vlenb"
 
 val csr_name : csreg -> string
 overload to_str = {csr_name}