export to smtlib

[Ckaf]

Hello, I am attempting to export a Verilog file to smtlib and am receiving errors or an empty file. Could someone clarify how complete the functionality is or what the pipeline formats are for conversion?

P.S. I am also trying to figure out how to get the verif dialect, since I am unable to do so.

[TaoBi22]

Hi @Ckaf!

We don't really have a path from Verilog to a generically usable SMTLIB output currently - the reason for this is that our flow from hardware to SMTLIB targets model checking, so the IR node that actually indicates we add an SMTLIB assertion is an assertion in the IR (since anything that isn't in the fan-in to an assertion can be ignored for model-checking - this is probably why you were seeing empty files).

As a temporary workaround, it should work to try adding some arbitrary assertion on the output of your module and running that through the lowerings to SMT - that should produce some SMTLIB which calculates the output of your module and applies that assertion against it. Note that this will only work with a purely combinational module (due to the complications of representing state in SMTLIB).

In the long-run it would definitely be nice to have a way to emit SMTLIB corresponding to hardware without requiring an assertion - having discussed this with @maerhart, the best way to do this is probably with a modification to the HWToSMT pass that declares constants that correspond to the module outputs. I'll add this to my todo list, and I'll drop another comment here if I get the time to put something together!