Add RequireProperty and EnsureProperty #4681
Conversation
1f23392 to
042326f
Compare
| /** Require that a property holds as a pre-condition of a contract. Behaves like | ||
| * an `AssertProperty` if used outside of a contract. | ||
| * | ||
| * Use like `RequireProperty(p)`. See `AssertPropertyLike.apply` for optional | ||
| * clock, disable_iff, and label parameters. | ||
| */ |
There was a problem hiding this comment.
This applies to all ScalaDoc so perhaps better left to a follow on docs update, but There's no need to look at AssertPropertyLike.apply, all apply methods are inherited and thus available on all of these objects.
Also rather than "Use like" we should just put a ScalaDoc example.
There was a problem hiding this comment.
Good point. I can do a pass over the LTL stuff in a follow-up PR to clean the docs up in one go. An example for each would be nice 👍
| */ | ||
| object EnsureProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assert) { | ||
| protected def createIntrinsic(label: Option[String])(implicit sourceInfo: SourceInfo) = VerifEnsureIntrinsic(label) | ||
| } |
There was a problem hiding this comment.
New APIs need to be added to src/main/scala-3 as well or we are just creating more work for ourselves in the future.
There was a problem hiding this comment.
None of this currently exists in src/main/scala-3. It's going to be easier to do this separately in one go, instead of turning a PR adding a few APIs into a PR that does Scala 3 migration plus adding a few APIs.
| * Use like `EnsureProperty(p)`. See `AssertPropertyLike.apply` for optional | ||
| * clock, disable_iff, and label parameters. | ||
| */ | ||
| object EnsureProperty extends AssertPropertyLike(defaultLayer = layers.Verification.Assert) { |
There was a problem hiding this comment.
How does AssumeProperty differ from AssertProperty and how does EnsureProperty differ from AssertProperty when used in a formal contract?
There was a problem hiding this comment.
They are interpreted as assume or assert depending on whether the contract itself is checked, or whether it is assumed to hold to simplify parent proofs. I've added a few more sentences to roughly explain what happens.
Add support for CIRCT's `circt_verif_require` and `circt_verif_ensure` intrinsics. These interact with the formal contracts implemented in CIRCT and translate to asserts or assumes depending on whether the contract is checked or applied. They lower to asserts if used outside of a contract. Chisel itself has no support for contracts yet, such that these two additions behave like `AssertProperty` in practice. As soon as contracts are added to Chisel though, they can be used to formulate the pre- and post-conditions of those contracts.
042326f to
627679e
Compare
There was a problem hiding this comment.
LGTM
@jackkoenig: The marginal cost of migrating this patch to Scala 3 on top of the cost of migrating the whole file to Scala 3 is minimal. So, I think we can just do this in one go like Fabian is suggesting.
| private[chisel3] object VerifEnsureIntrinsic { | ||
| def apply(label: Option[String] = None)(prop: Bool, enable: Option[Bool])(implicit sourceInfo: SourceInfo) = | ||
| VerifAssertLikeIntrinsic("ensure", label)(prop, enable) | ||
| } |
There was a problem hiding this comment.
In a follow-up patch, all of these factories could be combined into a single trait with an abstract def intrinsicName: String method.
There was a problem hiding this comment.
Good idea, added #4711 to track.
Add support for CIRCT's
circt_verif_requireandcirct_verif_ensureintrinsics. These interact with the formal contracts implemented in CIRCT and translate to asserts or assumes depending on whether the contract is checked or applied. They lower to asserts if used outside of a contract.Chisel itself has no support for contracts yet, such that these two additions behave like
AssertPropertyin practice. As soon as contracts are added to Chisel though, they can be used to formulate the pre- and post-conditions of those contracts.Contributor Checklist
docs/src?Type of Improvement
Desired Merge Strategy
Release Notes
Reviewer Checklist (only modified by reviewer)
3.6.x,5.x, or6.xdepending on impact, API modification or big change:7.0)?Enable auto-merge (squash)and clean up the commit message.Create a merge commit.