diff --git a/model/riscv_insts_vext_fp.sail b/model/riscv_insts_vext_fp.sail index 5c8e4c02d..0b36b01b6 100755 --- 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 index 0f1dfeecf..ce9cd6237 100644 --- 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 index 3feb97a00..358836b02 100755 --- 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 index 52b7c647e..6796060e1 100755 --- 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 index 3e730202b..d8309ecc4 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -844,9 +844,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, @@ -856,29 +856,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 index 3a2e0ac6a..5e4529017 100644 --- 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,