summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/kit/kit.h22
-rw-r--r--src/opt/kit/kitDsd.c222
-rw-r--r--src/opt/kit/kitGraph.c3
-rw-r--r--src/opt/kit/kitTruth.c67
-rw-r--r--src/opt/lpk/lpk.h1
-rw-r--r--src/opt/lpk/lpkCore.c258
-rw-r--r--src/opt/lpk/lpkCut.c14
-rw-r--r--src/opt/lpk/lpkInt.h6
-rw-r--r--src/opt/lpk/lpkMan.c2
-rw-r--r--src/opt/lpk/lpkMap.c194
-rw-r--r--src/opt/lpk/lpkMux.c163
-rw-r--r--src/opt/lpk/lpkSets.c55
-rw-r--r--src/opt/res/module.make1
-rw-r--r--src/opt/res/resCore.c52
-rw-r--r--src/opt/res/resUpdate.c123
-rw-r--r--src/opt/rwr/rwrEva.c2
16 files changed, 684 insertions, 501 deletions
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index 229b0bce..e9a389e0 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -121,7 +121,7 @@ struct Kit_DsdNtk_t_
unsigned char Root; // the root of the tree
unsigned * pMem; // memory for the truth tables (memory manager?)
unsigned * pSupps; // supports of the nodes
- Kit_DsdObj_t * pNodes[0]; // the nodes
+ Kit_DsdObj_t** pNodes; // the nodes
};
// DSD manager
@@ -260,7 +260,15 @@ static inline int Kit_TruthFindFirstBit( unsigned * pIn, int nVars )
int w;
for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
if ( pIn[w] )
- return Kit_WordFindFirstBit(pIn[w]);
+ return 32*w + Kit_WordFindFirstBit(pIn[w]);
+ return -1;
+}
+static inline int Kit_TruthFindFirstZero( unsigned * pIn, int nVars )
+{
+ int w;
+ for ( w = 0; w < Kit_TruthWordNum(nVars); w++ )
+ if ( ~pIn[w] )
+ return 32*w + Kit_WordFindFirstBit(~pIn[w]);
return -1;
}
static inline int Kit_TruthIsEqual( unsigned * pIn0, unsigned * pIn1, int nVars )
@@ -444,12 +452,18 @@ extern DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars
extern DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
/*=== kitDsd.c ==========================================================*/
+extern Kit_DsdMan_t * Kit_DsdManAlloc( int nVars );
+extern void Kit_DsdManFree( Kit_DsdMan_t * p );
extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
-extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
+extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp );
extern void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes );
+extern void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp );
extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk );
+extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
+extern Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux );
+extern void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
extern void Kit_DsdGetSupports( Kit_DsdNtk_t * p );
@@ -510,10 +524,12 @@ extern void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, i
extern void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
+extern int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 );
extern void Kit_TruthCountOnesInCofs( unsigned * pTruth, int nVars, short * pStore );
extern void Kit_TruthCountOnesInCofsSlow( unsigned * pTruth, int nVars, short * pStore, unsigned * pAux );
extern unsigned Kit_TruthHash( unsigned * pIn, int nWords );
extern unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars, char * pCanonPerm, short * pStore );
+extern char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile );
#ifdef __cplusplus
}
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index 8b6b6979..06377cba 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -91,6 +91,11 @@ Kit_DsdObj_t * Kit_DsdObjAlloc( Kit_DsdNtk_t * pNtk, Kit_Dsd_t Type, int nFans )
pObj->nFans = nFans;
pObj->Offset = Kit_DsdObjOffset( nFans );
// add the object
+ if ( pNtk->nNodes == pNtk->nNodesAlloc )
+ {
+ pNtk->nNodesAlloc *= 2;
+ pNtk->pNodes = REALLOC( Kit_DsdObj_t *, pNtk->pNodes, pNtk->nNodesAlloc );
+ }
assert( pNtk->nNodes < pNtk->nNodesAlloc );
pNtk->pNodes[pNtk->nNodes++] = pObj;
return pObj;
@@ -126,10 +131,9 @@ void Kit_DsdObjFree( Kit_DsdNtk_t * p, Kit_DsdObj_t * pObj )
Kit_DsdNtk_t * Kit_DsdNtkAlloc( int nVars )
{
Kit_DsdNtk_t * pNtk;
- int nSize = sizeof(Kit_DsdNtk_t) + sizeof(void *) * nVars;
- // allocate the network
- pNtk = (Kit_DsdNtk_t *)ALLOC( char, nSize );
- memset( pNtk, 0, nSize );
+ pNtk = ALLOC( Kit_DsdNtk_t, 1 );
+ memset( pNtk, 0, sizeof(Kit_DsdNtk_t) );
+ pNtk->pNodes = ALLOC( Kit_DsdObj_t *, nVars );
pNtk->nVars = nVars;
pNtk->nNodesAlloc = nVars;
pNtk->pMem = ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) );
@@ -154,6 +158,7 @@ void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk )
Kit_DsdNtkForEachObj( pNtk, pObj, i )
free( pObj );
FREE( pNtk->pSupps );
+ free( pNtk->pNodes );
free( pNtk->pMem );
free( pNtk );
}
@@ -275,7 +280,27 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
{
Kit_DsdNtk_t * pTemp;
pTemp = Kit_DsdExpand( pNtk );
- Kit_DsdPrint( stdout, pNtk );
+ Kit_DsdPrint( stdout, pTemp );
+ Kit_DsdNtkFree( pTemp );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Print the DSD formula.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
+{
+ Kit_DsdNtk_t * pTemp;
+ pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
+ Kit_DsdVerify( pTemp, pTruth, nVars );
+ Kit_DsdPrintExpanded( pTemp );
Kit_DsdNtkFree( pTemp );
}
@@ -290,11 +315,11 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
SeeAlso []
***********************************************************************/
-unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id )
+unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp )
{
Kit_DsdObj_t * pObj;
unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
- unsigned i, m, iLit, nMints, fCompl;
+ unsigned i, m, iLit, nMints, fCompl, fPartial = 0;
// get the node with this ID
pObj = Kit_DsdNtkObj( pNtk, Id );
@@ -304,6 +329,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
if ( pObj == NULL )
{
assert( Id < pNtk->nVars );
+ assert( !uSupp || uSupp != (uSupp & ~(1<<Id)) );
return pTruthRes;
}
@@ -320,7 +346,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
{
assert( pObj->nFans == 1 );
iLit = pObj->pFans[0];
- pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+ assert( Kit_DsdLitIsLeaf( pNtk, iLit ) );
+ pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
if ( Kit_DsdLitIsCompl(iLit) )
Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars );
else
@@ -329,8 +356,22 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
}
// collect the truth tables of the fanins
- Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
- pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) );
+ if ( uSupp )
+ {
+ Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+ if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) )
+ pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+ else
+ {
+ pTruthFans[i] = NULL;
+ fPartial = 1;
+ }
+ }
+ else
+ {
+ Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+ pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp );
+ }
// create the truth table
// simple gates
@@ -338,7 +379,8 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
{
Kit_TruthFill( pTruthRes, pNtk->nVars );
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
- Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
+ if ( pTruthFans[i] )
+ Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) );
return pTruthRes;
}
if ( pObj->Type == KIT_DSD_XOR )
@@ -347,8 +389,11 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
fCompl = 0;
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
{
- Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
- fCompl ^= Kit_DsdLitIsCompl(iLit);
+ if ( pTruthFans[i] )
+ {
+ Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
+ fCompl ^= Kit_DsdLitIsCompl(iLit);
+ }
}
if ( fCompl )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
@@ -356,6 +401,16 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
}
assert( pObj->Type == KIT_DSD_PRIME );
+ if ( uSupp && fPartial )
+ {
+ // find the only non-empty component
+ Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+ if ( pTruthFans[i] )
+ break;
+ assert( i < pObj->nFans );
+ return pTruthFans[i];
+ }
+
// get the truth table of the prime node
pTruthPrime = Kit_DsdObjTruth( pObj );
// get storage for the temporary minterm
@@ -387,16 +442,19 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i
SeeAlso []
***********************************************************************/
-unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk )
+unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp )
{
unsigned * pTruthRes;
int i;
- // assign elementary truth ables
+ // if support is specified, request that supports are available
+ if ( uSupp )
+ Kit_DsdGetSupports( pNtk );
+ // assign elementary truth tables
assert( pNtk->nVars <= p->nVars );
for ( i = 0; i < (int)pNtk->nVars; i++ )
Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars );
// compute truth table for each node
- pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) );
+ pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp );
// complement the truth table if needed
if ( Kit_DsdLitIsCompl(pNtk->Root) )
Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
@@ -419,13 +477,30 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes )
Kit_DsdMan_t * p;
unsigned * pTruth;
p = Kit_DsdManAlloc( pNtk->nVars );
- pTruth = Kit_DsdTruthCompute( p, pNtk );
+ pTruth = Kit_DsdTruthCompute( p, pNtk, 0 );
Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
Kit_DsdManFree( p );
}
/**Function*************************************************************
+ Synopsis [Derives the truth table of the DSD network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp )
+{
+ unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp );
+ Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars );
+}
+
+/**Function*************************************************************
+
Synopsis [Counts the number of blocks of the given number of inputs.]
Description []
@@ -1085,7 +1160,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
SeeAlso []
***********************************************************************/
-void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar )
+void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar, int nDecMux )
{
Kit_DsdObj_t * pRes, * pRes0, * pRes1;
int nWords = Kit_TruthWordNum(pObj->nFans);
@@ -1168,11 +1243,10 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
// call recursively
- Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0 );
- Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 );
+ Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
+ Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
return;
}
-//Extra_PrintBinary( stdout, pTruth, 1 << pObj->nFans ); printf( "\n" );
// create the new node
pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 );
@@ -1214,7 +1288,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
assert( 0 );
// decompose the remainder
assert( Kit_DsdObjTruth(pObj) == pTruth );
- Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1 );
+ Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1, nDecMux );
return;
}
pObj->fMark = 1;
@@ -1234,7 +1308,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
if ( uSupp0 == 0 || uSupp1 == 0 )
{
pObj->fMark = 0;
- Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
+ Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
return;
}
assert( uSupp0 && uSupp1 );
@@ -1275,7 +1349,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
if ( fEquals[1][0] && fEquals[1][1] )
pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]);
// decompose the remainder
- Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
+ Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
return;
}
}
@@ -1339,10 +1413,36 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
}
// decompose the remainder
- Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar );
+ Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux );
return;
}
}
+/*
+ // if all decomposition methods failed and we are still above the limit, perform MUX-decomposition
+ if ( nDecMux > 0 && (int)pObj->nFans > nDecMux )
+ {
+ int iBestVar = Kit_TruthBestCofVar( pTruth, pObj->nFans, pCofs2[0], pCofs2[1] );
+ uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans );
+ uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans );
+ // perform MUX decomposition
+ pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
+ pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans );
+ for ( k = 0; k < pObj->nFans; k++ )
+ pRes0->pFans[k] = pRes1->pFans[k] = pObj->pFans[k];
+ Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans );
+ Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans );
+ // update the current one
+ assert( pObj->Type == KIT_DSD_PRIME );
+ pTruth[0] = 0xCACACACA;
+ pObj->nFans = 3;
+ pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
+ pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
+ pObj->pFans[2] = pObj->pFans[iBestVar];
+ // call recursively
+ Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux );
+ Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux );
+ }
+*/
}
/**Function*************************************************************
@@ -1356,7 +1456,7 @@ void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uS
SeeAlso []
***********************************************************************/
-Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
+Kit_DsdNtk_t * Kit_DsdDecomposeInt( unsigned * pTruth, int nVars, int nDecMux )
{
Kit_DsdNtk_t * pNtk;
Kit_DsdObj_t * pObj;
@@ -1389,7 +1489,7 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
pObj->pFans[0] = Kit_DsdVar2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) );
return pNtk;
}
- Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root );
+ Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root, nDecMux );
return pNtk;
}
@@ -1404,6 +1504,38 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
SeeAlso []
***********************************************************************/
+Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
+{
+ return Kit_DsdDecomposeInt( pTruth, nVars, 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs decomposition of the truth table.]
+
+ Description [Uses MUXes to break-down large prime nodes.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nDecMux )
+{
+ return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs decomposition of the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
{
Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp;
@@ -1489,7 +1621,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
// recompute the truth table
p = Kit_DsdManAlloc( nVars );
- pTruthC = Kit_DsdTruthCompute( p, pNtk );
+ pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
@@ -1509,37 +1641,15 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
SeeAlso []
***********************************************************************/
-Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize )
+void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
{
-// Kit_DsdMan_t * p;
- Kit_DsdNtk_t * pNtk;//, * pTemp;
-// unsigned * pTruthC;
-// int Result;
-
- // decompose the function
- pNtk = Kit_DsdDecompose( pTruth, nVars );
-
-// pNtk = Kit_DsdExpand( pTemp = pNtk );
-// Kit_DsdNtkFree( pTemp );
-
-// Result = Kit_DsdCountLuts( pNtk, nLutSize );
-
-// printf( "\n" );
-// Kit_DsdPrint( stdout, pNtk );
-// printf( "Eval = %d.\n", Result );
-
-/*
- // recompute the truth table
+ Kit_DsdMan_t * p;
+ unsigned * pTruthC;
p = Kit_DsdManAlloc( nVars );
- pTruthC = Kit_DsdTruthCompute( p, pNtk );
+ pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
-*/
-
-// Kit_DsdNtkFree( pNtk );
-// return Result;
- return pNtk;
}
/**Function*************************************************************
@@ -1578,7 +1688,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
// recompute the truth table
p = Kit_DsdManAlloc( nVars );
- pTruthC = Kit_DsdTruthCompute( p, pNtk );
+ pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
// Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
// Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
@@ -1648,7 +1758,7 @@ void Kit_DsdPrecompute4Vars()
*/
p = Kit_DsdManAlloc( 4 );
- pTruthC = Kit_DsdTruthCompute( p, pNtk );
+ pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
diff --git a/src/opt/kit/kitGraph.c b/src/opt/kit/kitGraph.c
index 1123b90e..e2deb4ef 100644
--- a/src/opt/kit/kitGraph.c
+++ b/src/opt/kit/kitGraph.c
@@ -354,9 +354,10 @@ Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemor
Kit_Graph_t * pGraph;
int RetValue;
// derive SOP
- RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 ); // tried 1 and found not useful in "renode"
+ RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 1 ); // tried 1 and found not useful in "renode"
if ( RetValue == -1 )
return NULL;
+// printf( "Isop size = %d.\n", Vec_IntSize(vMemory) );
assert( RetValue == 0 || RetValue == 1 );
// derive factored form
pGraph = Kit_SopFactor( vMemory, RetValue, nVars, vMemory );
diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c
index dbf222c2..d41e5d4e 100644
--- a/src/opt/kit/kitTruth.c
+++ b/src/opt/kit/kitTruth.c
@@ -1061,6 +1061,48 @@ int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin )
/**Function*************************************************************
+ Synopsis [Find the best cofactoring variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthBestCofVar( unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
+{
+ int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
+ if ( Kit_TruthIsConst0(pTruth, nVars) || Kit_TruthIsConst1(pTruth, nVars) )
+ return -1;
+ // iterate through variables
+ iBestVar = -1;
+ nSuppSizeMin = KIT_INFINITY;
+ for ( i = 0; i < nVars; i++ )
+ {
+ // cofactor the functiona and get support sizes
+ Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
+ Kit_TruthCofactor1New( pCof1, pTruth, nVars, i );
+ nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
+ nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
+ nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
+ // compare this variable with other variables
+ if ( nSuppSizeMin > nSuppSizeCur )
+ {
+ nSuppSizeMin = nSuppSizeCur;
+ iBestVar = i;
+ }
+ }
+ assert( iBestVar != -1 );
+ // cofactor w.r.t. this variable
+ Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
+ Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+ return iBestVar;
+}
+
+
+/**Function*************************************************************
+
Synopsis [Counts the number of 1's in each cofactor.]
Description [The resulting numbers are stored in the array of shorts,
@@ -1566,6 +1608,31 @@ void Kit_TruthCountMintermsPrecomp()
}
}
+/**Function*************************************************************
+
+ Synopsis [Dumps truth table into a file.]
+
+ Description [Generates script file for reading into ABC.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
+{
+ static char pFileName[100];
+ FILE * pFile;
+ sprintf( pFileName, "s%03d", nFile );
+ pFile = fopen( pFileName, "w" );
+ fprintf( pFile, "rt " );
+ Extra_PrintHexadecimal( pFile, pTruth, nVars );
+ fprintf( pFile, "; bdd; sop; ps\n" );
+ fclose( pFile );
+ return pFileName;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
index 092b43e1..f1dcd528 100644
--- a/src/opt/lpk/lpk.h
+++ b/src/opt/lpk/lpk.h
@@ -47,6 +47,7 @@ struct Lpk_Par_t_
int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis
int fSatur; // iterate till saturation
int fZeroCost; // accept zero-cost replacements
+ int fFirst; // use root node and first cut only
int fVerbose; // the verbosiness flag
int fVeryVerbose; // additional verbose info printout
// internal parameters
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index cbd971e3..aa0368a9 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -17,7 +17,7 @@
Revision [$Id: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
***********************************************************************/
-
+
#include "lpkInt.h"
////////////////////////////////////////////////////////////////////////
@@ -30,6 +30,54 @@
/**Function*************************************************************
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_IfManStart( Lpk_Man_t * p )
+{
+ If_Par_t * pPars;
+ assert( p->pIfMan == NULL );
+ // set defaults
+ pPars = ALLOC( If_Par_t, 1 );
+ memset( pPars, 0, sizeof(If_Par_t) );
+ // user-controlable paramters
+ pPars->nLutSize = p->pPars->nLutSize;
+ pPars->nCutsMax = 16;
+ pPars->nFlowIters = 0; // 1
+ pPars->nAreaIters = 0; // 1
+ pPars->DelayTarget = -1;
+ pPars->fPreprocess = 0;
+ pPars->fArea = 1;
+ pPars->fFancy = 0;
+ pPars->fExpRed = 0; //
+ pPars->fLatchPaths = 0;
+ pPars->fSeqMap = 0;
+ pPars->fVerbose = 0;
+ // internal parameters
+ pPars->fTruth = 1;
+ pPars->fUsePerm = 0;
+ pPars->nLatches = 0;
+ pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
+ pPars->pTimesArr = NULL;
+ pPars->pTimesArr = NULL;
+ pPars->fUseBdds = 0;
+ pPars->fUseSops = 0;
+ pPars->fUseCnfs = 0;
+ pPars->fUseMv = 0;
+ // start the mapping manager and set its parameters
+ p->pIfMan = If_ManStart( pPars );
+ If_ManSetupSetAll( p->pIfMan, 1000 );
+ p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if at least one entry has changed.]
Description []
@@ -63,6 +111,112 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
/**Function*************************************************************
+ Synopsis [Prepares the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
+{
+ extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
+ Kit_DsdObj_t * pRoot;
+ If_Obj_t * pDriver, * ppLeaves[16];
+ Abc_Obj_t * pLeaf, * pObjNew;
+ int nGain, i, clk;
+// int nOldShared;
+
+ // check special cases
+ pRoot = Kit_DsdNtkRoot( pNtk );
+ if ( pRoot->Type == KIT_DSD_CONST1 )
+ {
+ if ( Kit_DsdLitIsCompl(pNtk->Root) )
+ pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
+ else
+ pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
+ Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+ p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+ return 1;
+ }
+ if ( pRoot->Type == KIT_DSD_VAR )
+ {
+ pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
+ if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
+ pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
+ Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+ p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
+ return 1;
+ }
+ assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
+
+ // start the mapping manager
+ if ( p->pIfMan == NULL )
+ Lpk_IfManStart( p );
+
+ // prepare the mapping manager
+ If_ManRestart( p->pIfMan );
+ // create the PI variables
+ for ( i = 0; i < p->pPars->nVarsMax; i++ )
+ ppLeaves[i] = If_ManCreateCi( p->pIfMan );
+ // set the arrival times
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+ p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
+ // prepare the PI cuts
+ If_ManSetupCiCutSets( p->pIfMan );
+ // create the internal nodes
+ p->fCalledOnce = 0;
+ p->nCalledSRed = 0;
+ pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
+ if ( pDriver == NULL )
+ return 0;
+ // create the PO node
+ If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
+
+ // perform mapping
+ p->pIfMan->pPars->fAreaOnly = 1;
+clk = clock();
+ If_ManPerformMappingComb( p->pIfMan );
+p->timeMap += clock() - clk;
+
+ // compute the gain in area
+ nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
+ if ( p->pPars->fVeryVerbose )
+ printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d. SReds = %d.\n",
+ pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level, p->nCalledSRed );
+
+ // quit if there is no gain
+ if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
+ return 0;
+
+ // quit if depth increases too much
+ if ( (int)p->pIfMan->RequiredGlo > Abc_ObjRequiredLevel(p->pObj) )
+ return 0;
+
+ // perform replacement
+ p->nGainTotal += nGain;
+ p->nChanges++;
+ if ( p->nCalledSRed )
+ p->nBenefited++;
+
+ // prepare the mapping manager
+ If_ManCleanNodeCopy( p->pIfMan );
+ If_ManCleanCutData( p->pIfMan );
+ // set the PIs of the cut
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
+ If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
+ // get the area of mapping
+ pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
+ pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
+ // perform replacement
+ Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Performs resynthesis for one node.]
Description []
@@ -74,13 +228,13 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
***********************************************************************/
int Lpk_ResynthesizeNode( Lpk_Man_t * p )
{
+ static int Count = 0;
+ char * pFileName;
Kit_DsdNtk_t * pDsdNtk;
Lpk_Cut_t * pCut;
unsigned * pTruth;
void * pDsd = NULL;
- int i, RetValue, clk;
-
- Lpk_Cut_t * pCutMax;
+ int i, nSuppSize, RetValue, clk;
// compute the cuts
clk = clock();
@@ -91,17 +245,6 @@ p->timeCuts += clock() - clk;
}
p->timeCuts += clock() - clk;
- // find the max volume cut
- pCutMax = NULL;
- for ( i = 0; i < p->nEvals; i++ )
- {
- pCut = p->pCuts + p->pEvals[i];
- if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes )
- pCutMax = pCut;
- }
- assert( pCutMax != NULL );
-
-
if ( p->pPars->fVeryVerbose )
printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
// try the good cuts
@@ -111,20 +254,34 @@ p->timeCuts += clock() - clk;
{
// get the cut
pCut = p->pCuts + p->pEvals[i];
+ if ( p->pPars->fFirst && i == 1 )
+ break;
- if ( pCut != pCutMax )
- continue;
+ if ( p->pObj->Id == 8835 )
+ {
+ int x = 0;
+ }
// compute the truth table
clk = clock();
pTruth = Lpk_CutTruth( p, pCut );
+ nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
p->timeTruth += clock() - clk;
-clk = clock();
- pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize );
-p->timeEval += clock() - clk;
+ pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves );
+// Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves );
+ // skip 16-input non-DSD because ISOP will not work
+ if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 )
+ {
+ Kit_DsdNtkFree( pDsdNtk );
+ continue;
+ }
- if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work
+ // if DSD has nodes that require splitting to fit them into LUTs
+ // we can skip those cuts that cannot lead to improvement
+ // (a full DSD network requires V = Nmin * (K-1) + 1 for improvement)
+ if ( Kit_DsdNonDsdSizeMax(pDsdNtk) > p->pPars->nLutSize &&
+ nSuppSize >= ((int)pCut->nNodes - (int)pCut->nNodesDup - 1) * (p->pPars->nLutSize - 1) + 1 )
{
Kit_DsdNtkFree( pDsdNtk );
continue;
@@ -133,15 +290,18 @@ p->timeEval += clock() - clk;
if ( p->pPars->fVeryVerbose )
{
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
- i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+ i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
Kit_DsdPrint( stdout, pDsdNtk );
+// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
+ pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
+ printf( "Saved truth table in file \"%s\".\n", pFileName );
}
// update the network
clk = clock();
- RetValue = Lpk_CutExplore( p, pCut, pDsdNtk );
+ RetValue = Lpk_ExploreCut( p, pCut, pDsdNtk );
+p->timeEval += clock() - clk;
Kit_DsdNtkFree( pDsdNtk );
-p->timeMap += clock() - clk;
if ( RetValue )
break;
}
@@ -187,16 +347,28 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax );
}
- // convert logic to AIGs
- Abc_NtkToAig( pNtk );
+
+ // convert into the AIG
+ if ( !Abc_NtkToAig(pNtk) )
+ {
+ fprintf( stdout, "Converting to BDD has failed.\n" );
+ return 0;
+ }
+ assert( Abc_NtkHasAig(pNtk) );
+
+ // set the number of levels
+ Abc_NtkLevel( pNtk );
+ Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// start the manager
p = Lpk_ManStart( pPars );
p->pNtk = pNtk;
p->nNodesTotal = Abc_NtkNodeNum(pNtk);
- p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes
+ p->vLevels = Vec_VecStart( pNtk->LevelMax );
if ( p->pPars->fSatur )
p->vVisited = Vec_VecStart( 0 );
+ if ( pPars->fVerbose )
+ p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
// iterate over the network
nNodesPrev = p->nNodesTotal;
@@ -213,8 +385,11 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
Abc_NtkForEachNode( pNtk, pObj, i )
{
// skip all except the final node
-// if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
-// continue;
+ if ( pPars->fFirst )
+ {
+ if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
+ continue;
+ }
if ( i >= nNodes )
break;
@@ -227,8 +402,8 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
p->pObj = pObj;
Lpk_ResynthesizeNode( p );
- if ( p->nChanges == 3 )
- break;
+// if ( p->nChanges == 3 )
+// break;
}
if ( !pPars->fVeryVerbose )
Extra_ProgressBarStop( pProgress );
@@ -241,19 +416,30 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
if ( !p->pPars->fSatur )
break;
- break;
+ if ( pPars->fFirst )
+ break;
}
+ Abc_NtkStopReverseLevels( pNtk );
if ( pPars->fVerbose )
{
- printf( "N = %5d (%3d) Cut = %5d (%4d) Change = %5d Gain = %5d (%5.2f %%) Iter = %2d\n",
- p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter );
- printf( "Non_DSD blocks: " );
+ p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
+ printf( "Reduction in nodes = %5d. (%.2f %%) ",
+ p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal );
+ printf( "Reduction in edges = %5d. (%.2f %%) ",
+ p->nTotalNets-p->nTotalNets2, 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
+ printf( "\n" );
+
+ printf( "Nodes = %5d (%3d) Cuts = %5d (%4d) Changes = %5d Iter = %2d Benefit = %d.\n",
+ p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, Iter, p->nBenefited );
+ printf( "Non-DSD:" );
for ( i = 3; i <= pPars->nVarsMax; i++ )
if ( p->nBlocks[i] )
- printf( "%d=%d ", i, p->nBlocks[i] );
+ printf( " %d=%d", i, p->nBlocks[i] );
printf( "\n" );
+
p->timeTotal = clock() - clk;
+ p->timeEval = p->timeEval - p->timeMap;
p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
PRTP( "Cuts ", p->timeCuts, p->timeTotal );
PRTP( "Truth ", p->timeTruth, p->timeTotal );
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index 251ec829..12dae15b 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -545,11 +545,11 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
pCut = p->pCuts + i;
if ( pCut->nLeaves < 2 )
continue;
- // compute the number of LUTs neede to implement this cut
+ // compute the minimum number of LUTs needed to implement this cut
// V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 );
pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
- if ( pCut->Weight <= 1.0 )
+ if ( pCut->Weight <= 1.001 )
continue;
pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
if ( pCut->fHasDsd )
@@ -566,7 +566,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
{
pCut = p->pCuts + p->pEvals[i];
pCut2 = p->pCuts + p->pEvals[i+1];
- if ( pCut->Weight >= pCut2->Weight )
+ if ( pCut->Weight >= pCut2->Weight - 0.001 )
continue;
Temp = p->pEvals[i];
p->pEvals[i] = p->pEvals[i+1];
@@ -574,6 +574,14 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
fChanges = 1;
}
} while ( fChanges );
+/*
+ for ( i = 0; i < p->nEvals; i++ )
+ {
+ pCut = p->pCuts + p->pEvals[i];
+ printf( "Cut %3d : W = %5.2f.\n", i, pCut->Weight );
+ }
+ printf( "\n" );
+*/
return 1;
}
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index fe442302..683e7b92 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -87,6 +87,7 @@ struct Lpk_Man_t_
// temporary variables
int fCofactoring; // working in the cofactoring mode
int fCalledOnce; // limits the depth of MUX cofactoring
+ int nCalledSRed; // the number of called to SRed
int pRefs[LPK_SIZE_MAX]; // fanin reference counters
int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves
// truth table representation
@@ -94,6 +95,7 @@ struct Lpk_Man_t_
Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes
// variable sets
Vec_Int_t * vSets[8];
+ Kit_DsdMan_t * pDsdMan;
// statistics
int nNodesTotal; // total number of nodes
int nNodesOver; // nodes with cuts over the limit
@@ -101,6 +103,9 @@ struct Lpk_Man_t_
int nCutsUseful; // useful cuts
int nGainTotal; // the gain in LUTs
int nChanges; // the number of changed nodes
+ int nBenefited; // the number of gainful that benefited from decomposition
+ int nTotalNets;
+ int nTotalNets2;
// counter of non-DSD blocks
int nBlocks[17];
// rutime
@@ -138,7 +143,6 @@ extern int Lpk_NodeCuts( Lpk_Man_t * p );
extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars );
extern void Lpk_ManStop( Lpk_Man_t * p );
/*=== lpkMap.c =========================================================*/
-extern int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk );
extern If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves );
extern If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult );
/*=== lpkMulti.c =======================================================*/
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index da8b0e3a..5dd54450 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -54,6 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
p->vCover = Vec_IntAlloc( 1 << 12 );
for ( i = 0; i < 8; i++ )
p->vSets[i] = Vec_IntAlloc(100);
+ p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax );
return p;
}
@@ -71,6 +72,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
void Lpk_ManStop( Lpk_Man_t * p )
{
int i;
+ Kit_DsdManFree( p->pDsdMan );
for ( i = 0; i < 8; i++ )
Vec_IntFree(p->vSets[i]);
if ( p->pIfMan )
diff --git a/src/opt/lpk/lpkMap.c b/src/opt/lpk/lpkMap.c
index c647fdf7..698aeea1 100644
--- a/src/opt/lpk/lpkMap.c
+++ b/src/opt/lpk/lpkMap.c
@@ -24,62 +24,12 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels );
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis [Prepares the mapping manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Lpk_IfManStart( Lpk_Man_t * p )
-{
- If_Par_t * pPars;
- assert( p->pIfMan == NULL );
- // set defaults
- pPars = ALLOC( If_Par_t, 1 );
- memset( pPars, 0, sizeof(If_Par_t) );
- // user-controlable paramters
- pPars->nLutSize = p->pPars->nLutSize;
- pPars->nCutsMax = 16;
- pPars->nFlowIters = 0; // 1
- pPars->nAreaIters = 0; // 1
- pPars->DelayTarget = -1;
- pPars->fPreprocess = 0;
- pPars->fArea = 1;
- pPars->fFancy = 0;
- pPars->fExpRed = 0; //
- pPars->fLatchPaths = 0;
- pPars->fSeqMap = 0;
- pPars->fVerbose = 0;
- // internal parameters
- pPars->fTruth = 0;
- pPars->fUsePerm = 0;
- pPars->nLatches = 0;
- pPars->pLutLib = NULL; // Abc_FrameReadLibLut();
- pPars->pTimesArr = NULL;
- pPars->pTimesArr = NULL;
- pPars->fUseBdds = 0;
- pPars->fUseSops = 0;
- pPars->fUseCnfs = 0;
- pPars->fUseMv = 0;
- // start the mapping manager and set its parameters
- p->pIfMan = If_ManStart( pPars );
- If_ManSetupSetAll( p->pIfMan, 1000 );
- p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 );
-}
-
-/**Function*************************************************************
-
Synopsis [Transforms the decomposition graph into the AIG.]
Description []
@@ -154,122 +104,10 @@ If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t *
SeeAlso []
***********************************************************************/
-int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
-{
- extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
- Kit_DsdObj_t * pRoot;
- If_Obj_t * pDriver, * ppLeaves[16];
- Abc_Obj_t * pLeaf, * pObjNew;
- int nGain, i;
-// int nOldShared;
-
- // check special cases
- pRoot = Kit_DsdNtkRoot( pNtk );
- if ( pRoot->Type == KIT_DSD_CONST1 )
- {
- if ( Kit_DsdLitIsCompl(pNtk->Root) )
- pObjNew = Abc_NtkCreateNodeConst0( p->pNtk );
- else
- pObjNew = Abc_NtkCreateNodeConst1( p->pNtk );
-
- // perform replacement
- pObjNew->Level = p->pObj->Level;
- Abc_ObjReplace( p->pObj, pObjNew );
- Res_UpdateNetworkLevel( pObjNew, p->vLevels );
- p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
- return 1;
- }
- if ( pRoot->Type == KIT_DSD_VAR )
- {
- pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] );
- if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) )
- pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew );
-
- // perform replacement
- pObjNew->Level = p->pObj->Level;
- Abc_ObjReplace( p->pObj, pObjNew );
- Res_UpdateNetworkLevel( pObjNew, p->vLevels );
- p->nGainTotal += pCut->nNodes - pCut->nNodesDup;
- return 1;
- }
- assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME );
-
- // start the mapping manager
- if ( p->pIfMan == NULL )
- Lpk_IfManStart( p );
-
- // prepare the mapping manager
- If_ManRestart( p->pIfMan );
- // create the PI variables
- for ( i = 0; i < p->pPars->nVarsMax; i++ )
- ppLeaves[i] = If_ManCreateCi( p->pIfMan );
- // set the arrival times
- Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
- p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level;
- // prepare the PI cuts
- If_ManSetupCiCutSets( p->pIfMan );
- // create the internal nodes
- p->fCalledOnce = 0;
- pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL );
- if ( pDriver == NULL )
- return 0;
- // create the PO node
- If_ManCreateCo( p->pIfMan, If_Regular(pDriver) );
-
- // perform mapping
- p->pIfMan->pPars->fAreaOnly = 1;
- If_ManPerformMappingComb( p->pIfMan );
-
- // compute the gain in area
- nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo;
- if ( p->pPars->fVeryVerbose )
- printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n",
- pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level );
-
- // quit if there is no gain
- if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) )
- return 0;
-
- // quit if depth increases too much
- if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel )
- return 0;
-
- // perform replacement
- p->nGainTotal += nGain;
- p->nChanges++;
-
- // prepare the mapping manager
- If_ManCleanNodeCopy( p->pIfMan );
- If_ManCleanCutData( p->pIfMan );
- // set the PIs of the cut
- Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i )
- If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf );
- // get the area of mapping
- pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover );
- pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
-
- // perform replacement
- pObjNew->Level = p->pObj->Level;
- Abc_ObjReplace( p->pObj, pObjNew );
- Res_UpdateNetworkLevel( pObjNew, p->vLevels );
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Prepares the mapping manager.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult )
{
Kit_DsdObj_t * pObj;
- If_Obj_t * pObjNew, * pFansNew[16];
+ If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
unsigned i, iLitFanin;
assert( iLit >= 0 );
@@ -325,20 +163,38 @@ If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLe
if ( pFansNew[i] == NULL )
return NULL;
}
-/*
+/*
if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
{
pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}
*/
+/*
+ if ( (int)pObj->nFans > p->pPars->nLutSize )
+ {
+ pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+// if ( pObjNew2 )
+// return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
+ }
+*/
// find best cofactoring variable
- if ( pObj->nFans > 3 && !p->fCalledOnce )
-// pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
- pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
- else
- pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+ if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
+ {
+ pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+ if ( pObjNew2 )
+ return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
+ }
+
+ pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
+
+ // add choice
+ if ( pObjNew && pObjNew2 )
+ {
+ If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
+ If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
+ }
return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}
diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c
index d9e013f0..7928f77e 100644
--- a/src/opt/lpk/lpkMux.c
+++ b/src/opt/lpk/lpkMux.c
@@ -39,18 +39,12 @@
SeeAlso []
***********************************************************************/
-int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
+int Lpk_MapTreeBestCofVar( Lpk_Man_t * p, unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 )
{
-// Kit_DsdNtk_t * ppNtks[2], * pTemp;
- unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
- unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin;
-// int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin;
-
// iterate through variables
iBestVar = -1;
- nSuppSizeMin = ABC_INFINITY;
-// nPrimeSizeMin = ABC_INFINITY;
+ nSuppSizeMin = KIT_INFINITY;
for ( i = 0; i < nVars; i++ )
{
// cofactor the functiona and get support sizes
@@ -59,44 +53,22 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars );
nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars );
nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1;
-/*
- // check the size of the largest prime components
- ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
- ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
- // compute the largest non-decomp block
- nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]);
- nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]);
- nPrimeSizeCur = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 );
-
- printf( "Evaluating variable %c:\n", 'a'+i );
-// Kit_DsdPrintExpanded( ppNtks[0] );
-// Kit_DsdPrintExpanded( ppNtks[1] );
-
- ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
- Kit_DsdNtkFree( pTemp );
-
- ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );
- Kit_DsdNtkFree( pTemp );
-
- Kit_DsdPrint( stdout, ppNtks[0] );
- Kit_DsdPrint( stdout, ppNtks[1] );
-
-// Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] );
-
- // free the networks
- Kit_DsdNtkFree( ppNtks[0] );
- Kit_DsdNtkFree( ppNtks[1] );
-*/
+ // skip cofactoring that goes above the limit
+ if ( nSuppSizeCur0 > p->pPars->nLutSize || nSuppSizeCur1 > p->pPars->nLutSize )
+ continue;
// compare this variable with other variables
- if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) )
+ if ( nSuppSizeMin > nSuppSizeCur )
{
nSuppSizeMin = nSuppSizeCur;
-// nPrimeSizeMin = nPrimeSizeCur;
iBestVar = i;
}
}
- printf( "\n" );
- assert( iBestVar != -1 );
+ // cofactor w.r.t. this variable
+ if ( iBestVar != -1 )
+ {
+ Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
+ Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+ }
return iBestVar;
}
@@ -113,18 +85,17 @@ int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars )
***********************************************************************/
If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
- If_Obj_t * pObj0, * pObj1;
- Kit_DsdNtk_t * ppNtks[2];
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
+ If_Obj_t * pObj0, * pObj1;
+ Kit_DsdNtk_t * ppNtks[2];
int iBestVar;
assert( nVars > 3 );
p->fCalledOnce = 1;
-
// cofactor w.r.t. the best variable
- iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars );
- Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar );
- Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar );
+ iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 );
+ if ( iBestVar == -1 )
+ return NULL;
// decompose the functions
ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
@@ -158,7 +129,7 @@ If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_O
***********************************************************************/
If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves )
{
- Kit_DsdNtk_t * pNtkDec, * pNtkComp;
+ Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp;
If_Obj_t * pObjNew;
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
@@ -172,80 +143,96 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I
unsigned * pCo0 = Vec_PtrEntry( p->vTtNodes, 9 );
unsigned * pCo1 = Vec_PtrEntry( p->vTtNodes, 10 );
unsigned * pCo = Vec_PtrEntry( p->vTtNodes, 11 );
- int TrueMint0, TrueMint1;
+ int TrueMint0, TrueMint1, FalseMint0, FalseMint1;
int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;
// determine if supp-red decomposition exists
uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
if ( uSubsets == 0 )
return NULL;
+ p->nCalledSRed++;
- // get the bound sets
- uSubset0 = uSubsets & 0xFFFF;
- uSubset1 = uSubsets >> 16;
// get the cofactors
Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );
- // find any true assignments of the cofactors
- TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars );
- TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars );
+
+ // get the bound sets
+ uSubset0 = uSubsets & 0xFFFF;
+ uSubset1 = uSubsets >> 16;
+
+ // compute the decomposed functions
+ ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
+ ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
+ ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
+ ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
+ Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
+ Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
+ Kit_DsdNtkFree( ppNtks[0] );
+ Kit_DsdNtkFree( ppNtks[1] );
+//Kit_DsdPrintFromTruth( pDec0, nVars );
+//Kit_DsdPrintFromTruth( pDec1, nVars );
+ // get the decomposed function
+ Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
+
+ // find any true assignments of the decomposed functions
+ TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars );
+ TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars );
assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
+ // find any false assignments of the decomposed functions
+ FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars );
+ FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars );
+ assert( FalseMint0 >= 0 && FalseMint1 >= 0 );
+
// cofactor the cofactors according to these minterms
- Kit_TruthCopy( pDec0, pCof0, nVars );
- Kit_TruthCopy( pDec1, pCof1, nVars );
+ Kit_TruthCopy( pCo00, pCof0, nVars );
+ Kit_TruthCopy( pCo01, pCof0, nVars );
for ( i = 0; i < nVars; i++ )
- if ( !(uSubset0 & (1 << i)) )
+ if ( uSubset0 & (1 << i) )
{
+ if ( FalseMint0 & (1 << i) )
+ Kit_TruthCofactor1( pCo00, nVars, i );
+ else
+ Kit_TruthCofactor0( pCo00, nVars, i );
if ( TrueMint0 & (1 << i) )
- Kit_TruthCofactor1( pDec0, nVars, i );
+ Kit_TruthCofactor1( pCo01, nVars, i );
else
- Kit_TruthCofactor0( pDec0, nVars, i );
+ Kit_TruthCofactor0( pCo01, nVars, i );
}
+ Kit_TruthCopy( pCo10, pCof1, nVars );
+ Kit_TruthCopy( pCo11, pCof1, nVars );
for ( i = 0; i < nVars; i++ )
- if ( !(uSubset1 & (1 << i)) )
+ if ( uSubset1 & (1 << i) )
{
+ if ( FalseMint1 & (1 << i) )
+ Kit_TruthCofactor1( pCo10, nVars, i );
+ else
+ Kit_TruthCofactor0( pCo10, nVars, i );
if ( TrueMint1 & (1 << i) )
- Kit_TruthCofactor1( pDec1, nVars, i );
+ Kit_TruthCofactor1( pCo11, nVars, i );
else
- Kit_TruthCofactor0( pDec1, nVars, i );
+ Kit_TruthCofactor0( pCo11, nVars, i );
}
- // get the decomposed function
- Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );
- // derive the remainders
- Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 );
- Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 );
- Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 );
- Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 );
- // quantify bound set variables
- for ( i = 0; i < nVars; i++ )
- if ( uSubset0 & (1 << i) )
- {
- Kit_TruthExist( pCo00, nVars, i );
- Kit_TruthExist( pCo01, nVars, i );
- }
- for ( i = 0; i < nVars; i++ )
- if ( uSubset1 & (1 << i) )
- {
- Kit_TruthExist( pCo10, nVars, i );
- Kit_TruthExist( pCo11, nVars, i );
- }
// derive the functions by composing them with the new variable (iVarReused)
Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
+//Kit_DsdPrintFromTruth( pCo0, nVars );
+//Kit_DsdPrintFromTruth( pCo1, nVars );
// derive the composition function
Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );
// process the decomposed function
pNtkDec = Kit_DsdDecompose( pDec, nVars );
- Kit_DsdPrint( stdout, pNtkDec );
- ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
- Kit_DsdNtkFree( pNtkDec );
-
- // process the composition function
pNtkComp = Kit_DsdDecompose( pCo, nVars );
- Kit_DsdPrint( stdout, pNtkComp );
+//Kit_DsdPrint( stdout, pNtkDec );
+//Kit_DsdPrint( stdout, pNtkComp );
+//printf( "cofactored variable %c\n", 'a' + iVar );
+//printf( "reused variable %c\n", 'a' + iVarReused );
+
+ ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );
+
+ Kit_DsdNtkFree( pNtkDec );
Kit_DsdNtkFree( pNtkComp );
return pObjNew;
}
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
index 721705cb..d0d56a86 100644
--- a/src/opt/lpk/lpkSets.c
+++ b/src/opt/lpk/lpkSets.c
@@ -104,7 +104,8 @@ unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets )
***********************************************************************/
unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
{
- unsigned uSupport, Entry, i;
+ unsigned uSupport, Entry;
+ int Number, i;
assert( p->nVars <= 16 );
Vec_IntClear( vSets );
Vec_IntPush( vSets, 0 );
@@ -120,8 +121,11 @@ unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
assert( (uSupport & 0xFFFF0000) == 0 );
Vec_IntPush( vSets, uSupport );
// set the remaining variables
- Vec_IntForEachEntry( vSets, Entry, i )
+ Vec_IntForEachEntry( vSets, Number, i )
+ {
+ Entry = Number;
Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) );
+ }
return uSupport;
}
@@ -157,10 +161,14 @@ void Lpk_PrintSetOne( int uSupport )
***********************************************************************/
void Lpk_PrintSets( Vec_Int_t * vSets )
{
- unsigned uSupport, i;
+ unsigned uSupport;
+ int Number, i;
printf( "Subsets(%d): ", Vec_IntSize(vSets) );
- Vec_IntForEachEntry( vSets, uSupport, i )
+ Vec_IntForEachEntry( vSets, Number, i )
+ {
+ uSupport = Number;
Lpk_PrintSetOne( uSupport );
+ }
printf( "\n" );
}
@@ -237,7 +245,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo
}
}
- // check if there are non-overlapping
+ // find the minimum overlap
nMinOver = 1000;
for ( s = 0; s < nUsed; s++ )
if ( nMinOver > Over[Used[s]] )
@@ -267,7 +275,7 @@ void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCo
// get the number of overlapping vars
pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) );
// get the support reduction
- pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
+ pEntry->SRed = pEntry->Size - 1 - pEntry->Over;
assert( pEntry->SRed > 0 );
}
}
@@ -318,13 +326,21 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
Vec_Int_t * vSets1 = p->vSets[1];
unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 );
unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 );
- int nSets, i, SizeMax;
+ int nSets, i, SizeMax;//, SRedMax;
unsigned Entry;
+ int fVerbose = p->pPars->fVeryVerbose;
+// int fVerbose = 0;
// collect decomposable subsets for each pair of cofactors
+ if ( fVerbose )
+ {
+ printf( "\nExploring support-reducing bound-sets of function:\n" );
+ Kit_DsdPrintFromTruth( pTruth, nVars );
+ }
nSets = 0;
for ( i = 0; i < nVars; i++ )
{
+ if ( fVerbose )
printf( "Evaluating variable %c:\n", 'a'+i );
// evaluate the cofactor pair
Kit_TruthCofactor0New( pCof0, pTruth, nVars, i );
@@ -334,13 +350,17 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp );
ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp );
+ if ( fVerbose )
Kit_DsdPrint( stdout, ppNtks[0] );
+ if ( fVerbose )
Kit_DsdPrint( stdout, ppNtks[1] );
// compute subsets
Lpk_ComputeSets( ppNtks[0], vSets0 );
Lpk_ComputeSets( ppNtks[1], vSets1 );
// print subsets
+ if ( fVerbose )
Lpk_PrintSets( vSets0 );
+ if ( fVerbose )
Lpk_PrintSets( vSets1 );
// free the networks
Kit_DsdNtkFree( ppNtks[0] );
@@ -350,7 +370,9 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
}
// print the results
+ if ( fVerbose )
printf( "\n" );
+ if ( fVerbose )
for ( i = 0; i < nSets; i++ )
Lpk_MapSuppPrintSet( pStore + i, i );
@@ -368,14 +390,33 @@ unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, i
SizeMax = pSet->Size;
}
}
+/*
+ // if the best is not choosen, select the one with largest reduction
+ SRedMax = 0;
+ if ( pSetBest == NULL )
+ {
+ for ( i = 0; i < nSets; i++ )
+ {
+ pSet = pStore + i;
+ if ( SRedMax < pSet->SRed )
+ {
+ pSetBest = pSet;
+ SRedMax = pSet->SRed;
+ }
+ }
+ }
+*/
if ( pSetBest == NULL )
{
+ if ( fVerbose )
printf( "Could not select a subset.\n" );
return 0;
}
else
{
+ if ( fVerbose )
printf( "Selected the following subset:\n" );
+ if ( fVerbose )
Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore );
}
diff --git a/src/opt/res/module.make b/src/opt/res/module.make
index 85936f5b..52d8a315 100644
--- a/src/opt/res/module.make
+++ b/src/opt/res/module.make
@@ -4,5 +4,4 @@ SRC += src/opt/res/resCore.c \
src/opt/res/resSat.c \
src/opt/res/resSim.c \
src/opt/res/resStrash.c \
- src/opt/res/resUpdate.c \
src/opt/res/resWin.c
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 1d0711f6..27e9b3ea 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -102,9 +102,9 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
p->pSim = Res_SimAlloc( pPars->nSimWords );
p->pMan = Int_ManAlloc( 512 );
p->vMem = Vec_IntAlloc( 0 );
- p->vResubs = Vec_VecStart( pPars->nCands );
+ p->vResubs = Vec_VecStart( pPars->nCands );
p->vResubsW = Vec_VecStart( pPars->nCands );
- p->vLevels = Vec_VecStart( 32 );
+ p->vLevels = Vec_VecStart( 32 );
return p;
}
@@ -123,6 +123,14 @@ void Res_ManFree( Res_Man_t * p )
{
if ( p->pPars->fVerbose )
{
+ printf( "Reduction in nodes = %5d. (%.2f %%) ",
+ p->nTotalNodes-p->nTotalNodes2,
+ 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
+ printf( "Reduction in edges = %5d. (%.2f %%) ",
+ p->nTotalNets-p->nTotalNets2,
+ 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
+ printf( "\n" );
+
printf( "Winds = %d. ", p->nWins );
printf( "Nodes = %d. (Ave = %5.1f) ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
printf( "Divs = %d. (Ave = %5.1f) ", p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
@@ -134,13 +142,6 @@ void Res_ManFree( Res_Man_t * p )
printf( "Cands = %d. ", p->nCandSets );
printf( "Proved = %d.", p->nProvedSets );
printf( "\n" );
- printf( "Reduction in nodes = %d. (%.2f %%) ",
- p->nTotalNodes-p->nTotalNodes2,
- 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
- printf( "Reduction in nets = %d. (%.2f %%) ",
- p->nTotalNets-p->nTotalNets2,
- 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
- printf( "\n" );
PRTP( "Windowing ", p->timeWin, p->timeTotal );
PRTP( "Divisors ", p->timeDiv, p->timeTotal );
@@ -153,7 +154,7 @@ void Res_ManFree( Res_Man_t * p )
PRTP( " simul ", p->timeSatSim, p->timeTotal );
PRTP( "Interpol ", p->timeInt, p->timeTotal );
PRTP( "Undating ", p->timeUpd, p->timeTotal );
- PRT( "TOTAL ", p->timeTotal );
+ PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
}
Res_WinFree( p->pWin );
if ( p->pAig ) Abc_NtkDelete( p->pAig );
@@ -169,6 +170,31 @@ void Res_ManFree( Res_Man_t * p )
/**Function*************************************************************
+ Synopsis [Incrementally updates level of the nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
+{
+ Abc_Obj_t * pObjNew, * pFanin;
+ int k;
+ // create the new node
+ pObjNew = Abc_NtkCreateNode( pObj->pNtk );
+ pObjNew->pData = pFunc;
+ Vec_PtrForEachEntry( vFanins, pFanin, k )
+ Abc_ObjAddFanin( pObjNew, pFanin );
+ // replace the old node by the new node
+ // update the level of the node
+ Abc_NtkUpdate( pObj, pObjNew, vLevels );
+}
+
+/**Function*************************************************************
+
Synopsis [Entrace into the resynthesis package.]
Description []
@@ -210,6 +236,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
// set the number of levels
Abc_NtkLevel( pNtk );
+ Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// try resynthesizing nodes in the topological order
nNodesOld = Abc_NtkObjNumMax(pNtk);
@@ -239,10 +266,10 @@ p->timeWin += clock() - clk;
Vec_PtrSize(p->pWin->vNodes),
Vec_PtrSize(p->pWin->vRoots) );
}
-
+
// collect the divisors
clk = clock();
- Res_WinDivisors( p->pWin, pObj->Level + pPars->nGrowthLevel - 1 );
+ Res_WinDivisors( p->pWin, Abc_ObjRequiredLevel(pObj) - 1 );
p->timeDiv += clock() - clk;
p->nWins++;
@@ -359,6 +386,7 @@ p->timeUpd += clock() - clk;
// printf( "\n" );
}
Extra_ProgressBarStop( pProgress );
+ Abc_NtkStopReverseLevels( pNtk );
p->timeSatSim += p->pSim->timeSat;
p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
diff --git a/src/opt/res/resUpdate.c b/src/opt/res/resUpdate.c
deleted file mode 100644
index fb858658..00000000
--- a/src/opt/res/resUpdate.c
+++ /dev/null
@@ -1,123 +0,0 @@
-/**CFile****************************************************************
-
- FileName [resUpdate.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Resynthesis package.]
-
- Synopsis [Updates the network after changes.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - January 15, 2007.]
-
- Revision [$Id: resUpdate.c,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "resInt.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Computes the level of the node using its fanin levels.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj )
-{
- Abc_Obj_t * pFanin;
- int i, Level = 0;
- Abc_ObjForEachFanin( pObj, pFanin, i )
- Level = ABC_MAX( Level, (int)pFanin->Level );
- return Level + 1;
-}
-
-/**Function*************************************************************
-
- Synopsis [Incrementally updates level of the nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
-{
- Abc_Obj_t * pFanout, * pTemp;
- int Lev, k, m;
- // check if level has changed
- if ( (int)pObjNew->Level == Res_UpdateNetworkLevelNew(pObjNew) )
- return;
- // start the data structure for level update
- Vec_VecClear( vLevels );
- Vec_VecPush( vLevels, pObjNew->Level, pObjNew );
- pObjNew->fMarkA = 1;
- // recursively update level
- Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, pObjNew->Level )
- {
- pTemp->fMarkA = 0;
- pTemp->Level = Res_UpdateNetworkLevelNew( pTemp );
- // if the level did not change, to need to check the fanout levels
- if ( (int)pTemp->Level == Lev )
- continue;
- // schedule fanout for level update
- Abc_ObjForEachFanout( pTemp, pFanout, m )
- if ( !Abc_ObjIsCo(pFanout) && !pFanout->fMarkA )
- {
- Vec_VecPush( vLevels, pFanout->Level, pFanout );
- pFanout->fMarkA = 1;
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Incrementally updates level of the nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
-{
- Abc_Obj_t * pObjNew, * pFanin;
- int k;
- // create the new node
- pObjNew = Abc_NtkCreateNode( pObj->pNtk );
- pObjNew->pData = pFunc;
- Vec_PtrForEachEntry( vFanins, pFanin, k )
- Abc_ObjAddFanin( pObjNew, pFanin );
- // replace the old node by the new node
- pObjNew->Level = pObj->Level;
- Abc_ObjReplace( pObj, pObjNew );
- // update the level of the node
- Res_UpdateNetworkLevel( pObjNew, vLevels );
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 0b97843a..9696b027 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -66,7 +66,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
p->nNodesConsidered++;
// get the required times
- Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY;
+ Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
// get the node's cuts
clk = clock();
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 02:01:02 +0000