Option to use btor2aiger to generate aig files from btor

YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows

Other

379 stars 74 forks source link

Option to use btor2aiger to generate aig files from btor #266

Open KrystalDelusion opened 4 months ago

KrystalDelusion commented 4 months ago

Add btor_aig option, with a value of on triggering aiger designs to build with write_btor and using btor2aiger instead of write_aiger. Includes a somewhat simple test which just runs the same design through SBY with and without this option enabled. Not currently documented as a (potentially) experimental feature.

KrystalDelusion commented 4 months ago

I'm not sure on the best place to put the python wrapper code for btor2aiger. @jix do you think it would fit in sby_core.py (or one of the other existing python files), or should I leave it in the tools folder but add it to the makefile to be installed under $(DESTDIR)$(PREFIX)/bin?

KrystalDelusion commented 3 months ago

Force pushed rebase to latest main and added a test to make test. Rerun ci once YosysHQ/Yosys#4320 is merged.