Replace vxrm/vxsat with vcsr[vxrm/vxsat]

Move all the vector CSR access code to `riscv_vext_control.sail`, remove the duplicate clauses and remove the unnecessary `vxrm`/`vxsat` registers in favour of the fields in `vcsr`.

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

model/riscv_insts_vext_utils.sail

@@ -399,7 +399,7 @@ val get_fixed_rounding_incr : forall ('m 'n : Int), ('m > 0 & 'n >= 0). (bits('m
 function get_fixed_rounding_incr(vec_elem, shift_amount) = {
   if shift_amount == 0 then 0b0
   else {
-    let rounding_mode = vxrm[1 .. 0];
+    let rounding_mode = vcsr[vxrm];
     match rounding_mode {
       0b00 => slice(vec_elem, shift_amount - 1, 1),
       0b01 => bool_to_bits(
@@ -415,10 +415,10 @@ function get_fixed_rounding_incr(vec_elem, shift_amount) = {
 val unsigned_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m)
 function unsigned_saturation(len, elem) = {
   if unsigned(elem) > unsigned(ones('m)) then {
-    vxsat = 0b1;
+    vcsr[vxsat] = 0b1;
     ones('m)
   } else {
-    vxsat = 0b0;
+    vcsr[vxsat] = 0b0;
     elem['m - 1 .. 0]
   }
 }
@@ -427,13 +427,13 @@ function unsigned_saturation(len, elem) = {
 val signed_saturation : forall ('m 'n: Int), ('n >= 'm > 1). (int('m), bits('n)) -> bits('m)
 function signed_saturation(len, elem) = {
   if signed(elem) > signed(0b0 @ ones('m - 1)) then {
-    vxsat = 0b1;
+    vcsr[vxsat] = 0b1;
     0b0 @ ones('m - 1)
   } else if signed(elem) < signed(0b1 @ zeros('m - 1)) then {
-    vxsat = 0b1;
+    vcsr[vxsat] = 0b1;
     0b1 @ zeros('m - 1)
   } else {
-    vxsat = 0b0;
+    vcsr[vxsat] = 0b0;
     elem['m - 1 .. 0]
   };
 }

model/riscv_insts_zicsr.sail

@@ -69,15 +69,6 @@ function clause read_CSR(0xB82 if xlen == 32) = minstret[63 .. 32]
 function clause read_CSR(0b1011000 /* 0xB00 */ @ index : bits(5) if unsigned(index) >= 3) = read_mhpmcounter(hpmidx_from_bits(index))
 function clause read_CSR(0b1011100 /* 0xB80 */ @ index : bits(5) if xlen == 32 & unsigned(index) >= 3) = read_mhpmcounterh(hpmidx_from_bits(index))
 
-/* vector */
-function clause read_CSR(0x008) = zero_extend(vstart)
-function clause read_CSR(0x009) = zero_extend(vxsat)
-function clause read_CSR(0x00A) = zero_extend(vxrm)
-function clause read_CSR(0x00F) = zero_extend(vcsr.bits)
-function clause read_CSR(0xC20) = vl
-function clause read_CSR(0xC21) = vtype.bits
-function clause read_CSR(0xC22) = vlenb
-
 /* trigger/debug */
 function clause read_CSR(0x7a0) = ~(tselect)  /* this indicates we don't have any trigger support */
 
@@ -187,15 +178,6 @@ function clause write_CSR(0x180, value) = { satp = legalize_satp(cur_Architectur
 /* user mode: seed (entropy source). writes are ignored */
 function clause write_CSR(0x015, value) = write_seed_csr()
 
-/* vector */
-function clause write_CSR(0x008, value) = { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); zero_extend(vstart) }
-function clause write_CSR(0x009, value) = { vxsat = value[0 .. 0]; zero_extend(vxsat) }
-function clause write_CSR(0x00A, value) = { vxrm = value[1 .. 0]; zero_extend(vxrm) }
-function clause write_CSR(0x00F, value) = { vcsr.bits = value[2 ..0]; zero_extend(vcsr.bits) }
-function clause write_CSR(0xC20, value) = { vl = value; vl }
-function clause write_CSR(0xC21, value) = { vtype.bits = value; vtype.bits }
-function clause write_CSR(0xC22, value) = { vlenb = value; vlenb }
-
 function clause execute CSR(csr, rs1, rd, is_imm, op) = {
   let rs1_val : xlenbits = if is_imm then zero_extend(rs1) else X(rs1);
   let isWrite : bool = match op {

model/riscv_sys_control.sail

@@ -557,11 +557,9 @@ function init_sys() -> unit = {
    * See riscv_vlen.sail for details.
    */
   vstart             = zero_extend(0b0);
-  vxsat              = 0b0;
-  vxrm               = 0b00;
-  vcsr[vxrm]       = vxrm;
-  vcsr[vxsat]      = vxsat;
   vl                 = zero_extend(0b0);
+  vcsr[vxrm]       = 0b00;
+  vcsr[vxsat]      = 0b0;
   vtype[vill]      = 0b1;
   vtype[reserved]  = zero_extend(0b0);
   vtype[vma]       = 0b0;

model/riscv_sys_regs.sail

@@ -856,8 +856,6 @@ function is_fiom_active() -> bool = {
 }
 /* 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
 

model/riscv_vext_control.sail

@@ -7,22 +7,25 @@
 /*=======================================================================================*/
 
 function clause is_CSR_defined (0x008) = true
-function clause is_CSR_defined (0xC20) = true
-function clause is_CSR_defined (0xC21) = true
-function clause is_CSR_defined (0xC22) = true
-
 function clause is_CSR_defined (0x009) = true
 function clause is_CSR_defined (0x00A) = true
 function clause is_CSR_defined (0x00F) = true
+function clause is_CSR_defined (0xC20) = true
+function clause is_CSR_defined (0xC21) = true
+function clause is_CSR_defined (0xC22) = true
 
-function clause read_CSR (0x009) = zero_extend(vcsr[vxsat])
-function clause read_CSR (0x00A) = zero_extend(vcsr[vxrm])
-function clause read_CSR (0x00F) = zero_extend(vcsr.bits)
-
-function clause read_CSR (0x009) = zero_extend(vcsr[vxsat])
-function clause read_CSR (0x00A) = zero_extend(vcsr[vxrm])
-function clause read_CSR (0x00F) = zero_extend(vcsr.bits)
+function clause read_CSR(0x008) = zero_extend(vstart)
+function clause read_CSR(0x009) = zero_extend(vcsr[vxsat])
+function clause read_CSR(0x00A) = zero_extend(vcsr[vxrm])
+function clause read_CSR(0x00F) = zero_extend(vcsr.bits)
+function clause read_CSR(0xC20) = vl
+function clause read_CSR(0xC21) = vtype.bits
+function clause read_CSR(0xC22) = vlenb
 
-function clause write_CSR (0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); zero_extend(vcsr[vxsat]) }
-function clause write_CSR (0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); zero_extend(vcsr[vxrm]) }
-function clause write_CSR (0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); zero_extend(vcsr.bits) }
+function clause write_CSR(0x008, value) = { let vstart_length = get_vlen_pow(); vstart = zero_extend(16, value[(vstart_length - 1) .. 0]); zero_extend(vstart) }
+function clause write_CSR(0x009, value) = { ext_write_vcsr (vcsr[vxrm], value[0 .. 0]); zero_extend(vcsr[vxsat]) }
+function clause write_CSR(0x00A, value) = { ext_write_vcsr (value[1 .. 0], vcsr[vxsat]); zero_extend(vcsr[vxrm]) }
+function clause write_CSR(0x00F, value) = { ext_write_vcsr (value [2 .. 1], value [0 .. 0]); zero_extend(vcsr.bits) }
+function clause write_CSR(0xC20, value) = { vl = value; vl }
+function clause write_CSR(0xC21, value) = { vtype.bits = value; vtype.bits }
+function clause write_CSR(0xC22, value) = { vlenb = value; vlenb }