RISC-V Vector Extension Supportvector-dev

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.

1 files changed, 95 insertions, 3 deletions

diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
index 81a6c76..f472ca2 100644
--- a/model/riscv_sys_regs.sail
+++ b/model/riscv_sys_regs.sail
@@ -153,6 +153,8 @@ val sys_enable_next = {c: "sys_enable_next", ocaml: "Platform.enable_next", _: "
 /* Whether FIOM bit of menvcfg/senvcfg is enabled. It must be enabled if
    supervisor mode is implemented and non-bare addressing modes are supported. */
 val sys_enable_writable_fiom = {c: "sys_enable_writable_fiom", ocaml: "Platform.enable_writable_fiom", _: "sys_enable_writable_fiom"} : unit -> bool
+/* whether misa.v was enabled at boot */
+val sys_enable_vext = {c: "sys_enable_vext", ocaml: "Platform.enable_vext", _: "sys_enable_vext"} : unit -> bool
 
 /* This function allows an extension to veto a write to Misa
    if it would violate an alignment restriction on
@@ -244,6 +246,7 @@ bitfield Mstatus : xlenbits = {
   FS   : 14 .. 13,
 
   MPP  : 12 .. 11,
+  VS   : 10 .. 9,
   SPP  : 8,
 
   MPIE : 7,
@@ -297,7 +300,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
    * that does not have a matching bitfield entry. All bits above 32 are handled
    * explicitly later.
    */
-  let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 11] @ 0b00 @ v[8 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0]));
+  let m : Mstatus = Mk_Mstatus(zero_extend(v[22 .. 7] @ 0b0 @ v[5 .. 3] @ 0b0 @ v[1 .. 0]));
 
   /* We don't have any extension context yet. */
   let m = update_XS(m, extStatus_to_bits(Off));
@@ -308,7 +311,8 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = {
    * FIXME: This should be made a platform parameter.
    */
   let m = if sys_enable_zfinx() then update_FS(m, extStatus_to_bits(Off)) else m;
-  let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
+  let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty |
+              extStatus_of_bits(m.VS()) == Dirty;
   let m = update_SD(m, bool_to_bits(dirty));
 
   /* We don't support dynamic changes to SXL and UXL. */
@@ -357,6 +361,8 @@ function haveFExt()    -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00)
 function haveDExt()    -> bool = (misa.D() == 0b1) & (mstatus.FS() != 0b00)
 /* Zfh (half-precision) extension depends on misa.F and mstatus.FS */
 function haveZfh()     -> bool = (misa.F() == 0b1) & (mstatus.FS() != 0b00)
+/* V extension has to enable both via misa.V as well as mstatus.VS */
+function haveVExt()    -> bool = (misa.V() == 0b1) & (mstatus.VS() != 0b00)
 
 /* Zhinx, Zfinx and Zdinx extensions (TODO: gate FCSR access on [mhs]stateen0 bit 1 when implemented) */
 function haveZhinx()   -> bool = sys_enable_zfinx()
@@ -592,6 +598,7 @@ bitfield Sstatus : xlenbits = {
   SUM  : 18,
   XS   : 16 .. 15,
   FS   : 14 .. 13,
+  VS   : 10 .. 9,
   SPP  : 8,
   SPIE : 5,
   UPIE : 4,
@@ -619,6 +626,7 @@ function lower_mstatus(m : Mstatus) -> Sstatus = {
   let s = update_SUM(s, m.SUM());
   let s = update_XS(s, m.XS());
   let s = update_FS(s, m.FS());
+  let s = update_VS(s, m.VS());
   let s = update_SPP(s, m.SPP());
   let s = update_SPIE(s, m.SPIE());
   let s = update_UPIE(s, m.UPIE());
@@ -634,7 +642,9 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = {
   let m = update_XS(m, s.XS());
   // See comment for mstatus.FS.
   let m = update_FS(m, s.FS());
-  let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty;
+  let m = update_VS(m, s.VS());
+  let dirty = extStatus_of_bits(m.FS()) == Dirty | extStatus_of_bits(m.XS()) == Dirty |
+              extStatus_of_bits(m.VS()) == Dirty;
   let m = update_SD(m, bool_to_bits(dirty));
 
   let m = update_SPP(m, s.SPP());
@@ -872,3 +882,85 @@ function is_fiom_active() -> bool = {
     User => (menvcfg.FIOM() | senvcfg.FIOM()) == 0b1,
   }
 }
+/* vector csrs */
+register vstart : bits(16) /* use the largest possible length of vstart */
+register vxsat  : bits(1)
+register vxrm   : bits(2)
+register vl     : xlenbits
+register vlenb  : xlenbits
+
+bitfield Vtype  : xlenbits = {
+  vill      : xlen - 1,
+  reserved  : xlen - 2 .. 8,
+  vma       : 7,
+  vta       : 6,
+  vsew      : 5 .. 3,
+  vlmul     : 2 .. 0
+}
+register vtype : Vtype
+
+/* the dynamic selected element width (SEW) */
+/* this returns the power of 2 for SEW */
+val get_sew_pow : unit -> {|3, 4, 5, 6|} effect {escape, rreg}
+function get_sew_pow() = {
+  let SEW_pow : {|3, 4, 5, 6|} = match vtype.vsew() {
+    0b000 => 3,
+    0b001 => 4,
+    0b010 => 5,
+    0b011 => 6,
+    _     => {assert(false, "invalid vsew field in vtype"); 0}
+  };
+  SEW_pow
+}
+/* this returns the actual value of SEW */
+val get_sew : unit -> {|8, 16, 32, 64|} effect {escape, rreg}
+function get_sew() = {
+  match get_sew_pow() {
+    3 => 8,
+    4 => 16,
+    5 => 32,
+    6 => 64
+  }
+}
+/* this returns the value of SEW in bytes */
+val get_sew_bytes : unit -> {|1, 2, 4, 8|} effect {escape, rreg}
+function get_sew_bytes() = {
+  match get_sew_pow() {
+    3 => 1,
+    4 => 2,
+    5 => 4,
+    6 => 8
+  }
+}
+
+/* the vector register group multiplier (LMUL) */
+/* this returns the power of 2 for LMUL */
+val get_lmul_pow : unit -> {|-3, -2, -1, 0, 1, 2, 3|} effect {escape, rreg}
+function get_lmul_pow() = {
+  match vtype.vlmul() {
+    0b101 => -3,
+    0b110 => -2,
+    0b111 => -1,
+    0b000 => 0,
+    0b001 => 1,
+    0b010 => 2,
+    0b011 => 3,
+    _     => {assert(false, "invalid vlmul field in vtype"); 0}
+  }
+}
+
+enum agtype = { UNDISTURBED, AGNOSTIC }
+
+val decode_agtype : bits(1) -> agtype
+function decode_agtype(ag) = {
+  match ag {
+    0b0 => UNDISTURBED,
+    0b1 => AGNOSTIC
+  }
+}
+
+val get_vtype_vma : unit -> agtype effect {rreg}
+function get_vtype_vma() = decode_agtype(vtype.vma())
+
+val get_vtype_vta : unit -> agtype effect {rreg}
+function get_vtype_vta() = decode_agtype(vtype.vta())