From e8cf8415c5c8c31db650f549e54fd7a3aad48be0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Sep 2007 08:01:00 -0700 Subject: Version abc70909 --- src/aig/kit/cloud.c | 987 +++++++++++++++++++++++++++++++++++++++++++++++ src/aig/kit/cloud.h | 269 +++++++++++++ src/aig/kit/kit.h | 27 +- src/aig/kit/kitCloud.c | 368 ++++++++++++++++++ src/aig/kit/kitDsd.c | 240 ++++++++++-- src/aig/kit/kitTruth.c | 64 ++- src/aig/kit/module.make | 1 + src/base/abc/abcRefs.c | 4 +- src/base/abci/abc.c | 23 +- src/misc/vec/vecStr.h | 2 +- src/opt/lpk/lpk.h | 1 + src/opt/lpk/lpkAbcDec.c | 130 +++++-- src/opt/lpk/lpkAbcDsd.c | 407 ++++++++++++------- src/opt/lpk/lpkAbcMux.c | 150 ++++--- src/opt/lpk/lpkAbcUtil.c | 46 ++- src/opt/lpk/lpkCore.c | 163 ++++++-- src/opt/lpk/lpkCut.c | 122 +++++- src/opt/lpk/lpkInt.h | 81 ++-- src/opt/lpk/lpkMan.c | 28 +- src/opt/lpk/lpkSets.c | 4 +- 20 files changed, 2765 insertions(+), 352 deletions(-) create mode 100644 src/aig/kit/cloud.c create mode 100644 src/aig/kit/cloud.h create mode 100644 src/aig/kit/kitCloud.c (limited to 'src') diff --git a/src/aig/kit/cloud.c b/src/aig/kit/cloud.c new file mode 100644 index 00000000..6e6691f0 --- /dev/null +++ b/src/aig/kit/cloud.c @@ -0,0 +1,987 @@ +/**CFile**************************************************************** + + FileName [cloudCore.c] + + PackageName [Fast application-specific BDD package.] + + Synopsis [The package core.] + + Author [Alan Mishchenko ] + + Affiliation [ECE Department. Portland State University, Portland, Oregon.] + + Date [Ver. 1.0. Started - June 10, 2002.] + + Revision [$Id: cloudCore.c,v 1.0 2002/06/10 03:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "cloud.h" + +// the number of operators using cache +static int CacheOperNum = 4; + +// the ratio of cache size to the unique table size for each operator +static int CacheLogRatioDefault[4] = { + 2, // CLOUD_OPER_AND, + 8, // CLOUD_OPER_XOR, + 8, // CLOUD_OPER_BDIFF, + 8 // CLOUD_OPER_LEQ +}; + +// the ratio of cache size to the unique table size for each operator +static int CacheSize[4] = { + 2, // CLOUD_OPER_AND, + 2, // CLOUD_OPER_XOR, + 2, // CLOUD_OPER_BDIFF, + 2 // CLOUD_OPER_LEQ +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// static functions +static CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e ); +static void cloudCacheAllocate( CloudManager * dd, CloudOper oper ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function******************************************************************** + + Synopsis [Starts the cloud manager.] + + Description [The first arguments is the number of elementary variables used. + The second arguments is the number of bits of the unsigned integer used to + represent nodes in the unique table. If the second argument is 0, the package + assumes 23 to represent nodes, which is equivalent to 2^23 = 8,388,608 nodes.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudManager * Cloud_Init( int nVars, int nBits ) +{ + CloudManager * dd; + int i; + int clk1, clk2; + + assert( nVars <= 100000 ); + assert( nBits < 32 ); + + // assign the defaults + if ( nBits == 0 ) + nBits = CLOUD_NODE_BITS; + + // start the manager + dd = CALLOC( CloudManager, 1 ); + dd->nMemUsed += sizeof(CloudManager); + + // variables + dd->nVars = nVars; // the number of variables allocated + // bits + dd->bitsNode = nBits; // the number of bits used for the node + for ( i = 0; i < CacheOperNum; i++ ) + dd->bitsCache[i] = nBits - CacheLogRatioDefault[i]; + // shifts + dd->shiftUnique = 8*sizeof(unsigned) - (nBits + 1); // gets node index in the hash table + for ( i = 0; i < CacheOperNum; i++ ) + dd->shiftCache[i] = 8*sizeof(unsigned) - dd->bitsCache[i]; + // nodes + dd->nNodesAlloc = (1 << (nBits + 1)); // 2 ^ (nBits + 1) + dd->nNodesLimit = (1 << nBits); // 2 ^ nBits + + // unique table +clk1 = clock(); + dd->tUnique = CALLOC( CloudNode, dd->nNodesAlloc ); + dd->nMemUsed += sizeof(CloudNode) * dd->nNodesAlloc; +clk2 = clock(); +//PRT( "calloc() time", clk2 - clk1 ); + + // set up the constant node (the only node that is not in the hash table) + dd->nSignCur = 1; + dd->tUnique[0].s = dd->nSignCur; + dd->tUnique[0].v = CLOUD_CONST_INDEX; + dd->tUnique[0].e = CLOUD_VOID; + dd->tUnique[0].t = CLOUD_VOID; + dd->one = dd->tUnique; + dd->zero = Cloud_Not(dd->one); + dd->nNodesCur = 1; + + // special nodes + dd->pNodeStart = dd->tUnique + 1; + dd->pNodeEnd = dd->tUnique + dd->nNodesAlloc; + + // set up the elementary variables + dd->vars = ALLOC( CloudNode *, dd->nVars ); + dd->nMemUsed += sizeof(CloudNode *) * dd->nVars; + for ( i = 0; i < dd->nVars; i++ ) + dd->vars[i] = cloudMakeNode( dd, i, dd->one, dd->zero ); + + return dd; +}; + +/**Function******************************************************************** + + Synopsis [Stops the cloud manager.] + + Description [The first arguments tells show many elementary variables are used. + The second arguments tells how many bits of the unsigned integer are used + to represent regular nodes in the unique table.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Cloud_Quit( CloudManager * dd ) +{ + int i; + FREE( dd->ppNodes ); + free( dd->tUnique ); + free( dd->vars ); + for ( i = 0; i < 4; i++ ) + FREE( dd->tCaches[i] ); + free( dd ); +} + +/**Function******************************************************************** + + Synopsis [Prepares the manager for another run.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Cloud_Restart( CloudManager * dd ) +{ + int i; + assert( dd->one->s == dd->nSignCur ); + dd->nSignCur++; + dd->one->s++; + for ( i = 0; i < dd->nVars; i++ ) + dd->vars[i]->s++; + dd->nNodesCur = 1 + dd->nVars; +} + +/**Function******************************************************************** + + Synopsis [This optional function allocates operation cache of the given size.] + + Description [Cache for each operation is allocated independently when the first + operation of the given type is performed. The user can allocate cache of his/her + preferred size by calling Cloud_CacheAllocate before the first operation of the + given type is performed, but this call is optional. Argument "logratio" gives + the binary logarithm of the ratio of the size of the unique table to that of cache. + For example, if "logratio" is equal to 3, and the unique table will be 2^3=8 times + larger than cache; so, if unique table is 2^23 = 8,388,608 nodes, the cache size + will be 2^3=8 times smaller and equal to 2^20 = 1,048,576 entries.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int logratio ) +{ + assert( logratio > 0 ); // cache cannot be larger than the unique table + assert( logratio < dd->bitsNode ); // cache cannot be smaller than 2 entries + + if ( logratio ) + { + dd->bitsCache[oper] = dd->bitsNode - logratio; + dd->shiftCache[oper] = 8*sizeof(unsigned) - dd->bitsCache[oper]; + } + cloudCacheAllocate( dd, oper ); +} + +/**Function******************************************************************** + + Synopsis [Internal cache allocation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void cloudCacheAllocate( CloudManager * dd, CloudOper oper ) +{ + int nCacheEntries = (1 << dd->bitsCache[oper]); + + if ( CacheSize[oper] == 1 ) + { + dd->tCaches[oper] = (CloudCacheEntry2 *)CALLOC( CloudCacheEntry1, nCacheEntries ); + dd->nMemUsed += sizeof(CloudCacheEntry1) * nCacheEntries; + } + else if ( CacheSize[oper] == 2 ) + { + dd->tCaches[oper] = (CloudCacheEntry2 *)CALLOC( CloudCacheEntry2, nCacheEntries ); + dd->nMemUsed += sizeof(CloudCacheEntry2) * nCacheEntries; + } + else if ( CacheSize[oper] == 3 ) + { + dd->tCaches[oper] = (CloudCacheEntry2 *)CALLOC( CloudCacheEntry3, nCacheEntries ); + dd->nMemUsed += sizeof(CloudCacheEntry3) * nCacheEntries; + } +} + + + +/**Function******************************************************************** + + Synopsis [Returns or creates a new node] + + Description [Checks the unique table for the existance of the node. If the node is + present, returns the node. If the node is absent, creates a new node.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e ) +{ + CloudNode * pRes; + CLOUD_ASSERT(t); + CLOUD_ASSERT(e); + assert( v < Cloud_V(t) && v < Cloud_V(e) ); // variable should be above in the order + if ( Cloud_IsComplement(t) ) + { + pRes = cloudMakeNode( dd, v, Cloud_Not(t), Cloud_Not(e) ); + if ( pRes != CLOUD_VOID ) + pRes = Cloud_Not(pRes); + } + else + pRes = cloudMakeNode( dd, v, t, e ); + return pRes; +} + +/**Function******************************************************************** + + Synopsis [Returns or creates a new node] + + Description [Checks the unique table for the existance of the node. If the node is + present, returns the node. If the node is absent, creates a new node.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudNode * cloudMakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e ) +{ + CloudNode * entryUnique; + + CLOUD_ASSERT(t); + CLOUD_ASSERT(e); + + assert( ((int)v) >= 0 && ((int)v) < dd->nVars ); // the variable must be in the range + assert( v < Cloud_V(t) && v < Cloud_V(e) ); // variable should be above in the order + assert( !Cloud_IsComplement(t) ); // the THEN edge must not be complemented + + // make sure we are not searching for the constant node + assert( t && e ); + + // get the unique entry + entryUnique = dd->tUnique + cloudHashCudd3(v, t, e, dd->shiftUnique); + while ( entryUnique->s == dd->nSignCur ) + { + // compare the node + if ( entryUnique->v == v && entryUnique->t == t && entryUnique->e == e ) + { // the node is found + dd->nUniqueHits++; + return entryUnique; // returns the node + } + // increment the hash value modulus the hash table size + if ( ++entryUnique - dd->tUnique == dd->nNodesAlloc ) + entryUnique = dd->tUnique + 1; + // increment the number of steps through the table + dd->nUniqueSteps++; + } + dd->nUniqueMisses++; + + // check if the new node can be created + if ( ++dd->nNodesCur == dd->nNodesLimit ) + { // initiate the restart + printf( "Cloud needs restart!\n" ); +// fflush( stdout ); +// exit(1); + return CLOUD_VOID; + } + // create the node + entryUnique->s = dd->nSignCur; + entryUnique->v = v; + entryUnique->t = t; + entryUnique->e = e; + return entryUnique; // returns the node +} + + +/**Function******************************************************************** + + Synopsis [Performs the AND or two BDDs] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudNode * cloudBddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ) +{ + CloudNode * F, * G, * r; + CloudCacheEntry2 * cacheEntry; + CloudNode * fv, * fnv, * gv, * gnv, * t, * e; + CloudVar var; + + assert( f <= g ); + + // terminal cases + F = Cloud_Regular(f); + G = Cloud_Regular(g); + if ( F == G ) + { + if ( f == g ) + return f; + else + return dd->zero; + } + if ( F == dd->one ) + { + if ( f == dd->one ) + return g; + else + return f; + } + + // check cache + cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashCudd2(f, g, dd->shiftCache[CLOUD_OPER_AND]); +// cacheEntry = dd->tCaches[CLOUD_OPER_AND] + cloudHashBuddy2(f, g, dd->shiftCache[CLOUD_OPER_AND]); + r = cloudCacheLookup2( cacheEntry, dd->nSignCur, f, g ); + if ( r != CLOUD_VOID ) + { + dd->nCacheHits++; + return r; + } + dd->nCacheMisses++; + + + // compute cofactors + if ( cloudV(F) <= cloudV(G) ) + { + var = cloudV(F); + if ( Cloud_IsComplement(f) ) + { + fnv = Cloud_Not(cloudE(F)); + fv = Cloud_Not(cloudT(F)); + } + else + { + fnv = cloudE(F); + fv = cloudT(F); + } + } + else + { + var = cloudV(G); + fv = fnv = f; + } + + if ( cloudV(G) <= cloudV(F) ) + { + if ( Cloud_IsComplement(g) ) + { + gnv = Cloud_Not(cloudE(G)); + gv = Cloud_Not(cloudT(G)); + } + else + { + gnv = cloudE(G); + gv = cloudT(G); + } + } + else + { + gv = gnv = g; + } + + if ( fv <= gv ) + t = cloudBddAnd( dd, fv, gv ); + else + t = cloudBddAnd( dd, gv, fv ); + + if ( t == CLOUD_VOID ) + return CLOUD_VOID; + + if ( fnv <= gnv ) + e = cloudBddAnd( dd, fnv, gnv ); + else + e = cloudBddAnd( dd, gnv, fnv ); + + if ( e == CLOUD_VOID ) + return CLOUD_VOID; + + if ( t == e ) + r = t; + else + { + if ( Cloud_IsComplement(t) ) + { + r = cloudMakeNode( dd, var, Cloud_Not(t), Cloud_Not(e) ); + if ( r == CLOUD_VOID ) + return CLOUD_VOID; + r = Cloud_Not(r); + } + else + { + r = cloudMakeNode( dd, var, t, e ); + if ( r == CLOUD_VOID ) + return CLOUD_VOID; + } + } + cloudCacheInsert2( cacheEntry, dd->nSignCur, f, g, r ); + return r; +} + +/**Function******************************************************************** + + Synopsis [Performs the AND or two BDDs] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static inline CloudNode * cloudBddAnd_gate( CloudManager * dd, CloudNode * f, CloudNode * g ) +{ + if ( f <= g ) + return cloudBddAnd(dd,f,g); + else + return cloudBddAnd(dd,g,f); +} + +/**Function******************************************************************** + + Synopsis [Performs the AND or two BDDs] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ) +{ + if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID ) + return CLOUD_VOID; + CLOUD_ASSERT(f); + CLOUD_ASSERT(g); + if ( dd->tCaches[CLOUD_OPER_AND] == NULL ) + cloudCacheAllocate( dd, CLOUD_OPER_AND ); + return cloudBddAnd_gate( dd, f, g ); +} + +/**Function******************************************************************** + + Synopsis [Performs the OR or two BDDs] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g ) +{ + CloudNode * res; + if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID ) + return CLOUD_VOID; + CLOUD_ASSERT(f); + CLOUD_ASSERT(g); + if ( dd->tCaches[CLOUD_OPER_AND] == NULL ) + cloudCacheAllocate( dd, CLOUD_OPER_AND ); + res = cloudBddAnd_gate( dd, Cloud_Not(f), Cloud_Not(g) ); + res = Cloud_NotCond( res, res != CLOUD_VOID ); + return res; +} + +/**Function******************************************************************** + + Synopsis [Performs the XOR or two BDDs] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudNode * Cloud_bddXor( CloudManager * dd, CloudNode * f, CloudNode * g ) +{ + CloudNode * t0, * t1, * r; + if ( Cloud_Regular(f) == CLOUD_VOID || Cloud_Regular(g) == CLOUD_VOID ) + return CLOUD_VOID; + CLOUD_ASSERT(f); + CLOUD_ASSERT(g); + if ( dd->tCaches[CLOUD_OPER_AND] == NULL ) + cloudCacheAllocate( dd, CLOUD_OPER_AND ); + t0 = cloudBddAnd_gate( dd, f, Cloud_Not(g) ); + if ( t0 == CLOUD_VOID ) + return CLOUD_VOID; + t1 = cloudBddAnd_gate( dd, Cloud_Not(f), g ); + if ( t1 == CLOUD_VOID ) + return CLOUD_VOID; + r = Cloud_bddOr( dd, t0, t1 ); + return r; +} + + + +/**Function******************************************************************** + + Synopsis [Performs a DFS from f, clearing the LSB of the next + pointers.] + + Description [] + + SideEffects [None] + + SeeAlso [cloudSupport cloudDagSize] + +******************************************************************************/ +static void cloudClearMark( CloudManager * dd, CloudNode * n ) +{ + if ( !cloudNodeIsMarked(n) ) + return; + // clear visited flag + cloudNodeUnmark(n); + if ( cloudIsConstant(n) ) + return; + cloudClearMark( dd, cloudT(n) ); + cloudClearMark( dd, Cloud_Regular(cloudE(n)) ); +} + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cloud_Support.] + + Description [Performs the recursive step of Cloud_Support. Performs a + DFS from f. The support is accumulated in supp as a side effect. Uses + the LSB of the then pointer as visited flag.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +static void cloudSupport( CloudManager * dd, CloudNode * n, int * support ) +{ + if ( cloudIsConstant(n) || cloudNodeIsMarked(n) ) + return; + // set visited flag + cloudNodeMark(n); + support[cloudV(n)] = 1; + cloudSupport( dd, cloudT(n), support ); + cloudSupport( dd, Cloud_Regular(cloudE(n)), support ); +} + +/**Function******************************************************************** + + Synopsis [Finds the variables on which a DD depends.] + + Description [Finds the variables on which a DD depends. + Returns a BDD consisting of the product of the variables if + successful; NULL otherwise.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n ) +{ + CloudNode * res; + int * support, i; + + CLOUD_ASSERT(n); + + // allocate and initialize support array for cloudSupport + support = CALLOC( int, dd->nVars ); + + // compute support and clean up markers + cloudSupport( dd, Cloud_Regular(n), support ); + cloudClearMark( dd, Cloud_Regular(n) ); + + // transform support from array to cube + res = dd->one; + for ( i = dd->nVars - 1; i >= 0; i-- ) // for each level bottom-up + if ( support[i] == 1 ) + { + res = Cloud_bddAnd( dd, res, dd->vars[i] ); + if ( res == CLOUD_VOID ) + break; + } + FREE( support ); + return res; +} + +/**Function******************************************************************** + + Synopsis [Counts the variables on which a DD depends.] + + Description [Counts the variables on which a DD depends. + Returns the number of the variables if successful; Cloud_OUT_OF_MEM + otherwise.] + + SideEffects [None] + + SeeAlso [] + +******************************************************************************/ +int Cloud_SupportSize( CloudManager * dd, CloudNode * n ) +{ + int * support, i, count; + + CLOUD_ASSERT(n); + + // allocate and initialize support array for cloudSupport + support = CALLOC( int, dd->nVars ); + + // compute support and clean up markers + cloudSupport( dd, Cloud_Regular(n), support ); + cloudClearMark( dd, Cloud_Regular(n) ); + + // count support variables + count = 0; + for ( i = 0; i < dd->nVars; i++ ) + { + if ( support[i] == 1 ) + count++; + } + + FREE( support ); + return count; +} + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cloud_DagSize.] + + Description [Performs the recursive step of Cloud_DagSize. Returns the + number of nodes in the graph rooted at n.] + + SideEffects [None] + +******************************************************************************/ +static int cloudDagSize( CloudManager * dd, CloudNode * n ) +{ + int tval, eval; + if ( cloudNodeIsMarked(n) ) + return 0; + // set visited flag + cloudNodeMark(n); + if ( cloudIsConstant(n) ) + return 1; + tval = cloudDagSize( dd, cloudT(n) ); + eval = cloudDagSize( dd, Cloud_Regular(cloudE(n)) ); + return tval + eval + 1; + +} + +/**Function******************************************************************** + + Synopsis [Counts the number of nodes in a DD.] + + Description [Counts the number of nodes in a DD. Returns the number + of nodes in the graph rooted at node.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Cloud_DagSize( CloudManager * dd, CloudNode * n ) +{ + int res; + res = cloudDagSize( dd, Cloud_Regular( n ) ); + cloudClearMark( dd, Cloud_Regular( n ) ); + return res; + +} + + +/**Function******************************************************************** + + Synopsis [Performs the recursive step of Cloud_DagSize.] + + Description [Performs the recursive step of Cloud_DagSize. Returns the + number of nodes in the graph rooted at n.] + + SideEffects [None] + +******************************************************************************/ +static int Cloud_DagCollect_rec( CloudManager * dd, CloudNode * n, int * pCounter ) +{ + int tval, eval; + if ( cloudNodeIsMarked(n) ) + return 0; + // set visited flag + cloudNodeMark(n); + if ( cloudIsConstant(n) ) + { + dd->ppNodes[(*pCounter)++] = n; + return 1; + } + tval = Cloud_DagCollect_rec( dd, cloudT(n), pCounter ); + eval = Cloud_DagCollect_rec( dd, Cloud_Regular(cloudE(n)), pCounter ); + dd->ppNodes[(*pCounter)++] = n; + return tval + eval + 1; + +} + +/**Function******************************************************************** + + Synopsis [Counts the number of nodes in a DD.] + + Description [Counts the number of nodes in a DD. Returns the number + of nodes in the graph rooted at node.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Cloud_DagCollect( CloudManager * dd, CloudNode * n ) +{ + int res, Counter = 0; + if ( dd->ppNodes == NULL ) + dd->ppNodes = ALLOC( CloudNode *, dd->nNodesLimit ); + res = Cloud_DagCollect_rec( dd, Cloud_Regular( n ), &Counter ); + cloudClearMark( dd, Cloud_Regular( n ) ); + assert( res == Counter ); + return res; + +} + +/**Function******************************************************************** + + Synopsis [Counts the number of nodes in an array of DDs.] + + Description [Counts the number of nodes in a DD. Returns the number + of nodes in the graph rooted at node.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Cloud_SharingSize( CloudManager * dd, CloudNode ** pn, int nn ) +{ + int res, i; + res = 0; + for ( i = 0; i < nn; i++ ) + res += cloudDagSize( dd, Cloud_Regular( pn[i] ) ); + for ( i = 0; i < nn; i++ ) + cloudClearMark( dd, Cloud_Regular( pn[i] ) ); + return res; +} + + +/**Function******************************************************************** + + Synopsis [Returns one cube contained in the given BDD.] + + Description [] + + SideEffects [] + +******************************************************************************/ +CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * bFunc ) +{ + CloudNode * bFunc0, * bFunc1, * res; + + if ( Cloud_IsConstant(bFunc) ) + return bFunc; + + // cofactor + if ( Cloud_IsComplement(bFunc) ) + { + bFunc0 = Cloud_Not( cloudE(bFunc) ); + bFunc1 = Cloud_Not( cloudT(bFunc) ); + } + else + { + bFunc0 = cloudE(bFunc); + bFunc1 = cloudT(bFunc); + } + + // try to find the cube with the negative literal + res = Cloud_GetOneCube( dd, bFunc0 ); + if ( res == CLOUD_VOID ) + return CLOUD_VOID; + + if ( res != dd->zero ) + { + res = Cloud_bddAnd( dd, res, Cloud_Not(dd->vars[Cloud_V(bFunc)]) ); + } + else + { + // try to find the cube with the positive literal + res = Cloud_GetOneCube( dd, bFunc1 ); + if ( res == CLOUD_VOID ) + return CLOUD_VOID; + assert( res != dd->zero ); + res = Cloud_bddAnd( dd, res, dd->vars[Cloud_V(bFunc)] ); + } + return res; +} + +/**Function******************************************************************** + + Synopsis [Prints the BDD as a set of disjoint cubes to the standard output.] + + Description [] + + SideEffects [] + +******************************************************************************/ +void Cloud_bddPrint( CloudManager * dd, CloudNode * Func ) +{ + CloudNode * Cube; + int fFirst = 1; + + if ( Func == dd->zero ) + printf( "Constant 0." ); + else if ( Func == dd->one ) + printf( "Constant 1." ); + else + { + while ( 1 ) + { + Cube = Cloud_GetOneCube( dd, Func ); + if ( Cube == CLOUD_VOID || Cube == dd->zero ) + break; + if ( fFirst ) fFirst = 0; + else printf( " + " ); + Cloud_bddPrintCube( dd, Cube ); + Func = Cloud_bddAnd( dd, Func, Cloud_Not(Cube) ); + } + } + printf( "\n" ); +} + +/**Function******************************************************************** + + Synopsis [Prints one cube.] + + Description [] + + SideEffects [] + +******************************************************************************/ +void Cloud_bddPrintCube( CloudManager * dd, CloudNode * bCube ) +{ + CloudNode * bCube0, * bCube1; + + assert( !Cloud_IsConstant(bCube) ); + while ( 1 ) + { + // get the node structure + if ( Cloud_IsConstant(bCube) ) + break; + + // cofactor the cube + if ( Cloud_IsComplement(bCube) ) + { + bCube0 = Cloud_Not( cloudE(bCube) ); + bCube1 = Cloud_Not( cloudT(bCube) ); + } + else + { + bCube0 = cloudE(bCube); + bCube1 = cloudT(bCube); + } + + if ( bCube0 != dd->zero ) + { + assert( bCube1 == dd->zero ); + printf( "[%d]'", cloudV(bCube) ); + bCube = bCube0; + } + else + { + assert( bCube1 != dd->zero ); + printf( "[%d]", cloudV(bCube) ); + bCube = bCube1; + } + } +} + + +/**Function******************************************************************** + + Synopsis [Prints info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Cloud_PrintInfo( CloudManager * dd ) +{ + if ( dd == NULL ) return; + printf( "The number of unique table nodes allocated = %12d.\n", dd->nNodesAlloc ); + printf( "The number of unique table nodes present = %12d.\n", dd->nNodesCur ); + printf( "The number of unique table hits = %12d.\n", dd->nUniqueHits ); + printf( "The number of unique table misses = %12d.\n", dd->nUniqueMisses ); + printf( "The number of unique table steps = %12d.\n", dd->nUniqueSteps ); + printf( "The number of cache hits = %12d.\n", dd->nCacheHits ); + printf( "The number of cache misses = %12d.\n", dd->nCacheMisses ); + printf( "The current signature = %12d.\n", dd->nSignCur ); + printf( "The total memory in use = %12d.\n", dd->nMemUsed ); +} + +/**Function******************************************************************** + + Synopsis [Prints the state of the hash table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Cloud_PrintHashTable( CloudManager * dd ) +{ + int i; + + for ( i = 0; i < dd->nNodesAlloc; i++ ) + if ( dd->tUnique[i].v == CLOUD_CONST_INDEX ) + printf( "-" ); + else + printf( "+" ); + printf( "\n" ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/kit/cloud.h b/src/aig/kit/cloud.h new file mode 100644 index 00000000..ac9d45f4 --- /dev/null +++ b/src/aig/kit/cloud.h @@ -0,0 +1,269 @@ +/**CFile**************************************************************** + + FileName [cloud.h] + + PackageName [Fast application-specific BDD package.] + + Synopsis [Interface of the package.] + + Author [Alan Mishchenko ] + + Affiliation [ECE Department. Portland State University, Portland, Oregon.] + + Date [Ver. 1.0. Started - June 10, 2002.] + + Revision [$Id: cloud.h,v 1.0 2002/06/10 03:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __CLOUD_H__ +#define __CLOUD_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +#include +#include +#include +#include + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +//////////////////////////////////////////////////////////////////////// +// n | 2^n || n | 2^n || n | 2^n || n | 2^n // +//====================================================================// +// 1 | 2 || 9 | 512 || 17 | 131,072 || 25 | 33,554,432 // +// 2 | 4 || 10 | 1,024 || 18 | 262,144 || 26 | 67,108,864 // +// 3 | 8 || 11 | 2,048 || 19 | 524,288 || 27 | 134,217,728 // +// 4 | 16 || 12 | 4,096 || 20 | 1,048,576 || 28 | 268,435,456 // +// 5 | 32 || 13 | 8,192 || 21 | 2,097,152 || 29 | 536,870,912 // +// 6 | 64 || 14 | 16,384 || 22 | 4,194,304 || 30 | 1,073,741,824 // +// 7 | 128 || 15 | 32,768 || 23 | 8,388,608 || 31 | 2,147,483,648 // +// 8 | 256 || 16 | 65,536 || 24 | 16,777,216 || 32 | 4,294,967,296 // +//////////////////////////////////////////////////////////////////////// + +// data structure typedefs +typedef struct cloudManager CloudManager; +typedef unsigned CloudVar; +typedef unsigned CloudSign; +typedef struct cloudNode CloudNode; +typedef struct cloudCacheEntry1 CloudCacheEntry1; +typedef struct cloudCacheEntry2 CloudCacheEntry2; +typedef struct cloudCacheEntry3 CloudCacheEntry3; + +// operation codes used to set up the cache +typedef enum { + CLOUD_OPER_AND, + CLOUD_OPER_XOR, + CLOUD_OPER_BDIFF, + CLOUD_OPER_LEQ +} CloudOper; + +/* +// the number of operators using cache +static int CacheOperNum = 4; + +// the ratio of cache size to the unique table size for each operator +static int CacheLogRatioDefault[4] = { + 4, // CLOUD_OPER_AND, + 8, // CLOUD_OPER_XOR, + 8, // CLOUD_OPER_BDIFF, + 8 // CLOUD_OPER_LEQ +}; + +// the ratio of cache size to the unique table size for each operator +static int CacheSize[4] = { + 2, // CLOUD_OPER_AND, + 2, // CLOUD_OPER_XOR, + 2, // CLOUD_OPER_BDIFF, + 2 // CLOUD_OPER_LEQ +}; +*/ + +// data structure definitions +struct cloudManager // the fast bdd manager +{ + // variables + int nVars; // the number of variables allocated + // bits + int bitsNode; // the number of bits used for the node + int bitsCache[4]; // default: bitsNode - CacheSizeRatio[i] + // shifts + int shiftUnique; // 8*sizeof(unsigned) - (bitsNode + 1) + int shiftCache[4]; // 8*sizeof(unsigned) - bitsCache[i] + // nodes + int nNodesAlloc; // 2 ^ (bitsNode + 1) + int nNodesLimit; // 2 ^ bitsNode + int nNodesCur; // the current number of nodes (including const1 and vars) + // signature + CloudSign nSignCur; + + // statistics + int nMemUsed; // memory usage in bytes + // cache stats + int nUniqueHits; // hits in the unique table + int nUniqueMisses; // misses in the unique table + int nCacheHits; // hits in the caches + int nCacheMisses; // misses in the caches + // the number of steps through the hash table + int nUniqueSteps; + + // tables + CloudNode * tUnique; // the unique table to store BDD nodes + + // special nodes + CloudNode * pNodeStart; // the pointer to the first node + CloudNode * pNodeEnd; // the pointer to the first node out of the table + + // constants and variables + CloudNode * one; // the one function + CloudNode * zero; // the zero function + CloudNode ** vars; // the elementary variables + + // temporary storage for nodes + CloudNode ** ppNodes; + + // caches + CloudCacheEntry2 * tCaches[20]; // caches +}; + +struct cloudNode // representation of the node in the unique table +{ + CloudSign s; // signature + CloudVar v; // variable + CloudNode * e; // negative cofactor + CloudNode * t; // positive cofactor +}; +struct cloudCacheEntry1 // one-argument cache +{ + CloudSign s; // signature + CloudNode * a; // argument 1 + CloudNode * r; // result +}; +struct cloudCacheEntry2 // the two-argument cache +{ + CloudSign s; // signature + CloudNode * a; + CloudNode * b; + CloudNode * r; +}; +struct cloudCacheEntry3 // the three-argument cache +{ + CloudSign s; // signature + CloudNode * a; + CloudNode * b; + CloudNode * c; + CloudNode * r; +}; + + +// parameters +#define CLOUD_NODE_BITS 23 +#define CLOUD_ONE ((unsigned)0x00000001) +#define CLOUD_NOT_ONE ((unsigned)0xfffffffe) +#define CLOUD_VOID ((unsigned)0x00000000) + +#define CLOUD_CONST_INDEX ((unsigned)0x0fffffff) +#define CLOUD_MARK_ON ((unsigned)0x10000000) +#define CLOUD_MARK_OFF ((unsigned)0xefffffff) + +// hash functions a la Buddy +#define cloudHashBuddy2(x,y,s) ((((x)+(y))*((x)+(y)+1)/2) & ((1<<(32-(s)))-1)) +#define cloudHashBuddy3(x,y,z,s) (cloudHashBuddy2((cloudHashBuddy2((x),(y),(s))),(z),(s)) & ((1<<(32-(s)))-1)) +// hash functions a la Cudd +#define DD_P1 12582917 +#define DD_P2 4256249 +#define DD_P3 741457 +#define DD_P4 1618033999 +#define cloudHashCudd2(f,g,s) ((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2) >> (s)) +#define cloudHashCudd3(f,g,h,s) (((((unsigned)(f) * DD_P1 + (unsigned)(g)) * DD_P2 + (unsigned)(h)) * DD_P3) >> (s)) + +// node complementation (using node) +#define Cloud_Regular(p) ((CloudNode*)(((unsigned)(p)) & CLOUD_NOT_ONE)) // get the regular node (w/o bubble) +#define Cloud_Not(p) ((CloudNode*)(((unsigned)(p)) ^ CLOUD_ONE)) // complement the node +#define Cloud_NotCond(p,c) (((int)(c))? Cloud_Not(p):(p)) // complement the node conditionally +#define Cloud_IsComplement(p) ((int)(((unsigned)(p)) & CLOUD_ONE)) // check if complemented +// checking constants (using node) +#define Cloud_IsConstant(p) (((Cloud_Regular(p))->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX) +#define cloudIsConstant(p) (((p)->v & CLOUD_MARK_OFF) == CLOUD_CONST_INDEX) + +// retrieving values from the node (using node structure) +#define Cloud_V(p) ((Cloud_Regular(p))->v) +#define Cloud_E(p) ((Cloud_Regular(p))->e) +#define Cloud_T(p) ((Cloud_Regular(p))->t) +// retrieving values from the regular node (using node structure) +#define cloudV(p) ((p)->v) +#define cloudE(p) ((p)->e) +#define cloudT(p) ((p)->t) +// marking/unmarking (using node structure) +#define cloudNodeMark(p) ((p)->v |= CLOUD_MARK_ON) +#define cloudNodeUnmark(p) ((p)->v &= CLOUD_MARK_OFF) +#define cloudNodeIsMarked(p) ((int)((p)->v & CLOUD_MARK_ON)) + +// cache lookups and inserts (using node) +#define cloudCacheLookup1(p,sign,f) (((p)->s == (sign) && (p)->a == (f))? ((p)->r): (CLOUD_VOID)) +#define cloudCacheLookup2(p,sign,f,g) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g))? ((p)->r): (CLOUD_VOID)) +#define cloudCacheLookup3(p,sign,f,g,h) (((p)->s == (sign) && (p)->a == (f) && (p)->b == (g) && (p)->c == (h))? ((p)->r): (CLOUD_VOID)) +// cache inserts +#define cloudCacheInsert1(p,sign,f,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->r = (r))) +#define cloudCacheInsert2(p,sign,f,g,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->r = (r))) +#define cloudCacheInsert3(p,sign,f,g,h,r) (((p)->s = (sign)), ((p)->a = (f)), ((p)->b = (g)), ((p)->c = (h)), ((p)->r = (r))) + +//#define CLOUD_ASSERT(p) (assert((p) >= (dd->pNodeStart-1) && (p) < dd->pNodeEnd)) +#define CLOUD_ASSERT(p) assert((p) >= dd->tUnique && (p) < dd->tUnique+dd->nNodesAlloc) + +// utility macros +#ifndef ALLOC +#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) +#endif + +#ifndef CALLOC +#define CALLOC(type, num) ((type *) calloc((num), sizeof(type))) +#endif + +#ifndef FREE +#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) +#endif + +#ifndef PRT +#define PRT(a,t) fprintf( stdout, "%s = ", (a)); printf( "%.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) +#endif + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// +// starting/stopping +extern CloudManager * Cloud_Init( int nVars, int nBits ); +extern void Cloud_Quit( CloudManager * dd ); +extern void Cloud_Restart( CloudManager * dd ); +extern void Cloud_CacheAllocate( CloudManager * dd, CloudOper oper, int size ); +extern CloudNode * Cloud_MakeNode( CloudManager * dd, CloudVar v, CloudNode * t, CloudNode * e ); +// support and node count +extern CloudNode * Cloud_Support( CloudManager * dd, CloudNode * n ); +extern int Cloud_SupportSize( CloudManager * dd, CloudNode * n ); +extern int Cloud_DagSize( CloudManager * dd, CloudNode * n ); +extern int Cloud_DagCollect( CloudManager * dd, CloudNode * n ); +extern int Cloud_SharingSize( CloudManager * dd, CloudNode * * pn, int nn ); +// cubes +extern CloudNode * Cloud_GetOneCube( CloudManager * dd, CloudNode * n ); +extern void Cloud_bddPrint( CloudManager * dd, CloudNode * Func ); +extern void Cloud_bddPrintCube( CloudManager * dd, CloudNode * Cube ); +// operations +extern CloudNode * Cloud_bddAnd( CloudManager * dd, CloudNode * f, CloudNode * g ); +extern CloudNode * Cloud_bddOr( CloudManager * dd, CloudNode * f, CloudNode * g ); +// stats +extern void Cloud_PrintInfo( CloudManager * dd ); +extern void Cloud_PrintHashTable( CloudManager * dd ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h index 2ad9a6f0..06a93cf0 100644 --- a/src/aig/kit/kit.h +++ b/src/aig/kit/kit.h @@ -36,6 +36,7 @@ extern "C" { #include #include "vec.h" #include "extra.h" +#include "cloud.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -133,6 +134,10 @@ struct Kit_DsdMan_t_ int nWords; // the number of words in TTs Vec_Ptr_t * vTtElems; // elementary truth tables Vec_Ptr_t * vTtNodes; // the node truth tables + // BDD representation + CloudManager * dd; // BDD package + Vec_Ptr_t * vTtBdds; // the node truth tables + Vec_Int_t * vNodes; // temporary array for BDD nodes }; static inline int Kit_DsdVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } @@ -431,6 +436,16 @@ static inline void Kit_TruthMux( unsigned * pOut, unsigned * pIn0, unsigned * pI for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]); } +static inline void Kit_TruthMuxPhase( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, unsigned * pCtrl, int nVars, int fComp0 ) +{ + int w; + if ( fComp0 ) + for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = (~pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]); + else + for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = (pIn0[w] & ~pCtrl[w]) | (pIn1[w] & pCtrl[w]); +} static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar ) { unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; @@ -473,11 +488,18 @@ static inline void Kit_TruthIthVar( unsigned * pTruth, int nVars, int iVar ) 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 ); +/*=== kitCloud.c ==========================================================*/ +extern CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars ); +extern unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv ); +extern int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes ); +extern int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes ); +extern unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes ); +extern void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps ); /*=== kitDsd.c ==========================================================*/ extern Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes ); 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, unsigned uSupp ); +extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk ); 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_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec ); @@ -485,10 +507,12 @@ 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_DsdDecomposeExpand( 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 unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk ); extern unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p ); extern Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p ); extern Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] ); @@ -548,6 +572,7 @@ extern void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, i extern void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask ); extern void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar ); +extern void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 ); 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 ); diff --git a/src/aig/kit/kitCloud.c b/src/aig/kit/kitCloud.c new file mode 100644 index 00000000..7b160fea --- /dev/null +++ b/src/aig/kit/kitCloud.c @@ -0,0 +1,368 @@ +/**CFile**************************************************************** + + FileName [kitCloud.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Computation kit.] + + Synopsis [Procedures using BDD package CLOUD.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Dec 6, 2006.] + + Revision [$Id: kitCloud.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "kit.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +// internal representation of the function to be decomposed +typedef struct Kit_Mux_t_ Kit_Mux_t; +struct Kit_Mux_t_ +{ + unsigned v : 5; // variable + unsigned t : 12; // then edge + unsigned e : 12; // else edge + unsigned c : 1; // complemented attr of else edge + unsigned i : 1; // complemented attr of top node +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derive BDD from the truth table for 5 variable functions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +CloudNode * Kit_TruthToCloud5_rec( CloudManager * dd, unsigned uTruth, int nVars, int nVarsAll ) +{ + static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + CloudNode * pCof0, * pCof1; + unsigned uCof0, uCof1; + assert( nVars <= 5 ); + if ( uTruth == 0 ) + return dd->zero; + if ( uTruth == ~0 ) + return dd->one; + if ( nVars == 1 ) + { + if ( uTruth == uVars[0] ) + return dd->vars[nVarsAll-1]; + if ( uTruth == ~uVars[0] ) + return Cloud_Not(dd->vars[nVarsAll-1]); + assert( 0 ); + } +// Count++; + assert( nVars > 1 ); + uCof0 = uTruth & ~uVars[nVars-1]; + uCof1 = uTruth & uVars[nVars-1]; + uCof0 |= uCof0 << (1<<(nVars-1)); + uCof1 |= uCof1 >> (1<<(nVars-1)); + if ( uCof0 == uCof1 ) + return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll ); + if ( uCof0 == ~uCof1 ) + { + pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll ); + pCof1 = Cloud_Not( pCof0 ); + } + else + { + pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll ); + pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll ); + } + return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 ); +} + +/**Function******************************************************************** + + Synopsis [Compute BDD for the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudNode * Kit_TruthToCloud_rec( CloudManager * dd, unsigned * pTruth, int nVars, int nVarsAll ) +{ + CloudNode * pCof0, * pCof1; + unsigned * pTruth0, * pTruth1; + if ( nVars <= 5 ) + return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll ); + if ( Kit_TruthIsConst0(pTruth, nVars) ) + return dd->zero; + if ( Kit_TruthIsConst1(pTruth, nVars) ) + return dd->one; +// Count++; + pTruth0 = pTruth; + pTruth1 = pTruth + Kit_TruthWordNum(nVars-1); + if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) ) + return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll ); + if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) ) + { + pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll ); + pCof1 = Cloud_Not( pCof0 ); + } + else + { + pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll ); + pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll ); + } + return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 ); +} + +/**Function******************************************************************** + + Synopsis [Compute BDD for the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars ) +{ + CloudNode * pRes; + pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars ); +// printf( "%d/%d ", Count, Cloud_DagSize(dd, pRes) ); + return pRes; +} + +/**Function******************************************************************** + + Synopsis [Transforms the array of BDDs into the integer array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes ) +{ + Kit_Mux_t Mux; + int nNodes, i; + // collect BDD nodes + nNodes = Cloud_DagCollect( dd, pFunc ); + if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit + return 0; + assert( nNodes == Cloud_DagSize( dd, pFunc ) ); + assert( nNodes < dd->nNodesLimit ); + Vec_IntClear( vNodes ); + Vec_IntPush( vNodes, 0 ); // const1 node + dd->ppNodes[0]->s = 0; + for ( i = 1; i < nNodes; i++ ) + { + dd->ppNodes[i]->s = i; + Mux.v = dd->ppNodes[i]->v; + Mux.t = dd->ppNodes[i]->t->s; + Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s; + Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e); + Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0; + // put the MUX into the array + Vec_IntPush( vNodes, *((int *)&Mux) ); + } + assert( Vec_IntSize(vNodes) == nNodes ); + // reset signatures + for ( i = 0; i < nNodes; i++ ) + dd->ppNodes[i]->s = dd->nSignCur; + return 1; +} + +/**Function******************************************************************** + + Synopsis [Transforms the array of BDDs into the integer array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes ) +{ + CloudNode * pFunc; + Cloud_Restart( dd ); + pFunc = Kit_TruthToCloud( dd, pTruth, nVars ); + Vec_IntClear( vNodes ); + return Kit_CreateCloud( dd, pFunc, vNodes ); +} + +/**Function************************************************************* + + Synopsis [Computes composition of truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv ) +{ + unsigned * pThis, * pFan0, * pFan1; + Kit_Mux_t Mux; + int i, Entry; + assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) ); + pThis = Vec_PtrEntry( vStore, 0 ); + Kit_TruthFill( pThis, nVars ); + Vec_IntForEachEntryStart( vNodes, Entry, i, 1 ) + { + Mux = *((Kit_Mux_t *)&Entry); + assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars ); + pFan0 = Vec_PtrEntry( vStore, Mux.e ); + pFan1 = Vec_PtrEntry( vStore, Mux.t ); + pThis = Vec_PtrEntry( vStore, i ); + Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c ); + } + // complement the result + if ( Mux.i ) + Kit_TruthNot( pThis, pThis, nVars ); + return pThis; +} + +/**Function************************************************************* + + Synopsis [Computes composition of truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars, + unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes ) +{ + CloudNode * pFunc; + unsigned * pThis, * pFan0, * pFan1; + Kit_Mux_t Mux; + int i, Entry, RetValue; + // derive BDD from truth table + Cloud_Restart( dd ); + pFunc = Kit_TruthToCloud( dd, pTruth, nVars ); + // convert it into nodes + RetValue = Kit_CreateCloud( dd, pFunc, vNodes ); + if ( RetValue == 0 ) + printf( "Kit_TruthCompose(): Internal failure!!!\n" ); + // verify the result +// pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 ); +// if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) ) +// printf( "Failed!\n" ); + // compute truth table from the BDD + assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) ); + pThis = Vec_PtrEntry( vStore, 0 ); + Kit_TruthFill( pThis, nVarsAll ); + Vec_IntForEachEntryStart( vNodes, Entry, i, 1 ) + { + Mux = *((Kit_Mux_t *)&Entry); + pFan0 = Vec_PtrEntry( vStore, Mux.e ); + pFan1 = Vec_PtrEntry( vStore, Mux.t ); + pThis = Vec_PtrEntry( vStore, i ); + Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c ); + } + // complement the result + if ( Mux.i ) + Kit_TruthNot( pThis, pThis, nVarsAll ); + return pThis; +} + +/**Function******************************************************************** + + Synopsis [Compute BDD for the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps ) +{ + Kit_Mux_t Mux; + unsigned * puSuppAll, * pThis, * pFan0, * pFan1; + int i, v, Var, Entry, nSupps; + nSupps = 2 * nVars; + + // extend storage + if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) ) + Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) ); + puSuppAll = Vec_IntArray( vMemory ); + // clear storage for the const node + memset( puSuppAll, 0, sizeof(unsigned) * nSupps ); + // compute supports from nodes + Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 ) + { + Mux = *((Kit_Mux_t *)&Entry); + Var = nVars - 1 - Mux.v; + pFan0 = puSuppAll + nSupps * Mux.e; + pFan1 = puSuppAll + nSupps * Mux.t; + pThis = puSuppAll + nSupps * i; + for ( v = 0; v < nSupps; v++ ) + pThis[v] = pFan0[v] | pFan1[v] | (1<nVars = nVars; - p->nWords = Kit_TruthWordNum( p->nVars ); + p->nVars = nVars; + p->nWords = Kit_TruthWordNum( p->nVars ); p->vTtElems = Vec_PtrAllocTruthTables( p->nVars ); p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords ); + p->dd = Cloud_Init( 16, 13 ); + p->vTtBdds = Vec_PtrAllocSimInfo( (1<<12), p->nWords ); + p->vNodes = Vec_IntAlloc( 512 ); return p; } @@ -64,6 +67,9 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes ) ***********************************************************************/ void Kit_DsdManFree( Kit_DsdMan_t * p ) { + Cloud_Quit( p->dd ); + Vec_IntFree( p->vNodes ); + Vec_PtrFree( p->vTtBdds ); Vec_PtrFree( p->vTtElems ); Vec_PtrFree( p->vTtNodes ); free( p ); @@ -315,11 +321,140 @@ void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars ) SeeAlso [] ***********************************************************************/ -unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp ) +unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id ) { Kit_DsdObj_t * pObj; - unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16]; - unsigned i, m, iLit, nMints, fCompl, nPartial = 0; + unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp; + unsigned i, iLit, fCompl; +// unsigned m, nMints, * pTruthPrime, * pTruthMint; + + // get the node with this ID + pObj = Kit_DsdNtkObj( pNtk, Id ); + pTruthRes = Vec_PtrEntry( p->vTtNodes, Id ); + + // special case: literal of an internal node + if ( pObj == NULL ) + { + assert( Id < pNtk->nVars ); + return pTruthRes; + } + + // constant node + if ( pObj->Type == KIT_DSD_CONST1 ) + { + assert( pObj->nFans == 0 ); + Kit_TruthFill( pTruthRes, pNtk->nVars ); + return pTruthRes; + } + + // elementary variable node + if ( pObj->Type == KIT_DSD_VAR ) + { + assert( pObj->nFans == 1 ); + iLit = pObj->pFans[0]; + pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) ); + if ( Kit_DsdLitIsCompl(iLit) ) + Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars ); + else + Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars ); + return pTruthRes; + } + + // collect the truth tables of the fanins + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) ); + // create the truth table + + // simple gates + if ( pObj->Type == KIT_DSD_AND ) + { + Kit_TruthFill( pTruthRes, pNtk->nVars ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); + return pTruthRes; + } + if ( pObj->Type == KIT_DSD_XOR ) + { + Kit_TruthClear( pTruthRes, pNtk->nVars ); + fCompl = 0; + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + { + Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); + fCompl ^= Kit_DsdLitIsCompl(iLit); + } + if ( fCompl ) + Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); + return pTruthRes; + } + assert( pObj->Type == KIT_DSD_PRIME ); +/* + // get the truth table of the prime node + pTruthPrime = Kit_DsdObjTruth( pObj ); + // get storage for the temporary minterm + pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes); + + // go through the minterms + nMints = (1 << pObj->nFans); + Kit_TruthClear( pTruthRes, pNtk->nVars ); + for ( m = 0; m < nMints; m++ ) + { + if ( !Kit_TruthHasBit(pTruthPrime, m) ) + continue; + Kit_TruthFill( pTruthMint, pNtk->nVars ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<nVars ); + } +*/ + pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes ); + Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars ); + return pTruthRes; +} + +/**Function************************************************************* + + Synopsis [Derives the truth table of the DSD network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk ) +{ + unsigned * pTruthRes; + int i; + // assign elementary truth ables + 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) ); + // complement the truth table if needed + if ( Kit_DsdLitIsCompl(pNtk->Root) ) + Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); + return pTruthRes; +} + +/**Function************************************************************* + + Synopsis [Derives the truth table of the DSD node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Kit_DsdTruthComputeNodeOne_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp ) +{ + Kit_DsdObj_t * pObj; + unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp; + unsigned i, iLit, fCompl, nPartial = 0; +// unsigned m, nMints, * pTruthPrime, * pTruthMint; // get the node with this ID pObj = Kit_DsdNtkObj( pNtk, Id ); @@ -347,7 +482,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i assert( pObj->nFans == 1 ); iLit = pObj->pFans[0]; assert( Kit_DsdLitIsLeaf( pNtk, iLit ) ); - pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); + pTruthFans[0] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); if ( Kit_DsdLitIsCompl(iLit) ) Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars ); else @@ -360,7 +495,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i { Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) ) - pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); + pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); else { pTruthFans[i] = NULL; @@ -370,7 +505,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i else { Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) - pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); + pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); } // create the truth table @@ -410,7 +545,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i 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 @@ -428,6 +563,9 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<nVars ); } +*/ + pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes ); + Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars ); return pTruthRes; } @@ -442,7 +580,7 @@ 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 uSupp ) +unsigned * Kit_DsdTruthComputeOne( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp ) { unsigned * pTruthRes; int i; @@ -454,7 +592,7 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned 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), uSupp ); + pTruthRes = Kit_DsdTruthComputeNodeOne_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 ); @@ -475,9 +613,10 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp, int iVar, unsigned * pTruthDec ) { Kit_DsdObj_t * pObj; - unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16]; - unsigned i, m, iLit, nMints, fCompl, uSuppCur, uSuppFan, nPartial; int pfBoundSet[16]; + unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp; + unsigned i, iLit, fCompl, nPartial, uSuppFan, uSuppCur; +// unsigned m, nMints, * pTruthPrime, * pTruthMint; assert( uSupp > 0 ); // get the node with this ID @@ -507,7 +646,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk // if there is no intersection, or full intersection, use simple procedure if ( nPartial == 0 || nPartial == pObj->nFans ) - return Kit_DsdTruthComputeNode_rec( p, pNtk, Id, 0 ); + return Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Id, 0 ); // if support of the component includes some other variables // we need to continue constructing it as usual by the two-function procedure @@ -520,7 +659,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk if ( uSupp & Kit_DsdLitSupport(pNtk, iLit) ) pTruthFans[i] = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp, iVar, pTruthDec ); else - pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 ); + pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 ); } // create composition/decomposition functions @@ -556,7 +695,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk // solve the fanins and collect info, which components belong to the bound set Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) { - pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 ); + pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 ); pfBoundSet[i] = (int)((uSupp & Kit_DsdLitSupport(pNtk, iLit)) > 0); } @@ -603,7 +742,7 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk // set the corresponding component to be the new variable Kit_TruthIthVar( pTruthFans[i], pNtk->nVars, iVar ); } - +/* // get the truth table of the prime node pTruthPrime = Kit_DsdObjTruth( pObj ); // get storage for the temporary minterm @@ -621,6 +760,11 @@ unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<nVars ); } +*/ + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + assert( !Kit_DsdLitIsCompl(iLit) ); + pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes ); + Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars ); return pTruthRes; } @@ -647,12 +791,12 @@ unsigned * Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsign if ( (uSupp & uSuppAll) == 0 ) { Kit_TruthClear( pTruthDec, pNtk->nVars ); - return Kit_DsdTruthCompute( p, pNtk, 0 ); + return Kit_DsdTruthCompute( p, pNtk ); } // consider special case - support is fully contained if ( (uSupp & uSuppAll) == uSuppAll ) { - pTruthRes = Kit_DsdTruthCompute( p, pNtk, 0 ); + pTruthRes = Kit_DsdTruthCompute( p, pNtk ); Kit_TruthCopy( pTruthDec, pTruthRes, pNtk->nVars ); Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar ); return pTruthRes; @@ -684,7 +828,7 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes ) Kit_DsdMan_t * p; unsigned * pTruth; p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) ); - pTruth = Kit_DsdTruthCompute( p, pNtk, 0 ); + pTruth = Kit_DsdTruthCompute( p, pNtk ); Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars ); Kit_DsdManFree( p ); } @@ -720,7 +864,7 @@ void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSu ***********************************************************************/ void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp ) { - unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp ); + unsigned * pTruth = Kit_DsdTruthComputeOne( p, pNtk, uSupp ); Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars ); /* // verification @@ -836,6 +980,32 @@ int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk ) return nSizeMax; } +/**Function************************************************************* + + Synopsis [Finds the union of supports of the non-DSD blocks.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk ) +{ + Kit_DsdObj_t * pObj; + unsigned i, uSupport = 0; +// FREE( pNtk->pSupps ); + Kit_DsdGetSupports( pNtk ); + Kit_DsdNtkForEachObj( pNtk, pObj, i ) + { + if ( pObj->Type != KIT_DSD_PRIME ) + continue; + uSupport |= Kit_DsdLitSupport( pNtk, Kit_DsdVar2Lit(pObj->Id,0) ); + } + return uSupport; +} + /**Function************************************************************* @@ -1755,6 +1925,26 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars ) return Kit_DsdDecomposeInt( pTruth, nVars, 0 ); } +/**Function************************************************************* + + Synopsis [Performs decomposition of the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Kit_DsdNtk_t * Kit_DsdDecomposeExpand( unsigned * pTruth, int nVars ) +{ + Kit_DsdNtk_t * pNtk, * pTemp; + pNtk = Kit_DsdDecomposeInt( pTruth, nVars, 0 ); + pNtk = Kit_DsdExpand( pTemp = pNtk ); + Kit_DsdNtkFree( pTemp ); + return pNtk; +} + /**Function************************************************************* Synopsis [Performs decomposition of the truth table.] @@ -1867,7 +2057,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize ) // recompute the truth table p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) ); - pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 ); + pTruthC = Kit_DsdTruthCompute( p, pNtk ); if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) printf( "Verification failed.\n" ); Kit_DsdManFree( p ); @@ -1892,7 +2082,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars ) Kit_DsdMan_t * p; unsigned * pTruthC; p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 ); - pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 ); + pTruthC = Kit_DsdTruthCompute( p, pNtk ); if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) printf( "Verification failed.\n" ); Kit_DsdManFree( p ); @@ -1934,7 +2124,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars ) // recompute the truth table p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) ); - pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 ); + pTruthC = Kit_DsdTruthCompute( p, pNtk ); // Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" ); // Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" ); if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) @@ -2004,7 +2194,7 @@ void Kit_DsdPrecompute4Vars() */ p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) ); - pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 ); + pTruthC = Kit_DsdTruthCompute( p, pNtk ); if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) ) printf( "Verification failed.\n" ); Kit_DsdManFree( p ); diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c index d196b455..65389ef9 100644 --- a/src/aig/kit/kitTruth.c +++ b/src/aig/kit/kitTruth.c @@ -899,6 +899,68 @@ void Kit_TruthMuxVar( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int n } } +/**Function************************************************************* + + Synopsis [Multiplexes two functions with the given variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_TruthMuxVarPhase( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar, int fCompl0 ) +{ + int nWords = Kit_TruthWordNum( nVars ); + int i, k, Step; + + if ( fCompl0 == 0 ) + { + Kit_TruthMuxVar( pOut, pCof0, pCof1, nVars, iVar ); + return; + } + + assert( iVar < nVars ); + switch ( iVar ) + { + case 0: + for ( i = 0; i < nWords; i++ ) + pOut[i] = (~pCof0[i] & 0x55555555) | (pCof1[i] & 0xAAAAAAAA); + return; + case 1: + for ( i = 0; i < nWords; i++ ) + pOut[i] = (~pCof0[i] & 0x33333333) | (pCof1[i] & 0xCCCCCCCC); + return; + case 2: + for ( i = 0; i < nWords; i++ ) + pOut[i] = (~pCof0[i] & 0x0F0F0F0F) | (pCof1[i] & 0xF0F0F0F0); + return; + case 3: + for ( i = 0; i < nWords; i++ ) + pOut[i] = (~pCof0[i] & 0x00FF00FF) | (pCof1[i] & 0xFF00FF00); + return; + case 4: + for ( i = 0; i < nWords; i++ ) + pOut[i] = (~pCof0[i] & 0x0000FFFF) | (pCof1[i] & 0xFFFF0000); + return; + default: + Step = (1 << (iVar - 5)); + for ( k = 0; k < nWords; k += 2*Step ) + { + for ( i = 0; i < Step; i++ ) + { + pOut[i] = ~pCof0[i]; + pOut[Step+i] = pCof1[Step+i]; + } + pOut += 2*Step; + pCof0 += 2*Step; + pCof1 += 2*Step; + } + return; + } +} + /**Function************************************************************* Synopsis [Checks symmetry of two variables.] @@ -1623,7 +1685,7 @@ char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile ) { static char pFileName[100]; FILE * pFile; - sprintf( pFileName, "s%03d", nFile ); + sprintf( pFileName, "tt\\s%04d", nFile ); pFile = fopen( pFileName, "w" ); fprintf( pFile, "rt " ); Extra_PrintHexadecimal( pFile, pTruth, nVars ); diff --git a/src/aig/kit/module.make b/src/aig/kit/module.make index a01690d0..25c8e767 100644 --- a/src/aig/kit/module.make +++ b/src/aig/kit/module.make @@ -1,4 +1,5 @@ SRC += src/aig/kit/kitBdd.c \ + src/aig/kit/kitCloud.c src/aig/kit/cloud.c \ src/aig/kit/kitDsd.c \ src/aig/kit/kitFactor.c \ src/aig/kit/kitGraph.c \ diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index d30198c1..604c5ffa 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -45,8 +45,8 @@ static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ); int Abc_NodeMffcSize( Abc_Obj_t * pNode ) { int nConeSize1, nConeSize2; - assert( Abc_NtkIsStrash(pNode->pNtk) ); - assert( !Abc_ObjIsComplement( pNode ) ); +// assert( Abc_NtkIsStrash(pNode->pNtk) ); +// assert( !Abc_ObjIsComplement( pNode ) ); assert( Abc_ObjIsNode( pNode ) ); if ( Abc_ObjFaninNum(pNode) == 0 ) return 0; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 22a8ad54..a8888d81 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2979,22 +2979,20 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); -// printf("This command will be available soon\n"); -// return 0; - // set defaults memset( pPars, 0, sizeof(Lpk_Par_t) ); pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars) - pPars->nGrowthLevel = 1; // (L) the maximum number of increased levels + pPars->nGrowthLevel = 0; // (L) the maximum number of increased levels pPars->fSatur = 1; pPars->fZeroCost = 0; pPars->fFirst = 0; + pPars->fOldAlgo = 0; pPars->fVerbose = 0; pPars->fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfovwh" ) ) != EOF ) { switch ( c ) { @@ -3051,6 +3049,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': pPars->fFirst ^= 1; break; + case 'o': + pPars->fOldAlgo ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -3074,6 +3075,11 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "This command can only be applied to a logic network.\n" ); return 1; } + if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 3 ) + { + fprintf( pErr, "The number of shared variables (%d) is not in the range 0 <= S <= 3.\n", pPars->nVarsShared ); + return 1; + } // modify the current network if ( !Lpk_Resynthesize( pNtk, pPars ) ) @@ -3084,17 +3090,18 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: lutpack [-N ] [-Q ] [-S ] [-L ] [-szfvwh]\n" ); + fprintf( pErr, "usage: lutpack [-N ] [-Q ] [-S ] [-L ] [-szfovwh]\n" ); fprintf( pErr, "\t performs \"rewriting\" for LUT networks\n" ); fprintf( pErr, "\t-N : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax ); fprintf( pErr, "\t-Q : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver ); - fprintf( pErr, "\t-S : the max number of LUT inputs shared (0 <= num) [default = %d]\n", pPars->nVarsShared ); + fprintf( pErr, "\t-S : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared ); fprintf( pErr, "\t-L : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel ); fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" ); fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" ); fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" ); + fprintf( pErr, "\t-o : toggle using old implementation [default = %s]\n", pPars->fOldAlgo? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); - fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggle detailed printout of decomposed functions [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index ecf29f32..47367bc6 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -412,7 +412,7 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry ) SeeAlso [] ******************************************************************************/ -static inline Vec_StrBase10Log( unsigned Num ) +static inline int Vec_StrBase10Log( unsigned Num ) { int Res; assert( Num >= 0 ); diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h index f1dcd528..2a642db2 100644 --- a/src/opt/lpk/lpk.h +++ b/src/opt/lpk/lpk.h @@ -48,6 +48,7 @@ struct Lpk_Par_t_ int fSatur; // iterate till saturation int fZeroCost; // accept zero-cost replacements int fFirst; // use root node and first cut only + int fOldAlgo; // use old algorithm int fVerbose; // the verbosiness flag int fVeryVerbose; // additional verbose info printout // internal parameters diff --git a/src/opt/lpk/lpkAbcDec.c b/src/opt/lpk/lpkAbcDec.c index e9f8d0df..aa2d4bc0 100644 --- a/src/opt/lpk/lpkAbcDec.c +++ b/src/opt/lpk/lpkAbcDec.c @@ -39,17 +39,21 @@ SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Lpk_ImplementFun( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p ) +Abc_Obj_t * Lpk_ImplementFun( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p ) { extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory ); unsigned * pTruth; Abc_Obj_t * pObjNew; int i; + if ( p->fMark ) + pMan->nMuxes++; + else + pMan->nDsds++; // create the new node pObjNew = Abc_NtkCreateNode( pNtk ); for ( i = 0; i < (int)p->nVars; i++ ) - Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) ); - Abc_ObjLevelNew( pObjNew ); + Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(Vec_PtrEntry(vLeaves, p->pFanins[i])) ); + Abc_ObjSetLevel( pObjNew, Abc_ObjLevelNew(pObjNew) ); // assign the node's function pTruth = Lpk_FunTruth(p, 0); if ( p->nVars == 0 ) @@ -78,18 +82,48 @@ Abc_Obj_t * Lpk_ImplementFun( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld ) +Abc_Obj_t * Lpk_Implement_rec( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * pFun ) { - Lpk_Fun_t * pFun; - Abc_Obj_t * pRes; + Abc_Obj_t * pFanin, * pRes; int i; - for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeavesOld; i-- ) + // prepare the leaves of the function + for ( i = 0; i < (int)pFun->nVars; i++ ) { - pFun = Vec_PtrEntry( vLeaves, i ); - pRes = Lpk_ImplementFun( pNtk, vLeaves, pFun ); - Vec_PtrWriteEntry( vLeaves, i, pRes ); - Lpk_FunFree( pFun ); + pFanin = Vec_PtrEntry( vLeaves, pFun->pFanins[i] ); + if ( !Abc_ObjIsComplement(pFanin) ) + Lpk_Implement_rec( pMan, pNtk, vLeaves, (Lpk_Fun_t *)pFanin ); + pFanin = Vec_PtrEntry( vLeaves, pFun->pFanins[i] ); + assert( Abc_ObjIsComplement(pFanin) ); } + // construct the function + pRes = Lpk_ImplementFun( pMan, pNtk, vLeaves, pFun ); + // replace the function + Vec_PtrWriteEntry( vLeaves, pFun->Id, Abc_ObjNot(pRes) ); + Lpk_FunFree( pFun ); + return pRes; +} + +/**Function************************************************************* + + Synopsis [Implements the function.] + + Description [Returns the node implementing this function.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Lpk_Implement( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld ) +{ + Abc_Obj_t * pFanin, * pRes; + int i; + assert( nLeavesOld < Vec_PtrSize(vLeaves) ); + // mark implemented nodes + Vec_PtrForEachEntryStop( vLeaves, pFanin, i, nLeavesOld ) + Vec_PtrWriteEntry( vLeaves, i, Abc_ObjNot(pFanin) ); + // recursively construct starting from the first entry + pRes = Lpk_Implement_rec( pMan, pNtk, vLeaves, Vec_PtrEntry( vLeaves, nLeavesOld ) ); Vec_PtrShrink( vLeaves, nLeavesOld ); return pRes; } @@ -107,10 +141,13 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld SeeAlso [] ***********************************************************************/ -int Lpk_Decompose_rec( Lpk_Fun_t * p ) +int Lpk_Decompose_rec( Lpk_Man_t * pMan, Lpk_Fun_t * p ) { + static Lpk_Res_t Res0, * pRes0 = &Res0; Lpk_Res_t * pResMux, * pResDsd; Lpk_Fun_t * p2; + int clk; + // is only called for non-trivial blocks assert( p->nLutK >= 3 && p->nLutK <= 6 ); assert( p->nVars > p->nLutK ); @@ -120,18 +157,37 @@ int Lpk_Decompose_rec( Lpk_Fun_t * p ) // skip if delay bound is exceeded if ( Lpk_SuppDelay(p->uSupp, p->pDelays) > (int)p->nDelayLim ) return 0; + + // compute supports if needed + if ( !p->fSupports ) + Lpk_FunComputeCofSupps( p ); + + // check DSD decomposition +clk = clock(); + pResDsd = Lpk_DsdAnalize( pMan, p, pMan->pPars->nVarsShared ); +pMan->timeEvalDsdAn += clock() - clk; + if ( pResDsd && (pResDsd->nBSVars == (int)p->nLutK || pResDsd->nBSVars == (int)p->nLutK - 1) && + pResDsd->AreaEst <= (int)p->nAreaLim && pResDsd->DelayEst <= (int)p->nDelayLim ) + { +clk = clock(); + p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars ); +pMan->timeEvalDsdSp += clock() - clk; + assert( p2->nVars <= (int)p->nLutK ); + if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) ) + return 0; + return 1; + } + // check MUX decomposition - pResMux = Lpk_MuxAnalize( p ); +clk = clock(); + pResMux = Lpk_MuxAnalize( pMan, p ); +pMan->timeEvalMuxAn += clock() - clk; +// pResMux = NULL; assert( !pResMux || (pResMux->DelayEst <= (int)p->nDelayLim && pResMux->AreaEst <= (int)p->nAreaLim) ); // accept MUX decomposition if it is "good" if ( pResMux && pResMux->nSuppSizeS <= (int)p->nLutK && pResMux->nSuppSizeL <= (int)p->nLutK ) pResDsd = NULL; - else - { - pResDsd = Lpk_DsdAnalize( p ); - assert( !pResDsd || (pResDsd->DelayEst <= (int)p->nDelayLim && pResDsd->AreaEst <= (int)p->nAreaLim) ); - } - if ( pResMux && pResDsd ) + else if ( pResMux && pResDsd ) { // compare two decompositions if ( pResMux->AreaEst < pResDsd->AreaEst || @@ -144,18 +200,22 @@ int Lpk_Decompose_rec( Lpk_Fun_t * p ) assert( pResMux == NULL || pResDsd == NULL ); if ( pResMux ) { - p2 = Lpk_MuxSplit( p, pResMux->pCofVars[0], pResMux->Polarity ); - if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( p2 ) ) +clk = clock(); + p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity ); +pMan->timeEvalMuxSp += clock() - clk; + if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p2 ) ) return 0; - if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) ) + if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) ) return 0; return 1; } if ( pResDsd ) { - p2 = Lpk_DsdSplit( p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars ); +clk = clock(); + p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars ); +pMan->timeEvalDsdSp += clock() - clk; assert( p2->nVars <= (int)p->nLutK ); - if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) ) + if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) ) return 0; return 1; } @@ -193,17 +253,31 @@ void Lpk_DecomposeClean( Vec_Ptr_t * vLeaves, int nLeavesOld ) SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ) +Abc_Obj_t * Lpk_Decompose( Lpk_Man_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, unsigned * puSupps, int nLutK, int AreaLim, int DelayLim ) { Lpk_Fun_t * pFun; Abc_Obj_t * pObjNew = NULL; int nLeaves = Vec_PtrSize( vLeaves ); pFun = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim ); + if ( puSupps[0] || puSupps[1] ) + { +/* + int i; + Lpk_FunComputeCofSupps( pFun ); + for ( i = 0; i < nLeaves; i++ ) + { + assert( pFun->puSupps[2*i+0] == puSupps[2*i+0] ); + assert( pFun->puSupps[2*i+1] == puSupps[2*i+1] ); + } +*/ + memcpy( pFun->puSupps, puSupps, sizeof(unsigned) * 2 * nLeaves ); + pFun->fSupports = 1; + } Lpk_FunSuppMinimize( pFun ); if ( pFun->nVars <= pFun->nLutK ) - pObjNew = Lpk_ImplementFun( pNtk, vLeaves, pFun ); - else if ( Lpk_Decompose_rec(pFun) ) - pObjNew = Lpk_Implement( pNtk, vLeaves, nLeaves ); + pObjNew = Lpk_ImplementFun( p, pNtk, vLeaves, pFun ); + else if ( Lpk_Decompose_rec(p, pFun) ) + pObjNew = Lpk_Implement( p, pNtk, vLeaves, nLeaves ); Lpk_DecomposeClean( vLeaves, nLeaves ); return pObjNew; } diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c index f2e19945..f4095914 100644 --- a/src/opt/lpk/lpkAbcDsd.c +++ b/src/opt/lpk/lpkAbcDsd.c @@ -41,27 +41,37 @@ SeeAlso [] ***********************************************************************/ -int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs ) +int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs, unsigned uNonDecSupp ) { int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur; assert( nTruths > 0 ); VarBest = -1; Lpk_SuppForEachVar( p->uSupp, Var ) { + if ( (uNonDecSupp & (1 << Var)) == 0 ) + continue; nSuppMaxCur = 0; nSuppTotalCur = 0; for ( i = 0; i < nTruths; i++ ) { - Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var ); - Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var ); - nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars ); - nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars ); + if ( nTruths == 1 ) + { + nSuppSize0 = Kit_WordCountOnes( p->puSupps[2*Var+0] ); + nSuppSize1 = Kit_WordCountOnes( p->puSupps[2*Var+1] ); + } + else + { + Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var ); + Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var ); + nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars ); + nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars ); + } nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 ); nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 ); nSuppTotalCur += nSuppSize0 + nSuppSize1; } - if ( VarBest == -1 || nSuppTotalMin > nSuppTotalCur || - (nSuppTotalMin == nSuppTotalCur && nSuppMaxMin > nSuppMaxCur) ) + if ( VarBest == -1 || nSuppMaxMin > nSuppMaxCur || + (nSuppMaxMin == nSuppMaxCur && nSuppTotalMin > nSuppTotalCur) ) { VarBest = Var; nSuppMaxMin = nSuppMaxCur; @@ -173,6 +183,49 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax ) return vSets; } +/**Function************************************************************* + + Synopsis [Prints the sets of subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Lpk_PrintSetOne( int uSupport ) +{ + unsigned k; + for ( k = 0; k < 16; k++ ) + if ( uSupport & (1<> 16)) ) continue; - if ( Kit_WordCountOnes(Entry) <= nSizeMax ) + if ( Kit_WordCountOnes(Entry & 0xffff) <= nSizeMax ) Vec_IntPush( vSets, Entry ); } return vSets; @@ -204,7 +257,7 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSiz /**Function************************************************************* - Synopsis [Allocates truth tables for cofactors.] + Synopsis [Performs DSD-based decomposition of the function.] Description [] @@ -213,39 +266,69 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSiz SeeAlso [] ***********************************************************************/ -void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] ) +void Lpk_FunCompareBoundSets( Lpk_Fun_t * p, Vec_Int_t * vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t * pRes ) { - int i; - assert( nCofDepth <= 4 ); - ppTruths[0][0] = Lpk_FunTruth( p, 0 ); - if ( nCofDepth >= 1 ) - { - ppTruths[1][0] = Lpk_FunTruth( p, 1 ); - ppTruths[1][1] = Lpk_FunTruth( p, 2 ); - } - if ( nCofDepth >= 2 ) - { - ppTruths[2][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 4 ); - for ( i = 1; i < 4; i++ ) - ppTruths[2][i] = ppTruths[2][0] + Kit_TruthWordNum(p->nVars) * i; - } - if ( nCofDepth >= 3 ) + int fVerbose = 0; + unsigned uBoundSet; + int i, nVarsBS, nVarsRem, Delay, Area; + + // compare the resulting boundsets + memset( pRes, 0, sizeof(Lpk_Res_t) ); + Vec_IntForEachEntry( vBSets, uBoundSet, i ) { - ppTruths[3][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 8 ); - for ( i = 1; i < 8; i++ ) - ppTruths[3][i] = ppTruths[3][0] + Kit_TruthWordNum(p->nVars) * i; + if ( (uBoundSet & 0xFFFF) == 0 ) // skip empty boundset + continue; + if ( (uBoundSet & uNonDecSupp) == 0 ) // skip those boundsets that are not in the domain of interest + continue; + if ( (uBoundSet & uLateArrSupp) ) // skip those boundsets that are late arriving + continue; +if ( fVerbose ) +Lpk_PrintSetOne( uBoundSet ); + assert( (uBoundSet & (uBoundSet >> 16)) == 0 ); + nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF ); + if ( nVarsBS == 1 ) + continue; + assert( nVarsBS <= (int)p->nLutK - nCofDepth ); + nVarsRem = p->nVars - nVarsBS + 1; + Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK ); + Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays ); +if ( fVerbose ) +printf( "area = %d limit = %d delay = %d limit = %d\n", Area, (int)p->nAreaLim, Delay, (int)p->nDelayLim ); + if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim ) + continue; + if ( pRes->BSVars == 0 || pRes->nSuppSizeL > nVarsRem || (pRes->nSuppSizeL == nVarsRem && pRes->DelayEst > Delay) ) + { + pRes->nBSVars = nVarsBS; + pRes->BSVars = (uBoundSet & 0xFFFF); + pRes->nSuppSizeS = nVarsBS + nCofDepth; + pRes->nSuppSizeL = nVarsRem; + pRes->DelayEst = Delay; + pRes->AreaEst = Area; + } } - if ( nCofDepth >= 4 ) +if ( fVerbose ) +{ +if ( pRes->BSVars ) +{ +printf( "Found bound set " ); +Lpk_PrintSetOne( pRes->BSVars ); +printf( "\n" ); +} +else +printf( "Did not find boundsets.\n" ); +printf( "\n" ); +} + if ( pRes->BSVars ) { - ppTruths[4][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 16 ); - for ( i = 1; i < 16; i++ ) - ppTruths[4][i] = ppTruths[4][0] + Kit_TruthWordNum(p->nVars) * i; + assert( pRes->DelayEst <= (int)p->nDelayLim ); + assert( pRes->AreaEst <= (int)p->nAreaLim ); } } + /**Function************************************************************* - Synopsis [Allocates truth tables for cofactors.] + Synopsis [Finds late arriving inputs, which cannot be in the bound set.] Description [] @@ -254,14 +337,13 @@ void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[ SeeAlso [] ***********************************************************************/ -void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] ) +unsigned Lpk_DsdLateArriving( Lpk_Fun_t * p ) { - if ( nCofDepth >= 2 ) - free( ppTruths[2][0] ); - if ( nCofDepth >= 3 ) - free( ppTruths[3][0] ); - if ( nCofDepth >= 4 ) - free( ppTruths[4][0] ); + unsigned i, uLateArrSupp = 0; + Lpk_SuppForEachVar( p->uSupp, i ) + if ( p->pDelays[i] > (int)p->nDelayLim - 2 ) + uLateArrSupp |= (1 << i); + return uLateArrSupp; } /**Function************************************************************* @@ -275,58 +357,73 @@ void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5 SeeAlso [] ***********************************************************************/ -void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes ) +int Lpk_DsdAnalizeOne( Lpk_Fun_t * p, unsigned * ppTruths[5][16], Kit_DsdNtk_t * pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t * pRes ) { - unsigned * ppTruths[5][16]; + int fVerbose = 0; Vec_Int_t * pvBSets[4][8]; - Kit_DsdNtk_t * pNtkDec, * pTemp; - unsigned uBoundSet; - int i, k, nVarsBS, nVarsRem, Delay, Area; - assert( nCofDepth >= 0 && nCofDepth < 4 ); + unsigned uNonDecSupp, uLateArrSupp; + int i, k, nNonDecSize, nNonDecSizeMax; + assert( nCofDepth >= 1 && nCofDepth <= 3 ); assert( nCofDepth < (int)p->nLutK - 1 ); - Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths ); - // find the best cofactors - memset( pRes, 0, sizeof(Lpk_Res_t) ); - pRes->nCofVars = nCofDepth; - for ( i = 0; i < nCofDepth; i++ ) - pRes->pCofVars[i] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[i], 1<fSupports ); + + // find the support of the largest non-DSD block + nNonDecSizeMax = 0; + uNonDecSupp = p->uSupp; + for ( i = 0; i < (1<<(nCofDepth-1)); i++ ) + { + nNonDecSize = Kit_DsdNonDsdSizeMax( pNtks[i] ); + if ( nNonDecSizeMax < nNonDecSize ) + { + nNonDecSizeMax = nNonDecSize; + uNonDecSupp = Kit_DsdNonDsdSupports( pNtks[i] ); + } + else if ( nNonDecSizeMax == nNonDecSize ) + uNonDecSupp |= Kit_DsdNonDsdSupports( pNtks[i] ); + } + + // remove those variables that cannot be used because of delay constraints + // if variables arrival time is more than p->DelayLim - 2, it cannot be used + uLateArrSupp = Lpk_DsdLateArriving( p ); + if ( (uNonDecSupp & ~uLateArrSupp) == 0 ) + { + memset( pRes, 0, sizeof(Lpk_Res_t) ); + return 0; + } + + // find the next cofactoring variable + pCofVars[nCofDepth-1] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[nCofDepth-1], 1<<(nCofDepth-1), ppTruths[nCofDepth], uNonDecSupp & ~uLateArrSupp ); + // derive decomposed networks for ( i = 0; i < (1<nVars ); - pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp ); - pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtkDec, p->nLutK - nCofDepth ); - Kit_DsdNtkFree( pNtkDec ); + if ( pNtks[i] ) + Kit_DsdNtkFree( pNtks[i] ); + pNtks[i] = Kit_DsdDecomposeExpand( ppTruths[nCofDepth][i], p->nVars ); +if ( fVerbose ) +Kit_DsdPrint( stdout, pNtks[i] ); + pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtks[i], p->nLutK - nCofDepth ); // try restricting to those in uNonDecSupp!!! } + // derive the set of feasible boundsets for ( i = nCofDepth - 1; i >= 0; i-- ) for ( k = 0; k < (1<nLutK - nCofDepth ); - // compare the resulting boundsets - Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i ) + // compare bound-sets + Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes ); + // free the bound sets + for ( i = nCofDepth; i >= 0; i-- ) + for ( k = 0; k < (1<BSVars ) { - if ( uBoundSet == 0 ) - continue; - assert( (uBoundSet & (uBoundSet >> 16)) == 0 ); - nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF ); - assert( nVarsBS <= (int)p->nLutK - nCofDepth ); - nVarsRem = p->nVars - nVarsBS + nCofDepth + 1; - Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK ); - Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays ); - if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim ) - continue; - if ( pRes->BSVars == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem ) - { - pRes->nBSVars = nVarsBS; - pRes->BSVars = uBoundSet; - pRes->nSuppSizeS = nVarsBS; - pRes->nSuppSizeL = nVarsRem; - pRes->DelayEst = Delay; - pRes->AreaEst = Area; - } + pRes->nCofVars = nCofDepth; + for ( i = 0; i < nCofDepth; i++ ) + pRes->pCofVars[i] = pCofVars[i]; } - // free cofactor storage - Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths ); + return 1; } /**Function************************************************************* @@ -340,47 +437,105 @@ void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes ) SeeAlso [] ***********************************************************************/ -Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p ) -{ +Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared ) +{ static Lpk_Res_t Res0, * pRes0 = &Res0; static Lpk_Res_t Res1, * pRes1 = &Res1; static Lpk_Res_t Res2, * pRes2 = &Res2; static Lpk_Res_t Res3, * pRes3 = &Res3; - memset( pRes0, 0, sizeof(Lpk_Res_t) ); - memset( pRes1, 0, sizeof(Lpk_Res_t) ); - memset( pRes2, 0, sizeof(Lpk_Res_t) ); - memset( pRes3, 0, sizeof(Lpk_Res_t) ); + int fUseBackLooking = 1; + Lpk_Res_t * pRes = NULL; + Vec_Int_t * vBSets; + Kit_DsdNtk_t * pNtks[8] = {NULL}; + char pCofVars[5]; + int i; + + assert( p->nLutK >= 3 ); + assert( nShared >= 0 && nShared <= 3 ); assert( p->uSupp == Kit_BitMask(p->nVars) ); // try decomposition without cofactoring - Lpk_DsdAnalizeOne( p, 0, pRes0 ); - if ( pRes0->nBSVars == (int)p->nLutK && pRes0->AreaEst <= (int)p->nAreaLim && pRes0->DelayEst <= (int)p->nDelayLim ) - return pRes0; + pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars ); + if ( pMan->pPars->fVerbose ) + pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++; + vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK ); + Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 ); + Vec_IntFree( vBSets ); + + // check the result + if ( pRes0->nBSVars == (int)p->nLutK ) + { pRes = pRes0; goto finish; } + if ( pRes0->nBSVars == (int)p->nLutK - 1 ) + { pRes = pRes0; goto finish; } + if ( nShared == 0 ) + goto finish; + + // prepare storage + Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars ); // cofactor 1 time - if ( p->nLutK >= 3 ) - Lpk_DsdAnalizeOne( p, 1, pRes1 ); + if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) ) + goto finish; assert( pRes1->nBSVars <= (int)p->nLutK - 1 ); - if ( pRes1->nBSVars == (int)p->nLutK - 1 && pRes1->AreaEst <= (int)p->nAreaLim && pRes1->DelayEst <= (int)p->nDelayLim ) - return pRes1; + if ( pRes1->nBSVars == (int)p->nLutK - 1 ) + { pRes = pRes1; goto finish; } + if ( pRes0->nBSVars == (int)p->nLutK - 2 ) + { pRes = pRes0; goto finish; } + if ( pRes1->nBSVars == (int)p->nLutK - 2 ) + { pRes = pRes1; goto finish; } + if ( nShared == 1 ) + goto finish; // cofactor 2 times if ( p->nLutK >= 4 ) - Lpk_DsdAnalizeOne( p, 2, pRes2 ); - assert( pRes2->nBSVars <= (int)p->nLutK - 2 ); - if ( pRes2->nBSVars == (int)p->nLutK - 2 && pRes2->AreaEst <= (int)p->nAreaLim && pRes2->DelayEst <= (int)p->nDelayLim ) - return pRes2; + { + if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) ) + goto finish; + assert( pRes2->nBSVars <= (int)p->nLutK - 2 ); + if ( pRes2->nBSVars == (int)p->nLutK - 2 ) + { pRes = pRes2; goto finish; } + if ( fUseBackLooking ) + { + if ( pRes0->nBSVars == (int)p->nLutK - 3 ) + { pRes = pRes0; goto finish; } + if ( pRes1->nBSVars == (int)p->nLutK - 3 ) + { pRes = pRes1; goto finish; } + } + if ( pRes2->nBSVars == (int)p->nLutK - 3 ) + { pRes = pRes2; goto finish; } + if ( nShared == 2 ) + goto finish; + assert( nShared == 3 ); + } // cofactor 3 times if ( p->nLutK >= 5 ) - Lpk_DsdAnalizeOne( p, 3, pRes3 ); - assert( pRes3->nBSVars <= (int)p->nLutK - 3 ); - if ( pRes3->nBSVars == (int)p->nLutK - 3 && pRes3->AreaEst <= (int)p->nAreaLim && pRes3->DelayEst <= (int)p->nDelayLim ) - return pRes3; + { + if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) ) + goto finish; + assert( pRes3->nBSVars <= (int)p->nLutK - 3 ); + if ( pRes3->nBSVars == (int)p->nLutK - 3 ) + { pRes = pRes3; goto finish; } + if ( fUseBackLooking ) + { + if ( pRes0->nBSVars == (int)p->nLutK - 4 ) + { pRes = pRes0; goto finish; } + if ( pRes1->nBSVars == (int)p->nLutK - 4 ) + { pRes = pRes1; goto finish; } + if ( pRes2->nBSVars == (int)p->nLutK - 4 ) + { pRes = pRes2; goto finish; } + } + if ( pRes3->nBSVars == (int)p->nLutK - 4 ) + { pRes = pRes3; goto finish; } + } +finish: + // free the networks + for ( i = 0; i < (1<ppTruths[0][0], Lpk_FunTruth(p, 0), p->nVars ); // get the vacuous variable - iVacVar = pBSVars[0]; + iVacVar = Kit_WordFindFirstBit( uBoundSet ); // compute the cofactors - Lpk_FunAllocTruthTables( p, nCofVars + 1, ppTruths ); for ( i = 0; i < nCofVars; i++ ) for ( k = 0; k < (1<nVars, pCofVars[i] ); - Kit_TruthCofactor1New( ppTruths[i+1][2*k+1], ppTruths[i][k], p->nVars, pCofVars[i] ); + Kit_TruthCofactor0New( pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i][k], p->nVars, pCofVars[i] ); + Kit_TruthCofactor1New( pMan->ppTruths[i+1][2*k+1], pMan->ppTruths[i][k], p->nVars, pCofVars[i] ); } // decompose each cofactor w.r.t. the bound set nCofs = (1<nVars, p->nVars * 2 ); for ( k = 0; k < nCofs; k++ ) { - pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars ); - pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp ); - Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, iVacVar, ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] ); + pNtkDec = Kit_DsdDecomposeExpand( pMan->ppTruths[nCofVars][k], p->nVars ); + Kit_DsdTruthPartialTwo( pMan->pDsdMan, pNtkDec, uBoundSet, iVacVar, pMan->ppTruths[nCofVars+1][k], pMan->ppTruths[nCofVars+1][nCofs+k] ); Kit_DsdNtkFree( pNtkDec ); } - Kit_DsdManFree( pDsdMan ); - // compute the composition/decomposition functions (they will be in pTruth0/pTruth1) + // compute the composition/decomposition functions (they will be in pMan->ppTruths[1][0]/pMan->ppTruths[1][1]) for ( i = nCofVars; i >= 1; i-- ) for ( k = 0; k < (1<ppTruths[i][k], pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i+1][2*k+1], p->nVars, pCofVars[i-1] ); - // derive the new component - pNew = Lpk_FunDup( p, pTruth1 ); - // update the old component - Kit_TruthCopy( pTruth, pTruth0, p->nVars ); - p->uSupp = Kit_TruthSupport( pTruth0, p->nVars ); + // derive the new component (decomposition function) + pNew = Lpk_FunDup( p, pMan->ppTruths[1][1] ); + // update the old component (composition function) + Kit_TruthCopy( Lpk_FunTruth(p, 0), pMan->ppTruths[1][0], p->nVars ); + p->uSupp = Kit_TruthSupport( Lpk_FunTruth(p, 0), p->nVars ); p->pFanins[iVacVar] = pNew->Id; p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays ); // support minimize both + p->fSupports = 0; Lpk_FunSuppMinimize( p ); Lpk_FunSuppMinimize( pNew ); // update delay and area requirements pNew->nDelayLim = p->pDelays[iVacVar]; pNew->nAreaLim = 1; p->nAreaLim = p->nAreaLim - 1; - - // free cofactor storage - Lpk_FunFreeTruthTables( p, nCofVars + 1, ppTruths ); return pNew; } diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c index 159cae96..d6f579ee 100644 --- a/src/opt/lpk/lpkAbcMux.c +++ b/src/opt/lpk/lpkAbcMux.c @@ -28,51 +28,6 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [Computes cofactors w.r.t. the given var.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Lpk_FunComputeCofs( Lpk_Fun_t * p, int iVar ) -{ - unsigned * pTruth = Lpk_FunTruth( p, 0 ); - unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); - unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); - Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, iVar ); - Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, iVar ); -} - -/**Function************************************************************* - - Synopsis [Computes cofactors w.r.t. each variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps ) -{ - unsigned * pTruth = Lpk_FunTruth( p, 0 ); - unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); - unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); - int Var; - Lpk_SuppForEachVar( p->uSupp, Var ) - { - Lpk_FunComputeCofs( p, Var ); - puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars ); - puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars ); - } -} - /**Function************************************************************* Synopsis [Checks the possibility of MUX decomposition.] @@ -84,65 +39,68 @@ void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps ) SeeAlso [] ***********************************************************************/ -Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p ) +Lpk_Res_t * Lpk_MuxAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p ) { static Lpk_Res_t Res, * pRes = &Res; - unsigned puSupps[32]; - int nSuppSize0, nSuppSize1, nSuppSizeBest; + int nSuppSize0, nSuppSize1, nSuppSizeS, nSuppSizeL; int Var, Area, Polarity, Delay, Delay0, Delay1, DelayA, DelayB; memset( pRes, 0, sizeof(Lpk_Res_t) ); assert( p->uSupp == Kit_BitMask(p->nVars) ); - // get cofactor supports for each variable - Lpk_FunComputeCofSupps( p, puSupps ); + assert( p->fSupports ); // derive the delay and area after MUX-decomp with each var - and find the best var pRes->Variable = -1; Lpk_SuppForEachVar( p->uSupp, Var ) { - nSuppSize0 = Kit_WordCountOnes(puSupps[2*Var+0]); - nSuppSize1 = Kit_WordCountOnes(puSupps[2*Var+1]); + nSuppSize0 = Kit_WordCountOnes(p->puSupps[2*Var+0]); + nSuppSize1 = Kit_WordCountOnes(p->puSupps[2*Var+1]); + assert( nSuppSize0 < (int)p->nVars ); + assert( nSuppSize1 < (int)p->nVars ); + if ( nSuppSize0 < 1 || nSuppSize1 < 1 ) + continue; +//printf( "%d %d ", nSuppSize0, nSuppSize1 ); if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 ) { // include cof var into 0-block - DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<pDelays ); - DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays ); + DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<pDelays ); + DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1] , p->pDelays ); Delay0 = ABC_MAX( DelayA, DelayB + 1 ); // include cof var into 1-block - DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<pDelays ); - DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); + DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<pDelays ); + DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0] , p->pDelays ); Delay1 = ABC_MAX( DelayA, DelayB + 1 ); // get the best delay Delay = ABC_MIN( Delay0, Delay1 ); Area = 2; - Polarity = (int)(Delay1 == Delay); + Polarity = (int)(Delay == Delay1); } else if ( nSuppSize0 <= (int)p->nLutK - 2 ) { - DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<pDelays ); - DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays ); + DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<pDelays ); + DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1] , p->pDelays ); Delay = ABC_MAX( DelayA, DelayB + 1 ); Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK ); Polarity = 0; } else if ( nSuppSize1 <= (int)p->nLutK - 2 ) { - DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<pDelays ); - DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); + DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<pDelays ); + DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0] , p->pDelays ); Delay = ABC_MAX( DelayA, DelayB + 1 ); Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK ); Polarity = 1; } else if ( nSuppSize0 <= (int)p->nLutK ) { - DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<pDelays ); - DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); + DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<pDelays ); + DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0] , p->pDelays ); Delay = ABC_MAX( DelayA, DelayB + 1 ); Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ); Polarity = 1; } else if ( nSuppSize1 <= (int)p->nLutK ) { - DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<pDelays ); - DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays ); + DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<pDelays ); + DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1] , p->pDelays ); Delay = ABC_MAX( DelayA, DelayB + 1 ); Area = 1 + Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ); Polarity = 0; @@ -150,12 +108,12 @@ Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p ) else { // include cof var into 0-block - DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<pDelays ); - DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays ); + DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<pDelays ); + DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1] , p->pDelays ); Delay0 = ABC_MAX( DelayA, DelayB + 1 ); // include cof var into 1-block - DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<pDelays ); - DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); + DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<pDelays ); + DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0] , p->pDelays ); Delay1 = ABC_MAX( DelayA, DelayB + 1 ); // get the best delay Delay = ABC_MIN( Delay0, Delay1 ); @@ -163,20 +121,27 @@ Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p ) Area = Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize1, p->nLutK ); else Area = Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize0, p->nLutK ); - Polarity = (int)(Delay1 == Delay); + Polarity = (int)(Delay == Delay1); } // find the best variable if ( Delay > (int)p->nDelayLim ) continue; if ( Area > (int)p->nAreaLim ) continue; - if ( pRes->Variable == -1 || pRes->AreaEst > Area || (pRes->AreaEst == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) ) + nSuppSizeS = ABC_MIN( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity ); + nSuppSizeL = ABC_MAX( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity ); + if ( nSuppSizeL > (int)p->nVars ) + continue; + if ( pRes->Variable == -1 || pRes->AreaEst > Area || + (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL > nSuppSizeS + nSuppSizeL) || + (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL == nSuppSizeS + nSuppSizeL && pRes->DelayEst > Delay) ) { pRes->Variable = Var; pRes->Polarity = Polarity; pRes->AreaEst = Area; pRes->DelayEst = Delay; - nSuppSizeBest = nSuppSize0+nSuppSize1; + pRes->nSuppSizeS = nSuppSizeS; + pRes->nSuppSizeL = nSuppSizeL; } } return pRes->Variable == -1 ? NULL : pRes; @@ -193,16 +158,27 @@ Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p ) SeeAlso [] ***********************************************************************/ -Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol ) +Lpk_Fun_t * Lpk_MuxSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, int Var, int Pol ) { Lpk_Fun_t * pNew; unsigned * pTruth = Lpk_FunTruth( p, 0 ); unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); - int iVarVac; +// unsigned uSupp; + int iVarVac; assert( Var >= 0 && Var < (int)p->nVars ); assert( p->nAreaLim >= 2 ); - Lpk_FunComputeCofs( p, Var ); + assert( p->uSupp == Kit_BitMask(p->nVars) ); + Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var ); + Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var ); +/* +uSupp = Kit_TruthSupport( pTruth, p->nVars ); +Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" ); +uSupp = Kit_TruthSupport( pTruth0, p->nVars ); +Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" ); +uSupp = Kit_TruthSupport( pTruth1, p->nVars ); +Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n\n" ); +*/ // derive the new component pNew = Lpk_FunDup( p, Pol ? pTruth0 : pTruth1 ); // update the support of the old component @@ -211,29 +187,32 @@ Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol ) // update the truth table of the old component iVarVac = Kit_WordFindFirstBit( ~p->uSupp ); assert( iVarVac < (int)p->nVars ); - Kit_TruthIthVar( pTruth, p->nVars, Var ); + p->uSupp |= (1 << iVarVac); + Kit_TruthIthVar( pTruth, p->nVars, iVarVac ); if ( Pol ) - Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, iVarVac ); + Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, Var ); else - Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, iVarVac ); + Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, Var ); + assert( p->uSupp == Kit_TruthSupport(pTruth, p->nVars) ); // set the decomposed variable p->pFanins[iVarVac] = pNew->Id; p->pDelays[iVarVac] = p->nDelayLim - 1; // support minimize both + p->fSupports = 0; Lpk_FunSuppMinimize( p ); Lpk_FunSuppMinimize( pNew ); // update delay and area requirements pNew->nDelayLim = p->nDelayLim - 1; - if ( p->nVars <= p->nLutK ) - { - pNew->nAreaLim = p->nAreaLim - 1; - p->nAreaLim = 1; - } - else if ( pNew->nVars <= pNew->nLutK ) + if ( pNew->nVars <= pNew->nLutK ) { pNew->nAreaLim = 1; p->nAreaLim = p->nAreaLim - 1; } + else if ( p->nVars <= p->nLutK ) + { + pNew->nAreaLim = p->nAreaLim - 1; + p->nAreaLim = 1; + } else if ( p->nVars < pNew->nVars ) { pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2; @@ -244,7 +223,8 @@ Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol ) pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2; p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2; } - return p; + pNew->fMark = 1; + return pNew; } diff --git a/src/opt/lpk/lpkAbcUtil.c b/src/opt/lpk/lpkAbcUtil.c index 681ec092..3f917ce2 100644 --- a/src/opt/lpk/lpkAbcUtil.c +++ b/src/opt/lpk/lpkAbcUtil.c @@ -123,7 +123,7 @@ Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth ) memcpy( pNew->pFanins, p->pFanins, 16 ); memcpy( pNew->pDelays, p->pDelays, 16 ); Vec_PtrPush( p->vNodes, pNew ); - return p; + return pNew; } /**Function************************************************************* @@ -137,12 +137,15 @@ Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth ) SeeAlso [] ***********************************************************************/ -void Lpk_FunSuppMinimize( Lpk_Fun_t * p ) +int Lpk_FunSuppMinimize( Lpk_Fun_t * p ) { int i, k, nVarsNew; // compress the truth table if ( p->uSupp == Kit_BitMask(p->nVars) ) - return; + return 0; + // invalidate support info + p->fSupports = 0; +//Extra_PrintBinary( stdout, &p->uSupp, p->nVars ); printf( "\n" ); // minimize support nVarsNew = Kit_WordCountOnes(p->uSupp); Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 ); @@ -151,11 +154,48 @@ void Lpk_FunSuppMinimize( Lpk_Fun_t * p ) { p->pFanins[k] = p->pFanins[i]; p->pDelays[k] = p->pDelays[i]; +/* + if ( p->fSupports ) + { + p->puSupps[2*k+0] = p->puSupps[2*i+0]; + p->puSupps[2*k+1] = p->puSupps[2*i+1]; + } +*/ k++; } assert( k == nVarsNew ); p->nVars = k; p->uSupp = Kit_BitMask(p->nVars); + return 1; +} + +/**Function************************************************************* + + Synopsis [Computes cofactors w.r.t. each variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunComputeCofSupps( Lpk_Fun_t * p ) +{ + unsigned * pTruth = Lpk_FunTruth( p, 0 ); + unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); + unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); + int Var; + assert( p->fSupports == 0 ); +// Lpk_SuppForEachVar( p->uSupp, Var ) + for ( Var = 0; Var < (int)p->nVars; Var++ ) + { + Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var ); + Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var ); + p->puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars ); + p->puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars ); + } + p->fSupports = 1; } /**Function************************************************************* diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c index 37bfd956..6ea975aa 100644 --- a/src/opt/lpk/lpkCore.c +++ b/src/opt/lpk/lpkCore.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "lpkInt.h" +#include "cloud.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -127,6 +128,7 @@ int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk ) If_Obj_t * pDriver, * ppLeaves[16]; Abc_Obj_t * pLeaf, * pObjNew; int nGain, i, clk; + int nNodesBef; // int nOldShared; // check special cases @@ -201,6 +203,7 @@ p->timeMap += clock() - clk; if ( p->nCalledSRed ) p->nBenefited++; + nNodesBef = Abc_NtkNodeNum(p->pNtk); // prepare the mapping manager If_ManCleanNodeCopy( p->pIfMan ); If_ManCleanCutData( p->pIfMan ); @@ -212,6 +215,7 @@ p->timeMap += clock() - clk; pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) ); // perform replacement Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels ); +//printf( "%3d : %d-%d=%d(%d) \n", p->nChanges, nNodesBef, Abc_NtkNodeNum(p->pNtk), nNodesBef-Abc_NtkNodeNum(p->pNtk), nGain ); return 1; } @@ -232,8 +236,7 @@ int Lpk_ResynthesizeNode( Lpk_Man_t * p ) Kit_DsdNtk_t * pDsdNtk; Lpk_Cut_t * pCut; unsigned * pTruth; - void * pDsd = NULL; - int i, nSuppSize, RetValue, clk; + int i, k, nSuppSize, nCutNodes, RetValue, clk; // compute the cuts clk = clock(); @@ -258,9 +261,22 @@ p->timeCuts += clock() - clk; if ( p->pPars->fFirst && i == 1 ) break; + // skip bad cuts +// printf( "Mffc size = %d. ", Abc_NodeMffcLabel(p->pObj) ); + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize++; + nCutNodes = Abc_NodeMffcLabel(p->pObj); +// printf( "Mffc with cut = %d. ", nCutNodes ); + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize--; +// printf( "Mffc cut = %d. ", (int)pCut->nNodes - (int)pCut->nNodesDup ); +// printf( "\n" ); + if ( nCutNodes != (int)pCut->nNodes - (int)pCut->nNodesDup ) + continue; + // compute the truth table clk = clock(); - pTruth = Lpk_CutTruth( p, pCut ); + pTruth = Lpk_CutTruth( p, pCut, 0 ); nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves); p->timeTruth += clock() - clk; @@ -289,7 +305,7 @@ p->timeTruth += clock() - clk; printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); Kit_DsdPrint( stdout, pDsdNtk ); -// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves ); + Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves ); // pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ ); // printf( "Saved truth table in file \"%s\".\n", pFileName ); } @@ -305,6 +321,32 @@ p->timeEval += clock() - clk; return 1; } + +/**Function************************************************************* + + Synopsis [Computes supports of the cofactors of the function.] + + Description [This procedure should be called after Lpk_CutTruth(p,pCut,0)] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_ComputeSupports( Lpk_Man_t * p, Lpk_Cut_t * pCut, unsigned * pTruth ) +{ + unsigned * pTruthInv; + int RetValue1, RetValue2; + pTruthInv = Lpk_CutTruth( p, pCut, 1 ); + RetValue1 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruth, pCut->nLeaves, p->vBddDir ); + RetValue2 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruthInv, pCut->nLeaves, p->vBddInv ); + if ( RetValue1 && RetValue2 ) + Kit_TruthCofSupports( p->vBddDir, p->vBddInv, pCut->nLeaves, p->vMemory, p->puSupps ); + else + p->puSupps[0] = p->puSupps[1] = 0; +} + + /**Function************************************************************* Synopsis [Performs resynthesis for one node.] @@ -319,12 +361,13 @@ p->timeEval += clock() - clk; int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p ) { static int Count = 0; - Vec_Ptr_t * vLeaves; - Abc_Obj_t * pObjNew; + Abc_Obj_t * pObjNew, * pLeaf; Lpk_Cut_t * pCut; unsigned * pTruth; - void * pDsd = NULL; + int nNodesBef, nNodesAft, nCutNodes; int i, k, clk; + int Required = Abc_ObjRequiredLevel(p->pObj); +// CloudNode * pFun2;//, * pFun1; // compute the cuts clk = clock(); @@ -336,8 +379,8 @@ p->timeCuts += clock() - clk; p->timeCuts += clock() - clk; if ( p->pPars->fVeryVerbose ) - printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals ); - vLeaves = Vec_PtrAlloc( 32 ); + printf( "Node %5d : Mffc size = %5d. Cuts = %5d. Level = %2d. Req = %2d.\n", + p->pObj->Id, p->nMffc, p->nEvals, p->pObj->Level, Required ); // try the good cuts p->nCutsTotal += p->nCuts; p->nCutsUseful += p->nEvals; @@ -347,16 +390,48 @@ p->timeCuts += clock() - clk; pCut = p->pCuts + p->pEvals[i]; if ( p->pPars->fFirst && i == 1 ) break; +// if ( pCut->Weight < 1.05 ) +// continue; + + // skip bad cuts +// printf( "Mffc size = %d. ", Abc_NodeMffcLabel(p->pObj) ); + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize++; + nCutNodes = Abc_NodeMffcLabel(p->pObj); +// printf( "Mffc with cut = %d. ", nCutNodes ); + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize--; +// printf( "Mffc cut = %d. ", (int)pCut->nNodes - (int)pCut->nNodesDup ); +// printf( "\n" ); + if ( nCutNodes != (int)pCut->nNodes - (int)pCut->nNodesDup ) + continue; // collect nodes into the array - Vec_PtrClear( vLeaves ); + Vec_PtrClear( p->vLeaves ); for ( k = 0; k < (int)pCut->nLeaves; k++ ) - Vec_PtrPush( vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[i]) ); + Vec_PtrPush( p->vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[k]) ); // compute the truth table clk = clock(); - pTruth = Lpk_CutTruth( p, pCut ); + pTruth = Lpk_CutTruth( p, pCut, 0 ); p->timeTruth += clock() - clk; +clk = clock(); + Lpk_ComputeSupports( p, pCut, pTruth ); +p->timeSupps += clock() - clk; +//clk = clock(); +// pFun1 = Lpk_CutTruthBdd( p, pCut ); +//p->timeTruth2 += clock() - clk; +/* +clk = clock(); + Cloud_Restart( p->pDsdMan->dd ); + pFun2 = Kit_TruthToCloud( p->pDsdMan->dd, pTruth, pCut->nLeaves ); + RetValue = Kit_CreateCloud( p->pDsdMan->dd, pFun2, p->vBddNodes ); +p->timeTruth3 += clock() - clk; +*/ +// if ( pFun1 != pFun2 ) +// printf( "Truth tables do not agree!\n" ); +// else +// printf( "Fine!\n" ); if ( p->pPars->fVeryVerbose ) { @@ -364,22 +439,51 @@ p->timeTruth += clock() - clk; int nSuppSize = Extra_TruthSupportSize( pTruth, pCut->nLeaves ); printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); + Vec_PtrForEachEntry( p->vLeaves, pLeaf, k ) + printf( "%c=%d ", 'a'+k, Abc_ObjLevel(pLeaf) ); + printf( "\n" ); Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves ); // pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ ); // printf( "Saved truth table in file \"%s\".\n", pFileName ); } + if ( p->pObj->Id == 33 && i == 0 ) + { + int x = 0; + } // update the network + nNodesBef = Abc_NtkNodeNum(p->pNtk); clk = clock(); - pObjNew = Lpk_Decompose( p->pNtk, vLeaves, pTruth, p->pPars->nLutSize, - (int)pCut->nNodes - (int)pCut->nNodesDup - 1, Abc_ObjRequiredLevel(p->pObj) ); + pObjNew = Lpk_Decompose( p, p->pNtk, p->vLeaves, pTruth, p->puSupps, p->pPars->nLutSize, + (int)pCut->nNodes - (int)pCut->nNodesDup - 1 + (int)(p->pPars->fZeroCost > 0), Required ); p->timeEval += clock() - clk; + nNodesAft = Abc_NtkNodeNum(p->pNtk); // perform replacement if ( pObjNew ) + { + int nGain = (int)pCut->nNodes - (int)pCut->nNodesDup - (nNodesAft - nNodesBef); + assert( nGain >= 1 - p->pPars->fZeroCost ); + assert( Abc_ObjLevel(pObjNew) <= Required ); +/* + if ( nGain <= 0 ) + { + int x = 0; + } + if ( Abc_ObjLevel(pObjNew) > Required ) + { + int x = 0; + } +*/ + p->nGainTotal += nGain; + p->nChanges++; + if ( p->pPars->fVeryVerbose ) + printf( "Performed resynthesis: Gain = %2d. Level = %2d. Req = %2d.\n", nGain, Abc_ObjLevel(pObjNew), Required ); Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels ); +//printf( "%3d : %d-%d=%d(%d) \n", p->nChanges, nNodesBef, Abc_NtkNodeNum(p->pNtk), nNodesBef-Abc_NtkNodeNum(p->pNtk), nGain ); + break; + } } - Vec_PtrFree( vLeaves ); return 1; } @@ -443,7 +547,10 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) if ( p->pPars->fSatur ) p->vVisited = Vec_VecStart( 0 ); if ( pPars->fVerbose ) + { p->nTotalNets = Abc_NtkGetTotalFanins(pNtk); + p->nTotalNodes = Abc_NtkNodeNum(pNtk); + } // iterate over the network nNodesPrev = p->nNodesTotal; @@ -465,7 +572,6 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) ) continue; } - if ( i >= nNodes ) break; if ( !pPars->fVeryVerbose ) @@ -475,10 +581,10 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) continue; // resynthesize p->pObj = pObj; - Lpk_ResynthesizeNode( p ); - -// if ( p->nChanges == 3 ) -// break; + if ( p->pPars->fOldAlgo ) + Lpk_ResynthesizeNode( p ); + else + Lpk_ResynthesizeNodeNew( p ); } if ( !pPars->fVeryVerbose ) Extra_ProgressBarStop( pProgress ); @@ -498,15 +604,18 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) if ( pPars->fVerbose ) { +// Cloud_PrintInfo( p->pDsdMan->dd ); 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->nTotalNodes2 = Abc_NtkNodeNum(pNtk); + printf( "Node gain = %5d. (%.2f %%) ", + p->nTotalNodes-p->nTotalNodes2, 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes ); + printf( "Edge gain = %5d. (%.2f %%) ", p->nTotalNets-p->nTotalNets2, 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets ); + printf( "Muxes = %4d. Dsds = %4d.", p->nMuxes, p->nDsds ); 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] ) @@ -518,7 +627,13 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap; PRTP( "Cuts ", p->timeCuts, p->timeTotal ); PRTP( "Truth ", p->timeTruth, p->timeTotal ); + PRTP( "CSupps", p->timeSupps, p->timeTotal ); PRTP( "Eval ", p->timeEval, p->timeTotal ); + PRTP( " MuxAn", p->timeEvalMuxAn, p->timeEval ); + PRTP( " MuxSp", p->timeEvalMuxSp, p->timeEval ); + PRTP( " DsdAn", p->timeEvalDsdAn, p->timeEval ); + PRTP( " DsdSp", p->timeEvalDsdSp, p->timeEval ); + PRTP( " Other", p->timeEval-p->timeEvalMuxAn-p->timeEvalMuxSp-p->timeEvalDsdAn-p->timeEvalDsdSp, p->timeEval ); PRTP( "Map ", p->timeMap, p->timeTotal ); PRTP( "Other ", p->timeOther, p->timeTotal ); PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c index f5c0c66c..b2a743bd 100644 --- a/src/opt/lpk/lpkCut.c +++ b/src/opt/lpk/lpkCut.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "lpkInt.h" +#include "cloud.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -39,7 +40,99 @@ SeeAlso [] ***********************************************************************/ -unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount ) +CloudNode * Lpk_CutTruthBdd_rec( CloudManager * dd, Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars ) +{ + CloudNode * pTruth, * pTruth0, * pTruth1; + assert( !Hop_IsComplement(pObj) ); + if ( pObj->pData ) + { + assert( ((unsigned)pObj->pData) & 0xffff0000 ); + return pObj->pData; + } + // get the plan for a new truth table + if ( Hop_ObjIsConst1(pObj) ) + pTruth = dd->one; + else + { + assert( Hop_ObjIsAnd(pObj) ); + // compute the truth tables of the fanins + pTruth0 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin0(pObj), nVars ); + pTruth1 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin1(pObj), nVars ); + pTruth0 = Cloud_NotCond( pTruth0, Hop_ObjFaninC0(pObj) ); + pTruth1 = Cloud_NotCond( pTruth1, Hop_ObjFaninC1(pObj) ); + // creat the truth table of the node + pTruth = Cloud_bddAnd( dd, pTruth0, pTruth1 ); + } + pObj->pData = pTruth; + return pTruth; +} + +/**Function************************************************************* + + Synopsis [Verifies that the factoring is correct.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +CloudNode * Lpk_CutTruthBdd( Lpk_Man_t * p, Lpk_Cut_t * pCut ) +{ + CloudManager * dd = p->pDsdMan->dd; + Hop_Man_t * pManHop = p->pNtk->pManFunc; + Hop_Obj_t * pObjHop; + Abc_Obj_t * pObj, * pFanin; + CloudNode * pTruth; + int i, k, iCount = 0; + +// return NULL; +// Lpk_NodePrintCut( p, pCut ); + // initialize the leaves + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)dd->vars[pCut->nLeaves-1-i]; + + // construct truth table in the topological order + Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i ) + { + // get the local AIG + pObjHop = Hop_Regular(pObj->pData); + // clean the data field of the nodes in the AIG subgraph + Hop_ObjCleanData_rec( pObjHop ); + // set the initial truth tables at the fanins + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + assert( ((unsigned)pFanin->pCopy) & 0xffff0000 ); + Hop_ManPi( pManHop, k )->pData = pFanin->pCopy; + } + // compute the truth table of internal nodes + pTruth = Lpk_CutTruthBdd_rec( dd, pManHop, pObjHop, pCut->nLeaves ); + if ( Hop_IsComplement(pObj->pData) ) + pTruth = Cloud_Not(pTruth); + // set the truth table at the node + pObj->pCopy = (Abc_Obj_t *)pTruth; + + } + +// Cloud_bddPrint( dd, pTruth ); +// printf( "Bdd size = %d. Total nodes = %d.\n", Cloud_DagSize( dd, pTruth ), dd->nNodesCur-dd->nVars-1 ); + return pTruth; +} + + +/**Function************************************************************* + + Synopsis [Computes the truth table of one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * piCount ) { unsigned * pTruth, * pTruth0, * pTruth1; assert( !Hop_IsComplement(pObj) ); @@ -49,17 +142,17 @@ unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_ return pObj->pData; } // get the plan for a new truth table - pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ ); + pTruth = Vec_PtrEntry( vTtNodes, (*piCount)++ ); if ( Hop_ObjIsConst1(pObj) ) - Extra_TruthFill( pTruth, nVars ); + Kit_TruthFill( pTruth, nVars ); else { assert( Hop_ObjIsAnd(pObj) ); // compute the truth tables of the fanins - pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount ); - pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount ); + pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, piCount ); + pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, piCount ); // creat the truth table of the node - Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) ); + Kit_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) ); } pObj->pData = pTruth; return pTruth; @@ -76,7 +169,7 @@ unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_ SeeAlso [] ***********************************************************************/ -unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ) +unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv ) { Hop_Man_t * pManHop = p->pNtk->pManFunc; Hop_Obj_t * pObjHop; @@ -84,10 +177,11 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ) unsigned * pTruth; int i, k, iCount = 0; // Lpk_NodePrintCut( p, pCut ); + assert( pCut->nNodes > 0 ); // initialize the leaves Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) - pObj->pCopy = Vec_PtrEntry( p->vTtElems, i ); + pObj->pCopy = Vec_PtrEntry( p->vTtElems, fInv? pCut->nLeaves-1-i : i ); // construct truth table in the topological order Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i ) @@ -105,14 +199,22 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ) // compute the truth table of internal nodes pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount ); if ( Hop_IsComplement(pObj->pData) ) - Extra_TruthNot( pTruth, pTruth, pCut->nLeaves ); + Kit_TruthNot( pTruth, pTruth, pCut->nLeaves ); // set the truth table at the node pObj->pCopy = (Abc_Obj_t *)pTruth; } + // make sure direct truth table is stored elsewhere (assuming the first call for direct truth!!!) + if ( fInv == 0 ) + { + pTruth = Vec_PtrEntry( p->vTtNodes, iCount++ ); + Kit_TruthCopy( pTruth, (unsigned *)pObj->pCopy, pCut->nLeaves ); + } + assert( iCount <= Vec_PtrSize(p->vTtNodes) ); return pTruth; } + /**Function************************************************************* Synopsis [Returns 1 if at least one entry has changed.] @@ -535,8 +637,10 @@ int Lpk_NodeCuts( Lpk_Man_t * p ) // 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 = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize ); +// pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup - 1) / pCut->nLuts; //p->pPars->nLutsMax; pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax; if ( pCut->Weight <= 1.001 ) +// if ( pCut->Weight <= 0.999 ) continue; pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut ); if ( pCut->fHasDsd ) diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h index 32fb05b3..960599e4 100644 --- a/src/opt/lpk/lpkInt.h +++ b/src/opt/lpk/lpkInt.h @@ -90,12 +90,18 @@ struct Lpk_Man_t_ 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 + Vec_Ptr_t * vLeaves; // truth table representation Vec_Ptr_t * vTtElems; // elementary truth tables Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes + Vec_Int_t * vMemory; + Vec_Int_t * vBddDir; + Vec_Int_t * vBddInv; + unsigned puSupps[32]; // the supports of the cofactors + unsigned * ppTruths[5][16]; // variable sets Vec_Int_t * vSets[8]; - Kit_DsdMan_t * pDsdMan; + Kit_DsdMan_t* pDsdMan; // statistics int nNodesTotal; // total number of nodes int nNodesOver; // nodes with cuts over the limit @@ -104,17 +110,30 @@ struct Lpk_Man_t_ int nGainTotal; // the gain in LUTs int nChanges; // the number of changed nodes int nBenefited; // the number of gainful that benefited from decomposition + int nMuxes; + int nDsds; int nTotalNets; int nTotalNets2; + int nTotalNodes; + int nTotalNodes2; // counter of non-DSD blocks int nBlocks[17]; - // rutime + // runtime int timeCuts; int timeTruth; + int timeSupps; + int timeTruth2; + int timeTruth3; int timeEval; int timeMap; int timeOther; int timeTotal; + // runtime of eval + int timeEvalMuxAn; + int timeEvalMuxSp; + int timeEvalDsdAn; + int timeEvalDsdSp; + }; @@ -122,32 +141,35 @@ struct Lpk_Man_t_ typedef struct Lpk_Fun_t_ Lpk_Fun_t; struct Lpk_Fun_t_ { - Vec_Ptr_t * vNodes; // the array of leaves and decomposition nodes - unsigned int Id : 8; // the ID of this node - unsigned int nVars : 5; // the number of variables - unsigned int nLutK : 4; // the number of LUT inputs - unsigned int nAreaLim : 5; // the area limit (the largest allowed) - unsigned int nDelayLim : 10; // the delay limit (the largest allowed) - char pDelays[16]; // the delays of the inputs - char pFanins[16]; // the fanins of this function - unsigned uSupp; // the support of this component - unsigned pTruth[0]; // the truth table (contains room for three truth tables) + Vec_Ptr_t * vNodes; // the array of leaves and decomposition nodes + unsigned Id : 7; // the ID of this node + unsigned nVars : 5; // the number of variables + unsigned nLutK : 4; // the number of LUT inputs + unsigned nAreaLim : 5; // the area limit (the largest allowed) + unsigned nDelayLim : 9; // the delay limit (the largest allowed) + unsigned fSupports : 1; // supports of cofactors were precomputed + unsigned fMark : 1; // marks the MUX-based dec + unsigned uSupp; // the support of this component + unsigned puSupps[32]; // the supports of the cofactors + char pDelays[16]; // the delays of the inputs + char pFanins[16]; // the fanins of this function + unsigned pTruth[0]; // the truth table (contains room for three truth tables) }; // preliminary decomposition result typedef struct Lpk_Res_t_ Lpk_Res_t; struct Lpk_Res_t_ { - int nBSVars; // the number of bound set variables - unsigned BSVars; // the bound set - int nCofVars; // the number of cofactoring variables - char pCofVars[4]; // the cofactoring variables - int nSuppSizeS; // support size of the smaller (decomposed) function - int nSuppSizeL; // support size of the larger (composition) function - int DelayEst; // estimated delay of the decomposition - int AreaEst; // estimated area of the decomposition - int Variable; // variable in MUX decomposition - int Polarity; // polarity in MUX decomposition + int nBSVars; // the number of bound set variables + unsigned BSVars; // the bound set + int nCofVars; // the number of cofactoring variables + char pCofVars[4]; // the cofactoring variables + int nSuppSizeS; // support size of the smaller (decomposed) function + int nSuppSizeL; // support size of the larger (composition) function + int DelayEst; // estimated delay of the decomposition + int AreaEst; // estimated area of the decomposition + int Variable; // variable in MUX decomposition + int Polarity; // polarity in MUX decomposition }; static inline int Lpk_LutNumVars( int nLutsLim, int nLutK ) { return nLutsLim * (nLutK - 1) + 1; } @@ -177,25 +199,26 @@ static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num ) { assert( Num //////////////////////////////////////////////////////////////////////// /*=== lpkAbcDec.c ============================================================*/ -extern Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ); +extern Abc_Obj_t * Lpk_Decompose( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, unsigned * puSupps, int nLutK, int AreaLim, int DelayLim ); /*=== lpkAbcDsd.c ============================================================*/ -extern Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p ); -extern Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet ); +extern Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared ); +extern Lpk_Fun_t * Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet ); /*=== lpkAbcMux.c ============================================================*/ -extern Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p ); -extern Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol ); +extern Lpk_Res_t * Lpk_MuxAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p ); +extern Lpk_Fun_t * Lpk_MuxSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, int Var, int Pol ); /*=== lpkAbcUtil.c ============================================================*/ extern Lpk_Fun_t * Lpk_FunAlloc( int nVars ); extern void Lpk_FunFree( Lpk_Fun_t * p ); extern Lpk_Fun_t * Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ); extern Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth ); -extern void Lpk_FunSuppMinimize( Lpk_Fun_t * p ); +extern int Lpk_FunSuppMinimize( Lpk_Fun_t * p ); +extern void Lpk_FunComputeCofSupps( Lpk_Fun_t * p ); extern int Lpk_SuppDelay( unsigned uSupp, char * pDelays ); extern int Lpk_SuppToVars( unsigned uBoundSet, char * pVars ); /*=== lpkCut.c =========================================================*/ -extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ); +extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv ); extern int Lpk_NodeCuts( Lpk_Man_t * p ); /*=== lpkMap.c =========================================================*/ extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ); diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c index 5be198d7..af6a5307 100644 --- a/src/opt/lpk/lpkMan.c +++ b/src/opt/lpk/lpkMan.c @@ -42,9 +42,9 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) { Lpk_Man_t * p; - int i; + int i, nWords; assert( pPars->nLutsMax <= 16 ); - assert( pPars->nVarsMax > 0 ); + assert( pPars->nVarsMax > 0 && pPars->nVarsMax <= 16 ); p = ALLOC( Lpk_Man_t, 1 ); memset( p, 0, sizeof(Lpk_Man_t) ); p->pPars = pPars; @@ -52,9 +52,28 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax ); p->vTtNodes = Vec_PtrAllocSimInfo( 1024, Abc_TruthWordNum(pPars->nVarsMax) ); p->vCover = Vec_IntAlloc( 1 << 12 ); + p->vLeaves = Vec_PtrAlloc( 32 ); for ( i = 0; i < 8; i++ ) p->vSets[i] = Vec_IntAlloc(100); p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 ); + p->vMemory = Vec_IntAlloc( 1024 * 32 ); + p->vBddDir = Vec_IntAlloc( 256 ); + p->vBddInv = Vec_IntAlloc( 256 ); + // allocate temporary storage for truth tables + nWords = Kit_TruthWordNum(pPars->nVarsMax); + p->ppTruths[0][0] = ALLOC( unsigned, 32 * nWords ); + p->ppTruths[1][0] = p->ppTruths[0][0] + 1 * nWords; + for ( i = 1; i < 2; i++ ) + p->ppTruths[1][i] = p->ppTruths[1][0] + i * nWords; + p->ppTruths[2][0] = p->ppTruths[1][0] + 2 * nWords; + for ( i = 1; i < 4; i++ ) + p->ppTruths[2][i] = p->ppTruths[2][0] + i * nWords; + p->ppTruths[3][0] = p->ppTruths[2][0] + 4 * nWords; + for ( i = 1; i < 8; i++ ) + p->ppTruths[3][i] = p->ppTruths[3][0] + i * nWords; + p->ppTruths[4][0] = p->ppTruths[3][0] + 8 * nWords; + for ( i = 1; i < 16; i++ ) + p->ppTruths[4][i] = p->ppTruths[4][0] + i * nWords; return p; } @@ -72,6 +91,10 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) void Lpk_ManStop( Lpk_Man_t * p ) { int i; + free( p->ppTruths[0][0] ); + Vec_IntFree( p->vBddDir ); + Vec_IntFree( p->vBddInv ); + Vec_IntFree( p->vMemory ); Kit_DsdManFree( p->pDsdMan ); for ( i = 0; i < 8; i++ ) Vec_IntFree(p->vSets[i]); @@ -85,6 +108,7 @@ void Lpk_ManStop( Lpk_Man_t * p ) Vec_VecFree( p->vLevels ); if ( p->vVisited ) Vec_VecFree( p->vVisited ); + Vec_PtrFree( p->vLeaves ); Vec_IntFree( p->vCover ); Vec_PtrFree( p->vTtElems ); Vec_PtrFree( p->vTtNodes ); diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c index d0d56a86..90e46863 100644 --- a/src/opt/lpk/lpkSets.c +++ b/src/opt/lpk/lpkSets.c @@ -140,7 +140,7 @@ unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets ) SeeAlso [] ***********************************************************************/ -void Lpk_PrintSetOne( int uSupport ) +static void Lpk_PrintSetOne( int uSupport ) { unsigned k; for ( k = 0; k < 16; k++ ) @@ -159,7 +159,7 @@ void Lpk_PrintSetOne( int uSupport ) SeeAlso [] ***********************************************************************/ -void Lpk_PrintSets( Vec_Int_t * vSets ) +static void Lpk_PrintSets( Vec_Int_t * vSets ) { unsigned uSupport; int Number, i; -- cgit v1.2.3