Skip to content

Commit

Permalink
write_aig: Normalize symmetry in multiplication
Browse files Browse the repository at this point in the history
This bumps the `aig` submodule to bring in the changes from GaloisInc/aig#14,
which changes how `aig` performs multiplication to swap the order of arguments
if the first argument is a constant. This is because the algorithm that `mul`
uses to compute multiplication is biased in its order of arguments, and having
the second argument be a constant produces a network with more full adders,
which is generally more beneficial.  I have added a test case to check to see
if the test case from #1828 now produces identical AIGs regardless of the order
of arguments.

Fixes #1828.
  • Loading branch information
RyanGlScott committed Mar 6, 2023
1 parent 9d66afc commit c0bf31e
Show file tree
Hide file tree
Showing 4 changed files with 14 additions and 1 deletion.
2 changes: 1 addition & 1 deletion deps/aig
Submodule aig updated 1 files
+27 −1 src/Data/AIG/Operations.hs
2 changes: 2 additions & 0 deletions intTests/test1828/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
left.aig
right.aig
2 changes: 2 additions & 0 deletions intTests/test1828/test.saw
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
write_aig "left.aig" {{ \x -> x * 0x12345678 }};
write_aig "right.aig" {{ \x -> 0x12345678 * x }};
9 changes: 9 additions & 0 deletions intTests/test1828/test.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
set -e

# This test case uses `write_aiger` to produce AIG files for two nearly
# identical functions, where the only difference is the order of arguments (one
# symbolic and one concrete) in a bitvector multiplication. If the `aig` library
# does its job correctly, these should produce identical AIG files, so check
# this using `diff`.
$SAW test.saw
diff -ru left.aig right.aig

0 comments on commit c0bf31e

Please sign in to comment.