Replace vxrm/vxsat with vcsr[vxrm/vxsat]HEADmaster

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 <785369607@qq.com>

1 files changed, 6 insertions, 6 deletions

diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
index f71b373..78c445b 100755
--- a/model/riscv_insts_vext_utils.sail
+++ b/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]
   };
 }