-
Notifications
You must be signed in to change notification settings - Fork 62
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Bitblasting a multiplication by a constant should give a network of full adders #1828
Comments
Most likely, this issue revolves around the -- | Multiply two bitvectors with the same size, with result
-- of the same size as the arguments.
-- Overflow is silently discarded.
mul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
mul g x y = assert (length x == length y) $ do
-- Create mutable array to store result.
let n = length y
-- Function to update bits.
let updateBits i z | i == n = return z
updateBits i z = do
z' <- iteM g (y ! i) (add g z (shlC g x i)) (return z)
updateBits (i+1) z'
updateBits 0 $ replicate (length x) (falseLit g) This implements multiplication using a shift-and-add algorithm that adds multiples of What is interesting about this implementation is that when diff --git a/src/Data/AIG/Operations.hs b/src/Data/AIG/Operations.hs
index a48b11a..2c698a8 100644
--- a/src/Data/AIG/Operations.hs
+++ b/src/Data/AIG/Operations.hs
@@ -629,12 +629,14 @@ mul :: IsAIG l g => g s -> BV (l s) -> BV (l s) -> IO (BV (l s))
mul g x y = assert (length x == length y) $ do
-- Create mutable array to store result.
let n = length y
+ let zeroes = replicate (length x) (falseLit g)
-- Function to update bits.
let updateBits i z | i == n = return z
updateBits i z = do
- z' <- iteM g (y ! i) (add g z (shlC g x i)) (return z)
+ x' <- ite g (y ! i) x zeroes
+ z' <- add g z (shlC g x' i)
updateBits (i+1) z'
- updateBits 0 $ replicate (length x) (falseLit g)
+ updateBits 0 zeroes
-- | Unsigned multiply two bitvectors with size @m@ and size @n@,
-- resulting in a vector of size @m+n@. Note how the muxing has been pushed into the
Then running
I am not an expert on |
Another approach is to observe that |
I think it makes sense to normalize symmetry here, simply because it allows for more partial evaluation. In either approach, the old one or the one proposed above, the algorithm does a mux on I also feel like your proposed change above of pushing the |
This implements the idea in GaloisInc/saw-script#1828 (comment).
This implements the idea in GaloisInc/saw-script#1828 (comment).
I've pushed implementations of each of the ideas above as branches in the
@weaversa, can you try building SAW with each of these commits in the |
`mul` will now flip the order of arguments in `mul` if it detects that the first argument is a constant, as this can produce more desirable AIGs if the other argument is symbolic. This is part of an eventual fix for GaloisInc/saw-script#1828.
`mul` will now flip the order of arguments in `mul` if it detects that the first argument is a constant, as this can produce more desirable AIGs if the other argument is symbolic. This is part of an eventual fix for GaloisInc/saw-script#1828.
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.
…plication This tends to play better with libraries such as What4, which use a similar convention. See the Haddocks for `mul`. This is part of an eventual fix for GaloisInc/saw-script#1828.
…plication This tends to play better with libraries such as What4, which use a similar convention. See the Haddocks for `mul`. This is part of an eventual fix for GaloisInc/saw-script#1828.
`mul` will now flip the order of arguments in `mul` if it detects that the second argument is a constant, as this can produce more desirable AIGs if the other argument is symbolic. This is part of an eventual fix for GaloisInc/saw-script#1828.
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.
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.
If you bitblast a multiplication of a variable on the left by a constant on the right,
write_aig
will generate a representation that is a network of full adder circuits, which is useful for methods developed for analyzing circuits with full adders. But if you bitblast a constant multiplication where the variable is on the right, the resulting circuit looks very different, and does not use full adders.The following demonstrates the problem:
In
left.aig
, the circuit almost exclusively uses xors (d+c
andd+c+b
) and majority gates (17(b,c,d)
), whereasright.aig
looks very different.The text was updated successfully, but these errors were encountered: