summaryrefslogtreecommitdiffstats
path: root/src/opt/lpk/lpkMulti.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/lpk/lpkMulti.c')
-rw-r--r--src/opt/lpk/lpkMulti.c495
1 files changed, 495 insertions, 0 deletions
diff --git a/src/opt/lpk/lpkMulti.c b/src/opt/lpk/lpkMulti.c
new file mode 100644
index 00000000..82cf3578
--- /dev/null
+++ b/src/opt/lpk/lpkMulti.c
@@ -0,0 +1,495 @@
+/**CFile****************************************************************
+
+ FileName [lpkMulti.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Fast Boolean matching for LUT structures.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: lpkMulti.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "lpkInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Records variable order.]
+
+ Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_CreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] )
+{
+ Kit_DsdObj_t * pObj;
+ unsigned uSuppFanins, k;
+ int Above[16], Below[16];
+ int nAbove, nBelow, iFaninLit, i, x, y;
+ // iterate through the nodes
+ Kit_DsdNtkForEachObj( pNtk, pObj, i )
+ {
+ // collect fanin support of this node
+ nAbove = 0;
+ uSuppFanins = 0;
+ Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k )
+ {
+ if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) )
+ Above[nAbove++] = Kit_DsdLit2Var(iFaninLit);
+ else
+ uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit );
+ }
+ // find the below variables
+ nBelow = 0;
+ for ( y = 0; y < 16; y++ )
+ if ( uSuppFanins & (1 << y) )
+ Below[nBelow++] = y;
+ // create all pairs
+ for ( x = 0; x < nAbove; x++ )
+ for ( y = 0; y < nBelow; y++ )
+ pTable[Above[x]][Below[y]]++;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates commmon variable order.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_CreateCommonOrder( char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose )
+{
+ int Score[16] = {0}, pPres[16];
+ int i, y, x, iVarBest, ScoreMax, PrioCount;
+
+ // mark the present variables
+ for ( i = 0; i < nVars; i++ )
+ pPres[i] = 1;
+ // remove cofactored variables
+ for ( i = 0; i < nCBars; i++ )
+ pPres[piCofVar[i]] = 0;
+
+ // compute scores for each leaf
+ for ( i = 0; i < nVars; i++ )
+ {
+ if ( pPres[i] == 0 )
+ continue;
+ for ( y = 0; y < nVars; y++ )
+ Score[i] += pTable[i][y];
+ for ( x = 0; x < nVars; x++ )
+ Score[i] -= pTable[x][i];
+ }
+
+ // print the scores
+ if ( fVerbose )
+ {
+ printf( "Scores: " );
+ for ( i = 0; i < nVars; i++ )
+ printf( "%c=%d ", 'a'+i, Score[i] );
+ printf( " " );
+ printf( "Prios: " );
+ }
+
+ // derive variable priority
+ // variables with equal score receive the same priority
+ for ( i = 0; i < nVars; i++ )
+ pPrios[i] = 16;
+
+ // iterate until variables remain
+ for ( PrioCount = 1; ; PrioCount++ )
+ {
+ // find the present variable with the highest score
+ iVarBest = -1;
+ ScoreMax = -100000;
+ for ( i = 0; i < nVars; i++ )
+ {
+ if ( pPres[i] == 0 )
+ continue;
+ if ( ScoreMax < Score[i] )
+ {
+ ScoreMax = Score[i];
+ iVarBest = i;
+ }
+ }
+ if ( iVarBest == -1 )
+ break;
+ // give the next priority to all vars having this score
+ if ( fVerbose )
+ printf( "%d=", PrioCount );
+ for ( i = 0; i < nVars; i++ )
+ {
+ if ( pPres[i] == 0 )
+ continue;
+ if ( Score[i] == ScoreMax )
+ {
+ pPrios[i] = PrioCount;
+ pPres[i] = 0;
+ if ( fVerbose )
+ printf( "%c", 'a'+i );
+ }
+ }
+ if ( fVerbose )
+ printf( " " );
+ }
+ if ( fVerbose )
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Finds components with the highest priority.]
+
+ Description [Returns the number of components selected.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_FindHighest( Kit_DsdNtk_t ** ppNtks, int * piLits, int nSize, int * pPrio, int * pDecision )
+{
+ Kit_DsdObj_t * pObj;
+ unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge;
+ int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv;
+
+ // find individual support and total support
+ uSuppTotal = 0;
+ for ( i = 0; i < nSize; i++ )
+ {
+ pTriv[i] = 1;
+ if ( piLits[i] < 0 )
+ uSupps[i] = 0;
+ else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) )
+ uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] );
+ else
+ {
+ pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
+ if ( pObj->Type == KIT_DSD_PRIME )
+ {
+ pTriv[i] = 0;
+ uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] );
+ }
+ else
+ {
+ assert( pObj->nFans == 2 );
+ if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) )
+ pTriv[i] = 0;
+ uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] );
+ }
+ uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin;
+ }
+ assert( uSupps[i] <= 0xFFFF );
+ uSuppTotal |= uSupps[i];
+ }
+ if ( uSuppTotal == 0 )
+ return 0;
+
+ // find one support variable with the highest priority
+ PrioMin = ABC_INFINITY;
+ iVarMax = -1;
+ for ( i = 0; i < 16; i++ )
+ if ( uSuppTotal & (1 << i) )
+ if ( PrioMin > pPrio[i] )
+ {
+ PrioMin = pPrio[i];
+ iVarMax = i;
+ }
+ assert( iVarMax != -1 );
+
+ // select components, which have this variable
+ nComps = 0;
+ fOneNonTriv = 0;
+ uSuppLarge = 0;
+ for ( i = 0; i < nSize; i++ )
+ if ( uSupps[i] & (1<<iVarMax) )
+ {
+ if ( pTriv[i] || !fOneNonTriv )
+ {
+ if ( !pTriv[i] )
+ {
+ uSuppLarge = uSupps[i];
+ fOneNonTriv = 1;
+ }
+ pDecision[i] = 1;
+ nComps++;
+ }
+ else
+ pDecision[i] = 0;
+ }
+ else
+ pDecision[i] = 0;
+
+ // add other non-trivial not-taken components whose support is contained in the current large component support
+ if ( fOneNonTriv )
+ for ( i = 0; i < nSize; i++ )
+ if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 )
+ {
+ pDecision[i] = 1;
+ nComps++;
+ }
+
+ return nComps;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTreeMulti_rec( Lpk_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pPrio )
+{
+ Kit_DsdObj_t * pObj;
+ If_Obj_t * pObjsNew[4][8], * pResPrev;
+ int piLitsNew[8], pDecision[8];
+ int i, k, nComps, nSize;
+
+ // find which of the variables is highest in the order
+ nSize = (1 << nCBars);
+ nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision );
+ if ( nComps == 0 )
+ return If_Not( If_ManConst1(p->pIfMan) );
+
+ // iterate over the nodes
+ if ( p->pPars->fVeryVerbose )
+ printf( "Decision: " );
+ for ( i = 0; i < nSize; i++ )
+ {
+ if ( pDecision[i] )
+ {
+ if ( p->pPars->fVeryVerbose )
+ printf( "%d ", i );
+ assert( piLits[i] >= 0 );
+ pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) );
+ if ( pObj == NULL )
+ piLitsNew[i] = -2;
+ else if ( pObj->Type == KIT_DSD_PRIME )
+ piLitsNew[i] = pObj->pFans[0];
+ else
+ piLitsNew[i] = pObj->pFans[1];
+ }
+ else
+ piLitsNew[i] = piLits[i];
+ }
+ if ( p->pPars->fVeryVerbose )
+ printf( "\n" );
+
+ // call again
+ pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio );
+
+ // create new set of nodes
+ for ( i = 0; i < nSize; i++ )
+ {
+ if ( pDecision[i] )
+ pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev );
+ else if ( piLits[i] == -1 )
+ pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan);
+ else if ( piLits[i] == -2 )
+ pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) );
+ else
+ pObjsNew[nCBars][i] = pResPrev;
+ }
+
+ // create MUX using these outputs
+ for ( k = nCBars; k > 0; k-- )
+ {
+ nSize /= 2;
+ for ( i = 0; i < nSize; i++ )
+ pObjsNew[k-1][i] = If_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] );
+ }
+ assert( nSize == 1 );
+ return pObjsNew[0][0];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
+{
+ static Counter = 0;
+ If_Obj_t * pResult;
+ Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp;
+ Kit_DsdObj_t * pRoot;
+ int piCofVar[4], pPrios[16], pFreqs[16] = {0}, piLits[16];
+ int i, k, nCBars, nSize, nMemSize;
+ unsigned * ppCofs[4][8], uSupport;
+ char pTable[16][16] = {0};
+ int fVerbose = p->pPars->fVeryVerbose;
+
+ Counter++;
+// printf( "Run %d.\n", Counter );
+
+ // allocate storage for cofactors
+ nMemSize = Kit_TruthWordNum(nVars);
+ ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize );
+ nSize = 0;
+ for ( i = 0; i < 4; i++ )
+ for ( k = 0; k < 8; k++ )
+ ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++;
+ assert( nSize == 32 );
+
+ // find the best cofactoring variables
+ nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 );
+// nCBars = 2;
+// piCofVar[0] = 0;
+// piCofVar[1] = 1;
+
+
+ // copy the function
+ Kit_TruthCopy( ppCofs[0][0], pTruth, nVars );
+
+ // decompose w.r.t. these variables
+ for ( k = 0; k < nCBars; k++ )
+ {
+ nSize = (1 << k);
+ for ( i = 0; i < nSize; i++ )
+ {
+ Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] );
+ Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] );
+ }
+ }
+ nSize = (1 << nCBars);
+ // compute DSD networks
+ for ( i = 0; i < nSize; i++ )
+ {
+ ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars );
+ ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] );
+ Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
+ {
+ printf( "Cof%d%d: ", nCBars, i );
+ Kit_DsdPrint( stdout, ppNtks[i] );
+ }
+ }
+
+ // compute variable frequences
+ for ( i = 0; i < nSize; i++ )
+ {
+ uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars );
+ for ( k = 0; k < nVars; k++ )
+ if ( uSupport & (1<<k) )
+ pFreqs[k]++;
+ }
+
+ // find common variable order
+ for ( i = 0; i < nSize; i++ )
+ {
+ Kit_DsdGetSupports( ppNtks[i] );
+ Lpk_CreateVarOrder( ppNtks[i], pTable );
+ }
+ Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose );
+ // update priorities with frequences
+ for ( i = 0; i < nVars; i++ )
+ pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i;
+
+ if ( fVerbose )
+ printf( "After restructuring with priority:\n" );
+
+ if ( Counter == 1 )
+ {
+ int x = 0;
+ }
+ // transform all networks according to the variable order
+ for ( i = 0; i < nSize; i++ )
+ {
+ ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios );
+ Kit_DsdNtkFree( pTemp );
+ Kit_DsdGetSupports( ppNtks[i] );
+ assert( ppNtks[i]->pSupps[0] <= 0xFFFF );
+ // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible
+ Kit_DsdRotate( ppNtks[i], pFreqs );
+ // print the resulting networks
+ if ( fVerbose )
+ {
+ printf( "Cof%d%d: ", nCBars, i );
+ Kit_DsdPrint( stdout, ppNtks[i] );
+ }
+ }
+
+ for ( i = 0; i < nSize; i++ )
+ {
+ // collect the roots
+ pRoot = Kit_DsdNtkRoot(ppNtks[i]);
+ if ( pRoot->Type == KIT_DSD_CONST1 )
+ piLits[i] = Kit_DsdLitIsCompl(ppNtks[i]->Root)? -2: -1;
+ else if ( pRoot->Type == KIT_DSD_VAR )
+ piLits[i] = Kit_DsdLitNotCond( pRoot->pFans[0], Kit_DsdLitIsCompl(ppNtks[i]->Root) );
+ else
+ piLits[i] = ppNtks[i]->Root;
+ }
+
+
+ // recursively construct AIG for mapping
+ p->fCofactoring = 1;
+ pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios );
+ p->fCofactoring = 0;
+
+ if ( fVerbose )
+ printf( "\n" );
+
+ // verify the transformations
+ nSize = (1 << nCBars);
+ for ( i = 0; i < nSize; i++ )
+ Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] );
+ // mux the truth tables
+ for ( k = nCBars-1; k >= 0; k-- )
+ {
+ nSize = (1 << k);
+ for ( i = 0; i < nSize; i++ )
+ Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] );
+ }
+ if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) )
+ printf( "Verification failed.\n" );
+
+
+ // free the networks
+ for ( i = 0; i < 8; i++ )
+ if ( ppNtks[i] )
+ Kit_DsdNtkFree( ppNtks[i] );
+ free( ppCofs[0][0] );
+
+ return pResult;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 10:14:50 +0000