initial commit of public abc

1 files changed, 435 insertions, 0 deletions

diff --git a/src/base/abci/abcDress2.c b/src/base/abci/abcDress2.c
new file mode 100644
index 00000000..039a4fed
--- /dev/null
+++ b/src/base/abci/abcDress2.c
@@ -0,0 +1,435 @@
+/**CFile****************************************************************
+
+  FileName    [abcDressw.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Transfers names from one netlist to the other.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcDressw.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "aig.h"
+#include "dch.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+/*
+  Procedure Abc_NtkDressComputeEquivs() implemented in this file computes 
+  equivalence classes of objects of the two networks (pNtk1 and pNtk2).
+
+  It is possible that pNtk1 is the network before synthesis and pNtk2 is the
+  network after synthesis.  The equiv classes of nodes from these networks 
+  can be used to transfer the names from pNtk1 to pNtk2, or vice versa. 
+
+  The above procedure returns the array (Vec_Ptr_t) of integer arrays (Vec_Int_t).
+  Each of the integer arrays contains entries of one equivalence class.
+  Each entry (EquivId) contains the following information: 
+  (1) object ID, which is a number 'num', such that 0 <= 'num' < MaxId 
+      where MaxId is the largest ID of nodes in a network
+  (2) the polarity of the node, which is a binary number, 0 or 1, giving
+      the node's value when pattern (000...0) is applied to the inputs
+  (3) the number of the network, 0 or 1, which stands for pNtk1 and pNtk2, respectively
+  The first array in the array of arrays is empty, or contains nodes that 
+  are equivalent to a constant (if such nodes appear in the network).
+
+  Given EquivID defined above, use the APIs below to get its components.
+*/
+
+// declarations to be added to the application code
+extern int Abc_ObjEquivId2ObjId( int EquivId );
+extern int Abc_ObjEquivId2Polar( int EquivId );
+extern int Abc_ObjEquivId2NtkId( int EquivId );
+
+// definition that may remain in this file
+int Abc_ObjEquivId2ObjId( int EquivId ) { return  EquivId >> 2;      }
+int Abc_ObjEquivId2Polar( int EquivId ) { return (EquivId >> 1) & 1; }
+int Abc_ObjEquivId2NtkId( int EquivId ) { return  EquivId       & 1; }
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern Aig_Man_t *  Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+extern void         Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the dual output miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManCreateDualOutputMiter( Aig_Man_t * p1, Aig_Man_t * p2 )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManPiNum(p1) == Aig_ManPiNum(p2) );
+    assert( Aig_ManPoNum(p1) == Aig_ManPoNum(p2) );
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) );
+    // add first AIG
+    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p1, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    Aig_ManForEachNode( p1, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add second AIG
+    Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p2, pObj, i )
+        pObj->pData = Aig_ManPi( pNew, i );
+    Aig_ManForEachNode( p2, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add the outputs
+    for ( i = 0; i < Aig_ManPoNum(p1); i++ )
+    {
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(Aig_ManPo(p1, i)) );
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(Aig_ManPo(p2, i)) );
+    }
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets polarity attribute of each object in the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDressMapSetPolarity( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj, * pAnd;
+    int i;
+    // each node refers to the the strash copy whose polarity is set
+    Abc_NtkForEachObj( pNtk, pObj, i )
+    {
+        if ( (pAnd = Abc_ObjRegular(pObj->pCopy)) && Abc_ObjType(pAnd) != ABC_OBJ_NONE ) // strashed object is present and legal
+            pObj->fPhase = pAnd->fPhase ^ Abc_ObjIsComplement(pObj->pCopy);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create mapping of node IDs of pNtk into equiv classes of pMiter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkDressMapClasses( Aig_Man_t * pMiter, Abc_Ntk_t * pNtk )
+{
+    Vec_Int_t * vId2Lit;
+    Abc_Obj_t * pObj, * pAnd;
+    Aig_Obj_t * pObjMan, * pObjMiter, * pObjRepr;
+    int i;
+    vId2Lit = Vec_IntAlloc( 0 );
+    Vec_IntFill( vId2Lit, Abc_NtkObjNumMax(pNtk), -1 );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        // get the pointer to the miter node corresponding to pObj
+        if ( (pAnd = Abc_ObjRegular(pObj->pCopy)) && Abc_ObjType(pAnd) != ABC_OBJ_NONE &&          // strashed node is present and legal
+             (pObjMan = Aig_Regular((Aig_Obj_t *)pAnd->pCopy)) && Aig_ObjType(pObjMan) != AIG_OBJ_NONE &&       // AIG node is present and legal
+             (pObjMiter = Aig_Regular((Aig_Obj_t *)pObjMan->pData)) && Aig_ObjType(pObjMiter) != AIG_OBJ_NONE ) // miter node is present and legal
+        {
+            // get the representative of the miter node
+            pObjRepr = Aig_ObjRepr( pMiter, pObjMiter );
+            pObjRepr = pObjRepr? pObjRepr : pObjMiter;
+            // map pObj (whose ID is i) into the repr node ID (i.e. equiv class)
+            Vec_IntWriteEntry( vId2Lit, i, Aig_ObjId(pObjRepr) );
+        }
+    }
+    return vId2Lit;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the vector of given equivalence class of objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_ObjDressClass( Vec_Ptr_t * vRes, Vec_Int_t * vClass2Num, int Class )
+{
+    int ClassNumber;
+    assert( Class > 0 );
+    ClassNumber = Vec_IntEntry( vClass2Num, Class );
+    assert( ClassNumber != 0 );
+    if ( ClassNumber > 0 )
+        return (Vec_Int_t *)Vec_PtrEntry( vRes, ClassNumber ); // previous class
+    // create new class
+    Vec_IntWriteEntry( vClass2Num, Class, Vec_PtrSize(vRes) );
+    Vec_PtrPush( vRes, Vec_IntAlloc(4) );
+    return (Vec_Int_t *)Vec_PtrEntryLast( vRes ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the ID of a node in an equivalence class.]
+
+  Description [The ID is composed of three parts: object ID, followed
+  by one bit telling the phase of this node, followed by one bit
+  telling the network to which this node belongs.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ObjDressMakeId( Abc_Ntk_t * pNtk, int ObjId, int iNtk )
+{
+    return (ObjId << 2) | (Abc_NtkObj(pNtk,ObjId)->fPhase << 1) | iNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes equivalence classes of objects in pNtk1 and pNtk2.]
+
+  Description [Internal procedure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDressMapIds( Aig_Man_t * pMiter, Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+{
+    Vec_Ptr_t * vRes;
+    Vec_Int_t * vId2Lit1, * vId2Lit2, * vCounts0, * vCounts1, * vClassC, * vClass2Num;
+    int i, Class;
+    // start the classes
+    vRes = Vec_PtrAlloc( 1000 );
+    // set polarity of the nodes
+    Abc_NtkDressMapSetPolarity( pNtk1 );
+    Abc_NtkDressMapSetPolarity( pNtk2 );
+    // create mapping of node IDs of pNtk1/pNtk2 into the IDs of equiv classes of pMiter
+    vId2Lit1 = Abc_NtkDressMapClasses( pMiter, pNtk1 );
+    vId2Lit2 = Abc_NtkDressMapClasses( pMiter, pNtk2 );
+    // count the number of nodes in each equivalence class
+    vCounts0 = Vec_IntStart( Aig_ManObjNumMax(pMiter) );
+    Vec_IntForEachEntry( vId2Lit1, Class, i )
+        if ( Class >= 0 )
+            Vec_IntAddToEntry( vCounts0, Class, 1 );
+    vCounts1 = Vec_IntStart( Aig_ManObjNumMax(pMiter) );
+    Vec_IntForEachEntry( vId2Lit2, Class, i )
+        if ( Class >= 0 )
+            Vec_IntAddToEntry( vCounts1, Class, 1 );
+    // get the costant class
+    vClassC = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vId2Lit1, Class, i )
+        if ( Class == 0 )
+            Vec_IntPush( vClassC, Abc_ObjDressMakeId(pNtk1, i, 0) );
+    Vec_IntForEachEntry( vId2Lit2, Class, i )
+        if ( Class == 0 )
+            Vec_IntPush( vClassC, Abc_ObjDressMakeId(pNtk2, i, 1) );
+    Vec_PtrPush( vRes, vClassC );
+    // map repr node IDs into class numbers
+    vClass2Num = Vec_IntAlloc( 0 );
+    Vec_IntFill( vClass2Num, Aig_ManObjNumMax(pMiter), -1 );
+    // keep classes having at least one element from pNtk1 and one from pNtk2
+    Vec_IntForEachEntry( vId2Lit1, Class, i )
+        if ( Class > 0 && Vec_IntEntry(vCounts0, Class) && Vec_IntEntry(vCounts1, Class) )
+            Vec_IntPush( Abc_ObjDressClass(vRes, vClass2Num, Class), Abc_ObjDressMakeId(pNtk1, i, 0) );
+    Vec_IntForEachEntry( vId2Lit2, Class, i )
+        if ( Class > 0 && Vec_IntEntry(vCounts0, Class) && Vec_IntEntry(vCounts1, Class) )
+            Vec_IntPush( Abc_ObjDressClass(vRes, vClass2Num, Class), Abc_ObjDressMakeId(pNtk2, i, 1) );
+    // package them accordingly
+    Vec_IntFree( vClass2Num );
+    Vec_IntFree( vCounts0 );
+    Vec_IntFree( vCounts1 );
+    Vec_IntFree( vId2Lit1 );
+    Vec_IntFree( vId2Lit2 );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes equivalence classes of objects in pNtk1 and pNtk2.]
+
+  Description [Returns the array (Vec_Ptr_t) of integer arrays (Vec_Int_t).
+  Each of the integer arrays contains entries of one equivalence class.
+  Each entry contains the following information: the network number (0/1),
+  the polarity (0/1) and the object ID in the the network (0 <= num < MaxId)
+  where MaxId is the largest number of an ID of an object in that network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkDressComputeEquivs( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConflictLimit, int fVerbose )
+{
+    Dch_Pars_t Pars, * pPars = &Pars;
+    Abc_Ntk_t * pAig1, * pAig2;
+    Aig_Man_t * pMan1, * pMan2, * pMiter;
+    Vec_Ptr_t * vRes;
+    assert( !Abc_NtkIsStrash(pNtk1) );
+    assert( !Abc_NtkIsStrash(pNtk2) );
+    // convert network into AIG
+    pAig1 = Abc_NtkStrash( pNtk1, 1, 1, 0 );
+    pAig2 = Abc_NtkStrash( pNtk2, 1, 1, 0 );
+    pMan1 = Abc_NtkToDar( pAig1, 0, 0 );
+    pMan2 = Abc_NtkToDar( pAig2, 0, 0 );
+    // derive the miter
+    pMiter = Aig_ManCreateDualOutputMiter( pMan1, pMan2 );
+    // set up parameters for SAT sweeping
+    Dch_ManSetDefaultParams( pPars );
+    pPars->nBTLimit = nConflictLimit;
+    pPars->fVerbose = fVerbose;
+    // perform SAT sweeping
+    Dch_ComputeEquivalences( pMiter, pPars );
+    // now, pMiter is annotated with the equivl class info
+    // convert this info into the resulting array
+    vRes = Abc_NtkDressMapIds( pMiter, pNtk1, pNtk2 );
+    Aig_ManStop( pMiter );
+    Aig_ManStop( pMan1 );
+    Aig_ManStop( pMan2 );
+    Abc_NtkDelete( pAig1 );
+    Abc_NtkDelete( pAig2 );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints information about node equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDressPrintEquivs( Vec_Ptr_t * vRes )
+{
+    Vec_Int_t * vClass;
+    int i, k, Entry;
+    Vec_PtrForEachEntry( Vec_Int_t *, vRes, vClass, i )
+    {
+        printf( "Class %5d : ", i );
+        printf( "Num =%5d    ", Vec_IntSize(vClass) );
+        Vec_IntForEachEntry( vClass, Entry, k )
+            printf( "%5d%c%d ", 
+                Abc_ObjEquivId2ObjId(Entry), 
+                Abc_ObjEquivId2Polar(Entry)? '-':'+', 
+                Abc_ObjEquivId2NtkId(Entry) );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints information about node equivalences.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDressPrintStats( Vec_Ptr_t * vRes, int nNodes0, int nNodes1, int Time )
+{
+    Vec_Int_t * vClass;
+    int i, k, Entry;
+    int NegAll[2] = {0}, PosAll[2] = {0}, PairsAll = 0, PairsOne = 0;
+    int Pos[2], Neg[2];
+    // count the number of equivalences in each class
+    Vec_PtrForEachEntry( Vec_Int_t *, vRes, vClass, i )
+    {
+        Pos[0] = Pos[1] = 0;
+        Neg[0] = Neg[1] = 0;
+        Vec_IntForEachEntry( vClass, Entry, k )
+        {
+            if ( Abc_ObjEquivId2NtkId(Entry) )
+            {
+                if ( Abc_ObjEquivId2Polar(Entry) )
+                    Neg[1]++; // negative polarity in network 1
+                else
+                    Pos[1]++; // positive polarity in network 1
+            }
+            else
+            {
+                if ( Abc_ObjEquivId2Polar(Entry) )
+                    Neg[0]++; // negative polarity in network 0
+                else
+                    Pos[0]++; // positive polarity in network 0
+            }
+        }
+        PosAll[0] += Pos[0]; // total positive polarity in network 0
+        PosAll[1] += Pos[1]; // total positive polarity in network 1
+        NegAll[0] += Neg[0]; // total negative polarity in network 0
+        NegAll[1] += Neg[1]; // total negative polarity in network 1
+
+        // assuming that the name can be transferred to only one node
+        PairsAll += ABC_MIN(Neg[0] + Pos[0], Neg[1] + Pos[1]);
+        PairsOne += ABC_MIN(Neg[0], Neg[1]) + ABC_MIN(Pos[0], Pos[1]);
+    }
+    printf( "Total number of equiv classes                = %7d.\n", Vec_PtrSize(vRes) );
+    printf( "Participating nodes from both networks       = %7d.\n", NegAll[0]+PosAll[0]+NegAll[1]+PosAll[1] );
+    printf( "Participating nodes from the first network   = %7d. (%7.2f %% of nodes)\n", NegAll[0]+PosAll[0], 100.0*(NegAll[0]+PosAll[0])/(nNodes0+1) );
+    printf( "Participating nodes from the second network  = %7d. (%7.2f %% of nodes)\n", NegAll[1]+PosAll[1], 100.0*(NegAll[1]+PosAll[1])/(nNodes1+1) );
+    printf( "Node pairs (any polarity)                    = %7d. (%7.2f %% of names can be moved)\n", PairsAll, 100.0*PairsAll/(nNodes0+1) );
+    printf( "Node pairs (same polarity)                   = %7d. (%7.2f %% of names can be moved)\n", PairsOne, 100.0*PairsOne/(nNodes0+1) );
+    ABC_PRT( "Total runtime", Time );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transfers names from pNtk1 to pNtk2.]
+
+  Description [Internally calls new procedure for mapping node IDs of
+  both networks into the shared equivalence classes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDress2( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConflictLimit, int fVerbose )
+{
+    Vec_Ptr_t * vRes;
+    int clk = clock();
+    vRes = Abc_NtkDressComputeEquivs( pNtk1, pNtk2, nConflictLimit, fVerbose );
+//    Abc_NtkDressPrintEquivs( vRes );
+    Abc_NtkDressPrintStats( vRes, Abc_NtkNodeNum(pNtk1), Abc_NtkNodeNum(pNtk1), clock() - clk );
+    Vec_VecFree( (Vec_Vec_t *)vRes );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+