Version abc80313

3 files changed, 129 insertions, 3 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f311686d..f366a612 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -391,6 +391,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
         extern void Dar_LibStart();
         Dar_LibStart();
     }
+    {
+        extern Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
+//        Bdc_ManDecomposeTest( 0x0f0f0f0f, 3 );
+    }
 } 
 
 /**Function*************************************************************
@@ -10771,6 +10775,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fEdge       =  0;
     pPars->fCutMin     =  0;
     pPars->fSeqMap     =  0;
+    pPars->fBidec      =  0;
     pPars->fVerbose    =  0;
     // internal parameters
     pPars->fTruth      =  0;
@@ -10782,7 +10787,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->pFuncCost   =  NULL;   
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10880,6 +10885,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fLiftLeaves ^= 1;
             break;
+        case 'b':
+            pPars->fBidec ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -11008,7 +11016,7 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsvh]\n" );
+    fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsbvh]\n" );
     fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     fprintf( pErr, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -11025,6 +11033,7 @@ usage:
     fprintf( pErr, "\t-m       : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
 //    fprintf( pErr, "\t-t       : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
+    fprintf( pErr, "\t-b       : toggles deriving local AIGs using bi-decomposition [default = %s]\n", pPars->fBidec? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : prints the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 012b74cf..adf1f6e6 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1567,6 +1567,32 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Fast interpolation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
+{
+    extern void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
+    Aig_Man_t * pManOn, * pManOff;
+    // create internal AIGs
+    pManOn = Abc_NtkToDar( pNtkOn, 0 );
+    if ( pManOn == NULL )
+        return;
+    pManOff = Abc_NtkToDar( pNtkOff, 0 );
+    if ( pManOff == NULL )
+        return;
+    Aig_ManInterFast( pManOn, pManOff, fVerbose );
+    Aig_ManStop( pManOn );
+    Aig_ManStop( pManOff );
+}
 
 int timeCnf;
 int timeSat;
@@ -1587,12 +1613,15 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
 {
     Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
     Abc_Obj_t * pObj;
-    int i;
+    int i, clk = clock();
     if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
     {
         printf( "Currently works only for networks with equal number of POs.\n" );
         return NULL;
     }
+    // compute the fast interpolation time
+//    Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose );
+    // consider the case of one output
     if ( Abc_NtkCoNum(pNtkOn) == 1 )
         return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose );
     // start the new newtork
@@ -1636,6 +1665,7 @@ timeInt = 0;
 //    PRT( "CNF", timeCnf );
 //    PRT( "SAT", timeSat );
 //    PRT( "Int", timeInt );
+//    PRT( "Slow interpolation time", clock() - clk );
 
     // return the network
     if ( !Abc_NtkCheck( pNtkInter ) )
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index bf351a47..a20925b2 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -34,6 +34,7 @@ static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_O
 static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
 
 extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
+extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -84,6 +85,8 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     if ( pNtkNew == NULL )
         return NULL;
     If_ManStop( pIfMan );
+    if ( pPars->fBidec && pPars->nLutSize <= 8 )
+        Abc_NtkBidecResyn( pNtkNew );
 
     // duplicate EXDC
     if ( pNtk->pExdc )
@@ -309,7 +312,9 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
             Abc_NodeComplement( pNodeNew );
     }
     else
+    {
         pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj );
+    }
     If_ObjSetCopy( pIfObj, pNodeNew );
     return pNodeNew;
 }
@@ -545,6 +550,88 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
     return vNodes;
 }
 
+
+#include "bdc.h"
+#include "bdcInt.h"
+
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) );  }
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth )
+{
+    unsigned * pTruth;
+    Bdc_Fun_t * pFunc;
+    int i;
+    // derive truth table
+    pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+    if ( Hop_IsComplement(pRoot) )
+        Extra_TruthNot( pTruth, pTruth, nVars );
+    // decompose truth table
+    Bdc_ManDecompose( p, pTruth, NULL, nVars, NULL, 1000 );
+    // convert back into HOP
+    Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
+    for ( i = 0; i < nVars; i++ )
+        Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
+    for ( i = nVars + 1; i < p->nNodes; i++ )
+    {
+        pFunc = Bdc_FunWithId( p, i );
+        pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
+    }
+    return Bdc_FunCopyHop(p->pRoot);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk )
+{
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Bdc_Man_t * p;
+    Abc_Obj_t * pObj;
+    Vec_Int_t * vTruth;
+    int i, nGainTotal = 0, nNodes1, nNodes2;
+    int clk = clock();
+    pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk );
+    if ( pPars->nVarsMax > 8 )
+    {
+        printf( "Resynthesis is not performed.\n" );
+        return;
+    }
+    vTruth = Vec_IntAlloc( 0 );
+    p = Bdc_ManAlloc( pPars );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nNodes1 = Hop_DagSize(pObj->pData);
+        pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth );
+        nNodes2 = Hop_DagSize(pObj->pData);
+        nGainTotal += nNodes1 - nNodes2;
+    }
+//    printf( "LUTs = %d.  Total gain in AIG nodes = %d.  ", Abc_NtkNodeNum(pNtk), nGainTotal );
+//    PRT( "Time", clock() - clk );
+    Bdc_ManFree( p );
+    Vec_IntFree( vTruth );
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////