Improving bit-blasting of full-adder.

src/base/abci/abcGen.c

@@ -43,9 +43,12 @@ 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" ); 
+    if ( fNaive )
+    {
         fprintf( pFile, ".names a b k\n" ); 
         fprintf( pFile, "10 1\n" ); 
         fprintf( pFile, "01 1\n" ); 
@@ -56,6 +59,26 @@ void Abc_WriteFullAdder( FILE * pFile )
         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" ); 
 }

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 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
 {

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 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
 {