Version abc80729

1 files changed, 225 insertions, 0 deletions

diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c
new file mode 100644
index 00000000..f11b701f
--- /dev/null
+++ b/src/aig/dch/dchSim.c
@@ -0,0 +1,225 @@
+/**CFile****************************************************************
+
+  FileName    [dchSim.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Computation of equivalence classes using simulation.]
+
+  Synopsis    [Calls to the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 29, 2008.]
+
+  Revision    [$Id: dchSim.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "dchInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline unsigned * Dch_ObjSim( Vec_Ptr_t * vSims, Aig_Obj_t * pObj )
+{ 
+    return Vec_PtrEntry( vSims, pObj->Id ); 
+}
+static inline unsigned Dch_ObjRandomSim()    
+{ 
+    return Aig_ManRandom(0);               
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Perform random simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_PerformRandomSimulation( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords )
+{
+    unsigned * pSim, * pSim0, * pSim1;
+    Aig_Obj_t * pObj;
+    int i, k;
+
+    // assign const 1 sim info
+    pObj = Aig_ManConst1(pAig);
+    pSim = Dch_ObjSim( vSims, pObj );
+    memset( pSim, 0xff, sizeof(unsigned) * nWords );
+
+    // assign primary input random sim info
+    Aig_ManForEachPi( pAig, pObj, i )
+    {
+        pSim = Dch_ObjSim( vSims, pObj );
+        for ( k = 0; k < nWords; k++ )
+            pSim[k] = Dch_ObjRandomSim();
+    }
+
+    // simulate AIG in the topological order
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pSim0 = Dch_ObjSim( vSims, Aig_ObjFanin0(pObj) ); 
+        pSim1 = Dch_ObjSim( vSims, Aig_ObjFanin1(pObj) ); 
+        pSim  = Dch_ObjSim( vSims, pObj );
+
+        if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // both are compls
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = ~pSim0[k] & ~pSim1[k];
+        }
+        else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) // first one is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = ~pSim0[k] & pSim1[k];
+        }
+        else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // second one is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = pSim0[k] & ~pSim1[k];
+        }
+        else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // none is compl
+        {
+            for ( k = 0; k < nWords; k++ )
+                pSim[k] = pSim0[k] & pSim1[k];
+        }
+    }
+
+    // get simulation information for primary outputs
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Hashing nodes by sim info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_HashNodesBySimulationInfo( Aig_Man_t * pAig, Vec_Ptr_t * vSims, int nWords )
+{
+    unsigned * pSim0, * pSim1;
+    Aig_Obj_t * pObj, * pUnique;
+    int i, k, j, nodeId, Counter, c, CountNodes;
+
+    Vec_Int_t * vUniqueNodes, * vNodeCounters;
+
+    vUniqueNodes  = Vec_IntAlloc( 1000 );
+    vNodeCounters = Vec_IntStart( Aig_ManObjNumMax(pAig) );
+
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( Aig_ObjIsPo(pObj) )
+            continue;
+
+        // node's sim info
+        pSim0 = Dch_ObjSim( vSims, pObj );
+
+        Vec_IntForEachEntry( vUniqueNodes, nodeId, j )
+        {
+            pUnique = Aig_ManObj( pAig, nodeId );
+            // unique node's sim info
+            pSim1 = Dch_ObjSim( vSims, pUnique );
+
+            for ( k = 0; k < nWords; k++ )
+                if ( pSim0[k] != pSim1[k] )
+                    break;
+            if ( k == nWords ) // sim info is same as this node
+            {
+                Counter = Vec_IntEntry( vNodeCounters, nodeId );
+                Vec_IntWriteEntry( vNodeCounters, nodeId, Counter+1 );
+                break;
+            }
+        }
+
+        if ( j == Vec_IntSize(vUniqueNodes) ) // sim info of pObj is unique
+        {
+            Vec_IntPush( vUniqueNodes, pObj->Id );
+
+            Counter = Vec_IntEntry( vNodeCounters, pObj->Id );
+            assert( Counter == 0 );
+            Vec_IntWriteEntry( vNodeCounters, pObj->Id, Counter+1 );
+        }
+    }
+
+    Counter = 0;
+    Vec_IntForEachEntry( vNodeCounters, c, k )
+        if ( c > 1 )
+            Counter++;
+
+
+    printf( "Detected %d non-trivial candidate equivalence classes for %d nodes.\n", 
+        Counter, Vec_IntSize(vUniqueNodes) );
+
+    CountNodes = 0;
+    Vec_IntForEachEntry( vUniqueNodes, nodeId, k )
+    {
+        if (  Vec_IntEntry( vNodeCounters, nodeId ) == 1 )
+            continue;
+//        printf( "%d ", Vec_IntEntry( vNodeCounters, nodeId ) );
+        CountNodes += Vec_IntEntry( vNodeCounters, nodeId );
+    }
+//    printf( "\n" );
+    printf( "Nodes participating in non-trivial classes = %d.\n", CountNodes );
+
+
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives candidate equivalence classes of AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dch_Cla_t ** Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose )
+{
+    Dch_Cla_t ** ppClasses;  // place for equivalence classes
+    Aig_MmFlex_t * pMemCla;  // memory for equivalence classes
+    Vec_Ptr_t * vSims;
+
+    // start storage for equivalence classes
+    ppClasses  = CALLOC( Dch_Cla_t *, Aig_ManObjNumMax(pAig) );
+    pMemCla = Aig_MmFlexStart();
+
+    // allocate simulation information
+    vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
+
+    // run simulation
+    Dch_PerformRandomSimulation( pAig, vSims, nWords );
+
+    // hash nodes by sim info
+    Dch_HashNodesBySimulationInfo( pAig, vSims, nWords );
+
+    // collect equivalence classes
+//    ppClasses = NULL;
+
+    // clean up and return
+    Aig_MmFlexStop( pMemCla, 0 );
+    Vec_PtrFree( vSims );
+    return ppClasses;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+