All committers have signed the CLA.

Also, I should mention that this can't be merged until FIRRTL 1.4 releases and we update the FIRRTL dependency accordingly (https://github.com/freechipsproject/firrtl/milestone/15)

I'm open to suggestions other than formal for the package name, although I think it should be short (verification is a lot to type for every statement).

Since these are usable in contexts other than formal property checking (e.g. simulation), I would suggest property. This also aligns with the SystemVerilog syntax of declaring a property and assert|assume|cover-ing it.

It's notable that your actually code takes a msg: String = "" but you don't show it in your example in the PR comment... that was going to be the first thing I asked for :)

If I understand correctly, SV properties can also take a name of the property. Is there any way to capture that in this API?

If I understand correctly, SV properties can also take a name of the property. Is there any way to capture that in this API?

Not presently, since the underlying FIRRTL generated will have no way of associating that tag. But I think there is a lot of interest in making it possible to add labels/tags to FIRRTL statements: if we get that done then this feature should be a simple addition. As I understand from the 06/22 Chisel dev meeting notes, enabling statement tags is something that @ekiwi is investigating?

Hi Tom, thanks a lot for working on this!

objects under a new chisel3.formal package

I was initially thinking about just placing these statements in the chisel3 package since that follows our conventions with asset, printf and stop. However, I can see how the new assume and cover methods might clash with exisiting user defined methods.

to avoid clashing with the existing chisel3.assert

The plan should be to reimplement the existing chisel3.assert with the new facilities. @albert-magyar is working on a pass to take any firrtl assert and turn it into a when, printf, stop construct similar to what we are directly emitting for asserts now. This way people can decide to run this pass if they want the old behavior.

One thing that needs to be addressed is the fact that the "legacy" assert implementation did allow for format strings and a variable number of arguments, directly exposing the powers of the underlying printf. This can probably be emulated by generating an assert with an empty message and a when guarded printf in addition. For regular asserts that only have a simple string message, we can directly replace them with the new assert statement.

I also propose adding a past(signal, n) object

I am going to work on adding some verification function to Chisel (probably Rose, Fell, Stable, Past, CountOnes, IsOneHot, IsOneHotOrZero). Expect a PR soon.

I also propose adding a Chisel formal testing backend which sets up and runs a Symbiyosys instance, so that you can add formal verification checks as Chisel unit tests.

This would be cool! It should probably be a library similar to chisel-test.

Adding a formal testing backend would also lay the groundwork for creating a model checking tool that operates directly on FIRRTL as as a complement to Treadle.

My research is eventually going to take me into that direction. I might be able to add a SMTLib + Btor2 backend to Firrtl in the next couple of months. Writing a new model checker in Scala will take a lot longer.

As I understand from the 06/22 Chisel dev meeting notes, enabling statement tags is something that @ekiwi is investigating?

Yes. We are basically all in agreement that we want to have names for statements (many are also interested in being able to annotate statements). But we are bike shedding the syntax at the moment.
I assume that this name will behave similar to registers, i.e. it can be derrived from a Scala variable name or suggested with suggestName.

Once these statements have a name we could also add an option to generate a named property when emitting verification statements to SystemVerilog. However, this is not supported by the open source version of yosys and thus we will need a switch for it.

I also propose adding a past(signal, n) object in the formal package that constructs n shift registers in order to make statements about the value of a signal n clock cycles in the past.

I think that adding features like this to the core language (rather than a library) and relying on simple hardware translations has significant downsides. Specifically, this actually makes it harder to emit an idiomatic SVA assertion that reflects the user's intent.

I think that adding features like this to the core language (rather than a library) and relying on simple hardware translations has significant downsides.

Does chisel3.util count as a library or do you think it should go into a 3rd party library?
I was thinking about adding a Past method to chisel3.util.experimental.

Plus, past(signal, n) should be more familiar to System Verilog users and make it easier to port code into Chisel.

The problem with a naive implementation of past is that you need to specify the value that you get in the first cycle of your simulation or model checking run. If I understand the SystemVerilog standard correctly you would get a x. (The relevant section is 16.5.1 Sampling which specifies the "the default sampled value of an expression").

