Merge branch 'riscv:master' into quads

riscv · Apr 15, 2024 · 3607da3 · 3607da3
2 parents 71df5f8 + f1c043d
commit 3607da3
Show file tree

Hide file tree

Showing 6 changed files with 25 additions and 20 deletions.
diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail
@@ -371,6 +371,7 @@ function clause execute(VFUNARY0(vm, vs2, vfunary0, vd)) = {
   let num_elem = get_num_elem(LMUL_pow, SEW);
 
   if illegal_fp_normal(vd, vm, SEW, rm_3b) then { handle_illegal(); return RETIRE_FAIL };
+  assert(SEW != 8);
 
   let 'n = num_elem;
   let 'm = SEW;
@@ -618,6 +619,7 @@ function clause execute(VFNUNARY0(vm, vs2, vfnunary0, vd)) = {
   if  illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_widen, LMUL_pow_widen) |
       not(valid_reg_overlap(vs2, vd, LMUL_pow_widen, LMUL_pow))
   then { handle_illegal(); return RETIRE_FAIL };
+  assert(SEW != 64);
 
   let 'n = num_elem;
   let 'm = SEW;

diff --git a/model/riscv_insts_vext_mem.sail b/model/riscv_insts_vext_mem.sail
@@ -11,7 +11,7 @@
 /* Chapter 7: Vector Loads and Stores                                              */
 /* ******************************************************************************* */
 
-mapping nfields_int : bits(3) <-> {|1, 2, 3, 4, 5, 6, 7, 8|} = {
+mapping nfields_int : bits(3) <-> {1, 2, 3, 4, 5, 6, 7, 8} = {
   0b000     <-> 1,
   0b001     <-> 2,
   0b010     <-> 3,
@@ -47,14 +47,14 @@ mapping encdec_vlewidth : vlewidth <-> bits(3) = {
   VLE64     <-> 0b111
 }
 
-mapping vlewidth_bytesnumber : vlewidth <-> {|1, 2, 4, 8|} = {
+mapping vlewidth_bytesnumber : vlewidth <-> {1, 2, 4, 8} = {
   VLE8      <-> 1,
   VLE16     <-> 2,
   VLE32     <-> 4,
   VLE64     <-> 8
 }
 
-mapping vlewidth_pow : vlewidth <-> {|3, 4, 5, 6|} = {
+mapping vlewidth_pow : vlewidth <-> {3, 4, 5, 6} = {
   VLE8      <-> 3,
   VLE16     <-> 4,
   VLE32     <-> 5,

diff --git a/model/riscv_insts_vext_red.sail b/model/riscv_insts_vext_red.sail
@@ -185,7 +185,8 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
         FVV_VFREDOSUM   => fp_add(rm_3b, sum, vs2_val[i]),
         FVV_VFREDUSUM   => fp_add(rm_3b, sum, vs2_val[i]),
         FVV_VFREDMAX    => fp_max(sum, vs2_val[i]),
-        FVV_VFREDMIN    => fp_min(sum, vs2_val[i])
+        FVV_VFREDMIN    => fp_min(sum, vs2_val[i]),
+        _               => internal_error(__FILE__, __LINE__, "Widening op unexpected")
       }
     }
   };

diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
@@ -45,7 +45,7 @@ function assert_vstart(i) = {
  *  1. Valid element width of floating-point numbers
  *  2. Valid floating-point rounding mode
  */
-val valid_fp_op : ({|8, 16, 32, 64|}, bits(3)) -> bool
+val valid_fp_op : ({8, 16, 32, 64}, bits(3)) -> bool
 function valid_fp_op(SEW, rm_3b) = {
   /* 128-bit floating-point values will be supported in future extensions */
   let valid_sew = (SEW >= 16 & SEW <= 128);
@@ -146,38 +146,38 @@ function illegal_reduction_widen(SEW_widen, LMUL_pow_widen) = {
 }
 
 /* g. Normal check for floating-point instructions */
-val illegal_fp_normal : (regidx, bits(1), {|8, 16, 32, 64|}, bits(3)) -> bool
+val illegal_fp_normal : (regidx, bits(1), {8, 16, 32, 64}, bits(3)) -> bool
 function illegal_fp_normal(vd, vm, SEW, rm_3b) = {
   not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b))
 }
 
 /* h. Masked check for floating-point instructions encoded with vm = 0 */
-val illegal_fp_vd_masked : (regidx, {|8, 16, 32, 64|}, bits(3)) -> bool
+val illegal_fp_vd_masked : (regidx, {8, 16, 32, 64}, bits(3)) -> bool
 function illegal_fp_vd_masked(vd, SEW, rm_3b) = {
   not(valid_vtype()) | vd == 0b00000 | not(valid_fp_op(SEW, rm_3b))
 }
 
 /* i. Unmasked check for floating-point instructions encoded with vm = 1 */
-val illegal_fp_vd_unmasked : ({|8, 16, 32, 64|}, bits(3)) -> bool
+val illegal_fp_vd_unmasked : ({8, 16, 32, 64}, bits(3)) -> bool
 function illegal_fp_vd_unmasked(SEW, rm_3b) = {
   not(valid_vtype()) | not(valid_fp_op(SEW, rm_3b))
 }
 
 /* j. Variable width check for floating-point widening/narrowing instructions */
-val illegal_fp_variable_width : (regidx, bits(1), {|8, 16, 32, 64|}, bits(3), int, int) -> bool
+val illegal_fp_variable_width : (regidx, bits(1), {8, 16, 32, 64}, bits(3), int, int) -> bool
 function illegal_fp_variable_width(vd, vm, SEW, rm_3b, SEW_new, LMUL_pow_new) = {
   not(valid_vtype()) | not(valid_rd_mask(vd, vm)) | not(valid_fp_op(SEW, rm_3b)) |
   not(valid_eew_emul(SEW_new, LMUL_pow_new))
 }
 
 /* k. Normal check for floating-point reduction instructions */
-val illegal_fp_reduction : ({|8, 16, 32, 64|}, bits(3)) -> bool
+val illegal_fp_reduction : ({8, 16, 32, 64}, bits(3)) -> bool
 function illegal_fp_reduction(SEW, rm_3b) = {
   not(valid_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b))
 }
 
 /* l. Variable width check for floating-point widening reduction instructions */
-val illegal_fp_reduction_widen : ({|8, 16, 32, 64|}, bits(3), int, int) -> bool
+val illegal_fp_reduction_widen : ({8, 16, 32, 64}, bits(3), int, int) -> bool
 function illegal_fp_reduction_widen(SEW, rm_3b, SEW_widen, LMUL_pow_widen) = {
   not(valid_vtype()) | not(assert_vstart(0)) | not(valid_fp_op(SEW, rm_3b)) |
   not(valid_eew_emul(SEW_widen, LMUL_pow_widen))

diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail
@@ -849,9 +849,9 @@ 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|}
+val get_sew_pow : unit -> {3, 4, 5, 6}
 function get_sew_pow() = {
-  let SEW_pow : {|3, 4, 5, 6|} = match vtype[vsew] {
+  let SEW_pow : {3, 4, 5, 6} = match vtype[vsew] {
     0b000 => 3,
     0b001 => 4,
     0b010 => 5,
@@ -861,29 +861,31 @@ function get_sew_pow() = {
   SEW_pow
 }
 /* this returns the actual value of SEW */
-val get_sew : unit -> {|8, 16, 32, 64|}
+val get_sew : unit -> {8, 16, 32, 64}
 function get_sew() = {
   match get_sew_pow() {
     3 => 8,
     4 => 16,
     5 => 32,
-    6 => 64
+    6 => 64,
+    _ => {internal_error(__FILE__, __LINE__, "invalid SEW"); 8}
   }
 }
 /* this returns the value of SEW in bytes */
-val get_sew_bytes : unit -> {|1, 2, 4, 8|}
+val get_sew_bytes : unit -> {1, 2, 4, 8}
 function get_sew_bytes() = {
   match get_sew_pow() {
     3 => 1,
     4 => 2,
     5 => 4,
-    6 => 8
+    6 => 8,
+    _ => {internal_error(__FILE__, __LINE__, "invalid SEW"); 1}
   }
 }
 
 /* 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|}
+val get_lmul_pow : unit -> {-3, -2, -1, 0, 1, 2, 3}
 function get_lmul_pow() = {
   match vtype[vlmul] {
     0b101 => -3,

diff --git a/model/riscv_vlen.sail b/model/riscv_vlen.sail
@@ -8,7 +8,7 @@
 
 register elen : bits(1)
 
-val get_elen_pow : unit -> {|5, 6|}
+val get_elen_pow : unit -> {5, 6}
 
 function get_elen_pow() = match elen {
     0b0 => 5,
@@ -21,7 +21,7 @@ function get_elen_pow() = match elen {
 
 register vlen : bits(4)
 
-val get_vlen_pow : unit -> {|5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16|}
+val get_vlen_pow : unit -> {5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16}
 
 function get_vlen_pow() = match vlen {
     0b0000 => 5,