From a84c8174e73882f0cdd6433ca27b8222e87dbaa2 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 23 Sep 2015 16:04:06 -0700
Subject: Improving bit-blasting of full-adder.

---
 src/base/abci/abcGen.c  | 43 +++++++++++++++++++++++++++++++++----------
 src/base/cba/cbaBlast.c | 24 +++++++++++++++++++-----
 src/base/wlc/wlcBlast.c | 24 +++++++++++++++++++-----
 3 files changed, 71 insertions(+), 20 deletions(-)

diff --git a/src/base/abci/abcGen.c b/src/base/abci/abcGen.c
index f54dc407..26ee3f86 100644
--- a/src/base/abci/abcGen.c
+++ b/src/base/abci/abcGen.c
@@ -43,19 +43,42 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 void Abc_WriteFullAdder( FILE * pFile )
 {
+    int fNaive = 0;
     fprintf( pFile, ".model FA\n" );
     fprintf( pFile, ".inputs a b cin\n" ); 
     fprintf( pFile, ".outputs s cout\n" ); 
-    fprintf( pFile, ".names a b k\n" ); 
-    fprintf( pFile, "10 1\n" ); 
-    fprintf( pFile, "01 1\n" ); 
-    fprintf( pFile, ".names k cin s\n" ); 
-    fprintf( pFile, "10 1\n" ); 
-    fprintf( pFile, "01 1\n" ); 
-    fprintf( pFile, ".names a b cin cout\n" ); 
-    fprintf( pFile, "11- 1\n" ); 
-    fprintf( pFile, "1-1 1\n" ); 
-    fprintf( pFile, "-11 1\n" ); 
+    if ( fNaive )
+    {
+        fprintf( pFile, ".names a b k\n" ); 
+        fprintf( pFile, "10 1\n" ); 
+        fprintf( pFile, "01 1\n" ); 
+        fprintf( pFile, ".names k cin s\n" ); 
+        fprintf( pFile, "10 1\n" ); 
+        fprintf( pFile, "01 1\n" ); 
+        fprintf( pFile, ".names a b cin cout\n" ); 
+        fprintf( pFile, "11- 1\n" ); 
+        fprintf( pFile, "1-1 1\n" ); 
+        fprintf( pFile, "-11 1\n" ); 
+    }
+    else
+    {
+        fprintf( pFile, ".names a b and1\n" ); 
+        fprintf( pFile, "11 1\n" ); 
+        fprintf( pFile, ".names a b and1_\n" ); 
+        fprintf( pFile, "00 1\n" ); 
+        fprintf( pFile, ".names and1 and1_ xor\n" ); 
+        fprintf( pFile, "00 1\n" ); 
+
+        fprintf( pFile, ".names cin xor and2\n" ); 
+        fprintf( pFile, "11 1\n" ); 
+        fprintf( pFile, ".names cin xor and2_\n" ); 
+        fprintf( pFile, "00 1\n" ); 
+        fprintf( pFile, ".names and2 and2_ s\n" ); 
+        fprintf( pFile, "00 1\n" ); 
+
+        fprintf( pFile, ".names and1 and2 cout\n" ); 
+        fprintf( pFile, "00 0\n" ); 
+    }
     fprintf( pFile, ".end\n" ); 
     fprintf( pFile, "\n" ); 
 }
diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c
index b14b0bcd..322d4372 100644
--- a/src/base/cba/cbaBlast.c
+++ b/src/base/cba/cbaBlast.c
@@ -295,11 +295,25 @@ int Cba_BlastLessSigned( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
 }
 void Cba_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps )
 {
-    int Xor  = Gia_ManHashXor(pNew, a, b);
-    int And1 = Gia_ManHashAnd(pNew, a, b);
-    int And2 = Gia_ManHashAnd(pNew, c, Xor);
-    *ps      = Gia_ManHashXor(pNew, c, Xor);
-    *pc      = Gia_ManHashOr (pNew, And1, And2);
+    int fUseXor = 0;
+    if ( fUseXor )
+    {
+        int Xor  = Gia_ManHashXor(pNew, a, b);
+        int And1 = Gia_ManHashAnd(pNew, a, b);
+        int And2 = Gia_ManHashAnd(pNew, c, Xor);
+        *ps      = Gia_ManHashXor(pNew, c, Xor);
+        *pc      = Gia_ManHashOr (pNew, And1, And2);
+    }
+    else
+    {
+        int And1 = Gia_ManHashAnd(pNew, a, b);
+        int And1_= Gia_ManHashAnd(pNew, Abc_LitNot(a), Abc_LitNot(b));
+        int Xor  = Abc_LitNot(Gia_ManHashOr(pNew, And1, And1_));
+        int And2 = Gia_ManHashAnd(pNew, c, Xor);
+        int And2_= Gia_ManHashAnd(pNew, Abc_LitNot(c), Abc_LitNot(Xor));
+        *ps      = Abc_LitNot(Gia_ManHashOr(pNew, And2, And2_));
+        *pc      = Gia_ManHashOr (pNew, And1, And2);
+    }
 }
 int Cba_BlastAdder( Gia_Man_t * pNew, int Carry, int * pAdd0, int * pAdd1, int nBits ) // result is in pAdd0
 {
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 46fa8d78..757a8005 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -242,11 +242,25 @@ int Wlc_BlastLessSigned( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
 }
 void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps )
 {
-    int Xor  = Gia_ManHashXor(pNew, a, b);
-    int And1 = Gia_ManHashAnd(pNew, a, b);
-    int And2 = Gia_ManHashAnd(pNew, c, Xor);
-    *ps      = Gia_ManHashXor(pNew, c, Xor);
-    *pc      = Gia_ManHashOr (pNew, And1, And2);
+    int fUseXor = 0;
+    if ( fUseXor )
+    {
+        int Xor  = Gia_ManHashXor(pNew, a, b);
+        int And1 = Gia_ManHashAnd(pNew, a, b);
+        int And2 = Gia_ManHashAnd(pNew, c, Xor);
+        *ps      = Gia_ManHashXor(pNew, c, Xor);
+        *pc      = Gia_ManHashOr (pNew, And1, And2);
+    }
+    else
+    {
+        int And1 = Gia_ManHashAnd(pNew, a, b);
+        int And1_= Gia_ManHashAnd(pNew, Abc_LitNot(a), Abc_LitNot(b));
+        int Xor  = Abc_LitNot(Gia_ManHashOr(pNew, And1, And1_));
+        int And2 = Gia_ManHashAnd(pNew, c, Xor);
+        int And2_= Gia_ManHashAnd(pNew, Abc_LitNot(c), Abc_LitNot(Xor));
+        *ps      = Abc_LitNot(Gia_ManHashOr(pNew, And2, And2_));
+        *pc      = Gia_ManHashOr (pNew, And1, And2);
+    }
 }
 void Wlc_BlastAdder( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits ) // result is in pAdd0
 {
-- 
cgit v1.2.3