You can circumvent this problem by ensuring that past is only used when it contains a valid/non-default value. This is pretty simple if you have sequences, however with plain concurrent assertions as we have in Chisel it can be a bit more tricky. The author of the ZIPCpu blog for example recommends adding a f_past_valid register with the initial value of 0 for tracking whether a past value can be used: https://zipcpu.com/answer/2019/08/29/fv-answer04.html

After investigating this for a day, I think it would be a mistake for Chisel to provide a built-in past function.
Consider that four out of 12 of the Formal Verification Quizzes by ZIPCpu are about the pitfalls of the past function: Quiz 4, Quiz 6, Quiz 7, Quiz 10.

The use of the past function is not something that we should encourage. If you know enough to safely make use of it, you can always add a simple convenience function to your project or library. However, for new users I think past is a huge footgun and thus should not be part of the Chisel standard library. This includes all derived functions, i.e., stable, rose, fell.

The use of the past function is not something that we should encourage. If you know enough to safely make use of it, you can always add a simple convenience function to your project or library. However, for new users I think past is a huge footgun and thus should not be part of the Chisel standard library. This includes all derived functions, i.e., stable, rose, fell.

I see what you're getting at, but I actually think this is a good opportunity for Chisel to provide some safe defaults that address some of these pitfalls of $past without completely losing its benefits. Consider how the Chisel Module provides an implicit clock and reset. This helps users avoid gotchas with forgetting to set up resets and randomize states in simulation, but there is also RawModule if they need something other than the safe default behaviour.

Similarly, for formal we could have a safe defaults trait Formal that provides a past function with f_past_valid-like guarantees (e.g. by implicitly setting up a counter for time since last reset), and then a sharper trait RawFormal that only makes assert, assume, cover available. You'd use them by mixing the appropriate one into your Module e.g. class Foo extends Module with Formal. We could use trait Formal to encode other good practices as well, and guide users in the right direction for success. Similar to the rest of Chisel, the understanding would need to be clear that these conveniences ultimately become a restricted subset of Verilog (i.e. Chisel past wouldn't generate SV $past but instead would generate a shift register or something).

All that said, perhaps this stuff just belongs in a separate library, which users can optionally bring on for convenience. As long as Chisel facilitates assert, assume, cover that's do-able, although I think having really useful things like $past be in a separate library would be a missed opportunity.

Could we try just adding assert, assume, and cover to a verification package to start for 1.4?

to a verification package

Should it be a chisel3.experimental.verification package?
So that we are free to change the API later.

to a verification package

Should it be a chisel3.experimental.verification package?
So that we are free to change the API later.

Good point, that would be best!

@albert-magyar Can we make another Firrtl 1.4 snapshot? I don't think these CI tests can pass until the Firrtl 1.4 snapshot includes the model checking API.

https://github.com/freechipsproject/firrtl/commits/v1.4-20200603-SNAPSHOT

The build process is supposed to use FIRRTL master (you can see the build step here cloning FIRRTL and publishing it locally). However,

I can reproduce this not working locally... Looking into it.

I haven't looked to closely at all the code changes in here, but it looks good so far. I think the one other step would be to make the builtin assert (that existed in previous versions of Chisel) also use the verification statements.

I haven't looked to closely at all the code changes in here, but it looks good so far. I think the one other step would be to make the builtin assert (that existed in previous versions of Chisel) also use the verification statements.

@albert-magyar That requires some knowledge of how your pass that replaces asserts with when + printf + stop works. One corner case that I can think of is when you use assert with varargs you should probably emit a when + printf + assert and then your pass will replace the assert with a stop.

I haven't looked to closely at all the code changes in here, but it looks good so far. I think the one other step would be to make the builtin assert (that existed in previous versions of Chisel) also use the verification statements.

@albert-magyar That requires some knowledge of how your pass that replaces asserts with when + printf + stop works. One corner case that I can think of is when you use assert with varargs you should probably emit a when + printf + assert and then your pass will replace the assert with a stop.

I concur with Kevin here. We should consider how this new assert should interact with the old assert, but I think it could just as easily be in a follow-up to this toehold PR. Once we have a basic foundation in place and users can start experimenting with formal, there will be plenty of time to work through all the cool features that we could potentially add to figure out which ones are most worthy.

