initial commit of public abc

1 files changed, 308 insertions, 0 deletions

diff --git a/src/aig/gia/giaBidec.c b/src/aig/gia/giaBidec.c
new file mode 100644
index 00000000..fc17b582
--- /dev/null
+++ b/src/aig/gia/giaBidec.c
@@ -0,0 +1,308 @@
+/**CFile****************************************************************
+
+  FileName    [giaBidec.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Application of bi-decomposition to AIG minimization.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "bdc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Bdc_FunObjCopy( Bdc_Fun_t * pObj )     { return Gia_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) );  }
+static inline int Bdc_FunFanin0Copy( Bdc_Fun_t * pObj )  { return Bdc_FunObjCopy( Bdc_FuncFanin0(pObj) );                                        }
+static inline int Bdc_FunFanin1Copy( Bdc_Fun_t * pObj )  { return Bdc_FunObjCopy( Bdc_FuncFanin1(pObj) );                                        }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Gia_ManConvertAigToTruth_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vTruth, int nWords, Vec_Int_t * vVisited )
+{
+    unsigned * pTruth, * pTruth0, * pTruth1;
+    int i;
+    assert( !Gia_IsComplement(pObj) );
+    if ( Vec_IntGetEntry(p->vTruths, Gia_ObjId(p, pObj)) != -1 )
+        return (unsigned *)Vec_IntEntryP( vTruth, nWords * Vec_IntGetEntry(p->vTruths, Gia_ObjId(p, pObj)) );
+    // compute the truth tables of the fanins
+    pTruth0 = Gia_ManConvertAigToTruth_rec( p, Gia_ObjFanin0(pObj), vTruth, nWords, vVisited );
+    pTruth1 = Gia_ManConvertAigToTruth_rec( p, Gia_ObjFanin1(pObj), vTruth, nWords, vVisited );
+    // get room for the truth table
+    pTruth = Vec_IntFetch( vTruth, nWords );
+    // create the truth table of the node
+    if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & pTruth1[i];
+    else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = pTruth0[i] & ~pTruth1[i];
+    else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & pTruth1[i];
+    else // if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
+        for ( i = 0; i < nWords; i++ )
+            pTruth[i] = ~pTruth0[i] & ~pTruth1[i];
+    // save the visited node
+    Vec_IntSetEntry( p->vTruths, Gia_ObjId(p, pObj), Vec_IntSize(vVisited) );
+    Vec_IntPush( vVisited, Gia_ObjId(p, pObj) );
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes truth table of the node.]
+
+  Description [Assumes that the structural support is no more than 8 inputs.
+  Uses array vTruth to store temporary truth tables. The returned pointer should 
+  be used immediately.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited )
+{
+    static unsigned uTruths[8][8] = { // elementary truth tables
+        { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA },
+        { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC },
+        { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 },
+        { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 },
+        { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, 
+        { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, 
+        { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
+    };
+    Gia_Obj_t * pObj;
+    Vec_Ptr_t * vTtElems = NULL;
+    unsigned * pTruth;//, * pTruth2;
+    int i, nWords, nVars;
+    // get the number of variables and words
+    nVars  = Vec_IntSize( vLeaves );
+    nWords = Gia_TruthWordNum( nVars );
+    // check the case of a constant
+    if ( Gia_ObjIsConst0( Gia_Regular(pRoot) ) )
+    {
+        Vec_IntClear( vTruth );
+        // get room for the truth table
+        pTruth = Vec_IntFetch( vTruth, nWords );
+        if ( !Gia_IsComplement(pRoot) )
+            Gia_ManTruthClear( pTruth, nVars );
+        else
+            Gia_ManTruthFill( pTruth, nVars );
+        return pTruth;
+    }
+    // if the number of variables is more than 8, allocate truth tables
+    if ( nVars > 8 )
+        vTtElems = Vec_PtrAllocTruthTables( nVars );
+    // assign elementary truth tables
+    Vec_IntClear( vTruth );
+    Vec_IntClear( vVisited );
+    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
+    {
+        // get room for the truth table
+        pTruth = Vec_IntFetch( vTruth, nWords );
+        // assign elementary variable
+        if ( vTtElems )
+            Gia_ManTruthCopy( pTruth, (unsigned *)Vec_PtrEntry(vTtElems, i), nVars );
+        else
+            Gia_ManTruthCopy( pTruth, uTruths[i], nVars );
+        // save the visited node
+        Vec_IntSetEntry( p->vTruths, Gia_ObjId(p, pObj), Vec_IntSize(vVisited) );
+        Vec_IntPush( vVisited, Gia_ObjId(p, pObj) );
+    }
+    if ( vTtElems )
+        Vec_PtrFree( vTtElems );
+    // clear the marks and compute the truth table
+//    pTruth2 = Gia_ManConvertAigToTruth_rec( p, Gia_Regular(pRoot), vTruth, nWords, vVisited );
+    pTruth = Gia_ManConvertAigToTruth_rec( p, Gia_Regular(pRoot), vTruth, nWords, vVisited );
+    // copy the result
+//    Gia_ManTruthCopy( pTruth, pTruth2, nVars );
+    if ( Gia_IsComplement(pRoot) )
+        Gia_ManTruthNot( pTruth, pTruth, nVars );
+    // clean truth tables
+    Gia_ManForEachObjVec( vVisited, p, pObj, i )
+        Vec_IntSetEntry( p->vTruths, Gia_ObjId(p, pObj), -1 );
+    return pTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjPerformBidec( Bdc_Man_t * pManDec, 
+        Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pRoot, 
+        Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited )
+{
+    unsigned * pTruth;
+    Bdc_Fun_t * pFunc;
+    Gia_Obj_t * pFanin;
+    int i, iFan, nVars, nNodes;
+    // collect leaves of this gate
+    Vec_IntClear( vLeaves );
+    Gia_LutForEachFanin( p, Gia_ObjId(p, pRoot), iFan, i )
+        Vec_IntPush( vLeaves, iFan );
+    nVars = Vec_IntSize( vLeaves );
+    assert( nVars < 16 );
+    // derive truth table
+    pTruth = Gia_ManConvertAigToTruth( p, pRoot, vLeaves, vTruth, vVisited );
+//Extra_PrintBinary( stdout, pTruth, (1<<nVars) ); printf( "\n" );
+    if ( Gia_ManTruthIsConst0(pTruth, nVars) )
+    {
+//printf( "Node %d is const0\n", Gia_ObjId(p, pRoot) );
+        return 0;
+    }
+    if ( Gia_ManTruthIsConst1(pTruth, nVars) )
+    {
+//printf( "Node %d is const1\n", Gia_ObjId(p, pRoot) );
+        return 1;
+    }
+    // decompose truth table
+    Bdc_ManDecompose( pManDec, pTruth, NULL, nVars, NULL, 1000 );
+/*
+if ( Bdc_ManNodeNum(pManDec) == 0 )
+    printf( "Node %d has 0 bidec nodes\n", Gia_ObjId(p, pRoot) );
+if ( Kit_TruthSupportSize(pTruth, nVars) != nVars )
+{
+    printf( "Node %d has %d fanins and %d supp size\n", Gia_ObjId(p, pRoot), nVars, Kit_TruthSupportSize(pTruth, nVars) );
+    Gia_LutForEachFanin( p, Gia_ObjId(p, pRoot), iFan, i )
+    {
+        printf( "%d  ", Kit_TruthVarInSupport(pTruth, nVars, i) );
+        Gia_ObjPrint( p, Gia_ManObj(p, iFan) );
+    }
+//    Gia_ManPrintStats( p, 0 );
+}
+*/
+    // convert back into HOP
+    Bdc_FuncSetCopy( Bdc_ManFunc( pManDec, 0 ), Gia_ManConst1(pNew) );
+    Gia_ManForEachObjVec( vLeaves, p, pFanin, i )
+        Bdc_FuncSetCopyInt( Bdc_ManFunc( pManDec, i+1 ), Gia_ObjValue(pFanin) );
+    nNodes = Bdc_ManNodeNum( pManDec );
+    for ( i = nVars + 1; i < nNodes; i++ )
+    {
+        pFunc = Bdc_ManFunc( pManDec, i );
+        Bdc_FuncSetCopyInt( pFunc, Gia_ManHashAnd( pNew, Bdc_FunFanin0Copy(pFunc), Bdc_FunFanin1Copy(pFunc) ) );
+    }
+    return Bdc_FunObjCopy( Bdc_ManRoot(pManDec) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose )
+{
+    Bdc_Man_t * pManDec;
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Vec_Int_t * vLeaves, * vTruth, * vVisited;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, clk = clock();
+    pPars->nVarsMax = Gia_ManLutSizeMax( p );
+    pPars->fVerbose = fVerbose;
+    if ( pPars->nVarsMax < 2 )
+    {
+        printf( "Resynthesis is not performed when nodes have less than 2 inputs.\n" );
+        return NULL;
+    }
+    if ( pPars->nVarsMax > 15 )
+    {
+        printf( "Resynthesis is not performed when nodes have more than 15 inputs.\n" );
+        return NULL;
+    }
+    vLeaves  = Vec_IntAlloc( 0 );
+    vTruth   = Vec_IntAlloc( (1<<16) );
+    vVisited = Vec_IntAlloc( 0 );
+    // clean the old manager
+    Gia_ManCleanTruth( p );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    // start the new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+//    Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) );
+    pManDec = Bdc_ManAlloc( pPars );
+    Gia_ManForEachObj1( p, pObj, i )
+    {        
+        if ( Gia_ObjIsCi(pObj) ) // transfer the CI level (is it needed?)
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+        else if ( Gia_ObjIsLut(p, i) )
+            pObj->Value = Gia_ObjPerformBidec( pManDec, pNew, p, pObj, vLeaves, vTruth, vVisited );
+    }
+    Bdc_ManFree( pManDec );
+    // cleanup the AIG
+    Gia_ManHashStop( pNew );
+    // check the presence of dangling nodes
+    if ( Gia_ManHasDangling(pNew) )
+    {
+        pNew = Gia_ManCleanup( pTemp = pNew );
+        if ( Gia_ManAndNum(pNew) != Gia_ManAndNum(pTemp) )
+            printf( "Gia_ManPerformBidec() node count before and after: %6d and %6d.\n", Gia_ManAndNum(pNew), Gia_ManAndNum(pTemp) );
+        Gia_ManStop( pTemp );
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Vec_IntFree( vLeaves );
+    Vec_IntFree( vTruth );
+    Vec_IntFree( vVisited );
+    if ( fVerbose )
+    {
+//        printf( "Total gain in AIG nodes = %d.  ", Gia_ManObjNum(p)-Gia_ManObjNum(pNew) );
+//        ABC_PRT( "Total runtime", clock() - clk );
+    }
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+