This repository is no longer maintained and is only kept for archivation. Please, see the newest version AMulet2 instead.

==============================================

Our tool AMulet is able to verify and certify unsigned and signed integer multipliers given as AIGs.

Use ./build.sh to configure and build AMulet and the AIGER library in the aiger sub-directory.

Furthermore, you need to have installed gmp to run AMulet.

See test/README.md for testing AMulet.

Our tool has the following usage amulet <modus> <input.aig> <output files> [<option> ...] . See amulet -h for more detailed options.

For further information we refer to the papers:

Daniela Kaufmann, Armin Biere, Manuel Kauers. Verifying Large Multipliers by Combining SAT and Computer Algebra. In Proc. 19th Intl. Conf. on Formal Methods in Computer Aided Design (FMCAD'19), pages 28-36, IEEE 2019.

and

Daniela Kaufmann, Armin Biere, Manuel Kauers. SAT, Computer Algebra, Multipliers. In Vampire 2018 and Vampire 2019. The 5th and 6th Vampire Workshops, pages 1-18, EasyChair 2020.

Daniela Kaufmann

20.07.2020 AMulet Version 5: Improved:

• Final stage-adder detection for multipliers containing redundant binary addition trees.

16.06.2020 AMulet Version 4: Fixed:

• Fixed bugs in adder substitution for signed multipliers.

02.06.2020 AMulet Version 3: Added features:

• Option '-nss': to generate Nullstellensatz proofs instead of PAC proofs

11.05.2020 AMulet Version 2: Added features:

• Counter examples are generated whenever the final remainder is not 0.
• Option '-swap' swaps input bitvectors a,b and uses alternative names for internal variables.
• Option '-expanded-pac' can be used to generate PAC proofs, where antecedents are extended.
• Option '-print_idx ' allows to manually set the start of the index counter for PAC proofs.

19.03.2020 AMulet Version 1: Initial commit.