RISC-V Vector Extension Support

This PR adds the following:

General Framework and Configurations:

* Introduced the V extension's general framework and configuration setting instructions.
* Updated model/riscv_insts_vext_vset.sail and effect matching functions in riscv_vlen.sail.
* Addressed code formatting issues and made revisions post the Nov 22 meeting.
* Co-authored by Nicolas Brunie and Jessica Clarke.

Vector Load/Store Instructions:

* Integrated vector load and store instructions.
* Enhanced the implementation of SEW, LMUL, VLEN and removed real numbers from the code.
* Updated vstart settings and removed unnecessary assert statements.
* Rectified bugs in vleff instructions and overhauled coding styles.
* Incorporated guards for vector encdec clauses and optimized memory access post vector load/store failures.

Vector Integer/Fixed-Point Instructions:

* Added vector integer/fixed-point arithmetic and mask instructions.
* Improved vector EEW and EMUL checking functions and introduced illegal instruction check functions.
* Fine-tuned code formatting for vector instruction checks.

Vector Floating-Point Instructions:

* Rolled out vector floating-point instructions and updated their conversion counterparts.
* Refreshed copyright headers specific to the vector extension code.

Vector Reduction and Mask Instructions:

* Integrated vector mask and reduction instructions.
* Addressed register overlap checks for vector mask instructions.

Miscellaneous Enhancements and Fixes:

* Updated vector CSR vtype.vill settings and judgements.
* Systematized patterns for vector illegal instruction checks.
* Rectified issues in vector load/store and reduction operations.
* Purged redundant elements from the V extension code and vector floating-point functions.
* Cleaned up softfloat makefiles and renamed EXTZ and EXTS within the V extension code.
* Addressed a clang-format check issue and NaN boxing anomalies. Provided annotations for pending RVV configurations.
* Initialized default VLEN value and set vlenb CSR.
* Set constraints for vector variable initialization and added mstatus.VS settings specific to the 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

@@ -42,6 +42,11 @@ bool sys_enable_writable_fiom(unit u)
   return rv_enable_writable_fiom;
 }
 
+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

@@ -7,6 +7,7 @@ bool sys_enable_fdext(unit);
 bool sys_enable_zfinx(unit);
 bool sys_enable_writable_misa(unit);
 bool sys_enable_writable_fiom(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

@@ -13,6 +13,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

@@ -246,6 +246,7 @@ static int process_args(int argc, char **argv)
                     "N"
                     "I"
                     "F"
+                    "W"
                     "i"
                     "s"
                     "p"
@@ -300,6 +301,10 @@ static int 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

@@ -198,8 +198,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 {
@@ -327,3 +330,24 @@ 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)
+
+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}