Skip to content

Commit

Permalink
Use bool <-> bit mappings from riscv_types.sail
Browse files Browse the repository at this point in the history
Use these mappings and change the other functions to be aliases of them.
  • Loading branch information
Timmmm authored Jul 9, 2024
1 parent 809337e commit b6cdb53
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 18 deletions.
26 changes: 18 additions & 8 deletions model/prelude.sail
Original file line number Diff line number Diff line change
Expand Up @@ -99,18 +99,28 @@ 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,
}

// These aliases make the conversion direction a bit clearer.
function bool_to_bit(x : bool) -> bit = bool_bit(x)
function bit_to_bool(x : bit) -> bool = bool_bit(x)
function bool_to_bits(x : bool) -> bits(1) = bool_bits(x)
function bits_to_bool(x : bits(1)) -> bool = bool_bits(x)


val to_bits : forall 'l, 'l >= 0.(int('l), int) -> bits('l)
function to_bits (l, n) = get_slice_int(l, n, 0)

Expand Down
10 changes: 0 additions & 10 deletions model/riscv_types.sail
Original file line number Diff line number Diff line change
Expand Up @@ -356,16 +356,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,
Expand Down

0 comments on commit b6cdb53

Please sign in to comment.