Rachit Nigam

Normally solvers need to reset lots of state and disable various tactics that are not compatible with "incremental solving" (which is what push and pop require).

I think before merging this, we need to merge https://github.com/calyxir/calyx/issues/2061. @jiahanxie353 can you get the changes on that resolved so we can move forward with this PR?

This is interesting. I think we keep having to add ops because we don't have a good mechanism to talk about extern ops in the dialect. @cgyurgyik do you have...

@cgyurgyik exactly! We should build support for something like this in the Calyx dialect. A tricky thing is that we want to specify paths to Verilog files which implement the...

@cgyurgyik finally catching up to your comment. This is a good question about which ops we want to perform peephole optimizations on. In general, I think we should define them...

> Am I missing anything? Are you saying we should completely get rid of AddFNOp in TableGen [here](https://github.com/llvm/circt/blob/deb4fab619ad473bf24e1b40747fc03172240f9f/include/circt/Dialect/Calyx/CalyxPrimitives.td#L341)? I don't see an obvious way to introduce floating point add/mul without...

I'm not sure what is happening with the PR: the diff is too big for me to read the changes you've added.

@jiahanxie353 your pattern for float is: ``` float = @{ ASCII_DIGIT+ ~ "." ~ ASCII_DIGIT+ } ``` So how would the following thing match it: ``` 32'f1.0 ```

Another note from a synchronous chat: IEEE754 requires information on the number of bits being used.

Right, I ended up being pretty busy so didn't have time to check up on this.