Bool: add implication operator |->

[ekiwi-sifive]

Related issue: #1499

Type of change: new operator

Impact: API addition (no impact on existing code)

Development Phase: implementation

Release Notes

• Bool: now supports the implication operator a |-> b as a short hand for !a || b

[jackkoenig]

I'm not sure if this is something we should add to the Bool type. The issue is that there is some inconsistency here with SVA.

When there are no temporal operators, a |-> b == a implies b == !a || b, but when you have temporal properties in SVA, |-> is different than the other two. See https://stackoverflow.com/questions/24912264/systemverilog-implies-operator-vs for a detailed example.

[ekiwi-sifive]

I'm not sure if this is something we should add to the Bool type. The issue is that there is some inconsistency here with SVA.

Thanks for pointing me to that Stack Overflow discussion. While |-> is well defined on booleans, it seems like it can be confusing on sequences. However, Chisel does not support sequences and thus we should not have that problem.

However, I am very open to using -> instead of |-> as the implication operator if you think distancing from SV might help us avoid confusion. I was just a bit afraid that a lot of developers might confuse -> with its function in c++.

[ekiwi-sifive]

Another possible alternative would be => or ==>. However, I definitely don't want people to confuse this operator with |=> from SV, which always introduces sequence semantics.

[seldridge]

Bikeshed comment: Scala operator precedence should annoyingly be considered when choosing the leading character of new infix operators... |-> has the benefit of being low priority whereas -> would evaluate before Boolean operators. (I think I got that right.)

[ekiwi-sifive]

Bikeshed comment: Scala operator precedence should annoyingly be considered when choosing the leading character of new infix operators... |-> has the benefit of being low priority whereas -> would evaluate before Boolean operators. (I think I got that right.)

Thanks for pointing be to this Schuyler!

These are the SV operator precedences (high to low):

Operator
() {} :: .
(all unary operators)
**
* / %
- +
<< >> <<< >>>
< <= > >=
== != === !== ==? !=?
&
^ ~^ ^~
`
&&
`
?:
-> <->
= += -= ...
(concat)

[aswaterman]

-> is problematic for another reason: it's already used in Scala as an operator to create a tuple

scala> 1 -> 2
res2: (Int, Int) = (1,2)

How about just implies, which apparently also matches SVA? It's also lower priority than existing Boolean operators.

[ekiwi-sifive]

-> is problematic for another reason: it's already used in Scala as an operator to create a tuple

Thanks! I forgot about that.

How about just implies, which apparently also matches SVA? It's also lower priority than existing Boolean operators.

As far as I can tell implies only works on sequences, not on simple boolean expressions in SystemVerilog. Boolean expressions can be promoted to sequences, but that might than not be synthesizable.

My goal here is to provide a simple boolean operator that - while very useful in a verification context - can also easily be used for synthesizable hardware.

[ekiwi-sifive]

As far as I can tell implies only works on sequences, not on simple boolean expressions in SystemVerilog. Boolean expressions can be promoted to sequences, but that might than not be synthesizable.

OK. I have to correct this. While an answer to the StackOverflow question linked above claims that

the |-> is not allowed for properties (only for sequences and boolean expressions)

reading the spec a little more makes clear that |-> needs to go from a sequence_expr to a property_expr. The regular boolean implication operator in SV is actually -> which we cannot use as Andrew pointed out.

Wow, seems like there is a lot to consider and I do not have any clear preference anymore.

[aswaterman]

No strong prefs here, either, except to say that I would like some form of this operator to help me write more idiomatic assertions.

[jackkoenig]

Echoing @albert-magyar's comments (#1499 (comment)), I think we should organize all of these sequence and property-adjacent operators into a separate package. It seems desirable to capture these expressions in Scala ASTs so that we can easily provide multiple implementations rather than immediately mapping them to hardware, destroying that information and requiring it to be re-inferred in the FIRRTL. It also helps notionally separate the "hardware design" operations from the "property specification" operations.

[ekiwi-sifive]

I think we should organize all of these sequence and property-adjacent operators into a separate package.

It also helps notionally separate the "hardware design" operations from the "property specification" operations.

The implication operator that I am trying to implement here is supposed to be a "hardware design" operation, it does not have anything to do with sequences and is not temporal. My bad for starting with a syntax that is used for SVA sequences.

[ekiwi-sifive]

Running rg "!([^|])+\|\|" on the rocket chip code base brings up a bunch of examples where an implication operator would be useful, e.g.:

main/scala/amba/axi4/UserYanker.scala
55:      assert (!out.r.valid || r_valid) // Q must be ready faster than the response
76:      assert (!out.b.valid || b_valid) // Q must be ready faster than the response

