Use bool <-> bit mappings from riscv_types.sail everywhere

A minor refactor to use these mapping types everywhere instead of functions.
riscv · May 14, 2024 · de9c52c · de9c52c
1 parent e1242d8
commit de9c52c
Show file tree

Hide file tree

Showing 17 changed files with 83 additions and 90 deletions.
diff --git a/model/prelude.sail b/model/prelude.sail
@@ -100,16 +100,19 @@ overload zeros = {zeros_implicit}
 val ones : forall 'n, 'n >= 0 . implicit('n) -> bits('n)
 function ones (n) = sail_ones (n)
 
-val bool_to_bit : bool -> bit
-function bool_to_bit x = if x then bitone else bitzero
+mapping bool_bit : bool <-> bit = {
+ true <-> bitone,
+ false <-> bitzero,
+}
 
-val bool_to_bits : bool -> bits(1)
-function bool_to_bits x = [bool_to_bit(x)]
+mapping bool_bits : bool <-> bits(1) = {
+ true <-> 0b1,
+ false <-> 0b0,
+}
 
-val bit_to_bool : bit -> bool
-function bit_to_bool b = match b {
- bitone => true,
- bitzero => false
+mapping bool_not_bits : bool <-> bits(1) = {
+ true <-> 0b0,
+ false <-> 0b1,
 }
 
 val to_bits : forall 'l, 'l >= 0.(int('l), int) -> bits('l)

diff --git a/model/riscv_insts_base.sail b/model/riscv_insts_base.sail
@@ -67,7 +67,7 @@ function clause execute (RISCV_JAL(imm, rd)) = {
  },
  Ext_ControlAddr_OK(target) => {
  /* Perform standard alignment check */
- if bit_to_bool(target[1]) & not(haveRVC())
+ if bool_bit(target[1]) & not(haveRVC())
  then {
  handle_mem_exception(target, E_Fetch_Addr_Align());
  RETIRE_FAIL
@@ -131,7 +131,7 @@ function clause execute (BTYPE(imm, rs2, rs1, op)) = {
  RETIRE_FAIL
  },
  Ext_ControlAddr_OK(target) => {
- if bit_to_bool(target[1]) & not(haveRVC()) then {
+ if bool_bit(target[1]) & not(haveRVC()) then {
  handle_mem_exception(target, E_Fetch_Addr_Align());
  RETIRE_FAIL;
  } else {
@@ -175,8 +175,8 @@ function clause execute (ITYPE (imm, rs1, rd, op)) = {
  let immext : xlenbits = sign_extend(imm);
  let result : xlenbits = match op {
  RISCV_ADDI => rs1_val + immext,
- RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)),
- RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)),
+ RISCV_SLTI => zero_extend(bool_bits(rs1_val <_s immext)),
+ RISCV_SLTIU => zero_extend(bool_bits(rs1_val <_u immext)),
  RISCV_ANDI => rs1_val & immext,
  RISCV_ORI => rs1_val | immext,
  RISCV_XORI => rs1_val ^ immext
@@ -256,8 +256,8 @@ function clause execute (RTYPE(rs2, rs1, rd, op)) = {
  let rs2_val = X(rs2);
  let result : xlenbits = match op {
  RISCV_ADD => rs1_val + rs2_val,
- RISCV_SLT => zero_extend(bool_to_bits(rs1_val <_s rs2_val)),
- RISCV_SLTU => zero_extend(bool_to_bits(rs1_val <_u rs2_val)),
+ RISCV_SLT => zero_extend(bool_bits(rs1_val <_s rs2_val)),
+ RISCV_SLTU => zero_extend(bool_bits(rs1_val <_u rs2_val)),
  RISCV_AND => rs1_val & rs2_val,
  RISCV_OR => rs1_val | rs2_val,
  RISCV_XOR => rs1_val ^ rs2_val,

diff --git a/model/riscv_insts_dext.sail b/model/riscv_insts_dext.sail
@@ -801,7 +801,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FEQ_D)) = {
  riscv_f64Eq (rs1_val_D, rs2_val_D);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -813,7 +813,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLT_D)) = {
  riscv_f64Lt (rs1_val_D, rs2_val_D);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -825,7 +825,7 @@ function clause execute (F_BIN_TYPE_D(rs2, rs1, rd, FLE_D)) = {
  riscv_f64Le (rs1_val_D, rs2_val_D);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 

diff --git a/model/riscv_insts_fext.sail b/model/riscv_insts_fext.sail
@@ -925,7 +925,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FEQ_S)) = {
  riscv_f32Eq (rs1_val_S, rs2_val_S);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -937,7 +937,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLT_S)) = {
  riscv_f32Lt (rs1_val_S, rs2_val_S);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -949,7 +949,7 @@ function clause execute (F_BIN_TYPE_S(rs2, rs1, rd, FLE_S)) = {
  riscv_f32Le (rs1_val_S, rs2_val_S);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 

diff --git a/model/riscv_insts_vext_utils.sail b/model/riscv_insts_vext_utils.sail
@@ -574,10 +574,10 @@ function get_fixed_rounding_incr(vec_elem, shift_amount) = {
  let rounding_mode = vxrm[1 .. 0];
  match rounding_mode {
  0b00 => slice(vec_elem, shift_amount - 1, 1),
- 0b01 => bool_to_bits(
+ 0b01 => bool_bits(
  (slice(vec_elem, shift_amount - 1, 1) == 0b1) & (slice(vec_elem, 0, shift_amount - 1) != zeros() | slice(vec_elem, shift_amount, 1) == 0b1)),
  0b10 => 0b0,
- 0b11 => bool_to_bits(
+ 0b11 => bool_bits(
  not(slice(vec_elem, shift_amount, 1) == 0b1) & (slice(vec_elem, 0, shift_amount) != zeros()))
  }
  }

diff --git a/model/riscv_insts_vext_vm.sail b/model/riscv_insts_vext_vm.sail
@@ -47,8 +47,8 @@ function clause execute(VVMTYPE(funct6, vs2, vs1, vd)) = {
  foreach (i from 0 to (num_elem - 1)) {
  if mask[i] then {
  let res : bool = match funct6 {
- VVM_VMADC => unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1,
- VVM_VMSBC => unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_to_bits(vm_val[i])) < 0
+ VVM_VMADC => unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_bits(vm_val[i])) > 2 ^ SEW - 1,
+ VVM_VMSBC => unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_bits(vm_val[i])) < 0
  };
  result[i] = res
  }
@@ -164,8 +164,8 @@ function clause execute(VVMSTYPE(funct6, vs2, vs1, vd)) = {
  foreach (i from 0 to (num_elem - 1)) {
  if mask[i] then {
  result[i] = match funct6 {
- VVMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_to_bits(vm_val[i]))),
- VVMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_to_bits(vm_val[i])))
+ VVMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(vs1_val[i]) + unsigned(bool_bits(vm_val[i]))),
+ VVMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(vs1_val[i]) - unsigned(bool_bits(vm_val[i])))
  }
  }
  };
@@ -285,8 +285,8 @@ function clause execute(VXMTYPE(funct6, vs2, rs1, vd)) = {
  foreach (i from 0 to (num_elem - 1)) {
  if mask[i] then {
  let res : bool = match funct6 {
- VXM_VMADC => unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1,
- VXM_VMSBC => unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_to_bits(vm_val[i])) < 0
+ VXM_VMADC => unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_bits(vm_val[i])) > 2 ^ SEW - 1,
+ VXM_VMSBC => unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_bits(vm_val[i])) < 0
  };
  result[i] = res
  }
