Unify bit and bitvector(1) #1491
Conversation
Test Results 16 files 36 suites 0s ⏱️ Results for commit 3fb3863. ♻️ This comment has been updated with latest results. |
|
Pretty much every rewrite that assumes a bitvector literal is be rewritten to |
a873209 to
55a94a8
Compare
| { | ||
| "some" : { | ||
| "single_bit" : true | ||
| "single_bit" : [true] |
There was a problem hiding this comment.
Would it be annoying to add a special case in the config parsing to keep this working? I guess most config files should be using bool not bit for boolean flags so probably doesn't matter and might not be worth the effort.
There was a problem hiding this comment.
sail-riscv isn't using it, so I thought it might be better to avoid adding a special case and keep it simple.
There was a problem hiding this comment.
Sounds good to me, just spotted this will skimming over the test changes.
There was a problem hiding this comment.
I think the vast majority of test case changes are adding type bit = bitvector(1) to very old tests that don't include the prelude. There were a few very old tests that were actually writing vector('n, bit) when they wanted a bitvector and manually specifying external lem functions that were quite broken, but the fix there was mostly to just simplify the test to include the prelude.
dbd2efb to
d36acf4
Compare
For mostly historical reasons Sail has had a separate type `bit` which is distinct from bits(1). This was because (a long time ago), `bitvector(N)` and `vector(N, bit)` were the same type. Therefore `bit` could not be `vector(1, bit)` because that would be `vector(1, vector(1, bit))` and so on. Now `bitvector` and `vector` are different, so there is no reason to keep `bit` and `bitvector(1)` separate other than inertia (except for one caveat, discussed below). The downside of these types being different was that extracting a single bit into a bitvector has to be written as `[v[0]]`, i.e. extract the `bit` then put it back into a singleton bitvector. It also meant we had separate literals `bitzero` and `bitone` for the bit type, which is a bit ugly. The one caveat as mentioned for merging these two concepts is that it makes it ever so slightly trickier to write a Sail backend that uses a bitlist representation for bitvectors (in OCaml for example it is quite natural to map `bivector(1)` to `bit list` and `bit` to `bit`). The changes here are fairly substantial: * The literal constructors L_zero and L_one are removed from the AST * The V_bit value constructor is removed. V_vector is replaced with V_bitvector and V_vector. * [x,y,z] is treated as a concatenation of length-1 bitvectors (when not a generic vector expression). * For backwards compatability `bitzero` and `bitone` are aliases for `0b0` and `0b1` respectively. * The bit type is removed, and replaced with a type synonym in the prelude. * The CT_bit type is removed from the Jib IR. We could keep it for SystemVerilog generation, but it seems cleaner to just remove it too.
We no longer allow clauses with impossible constraints
Leave it in stdlib, but equivalent to eq_bits
This is a bit of hack, but mostly to see what it gets past CI and what needs to change.
Again fix is a bit hacky
Mark one monomorphisation test as expected fail for now
d36acf4 to
3fb3863
Compare
For mostly historical reasons Sail has had a separate type
bitwhich is distinct frombits(1). This was because (a long time ago),bitvector(N)andvector(N, bit)were the same type. Thereforebitcould not bevector(1, bit)because that would bevector(1, vector(1, bit))and so on. Nowbitvectorandvectorare different, so there is no reason to keepbitandbitvector(1)separate other than inertia (except for one caveat, discussed below).The downside of these types being different was that extracting a single bit into a bitvector has to be written as
[v[0]], i.e. extract thebitthen put it back into a singleton bitvector. It also meant we had separate literalsbitzeroandbitonefor the bit type, which is a bit ugly.The one caveat as mentioned for merging these two concepts is that it makes it ever so slightly trickier to write a Sail backend that uses a bitlist representation for bitvectors (in OCaml for example it is quite natural to map
bivector(1)tobit listandbittobit).The changes here are fairly substantial:
The literal constructors L_zero and L_one are removed from the AST
The V_bit value constructor is removed. V_vector is replaced with V_bitvector and V_vector.
[x,y,z] is treated as a concatenation of length-1 bitvectors (when not a generic vector expression).
For backwards compatability
bitzeroandbitoneare aliases for0b0and0b1respectively.The bit type is removed, and replaced with a type synonym in the prelude.
The CT_bit type is removed from the Jib IR. We could keep it for SystemVerilog generation, but it seems cleaner to just remove it too.