ABC is a logic synthesis and verification system developed by Alan Mishchenko, Prof. Robert Brayton and others. I did a few minor modifications to it for use with our SMT solver beaver. You can download my copy here: abc-70930-modified-1.tar.gz

How to install

One of the changes I did was to use autoconf, automake, which makes compilation as easy as: configure; make install. You can also provide --prefix as usual.

List of changes

• Build infrastructure using autoconf, automake.

• fConjuctionOfPOs flag for Abc_NtkMiterSat and Abc_NtkMiterSatCreate: by default these functions create a CNF in which the POs are OR'ed. If this flag is true, then they are AND'ed instead. That is, the CNF formula asserts that each of the PO is 1.

• Io_WriteCnf: added verbose flag to suppress messages when required. Added fConjunctionOfPOs flag, which is passed to NtkMiterSatCreate.

• Io_WriteAiger: fixed failure of 'assert (uLit0 < uLit1)' on one valid case.

• verCore.c: using 16 bits instead of 8 bits for signal indices (msb, lsb) in the verilog parser.

• Abc_NtkDoCheck now returns 0 if Abc_AigCheck fails. Before, it was only printing a message, which is useless when using ABC as a library.