@@ -402,8 +402,8 @@ function clause execute(VXMSTYPE(funct6, vs2, rs1, vd)) = {
  foreach (i from 0 to (num_elem - 1)) {
  if mask[i] then {
  result[i] = match funct6 {
- VXMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_to_bits(vm_val[i]))),
- VXMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_to_bits(vm_val[i])))
+ VXMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(rs1_val) + unsigned(bool_bits(vm_val[i]))),
+ VXMS_VSBC => to_bits(SEW, unsigned(vs2_val[i]) - unsigned(rs1_val) - unsigned(bool_bits(vm_val[i])))
  }
  }
  };
@@ -528,7 +528,7 @@ function clause execute(VIMTYPE(funct6, vs2, simm, vd)) = {
  foreach (i from 0 to (num_elem - 1)) {
  if mask[i] then {
  let res : bool = match funct6 {
- VIM_VMADC => unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_to_bits(vm_val[i])) > 2 ^ SEW - 1
+ VIM_VMADC => unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_bits(vm_val[i])) > 2 ^ SEW - 1
  };
  result[i] = res
  }
@@ -639,7 +639,7 @@ function clause execute(VIMSTYPE(funct6, vs2, simm, vd)) = {
  foreach (i from 0 to (num_elem - 1)) {
  if mask[i] then {
  result[i] = match funct6 {
- VIMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_to_bits(vm_val[i])))
+ VIMS_VADC => to_bits(SEW, unsigned(vs2_val[i]) + unsigned(imm_val) + unsigned(bool_bits(vm_val[i])))
  }
  }
  };

