Added min-cut-based refinement of gate-level abstraction (command &gla_refine).

1 files changed, 185 insertions, 0 deletions

diff --git a/src/opt/nwk/nwkAig.c b/src/opt/nwk/nwkAig.c
index 6254bc41..a4959c9a 100644
--- a/src/opt/nwk/nwkAig.c
+++ b/src/opt/nwk/nwkAig.c
@@ -103,6 +103,191 @@ Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fVerbose
     return vNodes;
 }
 
+
+
+#include "src/aig/gia/gia.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Collects reachable nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManColleacReached_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, Vec_Int_t * vLeaves )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+    {
+        Vec_IntPush( vLeaves, Gia_ObjId(p, pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Nwk_ManColleacReached_rec( p, Gia_ObjFanin0(pObj), vNodes, vLeaves );
+    Nwk_ManColleacReached_rec( p, Gia_ObjFanin1(pObj), vNodes, vLeaves );
+    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Nwk_Man_t * Nwk_ManCreateFromGia( Gia_Man_t * p, Vec_Int_t * vPPis, Vec_Int_t * vNodes, Vec_Int_t * vLeaves, Vec_Int_t ** pvMapInv )
+{
+    Nwk_Man_t * pNtk;
+    Nwk_Obj_t ** ppCopies;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vMaps;
+    int i;
+    assert( Vec_IntSize(vLeaves) >= Vec_IntSize(vPPis) );
+    Gia_ManCreateRefs( p );
+    pNtk = Nwk_ManAlloc();
+    pNtk->pName = Abc_UtilStrsav( p->pName );
+    pNtk->nFanioPlus = 0;
+    Hop_ManStop( pNtk->pManHop );
+    pNtk->pManHop = NULL;
+    // allocate
+    vMaps = Vec_IntAlloc( Vec_IntSize(vNodes) + Abc_MaxInt(Vec_IntSize(vPPis), Vec_IntSize(vLeaves)) + 1 );
+    ppCopies = ABC_ALLOC( Nwk_Obj_t *, Gia_ManObjNum(p) );
+    // copy objects
+    pObj = Gia_ManConst0(p);
+    ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 0, Gia_ObjRefs(p,pObj) );
+    Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
+    Gia_ManForEachObjVec( vLeaves, p, pObj, i )
+    {
+        ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) );
+        assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) );
+        Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
+    }
+/*
+    for ( i = Vec_IntSize(vLeaves); i < Vec_IntSize(vPPis); i++ )
+    {
+        pTemp = Nwk_ManCreateCi( pNtk, Gia_ObjRefs(p,pObj) );
+        Vec_IntPush( vMaps, 0 );// ???
+    }
+*/
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
+    {
+        ppCopies[Gia_ObjId(p,pObj)] = Nwk_ManCreateNode( pNtk, 2, Gia_ObjRefs(p,pObj) );
+        Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId0p(p,pObj)] );
+        Nwk_ObjAddFanin( ppCopies[Gia_ObjId(p,pObj)], ppCopies[Gia_ObjFaninId1p(p,pObj)] );
+        assert( Vec_IntSize(vMaps) == Nwk_ObjId(ppCopies[Gia_ObjId(p,pObj)]) );
+        Vec_IntPush( vMaps, Gia_ObjId(p,pObj) );
+    }
+    Gia_ManForEachObjVec( vPPis, p, pObj, i )
+    {
+        assert( ppCopies[Gia_ObjId(p,pObj)] != NULL );
+        Nwk_ObjAddFanin( Nwk_ManCreateCo(pNtk), ppCopies[Gia_ObjId(p,pObj)] );
+    }
+    for ( i = Vec_IntSize(vPPis); i < Vec_IntSize(vLeaves); i++ )
+        Nwk_ObjAddFanin( Nwk_ManCreateCo(pNtk), ppCopies[0] );
+    assert( Vec_IntSize(vMaps) == Vec_IntSize(vNodes) + Abc_MaxInt(Vec_IntSize(vPPis), Vec_IntSize(vLeaves)) + 1 );
+    ABC_FREE( ppCopies );
+    *pvMapInv = vMaps;
+    return pNtk;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns min-cut in the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose )
+{
+    Nwk_Man_t * pNtk;
+    Nwk_Obj_t * pNode;
+    Vec_Ptr_t * vMinCut;
+    Vec_Int_t * vPPis, * vNodes, * vLeaves, * vNodes2, * vLeaves2, * vMapInv;
+    Vec_Int_t * vCommon, * vDiff0, * vDiff1;
+    Gia_Obj_t * pObj;
+    int i, iObjId;
+    // get inputs
+    Gia_GlaCollectInputs( p, p->vGateClasses, NULL, &vPPis );
+    // collect nodes rechable from PPIs
+    vNodes = Vec_IntAlloc( 100 );
+    vLeaves = Vec_IntAlloc( 100 );
+    Gia_ManIncrementTravId( p );
+    Gia_ManForEachObjVec( vPPis, p, pObj, i )
+        Nwk_ManColleacReached_rec( p, pObj, vNodes, vLeaves );
+    // derive the new network
+    pNtk = Nwk_ManCreateFromGia( p, vPPis, vNodes, vLeaves, &vMapInv );
+    assert( Nwk_ManPiNum(pNtk) == Nwk_ManPoNum(pNtk) );
+    // create min-cut
+    vMinCut = Nwk_ManRetimeCutBackward( pNtk, Nwk_ManPiNum(pNtk), fVerbose );
+    // copy from the GIA back
+//    Aig_ManForEachObj( p, pObj, i )
+//        ((Nwk_Obj_t *)pObj->pData)->pCopy = pObj;
+    // mark min-cut nodes
+    vNodes2 = Vec_IntAlloc( 100 );
+    vLeaves2 = Vec_IntAlloc( 100 );
+    Gia_ManIncrementTravId( p );
+    Vec_PtrForEachEntry( Nwk_Obj_t *, vMinCut, pNode, i )
+    {
+        pObj = Gia_ManObj( p, Vec_IntEntry(vMapInv, Nwk_ObjId(pNode)) );
+        if ( Gia_ObjIsConst0(pObj) )
+            continue;
+        Nwk_ManColleacReached_rec( p, pObj, vNodes2, vLeaves2 );
+    }
+    if ( fVerbose )
+        printf( "Min-cut: %d -> %d.  Nodes %d -> %d.  ", Vec_IntSize(vPPis)+1, Vec_PtrSize(vMinCut), Vec_IntSize(vNodes), Vec_IntSize(vNodes2) );
+    Vec_IntFree( vPPis );
+    Vec_PtrFree( vMinCut );
+    Vec_IntFree( vMapInv );
+    Nwk_ManFree( pNtk );
+
+    // sort the results
+    Vec_IntSort( vNodes, 0 );
+    Vec_IntSort( vNodes2, 0 );
+    vCommon = Vec_IntAlloc( Vec_IntSize(vNodes) );
+    vDiff0 = Vec_IntAlloc( 100 );
+    vDiff1 = Vec_IntAlloc( 100 );
+    Vec_IntTwoSplit( vNodes, vNodes2, vCommon, vDiff0, vDiff1 );
+    if ( fVerbose )
+        printf( "Common = %d.  Diff0 = %d. Diff1 = %d.\n", Vec_IntSize(vCommon), Vec_IntSize(vDiff0), Vec_IntSize(vDiff1) );
+
+    // fill in
+    Vec_IntForEachEntry( vDiff0, iObjId, i )
+        Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
+
+    Vec_IntFree( vLeaves );
+    Vec_IntFree( vNodes );
+    Vec_IntFree( vLeaves2 );
+    Vec_IntFree( vNodes2 );
+
+    Vec_IntFree( vCommon );
+    Vec_IntFree( vDiff0 );
+    Vec_IntFree( vDiff1 );
+
+    // check abstraction
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Vec_IntEntry( p->vGateClasses, i ) == 0 )
+            continue;
+        assert( Gia_ObjIsConst0(pObj) || Gia_ObjIsRo(p, pObj) || Gia_ObjIsAnd(pObj) );
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////