From c0bf31e18939a638a062ee8449e1e5d785937506 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 6 Mar 2023 10:03:23 -0500 Subject: [PATCH] write_aig: Normalize symmetry in multiplication 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. --- deps/aig | 2 +- intTests/test1828/.gitignore | 2 ++ intTests/test1828/test.saw | 2 ++ intTests/test1828/test.sh | 9 +++++++++ 4 files changed, 14 insertions(+), 1 deletion(-) create mode 100644 intTests/test1828/.gitignore create mode 100644 intTests/test1828/test.saw create mode 100755 intTests/test1828/test.sh diff --git a/deps/aig b/deps/aig index 00f138637d..5ecac4bada 160000 --- a/deps/aig +++ b/deps/aig @@ -1 +1 @@ -Subproject commit 00f138637d8936566534103878ca895613b7f714 +Subproject commit 5ecac4bada3b905bf0af91a4da89bae398c20a56 diff --git a/intTests/test1828/.gitignore b/intTests/test1828/.gitignore new file mode 100644 index 0000000000..2e31392fa5 --- /dev/null +++ b/intTests/test1828/.gitignore @@ -0,0 +1,2 @@ +left.aig +right.aig diff --git a/intTests/test1828/test.saw b/intTests/test1828/test.saw new file mode 100644 index 0000000000..f839820e50 --- /dev/null +++ b/intTests/test1828/test.saw @@ -0,0 +1,2 @@ +write_aig "left.aig" {{ \x -> x * 0x12345678 }}; +write_aig "right.aig" {{ \x -> 0x12345678 * x }}; diff --git a/intTests/test1828/test.sh b/intTests/test1828/test.sh new file mode 100755 index 0000000000..a914d55337 --- /dev/null +++ b/intTests/test1828/test.sh @@ -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