amaranth icon indicating copy to clipboard operation
amaranth copied to clipboard

Do something with `Value.implies`

Open whitequark opened this issue 1 year ago • 2 comments

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:

  1. Deprecate and remove
  2. Deprecate use with signed operands (even though x | y or x ^ y all accept signed operands)
  3. Deprecate use with unequal length operands but allow signed operands
  4. Cast both operands with .bool() like return ~premise.bool() | conclusion.bool()
    • This is a hard compatibility break, though we can probably do a deprecation cycle?
  5. Something else

whitequark avatar Mar 25 '24 15:03 whitequark

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.

whitequark avatar Apr 15 '24 17:04 whitequark

Deprecated in #1337.

wanda-phi avatar May 07 '24 23:05 wanda-phi