main/scala/amba/axi4/Deinterleaver.scala
79:            assert (!dec || count =/= 0.U)
80:            assert (!inc || count =/= beats.U)
87:        when (!locked || (in.r.fire() && in.r.bits.last)) {

main/scala/amba/axis/Xbar.scala
98:      assert (!valids.reduce(_||_) || winner.reduce(_||_))

main/scala/util/MultiWidthFifo.scala
149:  assert(!little2big.io.out.valid || little2big.io.out.bits === lb_recv_data,
151:  assert(!big2little.io.out.valid || big2little.io.out.bits === bl_recv_data,
154:  assert(!lb_start_recv || little2big.io.count === UInt(4),
156:  assert(!bl_start_recv || big2little.io.count === UInt(8),


main/scala/rocket/DCache.scala
350:  val s2_no_alloc_hazard = if (!usingVM || pgIdxBits >= untagBits) false.B else {
597:      assert(!tl_out.d.valid || whole_opc.isOneOf(uncachedGrantOpcodes))

The majority are used in the context of an assertion, however, I don't think there is a reason to only restrict the implication operator to assertions since it only is a shorthand for !a || b.

[albert-magyar]

Echoing @albert-magyar's comments (#1499 (comment)), I think we should organize all of these sequence and property-adjacent operators into a separate package. It seems desirable to capture these expressions in Scala ASTs so that we can easily provide multiple implementations rather than immediately mapping them to hardware, destroying that information and requiring it to be re-inferred in the FIRRTL. It also helps notionally separate the "hardware design" operations from the "property specification" operations.

This also is more-or-less a perfect example of the kind of "collateral" that conveys information that is not fully captured in the IR that can be fluently captured with annotations. The interface between SVA and standard SV operators is at the atomic proposition level; this interface can translate robustly to targets. The general theme of late has been to do lots of things with annotations; this fits that pattern about as well as any other use case. I am not certainly not the biggest proponent of supporting things via annotations in general, but I think assertions intended to translate to rich downstream representations (that we will likely never fully re-implement) are a better fit than most things.

The majority are used in the context of an assertion, however, I don't think there is a reason to only restrict the implication operator to assertions since it only is a shorthand for !a || b.

While this is technically true, it is harder to reason about outside of an assertion context because you have to sensibly reason about the consequence of the negation of the implication by specifying a hardware behavior.

I would argue that the this...
when (locked implies (in.r.fire() && in.r.bits.last)) {

...is less clear than using basic booleans.
when (!locked || (in.r.fire() && in.r.bits.last)) {

However, that is clearly a matter of taste. There are certainly arguments for and against including of the bitstring operators that Chisel currently lacks.

[ekiwi-sifive]

This also is more-or-less a perfect example of the kind of "collateral" that conveys information that is not fully captured in the IR that can be fluently captured with annotations. The interface between SVA and standard SV operators is at the atomic proposition level; this interface can translate robustly to targets.

I agree that anything that has multi-cycle semantics including the past function should not be included with Chisel by default (see this comment of mine), however implication has well defined semantics on the "atomic proposition level" and it would be immediately useful to make open-source rocket-chip code more readable.

(Note that adding SVA sequences to rocket-chip would prohibit the use with open-source yosys.)

[jackkoenig]

it would be immediately useful to make open-source rocket-chip code more readable.

I think @albert-magyar's argument is that it is not more clear. Obviously this is opinion so I'd defer to designers on it. A mild concern I have is that having |-> in particular would imply to Verilog users that we support SVA so immediately they'd ask where are |=> and ##1 and the like. It may be better from the user-expectations perspective to just call it implies.

(Note that adding SVA sequences to rocket-chip would prohibit the use with open-source yosys.)

It doesn't if we support multiple backends for the sequences which is what I was trying to promote in my earlier comment (#1500 (comment)). Some temporal sequence support captured into an alternative AST and linked to the FIRRTL via annotations could be lowered to FIRRTL for backends like Yosys while enabling direct SVA emission on proprietary flows.

[ekiwi-sifive]

It may be better from the user-expectations perspective to just call it implies.

Yeah, I admit that the name was potentially chosen poorly. It is very sad that -> is not available since that is the SystemVerilog operator that I am trying to implement. implies is also a thing you apply to properties in SVA, so I guess there could be the same confusion around it.

I want to point out that without any of the other SVA operators, afaik |-> would have the same semantics as in SVA. If you want to implement a sequences DSL, you would have to add a custom Sequence type and overload the |-> operator for that separately.

It doesn't if we support multiple backends for the sequences which is what I was trying to promote in my earlier comment

I have been investigating this option for the last couple of days and I have come to the conclusion that while it is possible, it would probably take around 3-4 months of full time work to get this working well. Checkout yosys implementation which compiles SVA Sequences to DFAs: https://github.com/YosysHQ/yosys/blob/master/frontends/verific/verificsva.cc

[ekiwi-sifive]

@hcook and @johningalls-sifive , did you 👍 on @jackkoenig's comment because you agree that a |-> b is more confusing than just sticking with !a || b? Or did you 👍 because you would like to see SVA-style sequences in Chisel?

The first question is important in order to decide whether we should just close this PR.

[ingallsj]

I thumbs-up'd for this:

having |-> in particular would imply to Verilog users that we support SVA so immediately they'd ask where are |=> and ##1 and the like. It may be better from the user-expectations perspective to just call it implies.

[ingallsj]

I write a lot of my implies assertions currently in the form when (a) { assert(b) }, since I came from SystemVerilog-land and I'm used to thinking about assertions as implications rather than assert(!a || b).

[hcook]

I agree the pattern is a common one in circuit creation beyond just writing assertions, and if calling it out with a unique operator provides benefit to downstream tool consumers than I am all for adding an easy way to express it. I don't find that the particular example of when (locked implies (in.r.fire() && in.r.bits.last)) { is clearer to read than when (!locked || (in.r.fire() && in.r.bits.last)) { though... I guess i am voting in favor of further consideration of operators or english words especially if you are trying to encourage its use outside of assertions.

And I am contrasting this circuit use case to assert(locked implies cond, "...") which i do think parses well

I think when is really the problem here... if i read when A ??? B it is going to be a lot of work for ??? to make me backtrack and understand "actually we are talking about when !A here..." Maybe when B unless A? No wait that's B && !A ?... ugh not sure

And finally I don't think my stylistic disapproval of a secondary use case should prevent progress on the original primary one

[ekiwi-sifive]

if calling it out with a unique operator provides benefit to downstream tool consumers than I am all for adding an easy way to express it

The proposed change is never seen by any downstream tool, it is just syntactic sugar. (also, for any half-way decent logic optimizer, a -> b or !a || b should not make any difference in QoR)

And finally I don't think my stylistic disapproval of a secondary use case should prevent progress on the original primary one

I think I agree with your assessment that an implies operator - while great for assertions - doesn't really improve the readability for circuit signals.

Currently we use a regular UInt<1> signal to feed our assertions, thus adding an implies operator to this type in Chisel would automatically enable people to use it in assertions. People could also use it for other expressions but I think the consensus is that this actually negatively affects readability.

The other option floated by @jackkoenig and @albert-magyar would be pretty complicated if the sole purpose is adding syntactic sugar for implies. I agree with the goal of a Sequence library, however I believe that it will take quite some development while adding implies to the Bool class could be done today and will improve things immediately.

[albert-magyar]

I think maybe we are talking at cross purposes here. I definitely got a little too general in my original response, sorry for that; I was incorrectly mixing my thoughts on #1499 into this.

Here is my actual position:

• I think using a boolean implication outside of a verification context would generally reduce clarity. This is purely in response to the consideration of something like SV -> as a general hardware primitive to support. That doesn't mean I want to prevent it from being used that way, but that does take away some of the impetus for rolling it directly into the Bool API.

• I think a case can be made for adding implies (or whatever symbolic operator) separate from a larger assertion API. I think the logical companion is an iff to enhance clarity in lieu of ==, but that is probably less important.

• I am opposed to operator overloading that creates potential for confusion when juxtaposed with either SV or Scala built-in operators. This effectively rules out |=>, ->, and =>.

• More importantly, I do not see any issue with using |-> in Chisel assertions, since it would have the same semantics as SVA when applied to "assertion components" that are Chisel boolean expressions. However, since |-> is only allowed in SVA and not SV, I think it does not make sense to add it to the general Bool API.

An alternative is to add |-> to a "Chisel Assertion Construct" typeclass and to include implicits to let people write the following:

import chisel3.assertions._
...
  assert(a |-> b)

This in some way mirrors SVA, where the use of |-> on boolean expressions is a consequence of their automatic promotion.

[ekiwi-sifive]

Seems like there aren't enough people in favor of this.

[aswaterman]

Can I suggest reconsidering this idea, perhaps with the hopefully least controversial approach of adding a method named implies to Bool? It'll make assertions more idiomatic and doesn't seem to have too much baggage attached.

I agree with Kevin's remark that this is useful independent of a more fully featured assertion API.

[jackkoenig]

I'm happy with implies

[ekiwi]

See also: https://github.com/chipsalliance/rocket-chip/blob/c095dbc8fd7b4097a0540266bac3336fdef4b0d4/src/main/scala/formal/FormalUtils.scala#L205

(Some of these Utils probably should be added to the Chisel standard library, some of them could use some improvements, like TerniaryIf should probably just be an alias for Mux)