[circt-test] Add runner for circt-bmc #7857
Conversation
fabianschuiki
requested review from
maerhart,
uenoku,
seldridge and
leonardt
| # Use circt-opt to lower any `verif.formal` ops to `hw.module`s. Once circt-bmc | ||
| # natively supports `verif.formal`, we can directly run it on the input MLIR. |
There was a problem hiding this comment.
I think once we have this connection, we'd ideally just instantiate the circt-bmc pipeline and jit exec call in circt-test directly instead of going through a python script.
There was a problem hiding this comment.
That's definitely an option. Although I'm also a bit hesitant to conflate test discovery and scheduling with the actual implementation of a formal verification tool. Maybe something like circt-formal or circt-verify could implement the collection of LEC, BMC, induction, and other proofs, and circt-test would just call out to that tool? That way we could get rid of the runner in favor of just calling the tools directly. But a separation may be valuable regardless.
| cmd = ["circt-bmc", lowered_mlir] | ||
| cmd += ["-b", str(args.depth or 20)] | ||
| cmd += ["--module", args.test] | ||
| cmd += ["--shared-libs", "/usr/lib/libz3.so"] |
There was a problem hiding this comment.
Maybe get this path as an argument instead of hardcoding it?
There was a problem hiding this comment.
That would be nice. I'm not sure how to do that exactly, though. The idea was to prevent the user from having to configure the runners. It must be possible to type circt-test input.mlir and just have all the tests in there run. So maybe this should be an environment variable, or part of a local configuration file somehow? Or maybe the runner script should just try a few common locations for Z3 and otherwise report that circt-bmc is not available. But this should definitely be configurable somehow, but maybe just not as a command line argument on circt-test.
There was a problem hiding this comment.
Environment variable sounds even better if that's possible.
There was a problem hiding this comment.
Done! Turned this into an environment variable. Funny how integration tests flush out missing features and find issues 😬
| cl::opt<bool> runnerReadsMLIR{ | ||
| "mlir-runner", | ||
| cl::desc("Pass the MLIR file to the runner instead of Verilog"), | ||
| cl::init(false), cl::cat(cat)}; |
There was a problem hiding this comment.
Maybe make this an enum "runnerInputFormat" because BTOR2 could also be an option?
There was a problem hiding this comment.
Good point. This option is currently just a hack to manually get the runners going. My idea was to have the runners themselves report what kind of input format they need, if the corresponding tool is installed on the system and available, and for which kinds of tests (formal, simulation, etc.) the runner is used for. This and the -r option will go away at that point, and will be replaced with a way for the user to pick a tool by name, or provide a list of tool preferences, e.g. --tool sby,circt-bmc,vcf,jg.
|
Also, could you maybe add a small integration test for that? |
fabianschuiki
force-pushed
the
fschuiki/circt-bmc-runner
branch
from
9a34da2
to
95946b0
Compare
Add a runner script for `circt-bmc` to circt-test. This allows CIRCT's own model checker to be used to verify `verif.formal` operations in MLIR inputs. The user currently has to pass the runner to circt-test explicitly using the `-r` option. In the future, we'll want to add a mechanism to circt-test to list available runners, check if the needed software is installed on the system, and configure new local runners through some config file.
fabianschuiki
force-pushed
the
fschuiki/circt-bmc-runner
branch
from
95946b0
to
92ce587
Compare
Add a runner script for
circt-bmcto circt-test. This allows CIRCT's own model checker to be used to verifyverif.formaloperations in MLIR inputs. The user currently has to pass the runner to circt-test explicitly using the-roption. In the future, we'll want to add a mechanism to circt-test to list available runners, check if the needed software is installed on the system, and configure new local runners through some config file.