mirror of https://github.com/YosysHQ/abc.git
Version abc70909
This commit is contained in:
Alan Mishchenko
parent
9be1b07693
commit
e8cf8415c5
12
abc.dsp
12
abc.dsp
|
|
@ -2786,6 +2786,14 @@ SOURCE=.\src\aig\csw\cswTable.c
|
|||
# PROP Default_Filter ""
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\kit\cloud.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\kit\cloud.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\kit\kit.h
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
@ -2794,6 +2802,10 @@ SOURCE=.\src\aig\kit\kitBdd.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\kit\kitCloud.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\aig\kit\kitDsd.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -0,0 +1,987 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cloudCore.c]
|
||||
|
||||
PackageName [Fast application-specific BDD package.]
|
||||
|
||||
Synopsis [The package core.]
|
||||
|
||||
Author [Alan Mishchenko <alanmi@ece.pdx.edu>]
|
||||
|
||||
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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,269 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cloud.h]
|
||||
|
||||
PackageName [Fast application-specific BDD package.]
|
||||
|
||||
Synopsis [Interface of the package.]
|
||||
|
||||
Author [Alan Mishchenko <alanmi@ece.pdx.edu>]
|
||||
|
||||
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 <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include <assert.h>
|
||||
#include <time.h>
|
||||
|
||||
#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 ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
@ -36,6 +36,7 @@ extern "C" {
|
|||
#include <time.h>
|
||||
#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 );
|
||||
|
|
|
|||
|
|
@ -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<<Var);
|
||||
assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
|
||||
assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
|
||||
pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
|
||||
pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
|
||||
}
|
||||
// copy the result
|
||||
memcpy( puSupps, pThis, sizeof(unsigned) * nSupps );
|
||||
// compute the inverse
|
||||
|
||||
// extend storage
|
||||
if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddInv) )
|
||||
Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddInv) );
|
||||
puSuppAll = Vec_IntArray( vMemory );
|
||||
// clear storage for the const node
|
||||
memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
|
||||
// compute supports from nodes
|
||||
Vec_IntForEachEntryStart( vBddInv, Entry, i, 1 )
|
||||
{
|
||||
Mux = *((Kit_Mux_t *)&Entry);
|
||||
// Var = nVars - 1 - Mux.v;
|
||||
Var = 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<<Var);
|
||||
assert( pFan0[2*Var + 0] == pFan0[2*Var + 1] );
|
||||
assert( pFan1[2*Var + 0] == pFan1[2*Var + 1] );
|
||||
pThis[2*Var + 0] = pFan0[2*Var + 0];// | pFan0[2*Var + 1];
|
||||
pThis[2*Var + 1] = pFan1[2*Var + 0];// | pFan1[2*Var + 1];
|
||||
}
|
||||
|
||||
// merge supports
|
||||
for ( Var = 0; Var < nSupps; Var++ )
|
||||
puSupps[Var] = (puSupps[Var] & Kit_BitMask(Var/2)) | (pThis[Var] & ~Kit_BitMask(Var/2));
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
|
|
@ -44,10 +44,13 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
|
|||
Kit_DsdMan_t * p;
|
||||
p = ALLOC( Kit_DsdMan_t, 1 );
|
||||
memset( p, 0, sizeof(Kit_DsdMan_t) );
|
||||
p->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<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
|
||||
Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->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<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
|
||||
Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->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<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) );
|
||||
Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->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 );
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 \
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfvwh]\n" );
|
||||
fprintf( pErr, "usage: lutpack [-N <num>] [-Q <num>] [-S <num>] [-L <num>] [-szfovwh]\n" );
|
||||
fprintf( pErr, "\t performs \"rewriting\" for LUT networks\n" );
|
||||
fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
|
||||
fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
|
||||
fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num) [default = %d]\n", pPars->nVarsShared );
|
||||
fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
|
||||
fprintf( pErr, "\t-L <num> : 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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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<<k) )
|
||||
printf( "%c", 'a'+k );
|
||||
printf( " " );
|
||||
}
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints the sets of subsets.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static void Lpk_PrintSets( Vec_Int_t * vSets )
|
||||
{
|
||||
unsigned uSupport;
|
||||
int Number, i;
|
||||
printf( "Subsets(%d): ", Vec_IntSize(vSets) );
|
||||
Vec_IntForEachEntry( vSets, Number, i )
|
||||
{
|
||||
uSupport = Number;
|
||||
Lpk_PrintSetOne( uSupport );
|
||||
}
|
||||
printf( "\n" );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Merges two bound sets.]
|
||||
|
|
@ -196,74 +249,12 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSiz
|
|||
Entry = Entry0 | Entry1;
|
||||
if ( (Entry & (Entry >> 16)) )
|
||||
continue;
|
||||
if ( Kit_WordCountOnes(Entry) <= nSizeMax )
|
||||
if ( Kit_WordCountOnes(Entry & 0xffff) <= nSizeMax )
|
||||
Vec_IntPush( vSets, Entry );
|
||||
}
|
||||
return vSets;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Allocates truth tables for cofactors.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
|
||||
{
|
||||
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 )
|
||||
{
|
||||
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 ( nCofDepth >= 4 )
|
||||
{
|
||||
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;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Allocates truth tables for cofactors.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
|
||||
{
|
||||
if ( nCofDepth >= 2 )
|
||||
free( ppTruths[2][0] );
|
||||
if ( nCofDepth >= 3 )
|
||||
free( ppTruths[3][0] );
|
||||
if ( nCofDepth >= 4 )
|
||||
free( ppTruths[4][0] );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs DSD-based decomposition of the function.]
|
||||
|
|
@ -275,58 +266,84 @@ 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 )
|
||||
void Lpk_FunCompareBoundSets( Lpk_Fun_t * p, Vec_Int_t * vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t * pRes )
|
||||
{
|
||||
unsigned * ppTruths[5][16];
|
||||
Vec_Int_t * pvBSets[4][8];
|
||||
Kit_DsdNtk_t * pNtkDec, * pTemp;
|
||||
int fVerbose = 0;
|
||||
unsigned uBoundSet;
|
||||
int i, k, nVarsBS, nVarsRem, Delay, Area;
|
||||
assert( nCofDepth >= 0 && nCofDepth < 4 );
|
||||
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<<i, ppTruths[i+1] );
|
||||
// derive decomposed networks
|
||||
for ( i = 0; i < (1<<nCofDepth); i++ )
|
||||
{
|
||||
pNtkDec = Kit_DsdDecompose( ppTruths[nCofDepth][i], p->nVars );
|
||||
pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp );
|
||||
pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtkDec, p->nLutK - nCofDepth );
|
||||
Kit_DsdNtkFree( pNtkDec );
|
||||
}
|
||||
// derive the set of feasible boundsets
|
||||
for ( i = nCofDepth - 1; i >= 0; i-- )
|
||||
for ( k = 0; k < (1<<i); k++ )
|
||||
pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
|
||||
int i, nVarsBS, nVarsRem, Delay, Area;
|
||||
|
||||
// compare the resulting boundsets
|
||||
Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i )
|
||||
memset( pRes, 0, sizeof(Lpk_Res_t) );
|
||||
Vec_IntForEachEntry( vBSets, uBoundSet, i )
|
||||
{
|
||||
if ( uBoundSet == 0 )
|
||||
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 + nCofDepth + 1;
|
||||
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->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
|
||||
if ( pRes->BSVars == 0 || pRes->nSuppSizeL > nVarsRem || (pRes->nSuppSizeL == nVarsRem && pRes->DelayEst > Delay) )
|
||||
{
|
||||
pRes->nBSVars = nVarsBS;
|
||||
pRes->BSVars = uBoundSet;
|
||||
pRes->nSuppSizeS = nVarsBS;
|
||||
pRes->BSVars = (uBoundSet & 0xFFFF);
|
||||
pRes->nSuppSizeS = nVarsBS + nCofDepth;
|
||||
pRes->nSuppSizeL = nVarsRem;
|
||||
pRes->DelayEst = Delay;
|
||||
pRes->AreaEst = Area;
|
||||
}
|
||||
}
|
||||
// free cofactor storage
|
||||
Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths );
|
||||
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 )
|
||||
{
|
||||
assert( pRes->DelayEst <= (int)p->nDelayLim );
|
||||
assert( pRes->AreaEst <= (int)p->nAreaLim );
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Finds late arriving inputs, which cannot be in the bound set.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
unsigned Lpk_DsdLateArriving( Lpk_Fun_t * p )
|
||||
{
|
||||
unsigned i, uLateArrSupp = 0;
|
||||
Lpk_SuppForEachVar( p->uSupp, i )
|
||||
if ( p->pDelays[i] > (int)p->nDelayLim - 2 )
|
||||
uLateArrSupp |= (1 << i);
|
||||
return uLateArrSupp;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
@ -340,47 +357,185 @@ void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p )
|
||||
int Lpk_DsdAnalizeOne( Lpk_Fun_t * p, unsigned * ppTruths[5][16], Kit_DsdNtk_t * pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t * pRes )
|
||||
{
|
||||
int fVerbose = 0;
|
||||
Vec_Int_t * pvBSets[4][8];
|
||||
unsigned uNonDecSupp, uLateArrSupp;
|
||||
int i, k, nNonDecSize, nNonDecSizeMax;
|
||||
assert( nCofDepth >= 1 && nCofDepth <= 3 );
|
||||
assert( nCofDepth < (int)p->nLutK - 1 );
|
||||
assert( p->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<<nCofDepth); i++ )
|
||||
{
|
||||
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<<i); k++ )
|
||||
pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth );
|
||||
// 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<<i); k++ )
|
||||
Vec_IntFree( pvBSets[i][k] );
|
||||
|
||||
// copy the cofactoring variables
|
||||
if ( pRes->BSVars )
|
||||
{
|
||||
pRes->nCofVars = nCofDepth;
|
||||
for ( i = 0; i < nCofDepth; i++ )
|
||||
pRes->pCofVars[i] = pCofVars[i];
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs DSD-based decomposition of the function.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
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<<nShared); i++ )
|
||||
if ( pNtks[i] )
|
||||
Kit_DsdNtkFree( pNtks[i] );
|
||||
// choose the best under these conditions
|
||||
|
||||
return NULL;
|
||||
return pRes;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
@ -394,62 +549,50 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
|
||||
Lpk_Fun_t * Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet )
|
||||
{
|
||||
Lpk_Fun_t * pNew;
|
||||
Kit_DsdMan_t * pDsdMan;
|
||||
Kit_DsdNtk_t * pNtkDec, * pTemp;
|
||||
unsigned * pTruth = Lpk_FunTruth( p, 0 );
|
||||
unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
|
||||
unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
|
||||
unsigned * ppTruths[5][16];
|
||||
char pBSVars[5];
|
||||
int i, k, nVars, iVacVar, nCofs;
|
||||
// get the bound set variables
|
||||
nVars = Lpk_SuppToVars( uBoundSet, pBSVars );
|
||||
Kit_DsdNtk_t * pNtkDec;
|
||||
int i, k, iVacVar, nCofs;
|
||||
// prepare storage
|
||||
Kit_TruthCopy( pMan->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<<i); k++ )
|
||||
{
|
||||
Kit_TruthCofactor0New( ppTruths[i+1][2*k+0], ppTruths[i][k], p->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<<nCofVars);
|
||||
pDsdMan = Kit_DsdManAlloc( p->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<<i); k++ )
|
||||
Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i-1] );
|
||||
Kit_TruthMuxVar( pMan->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;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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<<Var), p->pDelays );
|
||||
DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays );
|
||||
DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->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<<Var), p->pDelays );
|
||||
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
|
||||
DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->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<<Var), p->pDelays );
|
||||
DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays );
|
||||
DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->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<<Var), p->pDelays );
|
||||
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
|
||||
DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->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<<Var), p->pDelays );
|
||||
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
|
||||
DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->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<<Var), p->pDelays );
|
||||
DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays );
|
||||
DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->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<<Var), p->pDelays );
|
||||
DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays );
|
||||
DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->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<<Var), p->pDelays );
|
||||
DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays );
|
||||
DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->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;
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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*************************************************************
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 )
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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 );
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
Loading…
Reference in New Issue