search

llvm / circt

Circuit IR Compilers and Tools
https://circt.org
Other
1.63k stars 285 forks source link

[Scheduling] Explore support for SMT solvers #3624

Open mikeurbach opened 2 years ago

mikeurbach commented 2 years ago

I don't know much about SMT, but I had a chat with @amaleewilson who does, and the conclusion was that it would be interesting to explore formulating the CIRCT scheduling problems as SMT problems and experimenting with SMT solvers. This would hopefully provide some novel real world problems for SMT researchers to measure against, and could potentially lead to wins for CIRCT users if these problems are particularly amenable to SMT solving. @jopperm not sure if you have any experience here, but curious to know your thoughts.

I think this would look like an integration similar to what has been set up for OR-tools, where we optionally depend on the SMT libraries and use a C++ API to construct the problem. Another angle could be to use a new import/export mechanism from the SSP dialect (opened a separate issue here), and export SMT formulations for offline experimentation.

We discussed using cvc5, a project Amalee contributes to. There is also smt-switch, which provides an umbrella API on top of several projects.

I will poke around with this a little bit, but if anyone else has interest, please feel free to jump in.

jopperm commented 2 years ago

Awesome, count me in to help! My knowledge of SMT is also basically just that this framework exists and is a viable approach for scheduling, but I haven't had time (or access to an expert :wink:) to explore this further. From the technical side, the integration of an SMT-based scheduler (or a family thereof) should be straightforward, as Mike already outlined.

uenoku commented 2 years ago

Interesting! I think SMT also has many other applications on PL/formal verification sides such as translation validation(e.g. mlir-tv), model checking (firrtl smt backend) etc. So my naive idea here is that we can maybe create SMT2 dialect and connect SMT2 dialect to SMT solvers (Z3/CVC etc). Then we can implement scheduling problem generation as a conversion from SSP to SMT2 dialect, which makes the work flow less monolithic. It might be a bit over engineering if we only use SMT as an off-the-shell solver of scheduling problem though.

(It's completely off-topic from CIRCT, but designing good intermediate representation for SMT itself sounds very interesting. There is some recent interesting work from aws https://github.com/awslabs/rust-smt-ir. I believe PL/formal verification is one area that MLIR can help to improve the composability of the entire ecosystem, which is very similar as CIRCT is trying to do for EDA tools)

mikeurbach commented 2 years ago

Having an SMT IR and converting to it sounds interesting indeed. Maybe longer term we can get to that model.

I believe at least for today, we generally encourage "production" flows to use the C++ circt::scheduling API, rather than building SSP IR. So I think my next step is to learn the C++ API of Z3/CVC and see if that can be hidden behind the circt::scheduling API. I think that work could be generally helpful; if an SMT2 dialect were to come into existence, we could hopefully re-use some C++ code.

fabianschuiki commented 2 years ago

I remember from looking at Boolector 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 text-based interface. I think you're basically supposed to just write some SMT-LIB formatted text into the stdin of a solver, then read and parse the output from stdout, then provide more input to stdin to do your incremental solving, and so on.

That might be cumbersome to use, and could be better wrapped in something like smt-switch. But I remember Claire Wolf saying that most of the academic SMT solver competitions use SMT-LIB v2 as input to the solvers, so this might be interesting to generate to share solver problems with those communities.