summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2007-09-09 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2007-09-09 08:01:00 -0700
commite8cf8415c5c8c31db650f549e54fd7a3aad48be0 (patch)
tree3eee40925efd4d8bd388d283c2a0232053fc90ac
parent9be1b076934b0410689c857cd71ef7d21a714b5f (diff)
downloadabc-e8cf8415c5c8c31db650f549e54fd7a3aad48be0.tar.gz
abc-e8cf8415c5c8c31db650f549e54fd7a3aad48be0.tar.bz2
abc-e8cf8415c5c8c31db650f549e54fd7a3aad48be0.zip
Version abc70909
-rw-r--r--abc.dsp12
-rw-r--r--src/aig/kit/cloud.c987
-rw-r--r--src/aig/kit/cloud.h269
-rw-r--r--src/aig/kit/kit.h27
-rw-r--r--src/aig/kit/kitCloud.c368
-rw-r--r--src/aig/kit/kitDsd.c240
-rw-r--r--src/aig/kit/kitTruth.c64
-rw-r--r--src/aig/kit/module.make1
-rw-r--r--src/base/abc/abcRefs.c4
-rw-r--r--src/base/abci/abc.c23
-rw-r--r--src/misc/vec/vecStr.h2
-rw-r--r--src/opt/lpk/lpk.h1
-rw-r--r--src/opt/lpk/lpkAbcDec.c130
-rw-r--r--src/opt/lpk/lpkAbcDsd.c407
-rw-r--r--src/opt/lpk/lpkAbcMux.c150
-rw-r--r--src/opt/lpk/lpkAbcUtil.c46
-rw-r--r--src/opt/lpk/lpkCore.c163
-rw-r--r--src/opt/lpk/lpkCut.c122
-rw-r--r--src/opt/lpk/lpkInt.h81
-rw-r--r--src/opt/lpk/lpkMan.c28
-rw-r--r--src/opt/lpk/lpkSets.c4
21 files changed, 2777 insertions, 352 deletions
diff --git a/abc.dsp b/abc.dsp
index 8f0d0ebb..e745903f 100644
--- a/abc.dsp
+++ b/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
diff --git a/src/aig/kit/cloud.c b/src/aig/kit/cloud.c
new file mode 100644
index 00000000..6e6691f0
--- /dev/null
+++ b/src/aig/kit/cloud.c
@@ -0,0 +1,987 @@
+/**CFile****************************************************************
+
+ FileName [cloudCore.c]
+
+ PackageName [Fast application-specific BDD package.]
+
+ Synopsis [The package core.]
+
+ Author [Alan Mishchenko <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 ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/kit/cloud.h b/src/aig/kit/cloud.h
new file mode 100644
index 00000000..ac9d45f4
--- /dev/null
+++ b/src/aig/kit/cloud.h
@@ -0,0 +1,269 @@
+/**CFile****************************************************************
+
+ FileName [cloud.h]
+
+ PackageName [Fast application-specific BDD package.]
+
+ Synopsis [Interface of the package.]
+
+ Author [Alan Mishchenko <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 ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 2ad9a6f0..06a93cf0 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -36,6 +36,7 @@ extern "C" {
#include <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 );
diff --git a/src/aig/kit/kitCloud.c b/src/aig/kit/kitCloud.c
new file mode 100644
index 00000000..7b160fea
--- /dev/null
+++ b/src/aig/kit/kitCloud.c
@@ -0,0 +1,368 @@
+/**CFile****************************************************************
+
+ FileName [kitCloud.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Computation kit.]
+
+ Synopsis [Procedures using BDD package CLOUD.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - Dec 6, 2006.]
+
+ Revision [$Id: kitCloud.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// internal representation of the function to be decomposed
+typedef struct Kit_Mux_t_ Kit_Mux_t;
+struct Kit_Mux_t_
+{
+ unsigned v : 5; // variable
+ unsigned t : 12; // then edge
+ unsigned e : 12; // else edge
+ unsigned c : 1; // complemented attr of else edge
+ unsigned i : 1; // complemented attr of top node
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Derive BDD from the truth table for 5 variable functions.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+CloudNode * Kit_TruthToCloud5_rec( CloudManager * dd, unsigned uTruth, int nVars, int nVarsAll )
+{
+ static unsigned uVars[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+ CloudNode * pCof0, * pCof1;
+ unsigned uCof0, uCof1;
+ assert( nVars <= 5 );
+ if ( uTruth == 0 )
+ return dd->zero;
+ if ( uTruth == ~0 )
+ return dd->one;
+ if ( nVars == 1 )
+ {
+ if ( uTruth == uVars[0] )
+ return dd->vars[nVarsAll-1];
+ if ( uTruth == ~uVars[0] )
+ return Cloud_Not(dd->vars[nVarsAll-1]);
+ assert( 0 );
+ }
+// Count++;
+ assert( nVars > 1 );
+ uCof0 = uTruth & ~uVars[nVars-1];
+ uCof1 = uTruth & uVars[nVars-1];
+ uCof0 |= uCof0 << (1<<(nVars-1));
+ uCof1 |= uCof1 >> (1<<(nVars-1));
+ if ( uCof0 == uCof1 )
+ return Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+ if ( uCof0 == ~uCof1 )
+ {
+ pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+ pCof1 = Cloud_Not( pCof0 );
+ }
+ else
+ {
+ pCof0 = Kit_TruthToCloud5_rec( dd, uCof0, nVars - 1, nVarsAll );
+ pCof1 = Kit_TruthToCloud5_rec( dd, uCof1, nVars - 1, nVarsAll );
+ }
+ return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
+}
+
+/**Function********************************************************************
+
+ Synopsis [Compute BDD for the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+CloudNode * Kit_TruthToCloud_rec( CloudManager * dd, unsigned * pTruth, int nVars, int nVarsAll )
+{
+ CloudNode * pCof0, * pCof1;
+ unsigned * pTruth0, * pTruth1;
+ if ( nVars <= 5 )
+ return Kit_TruthToCloud5_rec( dd, pTruth[0], nVars, nVarsAll );
+ if ( Kit_TruthIsConst0(pTruth, nVars) )
+ return dd->zero;
+ if ( Kit_TruthIsConst1(pTruth, nVars) )
+ return dd->one;
+// Count++;
+ pTruth0 = pTruth;
+ pTruth1 = pTruth + Kit_TruthWordNum(nVars-1);
+ if ( Kit_TruthIsEqual( pTruth0, pTruth1, nVars - 1 ) )
+ return Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+ if ( Kit_TruthIsOpposite( pTruth0, pTruth1, nVars - 1 ) )
+ {
+ pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+ pCof1 = Cloud_Not( pCof0 );
+ }
+ else
+ {
+ pCof0 = Kit_TruthToCloud_rec( dd, pTruth0, nVars - 1, nVarsAll );
+ pCof1 = Kit_TruthToCloud_rec( dd, pTruth1, nVars - 1, nVarsAll );
+ }
+ return Cloud_MakeNode( dd, nVarsAll - nVars, pCof1, pCof0 );
+}
+
+/**Function********************************************************************
+
+ Synopsis [Compute BDD for the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+CloudNode * Kit_TruthToCloud( CloudManager * dd, unsigned * pTruth, int nVars )
+{
+ CloudNode * pRes;
+ pRes = Kit_TruthToCloud_rec( dd, pTruth, nVars, nVars );
+// printf( "%d/%d ", Count, Cloud_DagSize(dd, pRes) );
+ return pRes;
+}
+
+/**Function********************************************************************
+
+ Synopsis [Transforms the array of BDDs into the integer array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Kit_CreateCloud( CloudManager * dd, CloudNode * pFunc, Vec_Int_t * vNodes )
+{
+ Kit_Mux_t Mux;
+ int nNodes, i;
+ // collect BDD nodes
+ nNodes = Cloud_DagCollect( dd, pFunc );
+ if ( nNodes >= (1<<12) ) // because in Kit_Mux_t edge is 12 bit
+ return 0;
+ assert( nNodes == Cloud_DagSize( dd, pFunc ) );
+ assert( nNodes < dd->nNodesLimit );
+ Vec_IntClear( vNodes );
+ Vec_IntPush( vNodes, 0 ); // const1 node
+ dd->ppNodes[0]->s = 0;
+ for ( i = 1; i < nNodes; i++ )
+ {
+ dd->ppNodes[i]->s = i;
+ Mux.v = dd->ppNodes[i]->v;
+ Mux.t = dd->ppNodes[i]->t->s;
+ Mux.e = Cloud_Regular(dd->ppNodes[i]->e)->s;
+ Mux.c = Cloud_IsComplement(dd->ppNodes[i]->e);
+ Mux.i = (i == nNodes - 1)? Cloud_IsComplement(pFunc) : 0;
+ // put the MUX into the array
+ Vec_IntPush( vNodes, *((int *)&Mux) );
+ }
+ assert( Vec_IntSize(vNodes) == nNodes );
+ // reset signatures
+ for ( i = 0; i < nNodes; i++ )
+ dd->ppNodes[i]->s = dd->nSignCur;
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis [Transforms the array of BDDs into the integer array.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+int Kit_CreateCloudFromTruth( CloudManager * dd, unsigned * pTruth, int nVars, Vec_Int_t * vNodes )
+{
+ CloudNode * pFunc;
+ Cloud_Restart( dd );
+ pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
+ Vec_IntClear( vNodes );
+ return Kit_CreateCloud( dd, pFunc, vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes composition of truth tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Kit_CloudToTruth( Vec_Int_t * vNodes, int nVars, Vec_Ptr_t * vStore, int fInv )
+{
+ unsigned * pThis, * pFan0, * pFan1;
+ Kit_Mux_t Mux;
+ int i, Entry;
+ assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
+ pThis = Vec_PtrEntry( vStore, 0 );
+ Kit_TruthFill( pThis, nVars );
+ Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
+ {
+ Mux = *((Kit_Mux_t *)&Entry);
+ assert( (int)Mux.e < i && (int)Mux.t < i && (int)Mux.v < nVars );
+ pFan0 = Vec_PtrEntry( vStore, Mux.e );
+ pFan1 = Vec_PtrEntry( vStore, Mux.t );
+ pThis = Vec_PtrEntry( vStore, i );
+ Kit_TruthMuxVarPhase( pThis, pFan0, pFan1, nVars, fInv? Mux.v : nVars-1-Mux.v, Mux.c );
+ }
+ // complement the result
+ if ( Mux.i )
+ Kit_TruthNot( pThis, pThis, nVars );
+ return pThis;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes composition of truth tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Kit_TruthCompose( CloudManager * dd, unsigned * pTruth, int nVars,
+ unsigned ** pInputs, int nVarsAll, Vec_Ptr_t * vStore, Vec_Int_t * vNodes )
+{
+ CloudNode * pFunc;
+ unsigned * pThis, * pFan0, * pFan1;
+ Kit_Mux_t Mux;
+ int i, Entry, RetValue;
+ // derive BDD from truth table
+ Cloud_Restart( dd );
+ pFunc = Kit_TruthToCloud( dd, pTruth, nVars );
+ // convert it into nodes
+ RetValue = Kit_CreateCloud( dd, pFunc, vNodes );
+ if ( RetValue == 0 )
+ printf( "Kit_TruthCompose(): Internal failure!!!\n" );
+ // verify the result
+// pFan0 = Kit_CloudToTruth( vNodes, nVars, vStore, 0 );
+// if ( !Kit_TruthIsEqual( pTruth, pFan0, nVars ) )
+// printf( "Failed!\n" );
+ // compute truth table from the BDD
+ assert( Vec_IntSize(vNodes) <= Vec_PtrSize(vStore) );
+ pThis = Vec_PtrEntry( vStore, 0 );
+ Kit_TruthFill( pThis, nVarsAll );
+ Vec_IntForEachEntryStart( vNodes, Entry, i, 1 )
+ {
+ Mux = *((Kit_Mux_t *)&Entry);
+ pFan0 = Vec_PtrEntry( vStore, Mux.e );
+ pFan1 = Vec_PtrEntry( vStore, Mux.t );
+ pThis = Vec_PtrEntry( vStore, i );
+ Kit_TruthMuxPhase( pThis, pFan0, pFan1, pInputs[nVars-1-Mux.v], nVarsAll, Mux.c );
+ }
+ // complement the result
+ if ( Mux.i )
+ Kit_TruthNot( pThis, pThis, nVarsAll );
+ return pThis;
+}
+
+/**Function********************************************************************
+
+ Synopsis [Compute BDD for the truth table.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+void Kit_TruthCofSupports( Vec_Int_t * vBddDir, Vec_Int_t * vBddInv, int nVars, Vec_Int_t * vMemory, unsigned * puSupps )
+{
+ Kit_Mux_t Mux;
+ unsigned * puSuppAll, * pThis, * pFan0, * pFan1;
+ int i, v, Var, Entry, nSupps;
+ nSupps = 2 * nVars;
+
+ // extend storage
+ if ( Vec_IntSize( vMemory ) < nSupps * Vec_IntSize(vBddDir) )
+ Vec_IntGrow( vMemory, nSupps * Vec_IntSize(vBddDir) );
+ puSuppAll = Vec_IntArray( vMemory );
+ // clear storage for the const node
+ memset( puSuppAll, 0, sizeof(unsigned) * nSupps );
+ // compute supports from nodes
+ Vec_IntForEachEntryStart( vBddDir, Entry, i, 1 )
+ {
+ Mux = *((Kit_Mux_t *)&Entry);
+ Var = nVars - 1 - Mux.v;
+ pFan0 = puSuppAll + nSupps * Mux.e;
+ pFan1 = puSuppAll + nSupps * Mux.t;
+ pThis = puSuppAll + nSupps * i;
+ for ( v = 0; v < nSupps; v++ )
+ pThis[v] = pFan0[v] | pFan1[v] | (1<<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 ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index 9c61bb6f..ada4ef09 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -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*************************************************************
@@ -1759,6 +1929,26 @@ Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
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.]
+
Description [Uses MUXes to break-down large prime nodes.]
SideEffects []
@@ -1867,7 +2057,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
// recompute the truth table
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
- pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+ pTruthC = Kit_DsdTruthCompute( p, pNtk );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
@@ -1892,7 +2082,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars )
Kit_DsdMan_t * p;
unsigned * pTruthC;
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 );
- pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+ pTruthC = Kit_DsdTruthCompute( p, pNtk );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
@@ -1934,7 +2124,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
// recompute the truth table
p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) );
- pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+ pTruthC = Kit_DsdTruthCompute( p, pNtk );
// Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" );
// Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" );
if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
@@ -2004,7 +2194,7 @@ void Kit_DsdPrecompute4Vars()
*/
p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) );
- pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 );
+ pTruthC = Kit_DsdTruthCompute( p, pNtk );
if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index d196b455..65389ef9 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -901,6 +901,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.]
Description []
@@ -1623,7 +1685,7 @@ char * Kit_TruthDumpToFile( unsigned * pTruth, int nVars, int nFile )
{
static char pFileName[100];
FILE * pFile;
- sprintf( pFileName, "s%03d", nFile );
+ sprintf( pFileName, "tt\\s%04d", nFile );
pFile = fopen( pFileName, "w" );
fprintf( pFile, "rt " );
Extra_PrintHexadecimal( pFile, pTruth, nVars );
diff --git a/src/aig/kit/module.make b/src/aig/kit/module.make
index a01690d0..25c8e767 100644
--- a/src/aig/kit/module.make
+++ b/src/aig/kit/module.make
@@ -1,4 +1,5 @@
SRC += src/aig/kit/kitBdd.c \
+ src/aig/kit/kitCloud.c src/aig/kit/cloud.c \
src/aig/kit/kitDsd.c \
src/aig/kit/kitFactor.c \
src/aig/kit/kitGraph.c \
diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c
index d30198c1..604c5ffa 100644
--- a/src/base/abc/abcRefs.c
+++ b/src/base/abc/abcRefs.c
@@ -45,8 +45,8 @@ static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference );
int Abc_NodeMffcSize( Abc_Obj_t * pNode )
{
int nConeSize1, nConeSize2;
- assert( Abc_NtkIsStrash(pNode->pNtk) );
- assert( !Abc_ObjIsComplement( pNode ) );
+// assert( Abc_NtkIsStrash(pNode->pNtk) );
+// assert( !Abc_ObjIsComplement( pNode ) );
assert( Abc_ObjIsNode( pNode ) );
if ( Abc_ObjFaninNum(pNode) == 0 )
return 0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 22a8ad54..a8888d81 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2979,22 +2979,20 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
-// printf("This command will be available soon\n");
-// return 0;
-
// set defaults
memset( pPars, 0, sizeof(Lpk_Par_t) );
pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure
pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC
pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars)
- pPars->nGrowthLevel = 1; // (L) the maximum number of increased levels
+ pPars->nGrowthLevel = 0; // (L) the maximum number of increased levels
pPars->fSatur = 1;
pPars->fZeroCost = 0;
pPars->fFirst = 0;
+ pPars->fOldAlgo = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfvwh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NQSLszfovwh" ) ) != EOF )
{
switch ( c )
{
@@ -3051,6 +3049,9 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
pPars->fFirst ^= 1;
break;
+ case 'o':
+ pPars->fOldAlgo ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -3074,6 +3075,11 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "This command can only be applied to a logic network.\n" );
return 1;
}
+ if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 3 )
+ {
+ fprintf( pErr, "The number of shared variables (%d) is not in the range 0 <= S <= 3.\n", pPars->nVarsShared );
+ return 1;
+ }
// modify the current network
if ( !Lpk_Resynthesize( pNtk, pPars ) )
@@ -3084,17 +3090,18 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: lutpack [-N <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;
}
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index ecf29f32..47367bc6 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -412,7 +412,7 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry )
SeeAlso []
******************************************************************************/
-static inline Vec_StrBase10Log( unsigned Num )
+static inline int Vec_StrBase10Log( unsigned Num )
{
int Res;
assert( Num >= 0 );
diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h
index f1dcd528..2a642db2 100644
--- a/src/opt/lpk/lpk.h
+++ b/src/opt/lpk/lpk.h
@@ -48,6 +48,7 @@ struct Lpk_Par_t_
int fSatur; // iterate till saturation
int fZeroCost; // accept zero-cost replacements
int fFirst; // use root node and first cut only
+ int fOldAlgo; // use old algorithm
int fVerbose; // the verbosiness flag
int fVeryVerbose; // additional verbose info printout
// internal parameters
diff --git a/src/opt/lpk/lpkAbcDec.c b/src/opt/lpk/lpkAbcDec.c
index e9f8d0df..aa2d4bc0 100644
--- a/src/opt/lpk/lpkAbcDec.c
+++ b/src/opt/lpk/lpkAbcDec.c
@@ -39,17 +39,21 @@
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Lpk_ImplementFun( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
+Abc_Obj_t * Lpk_ImplementFun( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p )
{
extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
unsigned * pTruth;
Abc_Obj_t * pObjNew;
int i;
+ if ( p->fMark )
+ pMan->nMuxes++;
+ else
+ pMan->nDsds++;
// create the new node
pObjNew = Abc_NtkCreateNode( pNtk );
for ( i = 0; i < (int)p->nVars; i++ )
- Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) );
- Abc_ObjLevelNew( pObjNew );
+ Abc_ObjAddFanin( pObjNew, Abc_ObjRegular(Vec_PtrEntry(vLeaves, p->pFanins[i])) );
+ Abc_ObjSetLevel( pObjNew, Abc_ObjLevelNew(pObjNew) );
// assign the node's function
pTruth = Lpk_FunTruth(p, 0);
if ( p->nVars == 0 )
@@ -78,18 +82,48 @@ Abc_Obj_t * Lpk_ImplementFun( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t *
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld )
+Abc_Obj_t * Lpk_Implement_rec( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * pFun )
{
- Lpk_Fun_t * pFun;
- Abc_Obj_t * pRes;
+ Abc_Obj_t * pFanin, * pRes;
int i;
- for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeavesOld; i-- )
+ // prepare the leaves of the function
+ for ( i = 0; i < (int)pFun->nVars; i++ )
{
- pFun = Vec_PtrEntry( vLeaves, i );
- pRes = Lpk_ImplementFun( pNtk, vLeaves, pFun );
- Vec_PtrWriteEntry( vLeaves, i, pRes );
- Lpk_FunFree( pFun );
+ pFanin = Vec_PtrEntry( vLeaves, pFun->pFanins[i] );
+ if ( !Abc_ObjIsComplement(pFanin) )
+ Lpk_Implement_rec( pMan, pNtk, vLeaves, (Lpk_Fun_t *)pFanin );
+ pFanin = Vec_PtrEntry( vLeaves, pFun->pFanins[i] );
+ assert( Abc_ObjIsComplement(pFanin) );
}
+ // construct the function
+ pRes = Lpk_ImplementFun( pMan, pNtk, vLeaves, pFun );
+ // replace the function
+ Vec_PtrWriteEntry( vLeaves, pFun->Id, Abc_ObjNot(pRes) );
+ Lpk_FunFree( pFun );
+ return pRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements the function.]
+
+ Description [Returns the node implementing this function.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Lpk_Implement( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld )
+{
+ Abc_Obj_t * pFanin, * pRes;
+ int i;
+ assert( nLeavesOld < Vec_PtrSize(vLeaves) );
+ // mark implemented nodes
+ Vec_PtrForEachEntryStop( vLeaves, pFanin, i, nLeavesOld )
+ Vec_PtrWriteEntry( vLeaves, i, Abc_ObjNot(pFanin) );
+ // recursively construct starting from the first entry
+ pRes = Lpk_Implement_rec( pMan, pNtk, vLeaves, Vec_PtrEntry( vLeaves, nLeavesOld ) );
Vec_PtrShrink( vLeaves, nLeavesOld );
return pRes;
}
@@ -107,10 +141,13 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld
SeeAlso []
***********************************************************************/
-int Lpk_Decompose_rec( Lpk_Fun_t * p )
+int Lpk_Decompose_rec( Lpk_Man_t * pMan, Lpk_Fun_t * p )
{
+ static Lpk_Res_t Res0, * pRes0 = &Res0;
Lpk_Res_t * pResMux, * pResDsd;
Lpk_Fun_t * p2;
+ int clk;
+
// is only called for non-trivial blocks
assert( p->nLutK >= 3 && p->nLutK <= 6 );
assert( p->nVars > p->nLutK );
@@ -120,18 +157,37 @@ int Lpk_Decompose_rec( Lpk_Fun_t * p )
// skip if delay bound is exceeded
if ( Lpk_SuppDelay(p->uSupp, p->pDelays) > (int)p->nDelayLim )
return 0;
+
+ // compute supports if needed
+ if ( !p->fSupports )
+ Lpk_FunComputeCofSupps( p );
+
+ // check DSD decomposition
+clk = clock();
+ pResDsd = Lpk_DsdAnalize( pMan, p, pMan->pPars->nVarsShared );
+pMan->timeEvalDsdAn += clock() - clk;
+ if ( pResDsd && (pResDsd->nBSVars == (int)p->nLutK || pResDsd->nBSVars == (int)p->nLutK - 1) &&
+ pResDsd->AreaEst <= (int)p->nAreaLim && pResDsd->DelayEst <= (int)p->nDelayLim )
+ {
+clk = clock();
+ p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
+pMan->timeEvalDsdSp += clock() - clk;
+ assert( p2->nVars <= (int)p->nLutK );
+ if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
+ return 0;
+ return 1;
+ }
+
// check MUX decomposition
- pResMux = Lpk_MuxAnalize( p );
+clk = clock();
+ pResMux = Lpk_MuxAnalize( pMan, p );
+pMan->timeEvalMuxAn += clock() - clk;
+// pResMux = NULL;
assert( !pResMux || (pResMux->DelayEst <= (int)p->nDelayLim && pResMux->AreaEst <= (int)p->nAreaLim) );
// accept MUX decomposition if it is "good"
if ( pResMux && pResMux->nSuppSizeS <= (int)p->nLutK && pResMux->nSuppSizeL <= (int)p->nLutK )
pResDsd = NULL;
- else
- {
- pResDsd = Lpk_DsdAnalize( p );
- assert( !pResDsd || (pResDsd->DelayEst <= (int)p->nDelayLim && pResDsd->AreaEst <= (int)p->nAreaLim) );
- }
- if ( pResMux && pResDsd )
+ else if ( pResMux && pResDsd )
{
// compare two decompositions
if ( pResMux->AreaEst < pResDsd->AreaEst ||
@@ -144,18 +200,22 @@ int Lpk_Decompose_rec( Lpk_Fun_t * p )
assert( pResMux == NULL || pResDsd == NULL );
if ( pResMux )
{
- p2 = Lpk_MuxSplit( p, pResMux->pCofVars[0], pResMux->Polarity );
- if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( p2 ) )
+clk = clock();
+ p2 = Lpk_MuxSplit( pMan, p, pResMux->Variable, pResMux->Polarity );
+pMan->timeEvalMuxSp += clock() - clk;
+ if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p2 ) )
return 0;
- if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) )
+ if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
return 0;
return 1;
}
if ( pResDsd )
{
- p2 = Lpk_DsdSplit( p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
+clk = clock();
+ p2 = Lpk_DsdSplit( pMan, p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars );
+pMan->timeEvalDsdSp += clock() - clk;
assert( p2->nVars <= (int)p->nLutK );
- if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) )
+ if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( pMan, p ) )
return 0;
return 1;
}
@@ -193,17 +253,31 @@ void Lpk_DecomposeClean( Vec_Ptr_t * vLeaves, int nLeavesOld )
SeeAlso []
***********************************************************************/
-Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim )
+Abc_Obj_t * Lpk_Decompose( Lpk_Man_t * p, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, unsigned * puSupps, int nLutK, int AreaLim, int DelayLim )
{
Lpk_Fun_t * pFun;
Abc_Obj_t * pObjNew = NULL;
int nLeaves = Vec_PtrSize( vLeaves );
pFun = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
+ if ( puSupps[0] || puSupps[1] )
+ {
+/*
+ int i;
+ Lpk_FunComputeCofSupps( pFun );
+ for ( i = 0; i < nLeaves; i++ )
+ {
+ assert( pFun->puSupps[2*i+0] == puSupps[2*i+0] );
+ assert( pFun->puSupps[2*i+1] == puSupps[2*i+1] );
+ }
+*/
+ memcpy( pFun->puSupps, puSupps, sizeof(unsigned) * 2 * nLeaves );
+ pFun->fSupports = 1;
+ }
Lpk_FunSuppMinimize( pFun );
if ( pFun->nVars <= pFun->nLutK )
- pObjNew = Lpk_ImplementFun( pNtk, vLeaves, pFun );
- else if ( Lpk_Decompose_rec(pFun) )
- pObjNew = Lpk_Implement( pNtk, vLeaves, nLeaves );
+ pObjNew = Lpk_ImplementFun( p, pNtk, vLeaves, pFun );
+ else if ( Lpk_Decompose_rec(p, pFun) )
+ pObjNew = Lpk_Implement( p, pNtk, vLeaves, nLeaves );
Lpk_DecomposeClean( vLeaves, nLeaves );
return pObjNew;
}
diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c
index f2e19945..f4095914 100644
--- a/src/opt/lpk/lpkAbcDsd.c
+++ b/src/opt/lpk/lpkAbcDsd.c
@@ -41,27 +41,37 @@
SeeAlso []
***********************************************************************/
-int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs )
+int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs, unsigned uNonDecSupp )
{
int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur;
assert( nTruths > 0 );
VarBest = -1;
Lpk_SuppForEachVar( p->uSupp, Var )
{
+ if ( (uNonDecSupp & (1 << Var)) == 0 )
+ continue;
nSuppMaxCur = 0;
nSuppTotalCur = 0;
for ( i = 0; i < nTruths; i++ )
{
- Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
- Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
- nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
- nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
+ if ( nTruths == 1 )
+ {
+ nSuppSize0 = Kit_WordCountOnes( p->puSupps[2*Var+0] );
+ nSuppSize1 = Kit_WordCountOnes( p->puSupps[2*Var+1] );
+ }
+ else
+ {
+ Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var );
+ Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var );
+ nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars );
+ nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars );
+ }
nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 );
nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 );
nSuppTotalCur += nSuppSize0 + nSuppSize1;
}
- if ( VarBest == -1 || nSuppTotalMin > nSuppTotalCur ||
- (nSuppTotalMin == nSuppTotalCur && nSuppMaxMin > nSuppMaxCur) )
+ if ( VarBest == -1 || nSuppMaxMin > nSuppMaxCur ||
+ (nSuppMaxMin == nSuppMaxCur && nSuppTotalMin > nSuppTotalCur) )
{
VarBest = Var;
nSuppMaxMin = nSuppMaxCur;
@@ -175,6 +185,49 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax )
/**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.]
Description []
@@ -196,7 +249,7 @@ 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;
@@ -204,7 +257,7 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSiz
/**Function*************************************************************
- Synopsis [Allocates truth tables for cofactors.]
+ Synopsis [Performs DSD-based decomposition of the function.]
Description []
@@ -213,39 +266,69 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSiz
SeeAlso []
***********************************************************************/
-void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
+void Lpk_FunCompareBoundSets( Lpk_Fun_t * p, Vec_Int_t * vBSets, int nCofDepth, unsigned uNonDecSupp, unsigned uLateArrSupp, Lpk_Res_t * pRes )
{
- int i;
- assert( nCofDepth <= 4 );
- ppTruths[0][0] = Lpk_FunTruth( p, 0 );
- if ( nCofDepth >= 1 )
- {
- ppTruths[1][0] = Lpk_FunTruth( p, 1 );
- ppTruths[1][1] = Lpk_FunTruth( p, 2 );
- }
- if ( nCofDepth >= 2 )
- {
- ppTruths[2][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 4 );
- for ( i = 1; i < 4; i++ )
- ppTruths[2][i] = ppTruths[2][0] + Kit_TruthWordNum(p->nVars) * i;
- }
- if ( nCofDepth >= 3 )
+ int fVerbose = 0;
+ unsigned uBoundSet;
+ int i, nVarsBS, nVarsRem, Delay, Area;
+
+ // compare the resulting boundsets
+ memset( pRes, 0, sizeof(Lpk_Res_t) );
+ Vec_IntForEachEntry( vBSets, uBoundSet, i )
{
- ppTruths[3][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 8 );
- for ( i = 1; i < 8; i++ )
- ppTruths[3][i] = ppTruths[3][0] + Kit_TruthWordNum(p->nVars) * i;
+ if ( (uBoundSet & 0xFFFF) == 0 ) // skip empty boundset
+ continue;
+ if ( (uBoundSet & uNonDecSupp) == 0 ) // skip those boundsets that are not in the domain of interest
+ continue;
+ if ( (uBoundSet & uLateArrSupp) ) // skip those boundsets that are late arriving
+ continue;
+if ( fVerbose )
+Lpk_PrintSetOne( uBoundSet );
+ assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
+ nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
+ if ( nVarsBS == 1 )
+ continue;
+ assert( nVarsBS <= (int)p->nLutK - nCofDepth );
+ nVarsRem = p->nVars - nVarsBS + 1;
+ Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
+ Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
+if ( fVerbose )
+printf( "area = %d limit = %d delay = %d limit = %d\n", Area, (int)p->nAreaLim, Delay, (int)p->nDelayLim );
+ if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
+ continue;
+ if ( pRes->BSVars == 0 || pRes->nSuppSizeL > nVarsRem || (pRes->nSuppSizeL == nVarsRem && pRes->DelayEst > Delay) )
+ {
+ pRes->nBSVars = nVarsBS;
+ pRes->BSVars = (uBoundSet & 0xFFFF);
+ pRes->nSuppSizeS = nVarsBS + nCofDepth;
+ pRes->nSuppSizeL = nVarsRem;
+ pRes->DelayEst = Delay;
+ pRes->AreaEst = Area;
+ }
}
- if ( nCofDepth >= 4 )
+if ( fVerbose )
+{
+if ( pRes->BSVars )
+{
+printf( "Found bound set " );
+Lpk_PrintSetOne( pRes->BSVars );
+printf( "\n" );
+}
+else
+printf( "Did not find boundsets.\n" );
+printf( "\n" );
+}
+ if ( pRes->BSVars )
{
- ppTruths[4][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 16 );
- for ( i = 1; i < 16; i++ )
- ppTruths[4][i] = ppTruths[4][0] + Kit_TruthWordNum(p->nVars) * i;
+ assert( pRes->DelayEst <= (int)p->nDelayLim );
+ assert( pRes->AreaEst <= (int)p->nAreaLim );
}
}
+
/**Function*************************************************************
- Synopsis [Allocates truth tables for cofactors.]
+ Synopsis [Finds late arriving inputs, which cannot be in the bound set.]
Description []
@@ -254,14 +337,13 @@ void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[
SeeAlso []
***********************************************************************/
-void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] )
+unsigned Lpk_DsdLateArriving( Lpk_Fun_t * p )
{
- if ( nCofDepth >= 2 )
- free( ppTruths[2][0] );
- if ( nCofDepth >= 3 )
- free( ppTruths[3][0] );
- if ( nCofDepth >= 4 )
- free( ppTruths[4][0] );
+ unsigned i, uLateArrSupp = 0;
+ Lpk_SuppForEachVar( p->uSupp, i )
+ if ( p->pDelays[i] > (int)p->nDelayLim - 2 )
+ uLateArrSupp |= (1 << i);
+ return uLateArrSupp;
}
/**Function*************************************************************
@@ -275,58 +357,73 @@ void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5
SeeAlso []
***********************************************************************/
-void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes )
+int Lpk_DsdAnalizeOne( Lpk_Fun_t * p, unsigned * ppTruths[5][16], Kit_DsdNtk_t * pNtks[], char pCofVars[], int nCofDepth, Lpk_Res_t * pRes )
{
- unsigned * ppTruths[5][16];
+ int fVerbose = 0;
Vec_Int_t * pvBSets[4][8];
- Kit_DsdNtk_t * pNtkDec, * pTemp;
- unsigned uBoundSet;
- int i, k, nVarsBS, nVarsRem, Delay, Area;
- assert( nCofDepth >= 0 && nCofDepth < 4 );
+ unsigned uNonDecSupp, uLateArrSupp;
+ int i, k, nNonDecSize, nNonDecSizeMax;
+ assert( nCofDepth >= 1 && nCofDepth <= 3 );
assert( nCofDepth < (int)p->nLutK - 1 );
- Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths );
- // find the best cofactors
- memset( pRes, 0, sizeof(Lpk_Res_t) );
- pRes->nCofVars = nCofDepth;
- for ( i = 0; i < nCofDepth; i++ )
- pRes->pCofVars[i] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[i], 1<<i, ppTruths[i+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++ )
{
- 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 );
+ 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 the resulting boundsets
- Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i )
+ // compare bound-sets
+ Lpk_FunCompareBoundSets( p, pvBSets[0][0], nCofDepth, uNonDecSupp, uLateArrSupp, pRes );
+ // free the bound sets
+ for ( i = nCofDepth; i >= 0; i-- )
+ for ( k = 0; k < (1<<i); k++ )
+ Vec_IntFree( pvBSets[i][k] );
+
+ // copy the cofactoring variables
+ if ( pRes->BSVars )
{
- if ( uBoundSet == 0 )
- continue;
- assert( (uBoundSet & (uBoundSet >> 16)) == 0 );
- nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF );
- assert( nVarsBS <= (int)p->nLutK - nCofDepth );
- nVarsRem = p->nVars - nVarsBS + nCofDepth + 1;
- Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK );
- Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays );
- if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim )
- continue;
- if ( pRes->BSVars == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem )
- {
- pRes->nBSVars = nVarsBS;
- pRes->BSVars = uBoundSet;
- pRes->nSuppSizeS = nVarsBS;
- pRes->nSuppSizeL = nVarsRem;
- pRes->DelayEst = Delay;
- pRes->AreaEst = Area;
- }
+ pRes->nCofVars = nCofDepth;
+ for ( i = 0; i < nCofDepth; i++ )
+ pRes->pCofVars[i] = pCofVars[i];
}
- // free cofactor storage
- Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths );
+ return 1;
}
/**Function*************************************************************
@@ -340,47 +437,105 @@ void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes )
SeeAlso []
***********************************************************************/
-Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p )
-{
+Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared )
+{
static Lpk_Res_t Res0, * pRes0 = &Res0;
static Lpk_Res_t Res1, * pRes1 = &Res1;
static Lpk_Res_t Res2, * pRes2 = &Res2;
static Lpk_Res_t Res3, * pRes3 = &Res3;
- memset( pRes0, 0, sizeof(Lpk_Res_t) );
- memset( pRes1, 0, sizeof(Lpk_Res_t) );
- memset( pRes2, 0, sizeof(Lpk_Res_t) );
- memset( pRes3, 0, sizeof(Lpk_Res_t) );
+ int fUseBackLooking = 1;
+ Lpk_Res_t * pRes = NULL;
+ Vec_Int_t * vBSets;
+ Kit_DsdNtk_t * pNtks[8] = {NULL};
+ char pCofVars[5];
+ int i;
+
+ assert( p->nLutK >= 3 );
+ assert( nShared >= 0 && nShared <= 3 );
assert( p->uSupp == Kit_BitMask(p->nVars) );
// try decomposition without cofactoring
- Lpk_DsdAnalizeOne( p, 0, pRes0 );
- if ( pRes0->nBSVars == (int)p->nLutK && pRes0->AreaEst <= (int)p->nAreaLim && pRes0->DelayEst <= (int)p->nDelayLim )
- return pRes0;
+ pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars );
+ if ( pMan->pPars->fVerbose )
+ pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++;
+ vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK );
+ Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 );
+ Vec_IntFree( vBSets );
+
+ // check the result
+ if ( pRes0->nBSVars == (int)p->nLutK )
+ { pRes = pRes0; goto finish; }
+ if ( pRes0->nBSVars == (int)p->nLutK - 1 )
+ { pRes = pRes0; goto finish; }
+ if ( nShared == 0 )
+ goto finish;
+
+ // prepare storage
+ Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars );
// cofactor 1 time
- if ( p->nLutK >= 3 )
- Lpk_DsdAnalizeOne( p, 1, pRes1 );
+ if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) )
+ goto finish;
assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
- if ( pRes1->nBSVars == (int)p->nLutK - 1 && pRes1->AreaEst <= (int)p->nAreaLim && pRes1->DelayEst <= (int)p->nDelayLim )
- return pRes1;
+ if ( pRes1->nBSVars == (int)p->nLutK - 1 )
+ { pRes = pRes1; goto finish; }
+ if ( pRes0->nBSVars == (int)p->nLutK - 2 )
+ { pRes = pRes0; goto finish; }
+ if ( pRes1->nBSVars == (int)p->nLutK - 2 )
+ { pRes = pRes1; goto finish; }
+ if ( nShared == 1 )
+ goto finish;
// cofactor 2 times
if ( p->nLutK >= 4 )
- Lpk_DsdAnalizeOne( p, 2, pRes2 );
- assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
- if ( pRes2->nBSVars == (int)p->nLutK - 2 && pRes2->AreaEst <= (int)p->nAreaLim && pRes2->DelayEst <= (int)p->nDelayLim )
- return pRes2;
+ {
+ if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) )
+ goto finish;
+ assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
+ if ( pRes2->nBSVars == (int)p->nLutK - 2 )
+ { pRes = pRes2; goto finish; }
+ if ( fUseBackLooking )
+ {
+ if ( pRes0->nBSVars == (int)p->nLutK - 3 )
+ { pRes = pRes0; goto finish; }
+ if ( pRes1->nBSVars == (int)p->nLutK - 3 )
+ { pRes = pRes1; goto finish; }
+ }
+ if ( pRes2->nBSVars == (int)p->nLutK - 3 )
+ { pRes = pRes2; goto finish; }
+ if ( nShared == 2 )
+ goto finish;
+ assert( nShared == 3 );
+ }
// cofactor 3 times
if ( p->nLutK >= 5 )
- Lpk_DsdAnalizeOne( p, 3, pRes3 );
- assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
- if ( pRes3->nBSVars == (int)p->nLutK - 3 && pRes3->AreaEst <= (int)p->nAreaLim && pRes3->DelayEst <= (int)p->nDelayLim )
- return pRes3;
+ {
+ if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) )
+ goto finish;
+ assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
+ if ( pRes3->nBSVars == (int)p->nLutK - 3 )
+ { pRes = pRes3; goto finish; }
+ if ( fUseBackLooking )
+ {
+ if ( pRes0->nBSVars == (int)p->nLutK - 4 )
+ { pRes = pRes0; goto finish; }
+ if ( pRes1->nBSVars == (int)p->nLutK - 4 )
+ { pRes = pRes1; goto finish; }
+ if ( pRes2->nBSVars == (int)p->nLutK - 4 )
+ { pRes = pRes2; goto finish; }
+ }
+ if ( pRes3->nBSVars == (int)p->nLutK - 4 )
+ { pRes = pRes3; goto finish; }
+ }
+finish:
+ // free the networks
+ for ( i = 0; i < (1<<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;
}
diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c
index 159cae96..d6f579ee 100644
--- a/src/opt/lpk/lpkAbcMux.c
+++ b/src/opt/lpk/lpkAbcMux.c
@@ -30,51 +30,6 @@
/**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.]
Description [Returns the best variable to use for 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;
}
diff --git a/src/opt/lpk/lpkAbcUtil.c b/src/opt/lpk/lpkAbcUtil.c
index 681ec092..3f917ce2 100644
--- a/src/opt/lpk/lpkAbcUtil.c
+++ b/src/opt/lpk/lpkAbcUtil.c
@@ -123,7 +123,7 @@ Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth )
memcpy( pNew->pFanins, p->pFanins, 16 );
memcpy( pNew->pDelays, p->pDelays, 16 );
Vec_PtrPush( p->vNodes, pNew );
- return p;
+ return pNew;
}
/**Function*************************************************************
@@ -137,12 +137,15 @@ Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth )
SeeAlso []
***********************************************************************/
-void Lpk_FunSuppMinimize( Lpk_Fun_t * p )
+int Lpk_FunSuppMinimize( Lpk_Fun_t * p )
{
int i, k, nVarsNew;
// compress the truth table
if ( p->uSupp == Kit_BitMask(p->nVars) )
- return;
+ return 0;
+ // invalidate support info
+ p->fSupports = 0;
+//Extra_PrintBinary( stdout, &p->uSupp, p->nVars ); printf( "\n" );
// minimize support
nVarsNew = Kit_WordCountOnes(p->uSupp);
Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
@@ -151,11 +154,48 @@ void Lpk_FunSuppMinimize( Lpk_Fun_t * p )
{
p->pFanins[k] = p->pFanins[i];
p->pDelays[k] = p->pDelays[i];
+/*
+ if ( p->fSupports )
+ {
+ p->puSupps[2*k+0] = p->puSupps[2*i+0];
+ p->puSupps[2*k+1] = p->puSupps[2*i+1];
+ }
+*/
k++;
}
assert( k == nVarsNew );
p->nVars = k;
p->uSupp = Kit_BitMask(p->nVars);
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes cofactors w.r.t. each variable.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_FunComputeCofSupps( Lpk_Fun_t * p )
+{
+ unsigned * pTruth = Lpk_FunTruth( p, 0 );
+ unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
+ unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
+ int Var;
+ assert( p->fSupports == 0 );
+// Lpk_SuppForEachVar( p->uSupp, Var )
+ for ( Var = 0; Var < (int)p->nVars; Var++ )
+ {
+ Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
+ Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
+ p->puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
+ p->puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
+ }
+ p->fSupports = 1;
}
/**Function*************************************************************
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 37bfd956..6ea975aa 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "lpkInt.h"
+#include "cloud.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -127,6 +128,7 @@ int Lpk_ExploreCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk )
If_Obj_t * pDriver, * ppLeaves[16];
Abc_Obj_t * pLeaf, * pObjNew;
int nGain, i, clk;
+ int nNodesBef;
// int nOldShared;
// check special cases
@@ -201,6 +203,7 @@ p->timeMap += clock() - clk;
if ( p->nCalledSRed )
p->nBenefited++;
+ nNodesBef = Abc_NtkNodeNum(p->pNtk);
// prepare the mapping manager
If_ManCleanNodeCopy( p->pIfMan );
If_ManCleanCutData( p->pIfMan );
@@ -212,6 +215,7 @@ p->timeMap += clock() - clk;
pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) );
// perform replacement
Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+//printf( "%3d : %d-%d=%d(%d) \n", p->nChanges, nNodesBef, Abc_NtkNodeNum(p->pNtk), nNodesBef-Abc_NtkNodeNum(p->pNtk), nGain );
return 1;
}
@@ -232,8 +236,7 @@ int Lpk_ResynthesizeNode( Lpk_Man_t * p )
Kit_DsdNtk_t * pDsdNtk;
Lpk_Cut_t * pCut;
unsigned * pTruth;
- void * pDsd = NULL;
- int i, nSuppSize, RetValue, clk;
+ int i, k, nSuppSize, nCutNodes, RetValue, clk;
// compute the cuts
clk = clock();
@@ -258,9 +261,22 @@ p->timeCuts += clock() - clk;
if ( p->pPars->fFirst && i == 1 )
break;
+ // skip bad cuts
+// printf( "Mffc size = %d. ", Abc_NodeMffcLabel(p->pObj) );
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize++;
+ nCutNodes = Abc_NodeMffcLabel(p->pObj);
+// printf( "Mffc with cut = %d. ", nCutNodes );
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize--;
+// printf( "Mffc cut = %d. ", (int)pCut->nNodes - (int)pCut->nNodesDup );
+// printf( "\n" );
+ if ( nCutNodes != (int)pCut->nNodes - (int)pCut->nNodesDup )
+ continue;
+
// compute the truth table
clk = clock();
- pTruth = Lpk_CutTruth( p, pCut );
+ pTruth = Lpk_CutTruth( p, pCut, 0 );
nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves);
p->timeTruth += clock() - clk;
@@ -289,7 +305,7 @@ p->timeTruth += clock() - clk;
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
Kit_DsdPrint( stdout, pDsdNtk );
-// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
+ Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
// pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
// printf( "Saved truth table in file \"%s\".\n", pFileName );
}
@@ -305,6 +321,32 @@ p->timeEval += clock() - clk;
return 1;
}
+
+/**Function*************************************************************
+
+ Synopsis [Computes supports of the cofactors of the function.]
+
+ Description [This procedure should be called after Lpk_CutTruth(p,pCut,0)]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Lpk_ComputeSupports( Lpk_Man_t * p, Lpk_Cut_t * pCut, unsigned * pTruth )
+{
+ unsigned * pTruthInv;
+ int RetValue1, RetValue2;
+ pTruthInv = Lpk_CutTruth( p, pCut, 1 );
+ RetValue1 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruth, pCut->nLeaves, p->vBddDir );
+ RetValue2 = Kit_CreateCloudFromTruth( p->pDsdMan->dd, pTruthInv, pCut->nLeaves, p->vBddInv );
+ if ( RetValue1 && RetValue2 )
+ Kit_TruthCofSupports( p->vBddDir, p->vBddInv, pCut->nLeaves, p->vMemory, p->puSupps );
+ else
+ p->puSupps[0] = p->puSupps[1] = 0;
+}
+
+
/**Function*************************************************************
Synopsis [Performs resynthesis for one node.]
@@ -319,12 +361,13 @@ p->timeEval += clock() - clk;
int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p )
{
static int Count = 0;
- Vec_Ptr_t * vLeaves;
- Abc_Obj_t * pObjNew;
+ Abc_Obj_t * pObjNew, * pLeaf;
Lpk_Cut_t * pCut;
unsigned * pTruth;
- void * pDsd = NULL;
+ int nNodesBef, nNodesAft, nCutNodes;
int i, k, clk;
+ int Required = Abc_ObjRequiredLevel(p->pObj);
+// CloudNode * pFun2;//, * pFun1;
// compute the cuts
clk = clock();
@@ -336,8 +379,8 @@ p->timeCuts += clock() - clk;
p->timeCuts += clock() - clk;
if ( p->pPars->fVeryVerbose )
- printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals );
- vLeaves = Vec_PtrAlloc( 32 );
+ printf( "Node %5d : Mffc size = %5d. Cuts = %5d. Level = %2d. Req = %2d.\n",
+ p->pObj->Id, p->nMffc, p->nEvals, p->pObj->Level, Required );
// try the good cuts
p->nCutsTotal += p->nCuts;
p->nCutsUseful += p->nEvals;
@@ -347,16 +390,48 @@ p->timeCuts += clock() - clk;
pCut = p->pCuts + p->pEvals[i];
if ( p->pPars->fFirst && i == 1 )
break;
+// if ( pCut->Weight < 1.05 )
+// continue;
+
+ // skip bad cuts
+// printf( "Mffc size = %d. ", Abc_NodeMffcLabel(p->pObj) );
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize++;
+ nCutNodes = Abc_NodeMffcLabel(p->pObj);
+// printf( "Mffc with cut = %d. ", nCutNodes );
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ Abc_NtkObj(p->pNtk, pCut->pLeaves[k])->vFanouts.nSize--;
+// printf( "Mffc cut = %d. ", (int)pCut->nNodes - (int)pCut->nNodesDup );
+// printf( "\n" );
+ if ( nCutNodes != (int)pCut->nNodes - (int)pCut->nNodesDup )
+ continue;
// collect nodes into the array
- Vec_PtrClear( vLeaves );
+ Vec_PtrClear( p->vLeaves );
for ( k = 0; k < (int)pCut->nLeaves; k++ )
- Vec_PtrPush( vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[i]) );
+ Vec_PtrPush( p->vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[k]) );
// compute the truth table
clk = clock();
- pTruth = Lpk_CutTruth( p, pCut );
+ pTruth = Lpk_CutTruth( p, pCut, 0 );
p->timeTruth += clock() - clk;
+clk = clock();
+ Lpk_ComputeSupports( p, pCut, pTruth );
+p->timeSupps += clock() - clk;
+//clk = clock();
+// pFun1 = Lpk_CutTruthBdd( p, pCut );
+//p->timeTruth2 += clock() - clk;
+/*
+clk = clock();
+ Cloud_Restart( p->pDsdMan->dd );
+ pFun2 = Kit_TruthToCloud( p->pDsdMan->dd, pTruth, pCut->nLeaves );
+ RetValue = Kit_CreateCloud( p->pDsdMan->dd, pFun2, p->vBddNodes );
+p->timeTruth3 += clock() - clk;
+*/
+// if ( pFun1 != pFun2 )
+// printf( "Truth tables do not agree!\n" );
+// else
+// printf( "Fine!\n" );
if ( p->pPars->fVeryVerbose )
{
@@ -364,22 +439,51 @@ p->timeTruth += clock() - clk;
int nSuppSize = Extra_TruthSupportSize( pTruth, pCut->nLeaves );
printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ",
i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight );
+ Vec_PtrForEachEntry( p->vLeaves, pLeaf, k )
+ printf( "%c=%d ", 'a'+k, Abc_ObjLevel(pLeaf) );
+ printf( "\n" );
Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves );
// pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ );
// printf( "Saved truth table in file \"%s\".\n", pFileName );
}
+ if ( p->pObj->Id == 33 && i == 0 )
+ {
+ int x = 0;
+ }
// update the network
+ nNodesBef = Abc_NtkNodeNum(p->pNtk);
clk = clock();
- pObjNew = Lpk_Decompose( p->pNtk, vLeaves, pTruth, p->pPars->nLutSize,
- (int)pCut->nNodes - (int)pCut->nNodesDup - 1, Abc_ObjRequiredLevel(p->pObj) );
+ pObjNew = Lpk_Decompose( p, p->pNtk, p->vLeaves, pTruth, p->puSupps, p->pPars->nLutSize,
+ (int)pCut->nNodes - (int)pCut->nNodesDup - 1 + (int)(p->pPars->fZeroCost > 0), Required );
p->timeEval += clock() - clk;
+ nNodesAft = Abc_NtkNodeNum(p->pNtk);
// perform replacement
if ( pObjNew )
+ {
+ int nGain = (int)pCut->nNodes - (int)pCut->nNodesDup - (nNodesAft - nNodesBef);
+ assert( nGain >= 1 - p->pPars->fZeroCost );
+ assert( Abc_ObjLevel(pObjNew) <= Required );
+/*
+ if ( nGain <= 0 )
+ {
+ int x = 0;
+ }
+ if ( Abc_ObjLevel(pObjNew) > Required )
+ {
+ int x = 0;
+ }
+*/
+ p->nGainTotal += nGain;
+ p->nChanges++;
+ if ( p->pPars->fVeryVerbose )
+ printf( "Performed resynthesis: Gain = %2d. Level = %2d. Req = %2d.\n", nGain, Abc_ObjLevel(pObjNew), Required );
Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels );
+//printf( "%3d : %d-%d=%d(%d) \n", p->nChanges, nNodesBef, Abc_NtkNodeNum(p->pNtk), nNodesBef-Abc_NtkNodeNum(p->pNtk), nGain );
+ break;
+ }
}
- Vec_PtrFree( vLeaves );
return 1;
}
@@ -443,7 +547,10 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
if ( p->pPars->fSatur )
p->vVisited = Vec_VecStart( 0 );
if ( pPars->fVerbose )
+ {
p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
+ p->nTotalNodes = Abc_NtkNodeNum(pNtk);
+ }
// iterate over the network
nNodesPrev = p->nNodesTotal;
@@ -465,7 +572,6 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) )
continue;
}
-
if ( i >= nNodes )
break;
if ( !pPars->fVeryVerbose )
@@ -475,10 +581,10 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
continue;
// resynthesize
p->pObj = pObj;
- Lpk_ResynthesizeNode( p );
-
-// if ( p->nChanges == 3 )
-// break;
+ if ( p->pPars->fOldAlgo )
+ Lpk_ResynthesizeNode( p );
+ else
+ Lpk_ResynthesizeNodeNew( p );
}
if ( !pPars->fVeryVerbose )
Extra_ProgressBarStop( pProgress );
@@ -498,15 +604,18 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
if ( pPars->fVerbose )
{
+// Cloud_PrintInfo( p->pDsdMan->dd );
p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
- printf( "Reduction in nodes = %5d. (%.2f %%) ",
- p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal );
- printf( "Reduction in edges = %5d. (%.2f %%) ",
+ p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
+ printf( "Node gain = %5d. (%.2f %%) ",
+ p->nTotalNodes-p->nTotalNodes2, 100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
+ printf( "Edge gain = %5d. (%.2f %%) ",
p->nTotalNets-p->nTotalNets2, 100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
+ printf( "Muxes = %4d. Dsds = %4d.", p->nMuxes, p->nDsds );
printf( "\n" );
-
printf( "Nodes = %5d (%3d) Cuts = %5d (%4d) Changes = %5d Iter = %2d Benefit = %d.\n",
p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, Iter, p->nBenefited );
+
printf( "Non-DSD:" );
for ( i = 3; i <= pPars->nVarsMax; i++ )
if ( p->nBlocks[i] )
@@ -518,7 +627,13 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap;
PRTP( "Cuts ", p->timeCuts, p->timeTotal );
PRTP( "Truth ", p->timeTruth, p->timeTotal );
+ PRTP( "CSupps", p->timeSupps, p->timeTotal );
PRTP( "Eval ", p->timeEval, p->timeTotal );
+ PRTP( " MuxAn", p->timeEvalMuxAn, p->timeEval );
+ PRTP( " MuxSp", p->timeEvalMuxSp, p->timeEval );
+ PRTP( " DsdAn", p->timeEvalDsdAn, p->timeEval );
+ PRTP( " DsdSp", p->timeEvalDsdSp, p->timeEval );
+ PRTP( " Other", p->timeEval-p->timeEvalMuxAn-p->timeEvalMuxSp-p->timeEvalDsdAn-p->timeEvalDsdSp, p->timeEval );
PRTP( "Map ", p->timeMap, p->timeTotal );
PRTP( "Other ", p->timeOther, p->timeTotal );
PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index f5c0c66c..b2a743bd 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "lpkInt.h"
+#include "cloud.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -39,7 +40,99 @@
SeeAlso []
***********************************************************************/
-unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount )
+CloudNode * Lpk_CutTruthBdd_rec( CloudManager * dd, Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars )
+{
+ CloudNode * pTruth, * pTruth0, * pTruth1;
+ assert( !Hop_IsComplement(pObj) );
+ if ( pObj->pData )
+ {
+ assert( ((unsigned)pObj->pData) & 0xffff0000 );
+ return pObj->pData;
+ }
+ // get the plan for a new truth table
+ if ( Hop_ObjIsConst1(pObj) )
+ pTruth = dd->one;
+ else
+ {
+ assert( Hop_ObjIsAnd(pObj) );
+ // compute the truth tables of the fanins
+ pTruth0 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin0(pObj), nVars );
+ pTruth1 = Lpk_CutTruthBdd_rec( dd, pMan, Hop_ObjFanin1(pObj), nVars );
+ pTruth0 = Cloud_NotCond( pTruth0, Hop_ObjFaninC0(pObj) );
+ pTruth1 = Cloud_NotCond( pTruth1, Hop_ObjFaninC1(pObj) );
+ // creat the truth table of the node
+ pTruth = Cloud_bddAnd( dd, pTruth0, pTruth1 );
+ }
+ pObj->pData = pTruth;
+ return pTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Verifies that the factoring is correct.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+CloudNode * Lpk_CutTruthBdd( Lpk_Man_t * p, Lpk_Cut_t * pCut )
+{
+ CloudManager * dd = p->pDsdMan->dd;
+ Hop_Man_t * pManHop = p->pNtk->pManFunc;
+ Hop_Obj_t * pObjHop;
+ Abc_Obj_t * pObj, * pFanin;
+ CloudNode * pTruth;
+ int i, k, iCount = 0;
+
+// return NULL;
+// Lpk_NodePrintCut( p, pCut );
+ // initialize the leaves
+ Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)dd->vars[pCut->nLeaves-1-i];
+
+ // construct truth table in the topological order
+ Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
+ {
+ // get the local AIG
+ pObjHop = Hop_Regular(pObj->pData);
+ // clean the data field of the nodes in the AIG subgraph
+ Hop_ObjCleanData_rec( pObjHop );
+ // set the initial truth tables at the fanins
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ {
+ assert( ((unsigned)pFanin->pCopy) & 0xffff0000 );
+ Hop_ManPi( pManHop, k )->pData = pFanin->pCopy;
+ }
+ // compute the truth table of internal nodes
+ pTruth = Lpk_CutTruthBdd_rec( dd, pManHop, pObjHop, pCut->nLeaves );
+ if ( Hop_IsComplement(pObj->pData) )
+ pTruth = Cloud_Not(pTruth);
+ // set the truth table at the node
+ pObj->pCopy = (Abc_Obj_t *)pTruth;
+
+ }
+
+// Cloud_bddPrint( dd, pTruth );
+// printf( "Bdd size = %d. Total nodes = %d.\n", Cloud_DagSize( dd, pTruth ), dd->nNodesCur-dd->nVars-1 );
+ return pTruth;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth table of one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * piCount )
{
unsigned * pTruth, * pTruth0, * pTruth1;
assert( !Hop_IsComplement(pObj) );
@@ -49,17 +142,17 @@ unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_
return pObj->pData;
}
// get the plan for a new truth table
- pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ );
+ pTruth = Vec_PtrEntry( vTtNodes, (*piCount)++ );
if ( Hop_ObjIsConst1(pObj) )
- Extra_TruthFill( pTruth, nVars );
+ Kit_TruthFill( pTruth, nVars );
else
{
assert( Hop_ObjIsAnd(pObj) );
// compute the truth tables of the fanins
- pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount );
- pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount );
+ pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, piCount );
+ pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, piCount );
// creat the truth table of the node
- Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
+ Kit_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) );
}
pObj->pData = pTruth;
return pTruth;
@@ -76,7 +169,7 @@ unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_
SeeAlso []
***********************************************************************/
-unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
+unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv )
{
Hop_Man_t * pManHop = p->pNtk->pManFunc;
Hop_Obj_t * pObjHop;
@@ -84,10 +177,11 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
unsigned * pTruth;
int i, k, iCount = 0;
// Lpk_NodePrintCut( p, pCut );
+ assert( pCut->nNodes > 0 );
// initialize the leaves
Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
- pObj->pCopy = Vec_PtrEntry( p->vTtElems, i );
+ pObj->pCopy = Vec_PtrEntry( p->vTtElems, fInv? pCut->nLeaves-1-i : i );
// construct truth table in the topological order
Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
@@ -105,14 +199,22 @@ unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut )
// compute the truth table of internal nodes
pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount );
if ( Hop_IsComplement(pObj->pData) )
- Extra_TruthNot( pTruth, pTruth, pCut->nLeaves );
+ Kit_TruthNot( pTruth, pTruth, pCut->nLeaves );
// set the truth table at the node
pObj->pCopy = (Abc_Obj_t *)pTruth;
}
+ // make sure direct truth table is stored elsewhere (assuming the first call for direct truth!!!)
+ if ( fInv == 0 )
+ {
+ pTruth = Vec_PtrEntry( p->vTtNodes, iCount++ );
+ Kit_TruthCopy( pTruth, (unsigned *)pObj->pCopy, pCut->nLeaves );
+ }
+ assert( iCount <= Vec_PtrSize(p->vTtNodes) );
return pTruth;
}
+
/**Function*************************************************************
Synopsis [Returns 1 if at least one entry has changed.]
@@ -535,8 +637,10 @@ int Lpk_NodeCuts( Lpk_Man_t * p )
// compute the minimum number of LUTs needed to implement this cut
// V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0]
pCut->nLuts = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize );
+// pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup - 1) / pCut->nLuts; //p->pPars->nLutsMax;
pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
if ( pCut->Weight <= 1.001 )
+// if ( pCut->Weight <= 0.999 )
continue;
pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut );
if ( pCut->fHasDsd )
diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h
index 32fb05b3..960599e4 100644
--- a/src/opt/lpk/lpkInt.h
+++ b/src/opt/lpk/lpkInt.h
@@ -90,12 +90,18 @@ struct Lpk_Man_t_
int nCalledSRed; // the number of called to SRed
int pRefs[LPK_SIZE_MAX]; // fanin reference counters
int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves
+ Vec_Ptr_t * vLeaves;
// truth table representation
Vec_Ptr_t * vTtElems; // elementary truth tables
Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes
+ Vec_Int_t * vMemory;
+ Vec_Int_t * vBddDir;
+ Vec_Int_t * vBddInv;
+ unsigned puSupps[32]; // the supports of the cofactors
+ unsigned * ppTruths[5][16];
// variable sets
Vec_Int_t * vSets[8];
- Kit_DsdMan_t * pDsdMan;
+ Kit_DsdMan_t* pDsdMan;
// statistics
int nNodesTotal; // total number of nodes
int nNodesOver; // nodes with cuts over the limit
@@ -104,17 +110,30 @@ struct Lpk_Man_t_
int nGainTotal; // the gain in LUTs
int nChanges; // the number of changed nodes
int nBenefited; // the number of gainful that benefited from decomposition
+ int nMuxes;
+ int nDsds;
int nTotalNets;
int nTotalNets2;
+ int nTotalNodes;
+ int nTotalNodes2;
// counter of non-DSD blocks
int nBlocks[17];
- // rutime
+ // runtime
int timeCuts;
int timeTruth;
+ int timeSupps;
+ int timeTruth2;
+ int timeTruth3;
int timeEval;
int timeMap;
int timeOther;
int timeTotal;
+ // runtime of eval
+ int timeEvalMuxAn;
+ int timeEvalMuxSp;
+ int timeEvalDsdAn;
+ int timeEvalDsdSp;
+
};
@@ -122,32 +141,35 @@ struct Lpk_Man_t_
typedef struct Lpk_Fun_t_ Lpk_Fun_t;
struct Lpk_Fun_t_
{
- Vec_Ptr_t * vNodes; // the array of leaves and decomposition nodes
- unsigned int Id : 8; // the ID of this node
- unsigned int nVars : 5; // the number of variables
- unsigned int nLutK : 4; // the number of LUT inputs
- unsigned int nAreaLim : 5; // the area limit (the largest allowed)
- unsigned int nDelayLim : 10; // the delay limit (the largest allowed)
- char pDelays[16]; // the delays of the inputs
- char pFanins[16]; // the fanins of this function
- unsigned uSupp; // the support of this component
- unsigned pTruth[0]; // the truth table (contains room for three truth tables)
+ Vec_Ptr_t * vNodes; // the array of leaves and decomposition nodes
+ unsigned Id : 7; // the ID of this node
+ unsigned nVars : 5; // the number of variables
+ unsigned nLutK : 4; // the number of LUT inputs
+ unsigned nAreaLim : 5; // the area limit (the largest allowed)
+ unsigned nDelayLim : 9; // the delay limit (the largest allowed)
+ unsigned fSupports : 1; // supports of cofactors were precomputed
+ unsigned fMark : 1; // marks the MUX-based dec
+ unsigned uSupp; // the support of this component
+ unsigned puSupps[32]; // the supports of the cofactors
+ char pDelays[16]; // the delays of the inputs
+ char pFanins[16]; // the fanins of this function
+ unsigned pTruth[0]; // the truth table (contains room for three truth tables)
};
// preliminary decomposition result
typedef struct Lpk_Res_t_ Lpk_Res_t;
struct Lpk_Res_t_
{
- int nBSVars; // the number of bound set variables
- unsigned BSVars; // the bound set
- int nCofVars; // the number of cofactoring variables
- char pCofVars[4]; // the cofactoring variables
- int nSuppSizeS; // support size of the smaller (decomposed) function
- int nSuppSizeL; // support size of the larger (composition) function
- int DelayEst; // estimated delay of the decomposition
- int AreaEst; // estimated area of the decomposition
- int Variable; // variable in MUX decomposition
- int Polarity; // polarity in MUX decomposition
+ int nBSVars; // the number of bound set variables
+ unsigned BSVars; // the bound set
+ int nCofVars; // the number of cofactoring variables
+ char pCofVars[4]; // the cofactoring variables
+ int nSuppSizeS; // support size of the smaller (decomposed) function
+ int nSuppSizeL; // support size of the larger (composition) function
+ int DelayEst; // estimated delay of the decomposition
+ int AreaEst; // estimated area of the decomposition
+ int Variable; // variable in MUX decomposition
+ int Polarity; // polarity in MUX decomposition
};
static inline int Lpk_LutNumVars( int nLutsLim, int nLutK ) { return nLutsLim * (nLutK - 1) + 1; }
@@ -177,25 +199,26 @@ static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num ) { assert( Num
////////////////////////////////////////////////////////////////////////
/*=== lpkAbcDec.c ============================================================*/
-extern Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
+extern Abc_Obj_t * Lpk_Decompose( Lpk_Man_t * pMan, Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, unsigned * puSupps, int nLutK, int AreaLim, int DelayLim );
/*=== lpkAbcDsd.c ============================================================*/
-extern Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p );
-extern Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
+extern Lpk_Res_t * Lpk_DsdAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p, int nShared );
+extern Lpk_Fun_t * Lpk_DsdSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet );
/*=== lpkAbcMux.c ============================================================*/
-extern Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p );
-extern Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol );
+extern Lpk_Res_t * Lpk_MuxAnalize( Lpk_Man_t * pMan, Lpk_Fun_t * p );
+extern Lpk_Fun_t * Lpk_MuxSplit( Lpk_Man_t * pMan, Lpk_Fun_t * p, int Var, int Pol );
/*=== lpkAbcUtil.c ============================================================*/
extern Lpk_Fun_t * Lpk_FunAlloc( int nVars );
extern void Lpk_FunFree( Lpk_Fun_t * p );
extern Lpk_Fun_t * Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim );
extern Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth );
-extern void Lpk_FunSuppMinimize( Lpk_Fun_t * p );
+extern int Lpk_FunSuppMinimize( Lpk_Fun_t * p );
+extern void Lpk_FunComputeCofSupps( Lpk_Fun_t * p );
extern int Lpk_SuppDelay( unsigned uSupp, char * pDelays );
extern int Lpk_SuppToVars( unsigned uBoundSet, char * pVars );
/*=== lpkCut.c =========================================================*/
-extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut );
+extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fInv );
extern int Lpk_NodeCuts( Lpk_Man_t * p );
/*=== lpkMap.c =========================================================*/
extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars );
diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c
index 5be198d7..af6a5307 100644
--- a/src/opt/lpk/lpkMan.c
+++ b/src/opt/lpk/lpkMan.c
@@ -42,9 +42,9 @@
Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
{
Lpk_Man_t * p;
- int i;
+ int i, nWords;
assert( pPars->nLutsMax <= 16 );
- assert( pPars->nVarsMax > 0 );
+ assert( pPars->nVarsMax > 0 && pPars->nVarsMax <= 16 );
p = ALLOC( Lpk_Man_t, 1 );
memset( p, 0, sizeof(Lpk_Man_t) );
p->pPars = pPars;
@@ -52,9 +52,28 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax );
p->vTtNodes = Vec_PtrAllocSimInfo( 1024, Abc_TruthWordNum(pPars->nVarsMax) );
p->vCover = Vec_IntAlloc( 1 << 12 );
+ p->vLeaves = Vec_PtrAlloc( 32 );
for ( i = 0; i < 8; i++ )
p->vSets[i] = Vec_IntAlloc(100);
p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 );
+ p->vMemory = Vec_IntAlloc( 1024 * 32 );
+ p->vBddDir = Vec_IntAlloc( 256 );
+ p->vBddInv = Vec_IntAlloc( 256 );
+ // allocate temporary storage for truth tables
+ nWords = Kit_TruthWordNum(pPars->nVarsMax);
+ p->ppTruths[0][0] = ALLOC( unsigned, 32 * nWords );
+ p->ppTruths[1][0] = p->ppTruths[0][0] + 1 * nWords;
+ for ( i = 1; i < 2; i++ )
+ p->ppTruths[1][i] = p->ppTruths[1][0] + i * nWords;
+ p->ppTruths[2][0] = p->ppTruths[1][0] + 2 * nWords;
+ for ( i = 1; i < 4; i++ )
+ p->ppTruths[2][i] = p->ppTruths[2][0] + i * nWords;
+ p->ppTruths[3][0] = p->ppTruths[2][0] + 4 * nWords;
+ for ( i = 1; i < 8; i++ )
+ p->ppTruths[3][i] = p->ppTruths[3][0] + i * nWords;
+ p->ppTruths[4][0] = p->ppTruths[3][0] + 8 * nWords;
+ for ( i = 1; i < 16; i++ )
+ p->ppTruths[4][i] = p->ppTruths[4][0] + i * nWords;
return p;
}
@@ -72,6 +91,10 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars )
void Lpk_ManStop( Lpk_Man_t * p )
{
int i;
+ free( p->ppTruths[0][0] );
+ Vec_IntFree( p->vBddDir );
+ Vec_IntFree( p->vBddInv );
+ Vec_IntFree( p->vMemory );
Kit_DsdManFree( p->pDsdMan );
for ( i = 0; i < 8; i++ )
Vec_IntFree(p->vSets[i]);
@@ -85,6 +108,7 @@ void Lpk_ManStop( Lpk_Man_t * p )
Vec_VecFree( p->vLevels );
if ( p->vVisited )
Vec_VecFree( p->vVisited );
+ Vec_PtrFree( p->vLeaves );
Vec_IntFree( p->vCover );
Vec_PtrFree( p->vTtElems );
Vec_PtrFree( p->vTtNodes );
diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c
index d0d56a86..90e46863 100644
--- a/src/opt/lpk/lpkSets.c
+++ b/src/opt/lpk/lpkSets.c
@@ -140,7 +140,7 @@ unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets )
SeeAlso []
***********************************************************************/
-void Lpk_PrintSetOne( int uSupport )
+static void Lpk_PrintSetOne( int uSupport )
{
unsigned k;
for ( k = 0; k < 16; k++ )
@@ -159,7 +159,7 @@ void Lpk_PrintSetOne( int uSupport )
SeeAlso []
***********************************************************************/
-void Lpk_PrintSets( Vec_Int_t * vSets )
+static void Lpk_PrintSets( Vec_Int_t * vSets )
{
unsigned uSupport;
int Number, i;