diff --git a/model/prelude.sail b/model/prelude.sail index 028af2126..213fc9c50 100644 --- 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 index 9c4630b33..97d5e77c6 100644 --- 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 index 03b582434..d7d396c8b 100644 --- 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 index e4afb30d5..4b9065866 100644 --- 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 index 6796060e1..bd9146aaa 100755 --- 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 index 1f963e771..1506c79ae 100755 --- 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 index b535701c8..a902de5e2 100644 --- 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 index 1443daf3d..ad24e6745 100644 --- 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 index 5522bad22..bbac6881e 100644 --- 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 index 497a44178..ad517a24a 100644 --- 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 { diff --git a/model/riscv_softfloat_interface.sail b/model/riscv_softfloat_interface.sail index 3a673feb8..0d3c1b71f 100644 --- a/model/riscv_softfloat_interface.sail +++ b/model/riscv_softfloat_interface.sail @@ -400,105 +400,105 @@ val extern_f16Lt = {c: "softfloat_f16lt", ocaml: "Softfloat.f16_lt", lem: "s val riscv_f16Lt : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Lt (v1, v2) = { extern_f16Lt(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f16Lt_quiet = {c: "softfloat_f16lt_quiet", ocaml: "Softfloat.f16_lt_quiet", lem: "softfloat_f16_lt_quiet"} : (bits_H, bits_H) -> unit val riscv_f16Lt_quiet : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Lt_quiet (v1, v2) = { extern_f16Lt_quiet(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f16Le = {c: "softfloat_f16le", ocaml: "Softfloat.f16_le", lem: "softfloat_f16_le"} : (bits_H, bits_H) -> unit val riscv_f16Le : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Le (v1, v2) = { extern_f16Le(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f16Le_quiet = {c: "softfloat_f16le_quiet", ocaml: "Softfloat.f16_le_quiet", lem: "softfloat_f16_le_quiet"} : (bits_H, bits_H) -> unit val riscv_f16Le_quiet : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Le_quiet (v1, v2) = { extern_f16Le_quiet(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f16Eq = {c: "softfloat_f16eq", ocaml: "Softfloat.f16_eq", lem: "softfloat_f16_eq"} : (bits_H, bits_H) -> unit val riscv_f16Eq : (bits_H, bits_H) -> (bits_fflags, bool) function riscv_f16Eq (v1, v2) = { extern_f16Eq(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f32Lt = {c: "softfloat_f32lt", ocaml: "Softfloat.f32_lt", lem: "softfloat_f32_lt"} : (bits_S, bits_S) -> unit val riscv_f32Lt : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt (v1, v2) = { extern_f32Lt(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f32Lt_quiet = {c: "softfloat_f32lt_quiet", ocaml: "Softfloat.f32_lt_quiet", lem: "softfloat_f32_lt_quiet"} : (bits_S, bits_S) -> unit val riscv_f32Lt_quiet : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Lt_quiet (v1, v2) = { extern_f32Lt_quiet(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f32Le = {c: "softfloat_f32le", ocaml: "Softfloat.f32_le", lem: "softfloat_f32_le"} : (bits_S, bits_S) -> unit val riscv_f32Le : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Le (v1, v2) = { extern_f32Le(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f32Le_quiet = {c: "softfloat_f32le_quiet", ocaml: "Softfloat.f32_le_quiet", lem: "softfloat_f32_le_quiet"} : (bits_S, bits_S) -> unit val riscv_f32Le_quiet : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Le_quiet (v1, v2) = { extern_f32Le_quiet(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f32Eq = {c: "softfloat_f32eq", ocaml: "Softfloat.f32_eq", lem: "softfloat_f32_eq"} : (bits_S, bits_S) -> unit val riscv_f32Eq : (bits_S, bits_S) -> (bits_fflags, bool) function riscv_f32Eq (v1, v2) = { extern_f32Eq(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f64Lt = {c: "softfloat_f64lt", ocaml: "Softfloat.f64_lt", lem: "softfloat_f64_lt"} : (bits_D, bits_D) -> unit val riscv_f64Lt : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt (v1, v2) = { extern_f64Lt(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f64Lt_quiet = {c: "softfloat_f64lt_quiet", ocaml: "Softfloat.f64_lt_quiet", lem: "softfloat_f64_lt_quiet"} : (bits_D, bits_D) -> unit val riscv_f64Lt_quiet : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Lt_quiet (v1, v2) = { extern_f64Lt_quiet(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f64Le = {c: "softfloat_f64le", ocaml: "Softfloat.f64_le", lem: "softfloat_f64_le"} : (bits_D, bits_D) -> unit val riscv_f64Le : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Le (v1, v2) = { extern_f64Le(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f64Le_quiet = {c: "softfloat_f64le_quiet", ocaml: "Softfloat.f64_le_quiet", lem: "softfloat_f64_le_quiet"} : (bits_D, bits_D) -> unit val riscv_f64Le_quiet : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Le_quiet (v1, v2) = { extern_f64Le_quiet(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f64Eq = {c: "softfloat_f64eq", ocaml: "Softfloat.f64_eq", lem: "softfloat_f64_eq"} : (bits_D, bits_D) -> unit val riscv_f64Eq : (bits_D, bits_D) -> (bits_fflags, bool) function riscv_f64Eq (v1, v2) = { extern_f64Eq(v1, v2); - (float_fflags[4 .. 0], bit_to_bool(float_result[0])) + (float_fflags[4 .. 0], bool_bit(float_result[0])) } val extern_f16roundToInt = {c: "softfloat_f16roundToInt", ocaml: "Softfloat.f16_round_to_int", lem: "softfloat_f16_round_to_int"} : (bits_rm, bits_H, bool) -> unit diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 1baa33701..b372af5e6 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -166,10 +166,10 @@ val cancel_reservation = {ocaml: "Platform.cancel_reservation", interpreter: "Pl */ function exception_delegatee(e : ExceptionType, p : Privilege) -> Privilege = { let idx = num_of_ExceptionType(e); - let super = bit_to_bool(medeleg.bits[idx]); + let super = bool_bit(medeleg.bits[idx]); /* if S-mode is absent, medeleg delegates to U-mode if 'N' is supported. */ let user = if haveSupMode() - then super & haveNExt() & bit_to_bool(sedeleg.bits[idx]) + then super & haveNExt() & bool_bit(sedeleg.bits[idx]) else super & haveNExt(); let deleg = if haveUsrMode() & user then User else if haveSupMode() & super then Supervisor @@ -327,7 +327,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen match (del_priv) { Machine => { - mcause[IsInterrupt] = bool_to_bits(intr); + mcause[IsInterrupt] = bool_bits(intr); mcause[Cause] = zero_extend(c); mstatus[MPIE] = mstatus[MIE]; @@ -348,7 +348,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen Supervisor => { assert (haveSupMode(), "no supervisor mode present for delegation"); - scause[IsInterrupt] = bool_to_bits(intr); + scause[IsInterrupt] = bool_bits(intr); scause[Cause] = zero_extend(c); mstatus[SPIE] = mstatus[SIE]; @@ -373,7 +373,7 @@ function trap_handler(del_priv : Privilege, intr : bool, c : exc_code, pc : xlen User => { assert(haveUsrMode(), "no user mode present for delegation"); - ucause[IsInterrupt] = bool_to_bits(intr); + ucause[IsInterrupt] = bool_bits(intr); ucause[Cause] = zero_extend(c); mstatus[UPIE] = mstatus[UIE]; @@ -482,20 +482,20 @@ function init_sys() -> unit = { misa[MXL] = arch_to_bits(if sizeof(xlen) == 32 then RV32 else RV64); misa[A] = 0b1; /* atomics */ - misa[C] = bool_to_bits(sys_enable_rvc()); /* RVC */ + misa[C] = bool_bits(sys_enable_rvc()); /* RVC */ misa[I] = 0b1; /* base integer ISA */ misa[M] = 0b1; /* integer multiply/divide */ misa[U] = 0b1; /* user-mode */ misa[S] = 0b1; /* supervisor-mode */ - misa[V] = bool_to_bits(sys_enable_vext()); /* vector extension */ + misa[V] = bool_bits(sys_enable_vext()); /* vector extension */ if sys_enable_fdext() & sys_enable_zfinx() then internal_error(__FILE__, __LINE__, "F and Zfinx cannot both be enabled!"); /* We currently support both F and D */ - misa[F] = bool_to_bits(sys_enable_fdext()); /* single-precision */ + misa[F] = bool_bits(sys_enable_fdext()); /* single-precision */ misa[D] = if sizeof(flen) >= 64 - then bool_to_bits(sys_enable_fdext()) /* double-precision */ + then bool_bits(sys_enable_fdext()) /* double-precision */ else 0b0; mstatus = set_mstatus_SXL(mstatus, misa[MXL]); diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index 6c66492b4..8bc314fb4 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -262,7 +262,7 @@ function legalize_mstatus(o : Mstatus, v : xlenbits) -> Mstatus = { let m = if sys_enable_zfinx() then [m with FS = extStatus_to_bits(Off)] else m; let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty | extStatus_of_bits(m[VS]) == Dirty; - let m = [m with SD = bool_to_bits(dirty)]; + let m = [m with SD = bool_bits(dirty)]; /* We don't support dynamic changes to SXL and UXL. */ let m = set_mstatus_SXL(m, get_mstatus_SXL(o)); @@ -580,7 +580,7 @@ function lift_sstatus(m : Mstatus, s : Sstatus) -> Mstatus = { let m = [m with VS = s[VS]]; let dirty = extStatus_of_bits(m[FS]) == Dirty | extStatus_of_bits(m[XS]) == Dirty | extStatus_of_bits(m[VS]) == Dirty; - let m = [m with SD = bool_to_bits(dirty)]; + let m = [m with SD = bool_bits(dirty)]; let m = [m with SPP = s[SPP]]; let m = [m with SPIE = s[SPIE]]; diff --git a/model/riscv_types.sail b/model/riscv_types.sail index 2b1c132ec..d0abec31e 100644 --- a/model/riscv_types.sail +++ b/model/riscv_types.sail @@ -357,16 +357,6 @@ enum extop_zbb = {RISCV_SEXTB, RISCV_SEXTH, RISCV_ZEXTH} enum zicondop = {RISCV_CZERO_EQZ, RISCV_CZERO_NEZ} -mapping bool_bits : bool <-> bits(1) = { - true <-> 0b1, - false <-> 0b0 -} - -mapping bool_not_bits : bool <-> bits(1) = { - true <-> 0b0, - false <-> 0b1 -} - // Get the bit encoding of word_width. mapping size_enc : word_width <-> bits(2) = { BYTE <-> 0b00, diff --git a/model/riscv_types_kext.sail b/model/riscv_types_kext.sail index 0ae260cb0..1ff092451 100644 --- a/model/riscv_types_kext.sail +++ b/model/riscv_types_kext.sail @@ -21,7 +21,7 @@ /* Auxiliary function for performing GF multiplicaiton */ val xt2 : bits(8) -> bits(8) function xt2(x) = { - (x << 1) ^ (if bit_to_bool(x[7]) then 0x1b else 0x00) + (x << 1) ^ (if bool_bit(x[7]) then 0x1b else 0x00) } val xt3 : bits(8) -> bits(8) @@ -30,10 +30,10 @@ function xt3(x) = x ^ xt2(x) /* Multiply 8-bit field element by 4-bit value for AES MixCols step */ val gfmul : (bits(8), bits(4)) -> bits(8) function gfmul( x, y) = { - (if bit_to_bool(y[0]) then x else 0x00) ^ - (if bit_to_bool(y[1]) then xt2( x) else 0x00) ^ - (if bit_to_bool(y[2]) then xt2(xt2( x)) else 0x00) ^ - (if bit_to_bool(y[3]) then xt2(xt2(xt2(x))) else 0x00) + (if bool_bit(y[0]) then x else 0x00) ^ + (if bool_bit(y[1]) then xt2( x) else 0x00) ^ + (if bool_bit(y[2]) then xt2(xt2( x)) else 0x00) ^ + (if bool_bit(y[3]) then xt2(xt2(xt2(x))) else 0x00) } /* 8-bit to 32-bit partial AES Mix Colum - forwards */ diff --git a/model/riscv_vext_regs.sail b/model/riscv_vext_regs.sail index ae61ad5a6..1332e7d06 100644 --- a/model/riscv_vext_regs.sail +++ b/model/riscv_vext_regs.sail @@ -384,7 +384,7 @@ function read_vmask(num_elem, vm, vrid) = { if vm == 0b1 then { result[i] = true } else { - result[i] = bit_to_bool(vreg_val[i]) + result[i] = bool_bit(vreg_val[i]) } }; @@ -403,7 +403,7 @@ function read_vmask_carry(num_elem, vm, vrid) = { if vm == 0b1 then { result[i] = false } else { - result[i] = bit_to_bool(vreg_val[i]) + result[i] = bool_bit(vreg_val[i]) } }; @@ -420,7 +420,7 @@ function write_vmask(num_elem, vrid, v) = { var result : vregtype = undefined; foreach (i from 0 to (num_elem - 1)) { - result[i] = bool_to_bit(v[i]) + result[i] = bool_bit(v[i]) }; foreach (i from num_elem to (VLEN - 1)) { /* Mask tail is always agnostic */ diff --git a/model/rvfi_dii.sail b/model/rvfi_dii.sail index d1ad480df..322fabe12 100644 --- a/model/rvfi_dii.sail +++ b/model/rvfi_dii.sail @@ -277,8 +277,8 @@ function rvfi_get_exec_packet_v2 () = { let packet = update_magic(packet, 0x32762d6563617274); // ASCII "trace-v2" (BE) let packet = update_basic_data(packet, rvfi_inst_data.bits); let packet = update_pc_data(packet, rvfi_pc_data.bits); - let packet = update_integer_data_available(packet, bool_to_bits(rvfi_int_data_present)); - let packet = update_memory_access_data_available(packet, bool_to_bits(rvfi_mem_data_present)); + let packet = update_integer_data_available(packet, bool_bits(rvfi_int_data_present)); + let packet = update_memory_access_data_available(packet, bool_bits(rvfi_mem_data_present)); // To simplify the implementation (so that we can return a fixed-size vector) // we always return a max-size packet from this function, and the C emulator // ensures that only trace_size bits are sent over the socket.