summaryrefslogtreecommitdiffstats
path: root/src/opt/rwr/rwrLib.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/rwr/rwrLib.c')
-rw-r--r--src/opt/rwr/rwrLib.c362
1 files changed, 362 insertions, 0 deletions
diff --git a/src/opt/rwr/rwrLib.c b/src/opt/rwr/rwrLib.c
new file mode 100644
index 00000000..1cdf350e
--- /dev/null
+++ b/src/opt/rwr/rwrLib.c
@@ -0,0 +1,362 @@
+/**CFile****************************************************************
+
+ FileName [rwrLib.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [DAG-aware AIG rewriting package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: rwrLib.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "rwr.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static Rwr_Node_t * Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume );
+static void Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Precomputes the forest in the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_ManPrecompute( Rwr_Man_t * p )
+{
+ Rwr_Node_t * p0, * p1;
+ int i, k, Level, Volume;
+ int LevelOld = -1;
+ int nNodes;
+
+ Vec_PtrForEachEntryStart( p->vForest, p0, i, 1 )
+ Vec_PtrForEachEntryStart( p->vForest, p1, k, 1 )
+ {
+ if ( LevelOld < (int)p0->Level )
+ {
+ LevelOld = p0->Level;
+ printf( "Starting level %d (at %d nodes).\n", LevelOld+1, i );
+ printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
+ p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+ }
+
+ if ( k == i )
+ break;
+// if ( p0->Level + p1->Level > 6 ) // hard
+// break;
+
+ if ( p0->Level + p1->Level > 5 ) // easy
+ break;
+
+// if ( p0->Level + p1->Level > 6 || (p0->Level == 3 && p1->Level == 3) )
+// break;
+
+ // compute the level and volume of the new nodes
+ Level = 1 + ABC_MAX( p0->Level, p1->Level );
+ Volume = 1 + Rwr_ManNodeVolume( p, p0, p1 );
+ // try four different AND nodes
+ Rwr_ManTryNode( p, p0 , p1 , 0, Level, Volume );
+ Rwr_ManTryNode( p, Rwr_Not(p0), p1 , 0, Level, Volume );
+ Rwr_ManTryNode( p, p0 , Rwr_Not(p1), 0, Level, Volume );
+ Rwr_ManTryNode( p, Rwr_Not(p0), Rwr_Not(p1), 0, Level, Volume );
+ // try EXOR
+ Rwr_ManTryNode( p, p0 , p1 , 1, Level, Volume + 1 );
+ // report the progress
+ if ( p->nConsidered % 50000000 == 0 )
+ printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
+ p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+ // quit after some time
+ if ( p->vForest->nSize == RWR_LIMIT + 5 )
+ {
+ printf( "Considered = %5d M. Found = %8d. Classes = %6d. Trying %7d.\n",
+ p->nConsidered/1000000, p->vForest->nSize, p->nClasses, i );
+ goto save;
+ }
+ }
+save :
+
+ // mark the relevant ones
+ Rwr_ManIncTravId( p );
+ k = 5;
+ nNodes = 0;
+ Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
+ if ( p0->uTruth == p->puCanons[p0->uTruth] )
+ {
+ Rwr_MarkUsed_rec( p, p0 );
+ nNodes++;
+ }
+
+ // compact the array by throwing away non-canonical
+ k = 5;
+ Vec_PtrForEachEntryStart( p->vForest, p0, i, 5 )
+ if ( p0->fUsed )
+ {
+ p->vForest->pArray[k] = p0;
+ p0->Id = k++;
+ }
+ p->vForest->nSize = k;
+ printf( "Total canonical = %4d. Total used = %5d.\n", nNodes, p->vForest->nSize );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManTryNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
+{
+ Rwr_Node_t * pOld, * pNew, ** ppPlace;
+ unsigned uTruth;
+ // compute truth table, level, volume
+ p->nConsidered++;
+ if ( fExor )
+ {
+// printf( "Considering EXOR of %d and %d.\n", p0->Id, p1->Id );
+ uTruth = (p0->uTruth ^ p1->uTruth);
+ }
+ else
+ uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) &
+ (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
+ // skip non-practical classes
+ if ( Level > 2 && !p->pPractical[p->puCanons[uTruth]] )
+ return NULL;
+ // enumerate through the nodes with the same canonical form
+ ppPlace = p->pTable + uTruth;
+ for ( pOld = *ppPlace; pOld; ppPlace = &pOld->pNext, pOld = pOld->pNext )
+ {
+ if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
+ return NULL;
+ if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
+ return NULL;
+// if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
+// return NULL;
+ }
+/*
+ // enumerate through the nodes with the opposite polarity
+ for ( pOld = p->pTable[~uTruth & 0xFFFF]; pOld; pOld = pOld->pNext )
+ {
+ if ( pOld->Level < (unsigned)Level && pOld->Volume < (unsigned)Volume )
+ return NULL;
+ if ( pOld->Level == (unsigned)Level && pOld->Volume < (unsigned)Volume )
+ return NULL;
+// if ( pOld->Level < (unsigned)Level && pOld->Volume == (unsigned)Volume )
+// return NULL;
+ }
+*/
+ // count the classes
+ if ( p->pTable[uTruth] == NULL && p->puCanons[uTruth] == uTruth )
+ p->nClasses++;
+ // create the new node
+ pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+ pNew->Id = p->vForest->nSize;
+ pNew->TravId = 0;
+ pNew->uTruth = uTruth;
+ pNew->Level = Level;
+ pNew->Volume = Volume;
+ pNew->fUsed = 0;
+ pNew->fExor = fExor;
+ pNew->p0 = p0;
+ pNew->p1 = p1;
+ pNew->pNext = NULL;
+ Vec_PtrPush( p->vForest, pNew );
+ *ppPlace = pNew;
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManAddNode( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1, int fExor, int Level, int Volume )
+{
+ Rwr_Node_t * pNew;
+ unsigned uTruth;
+ // compute truth table, leve, volume
+ p->nConsidered++;
+ if ( fExor )
+ uTruth = (p0->uTruth ^ p1->uTruth);
+ else
+ uTruth = (Rwr_IsComplement(p0)? ~Rwr_Regular(p0)->uTruth : Rwr_Regular(p0)->uTruth) &
+ (Rwr_IsComplement(p1)? ~Rwr_Regular(p1)->uTruth : Rwr_Regular(p1)->uTruth) & 0xFFFF;
+ // create the new node
+ pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+ pNew->Id = p->vForest->nSize;
+ pNew->TravId = 0;
+ pNew->uTruth = uTruth;
+ pNew->Level = Level;
+ pNew->Volume = Volume;
+ pNew->fUsed = 0;
+ pNew->fExor = fExor;
+ pNew->p0 = p0;
+ pNew->p1 = p1;
+ pNew->pNext = NULL;
+ Vec_PtrPush( p->vForest, pNew );
+ // do not add if the node is not essential
+ if ( uTruth != p->puCanons[uTruth] )
+ return pNew;
+
+ // add to the list
+ p->nAdded++;
+ if ( p->pTable[uTruth] == NULL )
+ p->nClasses++;
+ Rwr_ListAddToTail( p->pTable + uTruth, pNew );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute )
+{
+ Rwr_Node_t * pNew;
+ pNew = (Rwr_Node_t *)Extra_MmFixedEntryFetch( p->pMmNode );
+ pNew->Id = p->vForest->nSize;
+ pNew->TravId = 0;
+ pNew->uTruth = uTruth;
+ pNew->Level = 0;
+ pNew->Volume = 0;
+ pNew->fUsed = 1;
+ pNew->fExor = 0;
+ pNew->p0 = NULL;
+ pNew->p1 = NULL;
+ pNew->pNext = NULL;
+ Vec_PtrPush( p->vForest, pNew );
+ if ( fPrecompute )
+ Rwr_ListAddToTail( p->pTable + uTruth, pNew );
+ return pNew;
+}
+
+
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_MarkUsed_rec( Rwr_Man_t * p, Rwr_Node_t * pNode )
+{
+ if ( pNode->fUsed || pNode->TravId == p->nTravIds )
+ return;
+ pNode->TravId = p->nTravIds;
+ pNode->fUsed = 1;
+ Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p0) );
+ Rwr_MarkUsed_rec( p, Rwr_Regular(pNode->p1) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_Trav_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, int * pVolume )
+{
+ if ( pNode->fUsed || pNode->TravId == p->nTravIds )
+ return;
+ pNode->TravId = p->nTravIds;
+ (*pVolume)++;
+ if ( pNode->fExor )
+ (*pVolume)++;
+ Rwr_Trav_rec( p, Rwr_Regular(pNode->p0), pVolume );
+ Rwr_Trav_rec( p, Rwr_Regular(pNode->p1), pVolume );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Rwr_ManNodeVolume( Rwr_Man_t * p, Rwr_Node_t * p0, Rwr_Node_t * p1 )
+{
+ int Volume = 0;
+ Rwr_ManIncTravId( p );
+ Rwr_Trav_rec( p, p0, &Volume );
+ Rwr_Trav_rec( p, p1, &Volume );
+ return Volume;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Adds one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Rwr_ManIncTravId( Rwr_Man_t * p )
+{
+ Rwr_Node_t * pNode;
+ int i;
+ if ( p->nTravIds++ < 0x8FFFFFFF )
+ return;
+ Vec_PtrForEachEntry( p->vForest, pNode, i )
+ pNode->TravId = 0;
+ p->nTravIds = 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-04 09:16:26 +0000