Improving bit-blasting of full-adder.

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
 {