Improve Zicbom implementation. #718
Conversation
pmundkur
force-pushed
the
fix_cbie_reserved
branch
from
60d1bec to
de30f25
Compare
|
It wasn't incorrect. You can do anything with reserved values so I chose the (much) simpler implementation. And as you noted the legalisation prevents that value anyway (though I do like being able to detect mistakes in legalisation). I think splitting the instructions up is probably a good idea (makes embedding in the spec nicer)... but it is definitely more complex. Let's discuss it in the meeting on Monday. |
|
Sounds good; thanks for the review. Yeah, incorrect was probably too strong, apologies. I need to understand how we should handle reserved values; I'm not convinced we can do anything with them. |
|
Yeah I agree we don't quite have a clear strategy for reserved values. I think we should probably have a global flag that allows two modes of operation:
Let's discuss that too. |
model/riscv_insts_zicbom.sail
Outdated
| mapping encdec_cbie : cbie <-> bits(2) = { | ||
| CBIE_ILLEGAL <-> 0b00, | ||
| CBIE_EXEC_FLUSH <-> 0b01, | ||
| CBIE_RESERVED <-> 0b10, |
There was a problem hiding this comment.
How about handing the reserved value here instead?
- CBIE_RESERVED <-> 0b10,
+ backwards 0b10 => internal_error(__FILE__, __LINE__, "reserved CBIE"),
This would allow us to remove some matches below.
(Making it impossible to set the reserved value in *envcfg would be better, but that is a bigger change.)
There was a problem hiding this comment.
I don't think the encdec decoding of 10 to CBIE_RESERVED is an internal_error, so I'm not sure that's where it should be.
One of the goals of the PR was to get the privilege check in a form that can replace the pseudo-code in the Zicbom spec, and to be explicit about the handling of the reserved value there.
Afaict, the legalize_xenvcfg already make it impossible to set the reserved value.
There was a problem hiding this comment.
Afaict, the legalize_xenvcfg already make it impossible to set the reserved value.
But that's the point. The architecture's WARL rules mean it is architecturally impossible to ever have a reserved value in the register. So if it does end up happing, that is an internal error / assertion failure / whatever you want to call it; it is an impossible state that does not need any architecturally-defined behaviour. Ideally that state wouldn't even be representable, e.g. by having the actual state use an enum and convert it to bits in CSRRW etc.
There was a problem hiding this comment.
That is a good point: the encdec should not make the reserved value representable. I'll push a fix.
pmundkur
force-pushed
the
fix_cbie_reserved
branch
from
de30f25 to
ac14b5a
Compare
model/riscv_insts_zicbom.sail
Outdated
| CBIE_ILLEGAL <-> 0b00, | ||
| CBIE_EXEC_FLUSH <-> 0b01, | ||
| CBIE_EXEC_INVAL <-> 0b11, | ||
| backwards 0b11 => internal_error(__FILE__, __LINE__, "reserved CBIE"), |
There was a problem hiding this comment.
| backwards 0b11 => internal_error(__FILE__, __LINE__, "reserved CBIE"), | |
| backwards 0b10 => internal_error(__FILE__, __LINE__, "reserved CBIE"), |
Isn't it this one?
There was a problem hiding this comment.
Oops, good catch, thanks!
There was a problem hiding this comment.
I think it would be nice if the type system caught this kind of mistakes...
Can a bijective mapping be expressed in Sail?
Clarify the privilege checking of xenvcfg.CBIE in cbo.inval. The privilege check should extend to the hypervisor case, when two possible illegal exceptions could be thrown. This check as written doesn't match the pseudo-Sail in the CMO spec, but is arguably clearer. Make sure that the reserved CBIE value is not representable.
pmundkur
force-pushed
the
fix_cbie_reserved
branch
from
ac14b5a to
e0d14c5
Compare
The bitwise check of xenvcfg.CBIE to check whether cbo.inval was enabled was incorrect, since CBIE is a four-valued setting. Specifically, it decoupled the bits in the reserved value 0b10 of CBIE.
This fixes the handling of the reserved value, and also throws an internal error when it is detected to indicate a possible bug in xenvcfg legalization.
The privilege check should extend to the hypervisor case, when two different illegal exceptions could be thrown. This check as written doesn't match the pseudo-Sail in the CMO spec, but is arguably clearer.
I've left the CBCFE handling alone, since it works for the single bit case.
I'd like to make sure that the handling of no S-mode case is correct (the pseudo-Sail in the spec doesn't seem to handle it explicitly).