make sure vstart is zero when instruction early return

Author: KotorinMinami

model/riscv_insts_vext_fp_red.sail

@@ -32,10 +32,14 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
   let rm_3b = fcsr[FRM];
   let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */
 
-  if illegal_fp_reduction(SEW, rm_3b) then return Illegal_Instruction();
+  if illegal_fp_reduction(SEW, rm_3b) then {
+    return Illegal_Instruction();
+  };
   assert(SEW != 8);
 
-  if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
+  if unsigned(vl) == 0 then {
+    return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
+  };
 
   let 'n = num_elem_vs;
   let 'd = num_elem_vd;
@@ -66,7 +70,7 @@ function process_rfvv_single(funct6, vm, vs2, vs1, vd, num_elem_vs, SEW, LMUL_po
   write_single_element(SEW, 0, vd, sum);
   /* other elements in vd are treated as tail elements, currently remain unchanged */
   /* TODO: configuration support for agnostic behavior */
-  set_vstart(zeros());
+  // illegal_fp_reduction checks vstart == 0, and raises illegal-instruction otherwise.
   RETIRE_SUCCESS
 }
 
@@ -75,12 +79,16 @@ function process_rfvv_widening_reduction(funct6, vm, vs2, vs1, vd, num_elem_vs,
   let rm_3b          = fcsr[FRM];
   let SEW_widen      = SEW * 2;
 
-  if illegal_fp_widening_reduction(SEW, rm_3b, SEW_widen) then return Illegal_Instruction();
+  if illegal_fp_widening_reduction(SEW, rm_3b, SEW_widen) then {
+    return Illegal_Instruction();
+  };
   assert(SEW >= 16 & SEW_widen <= 64);
 
   let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */
 
-  if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
+  if unsigned(vl) == 0 then {
+    return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
+  };
 
   let 'n = num_elem_vs;
   let 'd = num_elem_vd;
@@ -106,7 +114,7 @@ function process_rfvv_widening_reduction(funct6, vm, vs2, vs1, vd, num_elem_vs,
   write_single_element(SEW_widen, 0, vd, sum);
   /* other elements in vd are treated as tail elements, currently remain unchanged */
   /* TODO: configuration support for agnostic behavior */
-  set_vstart(zeros());
+  // illegal_fp_widening_reduction checks vstart == 0, and raises illegal-instruction otherwise.
   RETIRE_SUCCESS
 }
 

model/riscv_insts_vext_red.sail

@@ -28,14 +28,18 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let LMUL_pow = get_lmul_pow();
   let SEW_widen = SEW * 2;
 
-  if illegal_widening_reduction(SEW_widen) then return Illegal_Instruction();
+  if illegal_widening_reduction(SEW_widen) then {
+    return Illegal_Instruction();
+  };
 
   assert(SEW_widen <= 64);
 
   let num_elem_vs = get_num_elem(LMUL_pow, SEW);
   let num_elem_vd = get_num_elem(0, SEW_widen); /* vd regardless of LMUL setting */
 
-  if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
+  if unsigned(vl) == 0 then {
+    return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
+  };
 
   let 'n = num_elem_vs;
   let 'd = num_elem_vd;
@@ -64,7 +68,7 @@ function clause execute(RIVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   write_single_element(SEW_widen, 0, vd, sum);
   /* other elements in vd are treated as tail elements, currently remain unchanged */
   /* TODO: configuration support for agnostic behavior */
-  set_vstart(zeros());
+  // illegal_widening_reduction checks vstart == 0, and raises illegal-instruction otherwise.
   RETIRE_SUCCESS
 }
 
@@ -100,9 +104,13 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   let num_elem_vs = get_num_elem(LMUL_pow, SEW);
   let num_elem_vd = get_num_elem(0, SEW); /* vd regardless of LMUL setting */
 
-  if illegal_reduction() then return Illegal_Instruction();
+  if illegal_reduction() then {
+    return Illegal_Instruction();
+  };
 
-  if unsigned(vl) == 0 then return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
+  if unsigned(vl) == 0 then {
+    return RETIRE_SUCCESS; /* if vl=0, no operation is performed */
+  };
 
   let 'n = num_elem_vs;
   let 'd = num_elem_vd;
@@ -135,7 +143,7 @@ function clause execute(RMVVTYPE(funct6, vm, vs2, vs1, vd)) = {
   write_single_element(SEW, 0, vd, sum);
   /* other elements in vd are treated as tail elements, currently remain unchanged */
   /* TODO: configuration support for agnostic behavior */
-  set_vstart(zeros());
+  // illegal_reduction checks vstart == 0, and raises illegal-instruction otherwise.
   RETIRE_SUCCESS
 }
 

model/riscv_insts_vext_vm.sail

@@ -43,7 +43,7 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = {
 
   let (initial_result, mask) : (bits('n), bits('n)) = match init_masked_result_carry(num_elem, SEW, LMUL_pow, vd_val) {
     Ok(v)   => v,
-    Err(()) => return Illegal_Instruction()
+    Err(()) => return Illegal_Instruction(),
   };
   var result = initial_result;