std_detect: RISC-V: implement implication to "C"

Just like we implemented relatively complex rules to imply other extensions
**from** "C" (and some others), this commit implements implication
**to** the "C" extension from others, complying the following text
in the ISA Manual (although there's no direct imply/depend references).

> The C extension is the superset of the following extensions:
>
> - Zca
> - Zcf if F is specified (RV32 only)
> - Zcd if D is specified

This is formally verified so that no other extension combinations
(*not* in this implementation) can (currently) imply the "C" extension.
This commit is contained in:
Tsukasa OI
2025-08-19 01:37:35 +00:00
parent 9eb4a26520
commit ee7627ee40

View File

@@ -119,11 +119,31 @@ pub(crate) fn imply_features(mut value: cache::Initializer) -> cache::Initialize
imply!(d | zfhmin | zfa => f); imply!(d | zfhmin | zfa => f);
imply!(zfbfmin => f); // and some of (not all) "Zfh" instructions. imply!(zfbfmin => f); // and some of (not all) "Zfh" instructions.
// Relatively complex implication rules from the "C" extension. // Relatively complex implication rules around the "C" extension.
// (from "C" and some others)
imply!(c => zca); imply!(c => zca);
imply!(c & d => zcd); imply!(c & d => zcd);
#[cfg(target_arch = "riscv32")] #[cfg(target_arch = "riscv32")]
imply!(c & f => zcf); imply!(c & f => zcf);
// (to "C"; defined as superset)
cfg_select! {
target_arch = "riscv32" => {
if value.test(Feature::d as u32) {
imply!(zcf & zcd => c);
} else if value.test(Feature::f as u32) {
imply!(zcf => c);
} else {
imply!(zca => c);
}
}
_ => {
if value.test(Feature::d as u32) {
imply!(zcd => c);
} else {
imply!(zca => c);
}
}
}
imply!(zicntr | zihpm | f | zfinx | zve32x => zicsr); imply!(zicntr | zihpm | f | zfinx | zve32x => zicsr);