Fabian Schuiki
Fabian Schuiki
Going to hit merge on this. We'll do a very blameful revert if this breaks anything :grimacing:
I remember from looking at [Boolector](https://boolector.github.io/docs/index.html) a few years back that it uses "SMT-LIB v2" which seems like it's a very popular standardized way to interact with solvers through a...
I'm going to close this PR but keep the branch around. With the `seq.firmem` op we'll get a better opportunity to implement this.
This is really nice! 🥳 I agree with @jackkoenig that using annotations is good to get things rolling, but we'll have to find a more permanent solution later. Firtool internally...
That sounds very exciting! What kind of additional information do you want to attach to the debug operations? You should be able to do so without changing the debug dialect...
Yeah you can also add attributes to ops that are not part of the debug dialect `*.td` file. That's very useful for experimenting and getting things up and running, before...
We have since gained the `sv.attributes` attribute on ops which allow us to communicate these pragmas in a uniform way. Closing this.
There's this pattern with symbol user verification where your op can resolve a symbol and verify invariants against it. I see potentially two ways to do this: 1. Embed the...
@maerhart I like your suggestion a lot. But you're also right in that it's a pretty big code change that we'd have to sequence before this PR here in order...
The symbol use verifier can still access the op referenced by the symbol though, right?