From eb05b49c74417885f1387d714f761cf54032e866 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 second argument is a constant. This has two benefits: * This ensures that `write_aig` will produce the same networks for `X * C` and `C * X`, where `C` is a constant and `X` is a variable. * The algorithm that `mul` uses to compute multiplication is biased in its order of arguments, and having the first argument be a constant tends to produce networks that ABC has an easier time verifying. (The FFS example under `doc/tutorial/code/ffs.c` is a notable example of this.) 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..adc0ca5666 160000 --- a/deps/aig +++ b/deps/aig @@ -1 +1 @@ -Subproject commit 00f138637d8936566534103878ca895613b7f714 +Subproject commit adc0ca56664804d5f1e7e8d8f794a5c1104068aa 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