Remove unnecessary matches for loads/stores #477
Conversation
Timmmm
force-pushed
the
user/timh/silly_switch
branch
2 times, most recently
from
21dddfb
to
5688986
Compare
Timmmm
force-pushed
the
user/timh/silly_switch
branch
from
5688986
to
ac301c0
Compare
|
This is ready now - I rebased it and fixed a small bug (mixing up |
Add a way to exclude tests by specifying an exclusion file
|
@billmcspadden-riscv I resolved the threads but I think we should merge #468 first (which is just the first commit from this PR) and then I'll rebase this and we can merge it. Hope that makes sense! |
Simplify the load/store code by removing the unnecessary matches on the access size. I have not done it for float loads/stores because that requires a separate change to make the float code generic over size. This also simplifies the AMO operation by not extending and truncating the values so many times, and removing the use of to_bits.
Timmmm
force-pushed
the
user/timh/silly_switch
branch
from
ac301c0
to
a6b656d
Compare
|
Ok this is rebased and ready to merge. |
|
IIRC those matches exist because previous Sail versions had trouble with monomorphisation of this code when generating theorem prover definitions. No idea if that is still the case. |
|
Ah interesting. @Alasdair do you know if that is still true? |
|
I don't think any of the output that's currently produced requires monomorphisation (because the Lem/Isabelle output is currently using bit lists). If I remember correctly, this part of the spec isn't a problem anyway at the moment, but the vector specifications need some tweaks. |
billmcspadden-riscv
removed
the
tgmm-agenda
Simplify the load/store code by removing the unnecessary matches on the access size. I have not done it for float loads/stores because that requires a separate change to make the float code generic over size.
Note, the first commit is #468 - only review the second.