diff --git a/model/riscv_insts_zbs.sail b/model/riscv_insts_zbs.sail
@@ -38,7 +38,7 @@ function clause execute (ZBS_IOP(shamt, rs1, rd, op)) = {
  else zero_extend(0b1) << shamt;
  let result : xlenbits = match op {
  RISCV_BCLRI => rs1_val & ~(mask),
- RISCV_BEXTI => zero_extend(bool_to_bits((rs1_val & mask) != zeros())),
+ RISCV_BEXTI => zero_extend(bool_bits((rs1_val & mask) != zeros())),
  RISCV_BINVI => rs1_val ^ mask,
  RISCV_BSETI => rs1_val | mask
  };
@@ -79,7 +79,7 @@ function clause execute (ZBS_RTYPE(rs2, rs1, rd, op)) = {
  else zero_extend(0b1) << rs2_val[5..0];
  let result : xlenbits = match op {
  RISCV_BCLR => rs1_val & ~(mask),
- RISCV_BEXT => zero_extend(bool_to_bits((rs1_val & mask) != zeros())),
+ RISCV_BEXT => zero_extend(bool_bits((rs1_val & mask) != zeros())),
  RISCV_BINV => rs1_val ^ mask,
  RISCV_BSET => rs1_val | mask
  };

diff --git a/model/riscv_insts_zfa.sail b/model/riscv_insts_zfa.sail
@@ -566,7 +566,7 @@ function clause execute(RISCV_FLEQ_H(rs2, rs1, rd)) = {
  riscv_f16Le_quiet (rs1_val_H, rs2_val_H);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -590,7 +590,7 @@ function clause execute(RISCV_FLTQ_H(rs2, rs1, rd)) = {
  riscv_f16Lt_quiet (rs1_val_H, rs2_val_H);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -614,7 +614,7 @@ function clause execute(RISCV_FLEQ_S(rs2, rs1, rd)) = {
  riscv_f32Le_quiet (rs1_val_S, rs2_val_S);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -638,7 +638,7 @@ function clause execute(RISCV_FLTQ_S(rs2, rs1, rd)) = {
  riscv_f32Lt_quiet (rs1_val_S, rs2_val_S);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -663,7 +663,7 @@ function clause execute(RISCV_FLEQ_D(rs2, rs1, rd)) = {
  riscv_f64Le_quiet (rs1_val_D, rs2_val_D);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -687,7 +687,7 @@ function clause execute(RISCV_FLTQ_D(rs2, rs1, rd)) = {
  riscv_f64Lt_quiet (rs1_val_D, rs2_val_D);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 

diff --git a/model/riscv_insts_zfh.sail b/model/riscv_insts_zfh.sail
@@ -416,7 +416,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FEQ_H)) = {
  riscv_f16Eq (rs1_val_H, rs2_val_H);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -428,7 +428,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLT_H)) = {
  riscv_f16Lt (rs1_val_H, rs2_val_H);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 
@@ -440,7 +440,7 @@ function clause execute (F_BIN_TYPE_H(rs2, rs1, rd, FLE_H)) = {
  riscv_f16Le (rs1_val_H, rs2_val_H);
 
  accrue_fflags(fflags);
- X(rd) = zero_extend(bool_to_bits(rd_val));
+ X(rd) = zero_extend(bool_bits(rd_val));
  RETIRE_SUCCESS
 }
 

diff --git a/model/riscv_jalr_seq.sail b/model/riscv_jalr_seq.sail
@@ -24,7 +24,7 @@ function clause execute (RISCV_JALR(imm, rs1, rd)) = {
  },
  Ext_ControlAddr_OK(addr) => {
  let target = [addr with 0 = bitzero]; /* clear addr[0] */
- if bit_to_bool(target[1]) & not(haveRVC()) then {
+ if bool_bit(target[1]) & not(haveRVC()) then {
  handle_mem_exception(target, E_Fetch_Addr_Align());
  RETIRE_FAIL
  } else {