YosysHQ / imctk

Incremental Model Checking Toolkit
Other
5 stars 2 forks source link

Do not require abc #22

Open jix opened 4 weeks ago

jix commented 4 weeks ago

We're currently only using a small part of abc and most of that only as a stopgap until the relevant already planned functionality is implemented natively.

The only part we're using where there's currently no plan to have a native functionality replacing our use of abc is abc's glucose2 which is a circuit-aware SAT solver with justification support. It happens to be a self contained SAT solver that doesn't depend on any other abc component, so we can depend on it without depending on or building any other part of abc.

Removing abc as dependency would be a significant reduction in non-incremental build time. It also avoids issues where some parts of abc use global state, print to stdout with no way to redirect or disable or cause other problems when using abc as a library.