@seldridge I appreciate you fixing the treadle/firrtl snapshot clobbering thing! It looks like there might be some lingering deprecation warning issues from treadle? https://app.circleci.com/pipelines/github/freechipsproject/chisel3/1925/workflows/0a062e7b-0b2a-4c44-bedb-7b08b8ef0702/jobs/7188/steps

No problem, @tdb-alcorn. Sorry about that. There's a series of issues here that are fixed:

• Add Treadle to CI builds #1516
• Fix unused import treadle#224 (CI check: Add documentation building to CI treadle#225)

However, one commit sneaked through FIRRTL CI and is causing problems, but the following is in the pipeline to fix it:

• Fix Fuzzer for 2.11 firrtl#1771 (CI check: Cross-build unidoc in CI firrtl#1772)

I believe that the appropriate interlocks are in place to prevent this happening again. 🤞

Alright, the current reason for CI failure is that there are too many scalastyle warnings. If the number of warnings exceeds 40, CI will fail. I believe that this PR introduced some Scalastyle errors (which can be checked with sbt scalastyle).

Alright, the current reason for CI failure is that there are too many scalastyle warnings. If the number of warnings exceeds 40, CI will fail. I believe that this PR introduced some Scalastyle errors (which can be checked with sbt scalastyle).

Thanks for figuring this out! I'm on it

@seldridge sorry to keep bugging you

The build is failing to find package repositories. I don't think (?) I could have caused this in the last two commits (they were all just style fixes). Here's the error:

[error] sbt.librarymanagement.ResolveException: Error downloading com.simplytyped:sbt-antlr4;sbtVersion=1.0;scalaVersion=2.12:0.8.2
[error]   Not found
[error]   Not found
[error]   not found: https://repo1.maven.org/maven2/com/simplytyped/sbt-antlr4_2.12_1.0/0.8.2/sbt-antlr4-0.8.2.pom
[error]   not found: /home/chisel/.ivy2/local/com.simplytyped/sbt-antlr4/scala_2.12/sbt_1.0/0.8.2/ivys/ivy.xml
[error]   not found: https://scalasbt.artifactoryonline.com/scalasbt/sbt-plugin-releases/com.simplytyped/sbt-antlr4/scala_2.12/sbt_1.0/0.8.2/ivys/ivy.xml
[error]   not found: https://download.eclipse.org/jgit/maven/com/simplytyped/sbt-antlr4_2.12_1.0/0.8.2/sbt-antlr4-0.8.2.pom
[error]   download error: Caught javax.net.ssl.SSLHandshakeException: java.security.cert.CertificateException: No subject alternative DNS name matching repo.scala-sbt.org found. (java.security.cert.CertificateException: No subject alternative DNS name matching repo.scala-sbt.org found.) while downloading https://repo.scala-sbt.org/scalasbt/sbt-plugin-releases/com.simplytyped/sbt-antlr4/scala_2.12/sbt_1.0/0.8.2/ivys/ivy.xml
[error]   download error: Caught javax.net.ssl.SSLHandshakeException: java.security.cert.CertificateException: No subject alternative DNS name matching repo.typesafe.com found. (java.security.cert.CertificateException: No subject alternative DNS name matching repo.typesafe.com found.) while downloading https://repo.typesafe.com/typesafe/ivy-releases/com.simplytyped/sbt-antlr4/scala_2.12/sbt_1.0/0.8.2/ivys/ivy.xml

That looks like flaky CI. 🤷‍♀️ I restarted it...

I've updated the PR description and release notes above to reflect the actual state of the PR.

Can we merge this?

@albert-magyar Wanted to manually squash some commits and keep the style changes in a separate commit before merging.

Yes, we just got the CI resolved with #1519. Sorry to make you go in circles with this, but if you can rebase on master and drop the scalastyle-related changes, I can merge it straight away.

@albert-magyar Done. After CI passes (🤞) we should be good to go

@tdb-alcorn Can please remove all of the scalastyle comments?
Sorry for the confusion, but we removed all of scalatyle from the repository in #1519 and we should avoid introducing comments for a tool that is no longer used.

Woops, I forgot I had added those. Removed now.