Integrating new MFS package with GIA manager.

1 files changed, 389 insertions, 0 deletions

diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
new file mode 100644
index 00000000..aebbb58e
--- /dev/null
+++ b/src/aig/gia/giaMfs.c
@@ -0,0 +1,389 @@
+/**CFile****************************************************************
+
+  FileName    [giaMfs.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Interface with the MFS package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaMfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "bool/kit/kit.h"
+#include "opt/sfm/sfm.h"
+#include "misc/tim/tim.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static word s_ElemVar  = ABC_CONST(0xAAAAAAAAAAAAAAAA);
+static word s_ElemVar2 = ABC_CONST(0xCCCCCCCCCCCCCCCC);
+
+extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManExtractMfs_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vId2Mfs, Vec_Wec_t * vFanins, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths, Vec_Wrd_t * vTruthsTemp )
+{
+    Vec_Int_t * vArray;
+    int i, Fanin;
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    assert( Gia_ObjIsLut(p, iObj) );
+    if ( !~pObj->Value )
+        return;
+    Gia_LutForEachFanin( p, iObj, Fanin, i )
+        Gia_ManExtractMfs_rec( p, Fanin, vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp );
+    pObj->Value = Vec_WecSize(vFanins);
+    vArray = Vec_WecPushLevel( vFanins );
+    Vec_IntGrow( vArray, Gia_ObjLutSize(p, iObj) );
+    Gia_LutForEachFanin( p, iObj, Fanin, i )
+        Vec_IntPush( vArray, Gia_ManObj(p, Fanin)->Value );
+    Vec_StrPush( vFixed, (char)0 );
+    Vec_WrdPush( vTruths, Gia_ObjComputeTruthTable6Lut(p, iObj, vTruthsTemp) );
+    Vec_IntWriteEntry( vId2Mfs, iObj, pObj->Value );
+}
+void Gia_ManExtractMfs_rec2( Gia_Man_t * p, int iObj, Vec_Int_t * vId2Mfs, Vec_Wec_t * vFanins, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths )
+{
+    Vec_Int_t * vArray;
+    Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManExtractMfs_rec2( p, Gia_ObjFaninId0(pObj, iObj), vId2Mfs, vFanins, vFixed, vTruths );
+    Gia_ManExtractMfs_rec2( p, Gia_ObjFaninId1(pObj, iObj), vId2Mfs, vFanins, vFixed, vTruths );
+    pObj->Value = Vec_WecSize(vFanins);
+    vArray = Vec_WecPushLevel( vFanins );
+    Vec_IntGrow( vArray, 2 );
+    Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value );
+    Vec_IntPush( vArray, Gia_ObjFanin1(pObj)->Value );
+    Vec_StrPush( vFixed, (char)1 );
+    Vec_WrdPush( vTruths, (Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar) & (Gia_ObjFaninC1(pObj) ? ~s_ElemVar2 : s_ElemVar2) );
+    Vec_IntWriteEntry( vId2Mfs, iObj, pObj->Value );
+}
+Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t ** pvId2Mfs )
+{
+    Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+    Vec_Int_t * vPoNodes;
+    Vec_Int_t * vId2Mfs;
+    Vec_Wec_t * vFanins;
+    Vec_Str_t * vFixed;
+    Vec_Wrd_t * vTruths, * vTruthsTemp;
+    Vec_Int_t * vArray;
+    Gia_Obj_t * pObj, * pObjBox;
+    int i, k, nRealPis, nRealPos, nPiNum, nPoNum, curCi, curCo;
+    assert( pManTime == NULL || Tim_ManCiNum(pManTime) == Gia_ManCiNum(p) );
+    assert( pManTime == NULL || Tim_ManCoNum(pManTime) == Gia_ManCoNum(p) );
+    // get the real number of PIs and POs
+    nRealPis = pManTime ? Tim_ManPiNum(pManTime) : Gia_ManCiNum(p);
+    nRealPos = pManTime ? Tim_ManPoNum(pManTime) : Gia_ManCoNum(p);
+    // create mapping from GIA into MFS
+    vId2Mfs  = Vec_IntStartFull( Gia_ManObjNum(p) );
+    // collect PO nodes
+    vPoNodes = Vec_IntAlloc( 1000 );
+    // create the arrays
+    vFanins  = Vec_WecAlloc( 1000 );
+    vFixed   = Vec_StrAlloc( 1000 );
+    vTruths  = Vec_WrdAlloc( 1000 );
+    vTruthsTemp = Vec_WrdStart( Gia_ManObjNum(p) );
+    // assign MFS ids to primary inputs
+    Gia_ManFillValue( p );
+    for ( i = 0; i < nRealPis; i++ )
+    {
+        pObj = Gia_ManPi( p, i );
+        pObj->Value = Vec_WecSize(vFanins);
+        Vec_WecPushLevel( vFanins );
+        Vec_StrPush( vFixed, (char)0 );
+        Vec_WrdPush( vTruths, (word)0 );
+        Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+    }
+    // assign MFS ids to black box outputs
+    curCi = nRealPis;
+    curCo = 0;
+    if ( pManTime )
+    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
+    {
+        if ( !Tim_ManBoxIsBlack(pManTime, i) )
+        {
+            // collect POs
+            for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
+            {
+                pObj = Gia_ManPo( p, curCo + k );
+                Vec_IntPush( vPoNodes, Gia_ObjId(p, pObj) );
+            }
+            // assign values to the PIs
+            for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
+            {
+                pObj = Gia_ManPi( p, curCi + k );
+                pObj->Value = Vec_WecSize(vFanins);
+                Vec_WecPushLevel( vFanins );
+                Vec_StrPush( vFixed, (char)1 );
+                Vec_WrdPush( vTruths, (word)0 );
+                Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+            }
+        }
+        curCo += Tim_ManBoxInputNum(pManTime, i);
+        curCi += Tim_ManBoxOutputNum(pManTime, i);
+    }
+    // collect POs
+//    for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ )
+    for ( i = Gia_ManCoNum(p) - nRealPos; i < Gia_ManCoNum(p); i++ )
+    {
+        pObj = Gia_ManPo( p, i );
+        Vec_IntPush( vPoNodes, Gia_ObjId(p, pObj) );
+    }
+    curCo += nRealPos;
+    // verify counts
+    assert( curCi == Gia_ManPiNum(p) );
+    assert( curCo == Gia_ManPoNum(p) );
+    // remeber the end of PIs
+    nPiNum = Vec_WecSize(vFanins);
+    nPoNum = Vec_IntSize(vPoNodes);
+    // assign value to constant node
+    pObj = Gia_ManConst0(p);
+    Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), Vec_WecSize(vFanins) );
+    pObj->Value = Vec_WecSize(vFanins);
+    Vec_WecPushLevel( vFanins );
+    Vec_StrPush( vFixed, (char)0 );
+    Vec_WrdPush( vTruths, (word)0 );
+    Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+    // create internal nodes
+    curCi = nRealPis;
+    curCo = 0;
+    if ( pManTime )
+    for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ )
+    {
+        // recursively add for box inputs
+        Gia_ManIncrementTravId( pBoxes );
+        for ( k = 0; k < Tim_ManBoxInputNum(pManTime, i); k++ )
+        {
+            // build logic
+            pObj = Gia_ManPo( p, curCo + k );
+            Gia_ManExtractMfs_rec( p, Gia_ObjFaninId0p(p, pObj), vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp );
+            // add buffer/inverter
+            pObj->Value = Vec_WecSize(vFanins);
+            vArray = Vec_WecPushLevel( vFanins );
+            Vec_IntGrow( vArray, 1 );
+            assert( !~Gia_ObjFanin0(pObj)->Value );
+            Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value );
+            Vec_StrPush( vFixed, (char)0 );
+            Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar );
+            Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+            // transfer to the PI
+            pObjBox = Gia_ManPi( pBoxes, k );
+            pObjBox->Value = pObj->Value;
+            Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+        }
+        if ( !Tim_ManBoxIsBlack(pManTime, i) )
+        {
+            pObjBox = Gia_ManConst0(pBoxes);
+            pObjBox->Value = Vec_WecSize(vFanins);
+            Vec_WecPushLevel( vFanins );
+            Vec_StrPush( vFixed, (char)0 );
+            Vec_WrdPush( vTruths, (word)0 );
+            Gia_ObjSetTravIdCurrent( pBoxes, pObjBox );
+            // add internal nodes and transfer
+            for ( k = 0; k < Tim_ManBoxOutputNum(pManTime, i); k++ )
+            {
+                // build logic
+                pObjBox = Gia_ManPo( pBoxes, curCi - Tim_ManPiNum(pManTime) + k );
+                Gia_ManExtractMfs_rec2( pBoxes, Gia_ObjFaninId0p(pBoxes, pObjBox), vId2Mfs, vFanins, vFixed, vTruths );
+                // add buffer/inverter
+                vArray = Vec_WecPushLevel( vFanins );
+                Vec_IntGrow( vArray, 1 );
+                assert( !~Gia_ObjFanin0(pObjBox)->Value );
+                Vec_IntPush( vArray, Gia_ObjFanin0(pObjBox)->Value );
+                Vec_StrPush( vFixed, (char)1 );
+                Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObjBox) ? ~s_ElemVar : s_ElemVar );
+                // transfer to the PI
+                pObj = Gia_ManPi( p, curCi + k );
+                pObj->Value = pObjBox->Value;
+            }
+        }
+        curCo += Tim_ManBoxInputNum(pManTime, i);
+        curCi += Tim_ManBoxOutputNum(pManTime, i);
+    }
+    // create POs with buffers
+    Gia_ManForEachObjVec( vPoNodes, p, pObj, i )
+    {
+        Gia_ManExtractMfs_rec( p, Gia_ObjFaninId0p(p, pObj), vId2Mfs, vFanins, vFixed, vTruths, vTruthsTemp );
+        pObj->Value = Vec_WecSize(vFanins);
+        // add buffer/inverter
+        vArray = Vec_WecPushLevel( vFanins );
+        Vec_IntGrow( vArray, 1 );
+        assert( !~Gia_ObjFanin0(pObj)->Value );
+        Vec_IntPush( vArray, Gia_ObjFanin0(pObj)->Value );
+        Vec_StrPush( vFixed, (char)0 );
+        Vec_WrdPush( vTruths, Gia_ObjFaninC0(pObj) ? ~s_ElemVar : s_ElemVar );
+        Vec_IntWriteEntry( vId2Mfs, Gia_ObjId(p, pObj), pObj->Value );
+    }
+    Vec_IntFree( vPoNodes );
+    Vec_WrdFree( vTruthsTemp );
+    *pvId2Mfs = vId2Mfs;
+    return Sfm_NtkConstruct( vFanins, nPiNum, nPoNum, vFixed, vTruths );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManInsertMfs( Gia_Man_t * p, Sfm_Ntk_t * pNtk, Vec_Int_t * vId2Mfs )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vMfsTopo, * vMfs2New, * vArray, * vCover;
+    int i, k, Fanin, iMfsId, iLitNew;
+    word * pTruth;
+    // collect MFS nodes in the topo order
+    vMfsTopo = Sfm_NtkDfs( pNtk );
+    // create mapping from MFS to new GIA literals
+    vMfs2New = Vec_IntStartFull( Vec_IntCap(vMfsTopo) );
+    // start new GIA
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    // map primary inputs
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        iMfsId = Vec_IntEntry( vId2Mfs, Gia_ObjId(p, pObj) );
+        assert( iMfsId >= 0 );
+        Vec_IntWriteEntry( vMfs2New, iMfsId, Gia_ManAppendCi(pNew) );
+    }
+    // map internal nodes
+    vCover = Vec_IntAlloc( 1 << 16 );
+    Vec_IntForEachEntry( vMfsTopo, iMfsId, i )
+    {
+        assert( Sfm_NodeReadUsed(pNtk, iMfsId) );
+        pTruth = Sfm_NodeReadTruth( pNtk, iMfsId );
+        if ( pTruth[0] == 0 || ~pTruth[0] == 0 )
+        {
+            Vec_IntWriteEntry( vMfs2New, iMfsId, 0 );
+            continue;
+        }
+        vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk
+        Vec_IntForEachEntry( vArray, Fanin, k )
+        {
+            iLitNew = Vec_IntEntry( vMfs2New, Fanin );
+            assert( iLitNew >= 0 );
+            Vec_IntWriteEntry( vArray, k, iLitNew );            
+        }
+        // derive new function
+        iLitNew = Kit_TruthToGia( pNew, (unsigned *)pTruth, Vec_IntSize(vArray), vCover, vArray, 0 );
+        Vec_IntWriteEntry( vMfs2New, iMfsId, iLitNew );
+    }
+    Vec_IntFree( vCover );
+    // map output nodes
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        iMfsId = Vec_IntEntry( vId2Mfs, Gia_ObjId(p, pObj) );
+        assert( iMfsId >= 0 );
+        vArray = Sfm_NodeReadFanins( pNtk, iMfsId ); // belongs to pNtk
+        assert( Vec_IntSize(vArray) == 1 );
+        // get the fanin
+        iLitNew = Vec_IntEntry( vMfs2New, Vec_IntEntry(vArray, 0) );
+        assert( iLitNew >= 0 );
+        // create CO
+        assert( pTruth[0] == s_ElemVar || ~pTruth[0] == s_ElemVar );
+        Gia_ManAppendCo( pNew, Abc_LitNotCond(iLitNew, (int)(pTruth[0] != s_ElemVar)) );
+    }
+    Vec_IntFree( vMfs2New );
+    Vec_IntFree( vMfsTopo );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars )
+{
+    Sfm_Ntk_t * pNtk;
+    Vec_Int_t * vId2Mfs;
+    Gia_Man_t * pNew;
+    int nFaninMax, nNodes;
+    assert( Gia_ManRegNum(p) == 0 );
+    assert( p->vMapping != NULL );
+    if ( p->pManTime != NULL && p->pAigExtra == NULL )
+    {
+        Abc_Print( 1, "Timing manager is given but there is no GIA of boxes.\n" );
+        return NULL;
+    }
+    // count fanouts
+    nFaninMax = Gia_ManLutSizeMax( p );
+    if ( nFaninMax > 6 )
+    {
+        Abc_Print( 1, "Currently \"&mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
+        return NULL;
+    }
+    // collect information
+    pNtk = Gia_ManExtractMfs( p, p->pAigExtra, &vId2Mfs );
+    // perform optimization
+    nNodes = Sfm_NtkPerform( pNtk, pPars );
+    // call the fast extract procedure
+    if ( nNodes == 0 )
+    {
+        Abc_Print( 1, "The network is not changed by \"&mfs\".\n" );
+        pNew = Gia_ManDup( p );
+        pNew->vMapping = Vec_IntDup( p->vMapping );
+    }
+    else
+    {
+        pNew = Gia_ManInsertMfs( p, pNtk, vId2Mfs );
+        if( pPars->fVerbose )
+            Abc_Print( 1, "The network has %d nodes changed by \"&mfs\".\n", nNodes );
+    }
+    Vec_IntFree( vId2Mfs );
+    Sfm_NtkFree( pNtk );
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+