amaranth
amaranth copied to clipboard
Do something with `Value.implies`
Value.implies is a rarely used and not well-known counterpart to __or__, __xor__, etc operators. It is defined as:
def implies(premise, conclusion):
return ~premise | conclusion
It was originally added to aid in the development of formal testbenches, but is obviously usable in any code:
m.d.comb += Assert((self.depth > 0).implies(~empty))
The problem with this operator is that it's bitwise and sign-extending, without warning (simply because the underlying logical operators are). This is extremely weird and it's difficult to see where this behavior would be desirable. In short, if premise and conclusion are both multi-bit, then the result is a logical OR of the arrow operator applied pairwise to each bit of the premise and conclusion.
What should we do with it? Options:
- Deprecate and remove
- Deprecate use with signed operands (even though
x | yorx ^ yall accept signed operands) - Deprecate use with unequal length operands but allow signed operands
- Cast both operands with
.bool()likereturn ~premise.bool() | conclusion.bool()- This is a hard compatibility break, though we can probably do a deprecation cycle?
- Something else
We have discussed this issue on the 2024-04-15 core subsystem meeting. Only options (1) and (4) were considered by anyone present, and there weren't compelling reasons to pick option (4). As such Value.implies will be deprecated and removed.
Deprecated in #1337.