search

llvm / circt

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

[Scheduling] Import/Export support for external problem formats #3623

Open mikeurbach opened 2 years ago

mikeurbach commented 2 years ago

Now that the SSP dialect is starting to land, one potentially enhancement is to import/export CIRCT scheduling problems into and out of well-defined solver formats. For example, SAT problems have a CNF format, and SMT problems have SMT2 format, etc. This might not be directly useful for flows using CIRCT's scheduling library, but at least being able to export problems could open the door for such flows to kick out problems in a well-known format for solver researchers to experiment offline.

jopperm commented 2 years ago

+1 on the idea, though I wouldn't coin this as an import/export format from/to SSP. I think what you're describing is more like a "one-sided scheduler": 1) take a Problem instance, 2) construct a concrete ILP/SAT/SMT/... formulation, and 3) emit that in an appropriate native solver format. However, SSP makes it possible to do this in a small standalone tool (ssp-translate, anyone? :wink:)

mikeurbach commented 2 years ago

Yes, I guess that one direction is the main path I thought of. ssp-translate with options like -export-smt etc is basically what I'm picturing.