summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abc/abc.h14
-rw-r--r--src/base/abc/abcSop.c4
-rw-r--r--src/base/abci/abc.c117
-rw-r--r--src/base/abci/abcDsdRes.c563
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/base/cmd/cmd.c6
-rw-r--r--src/base/io/io.c6
-rw-r--r--src/misc/vec/vecPtr.h39
-rw-r--r--src/opt/kit/kit.h6
-rw-r--r--src/opt/kit/kitDsd.c503
10 files changed, 1179 insertions, 80 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 79134898..bf4aeb0f 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -227,6 +227,20 @@ struct Abc_Lib_t_
void * pGenlib; // the genlib library used to map this design
};
+typedef struct Lut_Par_t_ Lut_Par_t;
+struct Lut_Par_t_
+{
+ // user-controlled parameters
+ int nLutsMax; // (N) the maximum number of LUTs in the structure
+ int nLutsOver; // (Q) the maximum number of LUTs not in the MFFC
+ int nVarsShared; // (S) the maximum number of shared variables (crossbars)
+ int fVerbose; // the verbosiness flag
+ int fVeryVerbose; // additional verbose info printout
+ // internal parameters
+ int nLutSize; // (K) the LUT size (determined by the input network)
+ int nVarsMax; // (V) the largest number of variables: V = N * (K-1) + 1
+};
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 01fa8e13..106901ab 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -922,8 +922,8 @@ char * Abc_SopFromTruthHex( char * pTruth )
{
pCube = pSopCover + i * (nVars + 3);
for ( b = 0; b < nVars; b++ )
- if ( Mint & (1 << (nVars-1-b)) )
-// if ( Mint & (1 << b) )
+// if ( Mint & (1 << (nVars-1-b)) )
+ if ( Mint & (1 << b) )
pCube[b] = '1';
else
pCube[b] = '0';
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e76c0261..753a2fb7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -63,6 +63,7 @@ static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandLutjam ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -217,6 +218,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "lutjam", Abc_CommandLutjam, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
@@ -2876,6 +2878,121 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandLutjam( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ Lut_Par_t Pars, * pPars = &Pars;
+ int c;
+ extern int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars );
+
+// printf( "Implementation of this command is not finished.\n" );
+// return 1;
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ memset( pPars, 0, sizeof(Lut_Par_t) );
+ pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure
+ pPars->nLutsOver = 1; // (Q) the maximum number of LUTs not in the MFFC
+ pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars)
+ pPars->fVerbose = 0;
+ pPars->fVeryVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NQSvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLutsMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLutsMax < 2 || pPars->nLutsMax > 8 )
+ goto usage;
+ break;
+ case 'Q':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-Q\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLutsOver = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLutsOver < 0 || pPars->nLutsOver > 8 )
+ goto usage;
+ break;
+ case 'S':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nVarsShared = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nVarsShared < 0 || pPars->nVarsShared > 4 )
+ goto usage;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( pErr, "This command can only be applied to a logic network.\n" );
+ return 1;
+ }
+
+ // modify the current network
+ if ( !Abc_LutResynthesize( pNtk, pPars ) )
+ {
+ fprintf( pErr, "Resynthesis has failed.\n" );
+ return 1;
+ }
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: lutjam [-N <num>] [-Q <num>] [-S <num>] [-vwh]\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-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-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c
new file mode 100644
index 00000000..68748577
--- /dev/null
+++ b/src/base/abci/abcDsdRes.c
@@ -0,0 +1,563 @@
+/**CFile****************************************************************
+
+ FileName [abcDsdRes.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis []
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcDsdRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define LUT_SIZE_MAX 16 // the largest size of the function
+#define LUT_CUTS_MAX 128 // the largest number of cuts considered
+
+typedef struct Lut_Man_t_ Lut_Man_t;
+typedef struct Lut_Cut_t_ Lut_Cut_t;
+
+struct Lut_Cut_t_
+{
+ unsigned nLeaves : 6; // (L) the number of leaves
+ unsigned nNodes : 6; // (M) the number of nodes
+ unsigned nNodesMarked : 6; // (Q) nodes outside of MFFC
+ unsigned nNodesMax : 6; // the max number of nodes
+ unsigned nLeavesMax : 6; // the max number of leaves
+ unsigned fHasDsd : 1; // set to 1 if the cut has structural DSD (and so cannot be used)
+ unsigned fMark : 1; // multipurpose mark
+// unsigned uSign[2]; // the signature
+ float Weight; // the weight of the cut: (M - Q)/N(V) (the larger the better)
+ int pLeaves[LUT_SIZE_MAX]; // the leaves of the cut
+ int pNodes[LUT_SIZE_MAX]; // the nodes of the cut
+};
+
+struct Lut_Man_t_
+{
+ // parameters
+ Lut_Par_t * pPars; // the set of parameters
+ // current representation
+ Abc_Ntk_t * pNtk; // the network
+ Abc_Obj_t * pObj; // the node to resynthesize
+ // cut representation
+ int nCuts; // the total number of cuts
+ int nCutsMax; // the largest possible number of cuts
+ int nEvals; // the number of good cuts
+ Lut_Cut_t pCuts[LUT_CUTS_MAX]; // the storage for cuts
+ int pEvals[LUT_SIZE_MAX]; // the good cuts
+ // temporary variables
+ int pRefs[LUT_SIZE_MAX]; // fanin reference counters
+ int pCands[LUT_SIZE_MAX]; // internal nodes pointing only to the leaves
+ // truth table representation
+ Vec_Ptr_t * vTtElems; // elementary truth tables
+ Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes
+};
+
+static int Abc_LutResynthesizeNode( Lut_Man_t * p );
+
+#define Abc_LutCutForEachLeaf( pNtk, pCut, pObj, i ) \
+ for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
+#define Abc_LutCutForEachNode( pNtk, pCut, pObj, i ) \
+ for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Lut_Man_t * Abc_LutManStart( Lut_Par_t * pPars )
+{
+ Lut_Man_t * p;
+ int i;
+ assert( pPars->nLutsMax <= 16 );
+ p = ALLOC( Lut_Man_t, 1 );
+ memset( p, 0, sizeof(Lut_Man_t) );
+ p->pPars = pPars;
+ p->nCutsMax = LUT_CUTS_MAX;
+ for ( i = 0; i < p->nCuts; i++ )
+ p->pCuts[i].nLeavesMax = p->pCuts[i].nNodesMax = LUT_SIZE_MAX;
+ p->vTtElems = Vec_PtrAllocTruthTables( pPars->nLutsMax );
+ p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nLutsMax) );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_LutManStop( Lut_Man_t * p )
+{
+ Vec_PtrFree( p->vTtElems );
+ Vec_PtrFree( p->vTtNodes );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs resynthesis for one network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars )
+{
+ Lut_Man_t * p;
+ Abc_Obj_t * pObj;
+ int i;
+ assert( Abc_NtkIsLogic(pNtk) );
+ // convert logic to AIGs
+ Abc_NtkToAig( pNtk );
+ // compute the levels
+ Abc_NtkLevel( pNtk );
+ // start the manager
+ p = Abc_LutManStart( pPars );
+ p->pNtk = pNtk;
+ // get the number of inputs
+ p->pPars->nLutSize = Abc_NtkGetFaninMax( pNtk );
+ p->pPars->nVarsMax = p->pPars->nLutsMax * (p->pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1
+ printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n",
+ p->pPars->nLutsMax, p->pPars->nLutSize, p->pPars->nLutsOver, p->pPars->nVarsShared, p->pPars->nVarsMax );
+ // consider all nodes
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ p->pObj = pObj;
+ Abc_LutResynthesizeNode( p );
+ }
+ Abc_LutManStop( p );
+ // check the resulting network
+ if ( !Abc_NtkCheck( pNtk ) )
+ {
+ printf( "Abc_LutResynthesize: The network check has failed.\n" );
+ return 0;
+ }
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the cut has structural DSD.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_LutNodeCutsCheckDsd( Lut_Man_t * p, Lut_Cut_t * pCut )
+{
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k, nCands, fLeavesOnly, RetValue;
+ assert( pCut->nLeaves > 0 );
+ // clear ref counters
+ memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves );
+ // mark cut leaves
+ Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
+ {
+ assert( pObj->fMarkA == 0 );
+ pObj->fMarkA = 1;
+ pObj->pCopy = (void *)i;
+ }
+ // ref leaves pointed from the internal nodes
+ nCands = 0;
+ Abc_LutCutForEachNode( p->pNtk, pCut, pObj, i )
+ {
+ fLeavesOnly = 1;
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ if ( pFanin->fMarkA )
+ p->pRefs[(int)pFanin->pCopy]++;
+ else
+ fLeavesOnly = 0;
+ if ( fLeavesOnly )
+ p->pCands[nCands++] = pObj->Id;
+ }
+ // look at the nodes that only point to the leaves
+ RetValue = 0;
+ for ( i = 0; i < nCands; i++ )
+ {
+ pObj = Abc_NtkObj( p->pNtk, p->pCands[i] );
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ {
+ assert( pFanin->fMarkA == 1 );
+ if ( p->pRefs[(int)pFanin->pCopy] > 1 )
+ break;
+ }
+ if ( k == Abc_ObjFaninNum(pFanin) )
+ {
+ RetValue = 1;
+ break;
+ }
+ }
+ // unmark cut leaves
+ Abc_LutCutForEachLeaf( p->pNtk, pCut, pObj, i )
+ pObj->fMarkA = 0;
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if pDom is contained in pCut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_LutNodeCutsOneDominance( Lut_Cut_t * pDom, Lut_Cut_t * pCut )
+{
+ int i, k;
+ for ( i = 0; i < (int)pDom->nLeaves; i++ )
+ {
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
+ break;
+ if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
+ return 0;
+ }
+ // every node in pDom is contained in pCut
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check if the cut exists.]
+
+ Description [Returns 1 if the cut exists.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_LutNodeCutsOneFilter( Lut_Cut_t * pCuts, int nCuts, Lut_Cut_t * pCutNew )
+{
+ Lut_Cut_t * pCut;
+ int i, k;
+// assert( pCutNew->uHash );
+ // try to find the cut
+ for ( i = 0; i < nCuts; i++ )
+ {
+ pCut = pCuts + i;
+ if ( pCut->nLeaves == 0 )
+ continue;
+ if ( pCut->nLeaves == pCutNew->nLeaves )
+ {
+// if ( pCut->uHash[0] == pCutNew->uHash[0] && pCut->uHash[1] == pCutNew->uHash[1] )
+ {
+ for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
+ if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] )
+ break;
+ if ( k == (int)pCutNew->nLeaves )
+ return 1;
+ }
+ continue;
+ }
+ if ( pCut->nLeaves < pCutNew->nLeaves )
+ {
+ // skip the non-contained cuts
+// if ( (pCut->uHash[0] & pCutNew->uHash[0]) != pCut->uHash[0] )
+// continue;
+// if ( (pCut->uHash[1] & pCutNew->uHash[1]) != pCut->uHash[1] )
+// continue;
+ // check containment seriously
+ if ( Abc_LutNodeCutsOneDominance( pCut, pCutNew ) )
+ return 1;
+ continue;
+ }
+ // check potential containment of other cut
+
+ // skip the non-contained cuts
+// if ( (pCut->uHash[0] & pCutNew->uHash[0]) != pCutNew->uHash[0] )
+// continue;
+// if ( (pCut->uHash[1] & pCutNew->uHash[1]) != pCutNew->uHash[1] )
+// continue;
+ // check containment seriously
+ if ( Abc_LutNodeCutsOneDominance( pCutNew, pCut ) )
+ pCut->nLeaves = 0; // removed
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the set of all cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_LutNodeCutsOne( Lut_Man_t * p, Lut_Cut_t * pCut, int Node )
+{
+ Lut_Cut_t * pCutNew;
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k, j;
+
+ // check if the cut can stand adding one more internal node
+ if ( pCut->nNodes == LUT_SIZE_MAX )
+ return;
+
+ // if the node is not in the MFFC, check the limit
+ pObj = Abc_NtkObj( p->pNtk, Node );
+ if ( !Abc_NodeIsTravIdCurrent(pObj) )
+ {
+ if ( (int)pCut->nNodesMarked == p->pPars->nLutsOver )
+ return;
+ assert( (int)pCut->nNodesMarked < p->pPars->nLutsOver );
+ }
+
+ // create the new set of leaves
+ pCutNew = p->pCuts + p->nCuts;
+ pCutNew->nLeaves = 0;
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ if ( pCut->pLeaves[i] != Node )
+ pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i];
+
+ // add new nodes
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ {
+ // find the place where this node belongs
+ for ( k = 0; k < (int)pCutNew->nLeaves; k++ )
+ if ( pCutNew->pLeaves[k] >= pFanin->Id )
+ break;
+ if ( pCutNew->pLeaves[k] == pFanin->Id )
+ continue;
+ // check if there is room
+ if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax )
+ return;
+ // move all the nodes
+ for ( j = pCutNew->nLeaves; j > k; j-- )
+ pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1];
+ pCutNew->pLeaves[k] = pFanin->Id;
+ pCutNew->nLeaves++;
+ assert( pCutNew->nLeaves <= LUT_SIZE_MAX );
+ }
+
+ // skip the contained cuts
+ if ( Abc_LutNodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) )
+ return;
+
+ // update the set of internal nodes
+ assert( pCut->nNodes < LUT_SIZE_MAX );
+ memcpy( pCutNew->pNodes, pCutNew->pNodes, pCut->nNodes * sizeof(int) );
+ pCutNew->pNodes[ pCut->nNodes++ ] = Node;
+
+ // add the marked node
+ pCutNew->nNodesMarked = pCut->nNodesMarked + !Abc_NodeIsTravIdCurrent(pObj);
+
+ // add the cut to storage
+ assert( p->nCuts < LUT_CUTS_MAX );
+ p->nCuts++;
+
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the set of all cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_LutNodeCuts( Lut_Man_t * p )
+{
+ Abc_Obj_t * pFanin;
+ Lut_Cut_t * pCut, * pCut2;
+ int i, k, Temp, nMffc, fChanges;
+
+ // mark the MFFC of the node with the current trav ID
+ nMffc = Abc_NodeMffcLabel( p->pObj );
+ assert( nMffc > 0 );
+ if ( nMffc == 1 )
+ return 0;
+
+ // initialize the first cut
+ pCut = p->pCuts;
+ // assign internal nodes
+ pCut->nNodes = 1;
+ pCut->pNodes[0] = p->pObj->Id;
+ pCut->nNodesMarked = 0;
+ // assign the leaves
+ pCut->nLeaves = Abc_ObjFaninNum( p->pObj );
+ Abc_ObjForEachFanin( p->pObj, pFanin, i )
+ pCut->pLeaves[i] = pFanin->Id;
+ // sort the leaves
+ do {
+ fChanges = 0;
+ for ( i = 0; i < (int)pCut->nLeaves - 1; i++ )
+ {
+ if ( pCut->pLeaves[i] <= pCut->pLeaves[i+1] )
+ continue;
+ Temp = pCut->pLeaves[i];
+ pCut->pLeaves[i] = pCut->pLeaves[i+1];
+ pCut->pLeaves[i+1] = Temp;
+ fChanges = 1;
+ }
+ } while ( fChanges );
+
+ // perform the cut computation
+ for ( i = 0; i < p->nCuts; i++ )
+ {
+ pCut = p->pCuts + p->pEvals[i];
+ if ( pCut->nLeaves == 0 )
+ continue;
+ // try to expand each fanin of each cut
+ for ( k = 0; k < (int)pCut->nLeaves; k++ )
+ {
+ Abc_LutNodeCutsOne( p, pCut, pCut->pLeaves[k] );
+ if ( p->nCuts == LUT_CUTS_MAX )
+ break;
+ }
+ if ( p->nCuts == LUT_CUTS_MAX )
+ break;
+ }
+
+ // compress the cuts by removing empty ones, decomposable ones, and those with negative Weight
+ p->nEvals = 0;
+ for ( i = 0; i < p->nCuts; i++ )
+ {
+ pCut = p->pCuts + p->pEvals[i];
+ pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesMarked) / p->pPars->nLutsMax;
+ pCut->fHasDsd = Abc_LutNodeCutsCheckDsd( p, pCut );
+ if ( pCut->nLeaves == 0 || pCut->Weight <= 1.0 || pCut->fHasDsd )
+ continue;
+ p->pEvals[p->nEvals++] = i;
+ }
+ if ( p->nEvals == 0 )
+ return 0;
+
+ // sort the cuts by Weight
+ do {
+ fChanges = 0;
+ for ( i = 0; i < p->nEvals - 1; i++ )
+ {
+ pCut = p->pCuts + p->pEvals[i];
+ pCut2 = p->pCuts + p->pEvals[i+1];
+ if ( pCut->Weight >= pCut2->Weight )
+ continue;
+ Temp = p->pEvals[i];
+ p->pEvals[i] = p->pEvals[i+1];
+ p->pEvals[i+1] = Temp;
+ fChanges = 1;
+ }
+ } while ( fChanges );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes the truth able of one cut.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Abc_LutCutTruth( Lut_Man_t * p, Lut_Cut_t * pCut )
+{
+ unsigned * pTruth = NULL;
+ return pTruth;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Implements the given DSD network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, void * pDsd )
+{
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs resynthesis for one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_LutResynthesizeNode( Lut_Man_t * p )
+{
+ Lut_Cut_t * pCut;
+ unsigned * pTruth;
+ void * pDsd;
+ int i;
+ // compute the cuts
+ if ( !Abc_LutNodeCuts( p ) )
+ return 0;
+ // try the good cuts
+ for ( i = 0; i < p->nEvals; i++ )
+ {
+ // get the cut
+ pCut = p->pCuts + p->pEvals[i];
+ // compute the truth table
+ pTruth = Abc_LutCutTruth( p, pCut );
+ // check decomposition
+ pDsd = /***/ NULL;
+ // if it is not DSD decomposable, return
+ if ( pDsd == NULL )
+ continue;
+ // update the network
+ Abc_LutCutUpdate( p, pCut, pDsd );
+ }
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index acac466b..e8eb6c7f 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -10,6 +10,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDebug.c \
src/base/abci/abcDress.c \
src/base/abci/abcDsd.c \
+ src/base/abci/abcDsdRes.c \
src/base/abci/abcEspresso.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFpga.c \
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 845f9d77..2dc03d5c 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1265,6 +1265,8 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
}
// write out the current network
+ if ( Abc_NtkIsLogic(pNtk) )
+ Abc_NtkToSop(pNtk, 0);
pNetlist = Abc_NtkToNetlist(pNtk);
if ( pNetlist == NULL )
{
@@ -1406,6 +1408,8 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
}
// write out the current network
+ if ( Abc_NtkIsLogic(pNtk) )
+ Abc_NtkToSop(pNtk, 0);
pNetlist = Abc_NtkToNetlist(pNtk);
if ( pNetlist == NULL )
{
@@ -1552,6 +1556,8 @@ int CmdCommandCapo( Abc_Frame_t * pAbc, int argc, char **argv )
}
// write out the current network
+ if ( Abc_NtkIsLogic(pNtk) )
+ Abc_NtkToSop(pNtk, 0);
pNetlist = Abc_NtkToNetlist(pNtk);
if ( pNetlist == NULL )
{
diff --git a/src/base/io/io.c b/src/base/io/io.c
index f0dabeb9..09d1a8a5 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -525,13 +525,13 @@ usage:
fprintf( pAbc->Err, "\t parses a formula representing DSD of a function\n" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tformula : the formula representing disjoint-support decomposition (DSD)\n" );
- fprintf( pAbc->Err, "\t Example of a formula: !(a*(b+CA(c,!d,e*f))*79B3(g,h,i,k))\n" );
+ fprintf( pAbc->Err, "\t Example of a formula: !(a*(b+CA(!d,e*f,c))*79B3(g,h,i,k))\n" );
fprintf( pAbc->Err, "\t where \'!\' is an INV, \'*\' is an AND, \'+\' is an XOR, \n" );
fprintf( pAbc->Err, "\t CA and 79B3 are hexadecimal representations of truth tables\n" );
- fprintf( pAbc->Err, "\t (in this case CA=11001010 is truth table of MUX(Ctrl,Data1,Data0))\n" );
+ fprintf( pAbc->Err, "\t (in this case CA=11001010 is truth table of MUX(Data0,Data1,Ctrl))\n" );
fprintf( pAbc->Err, "\t The lower chars (a,b,c,etc) are reserved for elementary variables.\n" );
fprintf( pAbc->Err, "\t The upper chars (A,B,C,etc) are reserved for hexadecimal digits.\n" );
- fprintf( pAbc->Err, "\t No spaces are allowed in the formula.\n" );
+ fprintf( pAbc->Err, "\t No spaces are allowed in formulas. In parantheses, LSB goes first.\n" );
return 1;
}
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index a53e439a..272e7b40 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -177,6 +177,45 @@ static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords )
/**Function*************************************************************
+ Synopsis [Allocates the array of truth tables for the given number of vars.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Vec_Ptr_t * Vec_PtrAllocTruthTables( int nVars )
+{
+ Vec_Ptr_t * p;
+ unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
+ unsigned * pTruth;
+ int i, k, nWords;
+ nWords = (nVars <= 5 ? 1 : (1 << (nVars - 5)));
+ p = Vec_PtrAllocSimInfo( nVars, nWords );
+ for ( i = 0; i < nVars; i++ )
+ {
+ pTruth = p->pArray[i];
+ if ( i < 5 )
+ {
+ for ( k = 0; k < nWords; k++ )
+ pTruth[k] = Masks[i];
+ }
+ else
+ {
+ for ( k = 0; k < nWords; k++ )
+ if ( k & (1 << (i-5)) )
+ pTruth[k] = ~(unsigned)0;
+ else
+ pTruth[k] = 0;
+ }
+ }
+ return p;
+}
+
+/**Function*************************************************************
+
Synopsis [Duplicates the integer array.]
Description []
diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h
index d779df7b..c08ea81a 100644
--- a/src/opt/kit/kit.h
+++ b/src/opt/kit/kit.h
@@ -293,6 +293,12 @@ static inline void Kit_TruthOr( unsigned * pOut, unsigned * pIn0, unsigned * pIn
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
pOut[w] = pIn0[w] | pIn1[w];
}
+static inline void Kit_TruthXor( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
+{
+ int w;
+ for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
+ pOut[w] = pIn0[w] ^ pIn1[w];
+}
static inline void Kit_TruthSharp( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
{
int w;
diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c
index b85aa4a4..dfe143be 100644
--- a/src/opt/kit/kitDsd.c
+++ b/src/opt/kit/kitDsd.c
@@ -24,31 +24,30 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+typedef struct Dsd_Man_t_ Dsd_Man_t;
typedef struct Dsd_Ntk_t_ Dsd_Ntk_t;
typedef struct Dsd_Obj_t_ Dsd_Obj_t;
-// network types
+// DSD node types
typedef enum {
KIT_DSD_NONE = 0, // 0: unknown
KIT_DSD_CONST1, // 1: constant 1
KIT_DSD_VAR, // 2: elementary variable
KIT_DSD_AND, // 3: multi-input AND
KIT_DSD_XOR, // 4: multi-input XOR
- KIT_DSD_MUX, // 5: multiplexer
- KIT_DSD_PRIME // 6: arbitrary function of 3+ variables
+ KIT_DSD_PRIME // 5: arbitrary function of 3+ variables
} Kit_Dsd_t;
-struct Dsd_Obj_t_
-{
- unsigned Id : 6; // the number of this node
- unsigned Type : 3; // none, const, var, AND, XOR, MUX, PRIME
- unsigned fMark : 1; // finished checking output
- unsigned Offset : 8; // offset to the truth table
- unsigned nRefs : 8; // offset to the truth table
- unsigned nFans : 6; // the number of fanins of this node
- unsigned char pFans[0]; // the fanin literals
+// DSD manager
+struct Dsd_Man_t_
+{
+ int nVars; // the maximum number of variables
+ int nWords; // the number of words in TTs
+ Vec_Ptr_t * vTtElems; // elementary truth tables
+ Vec_Ptr_t * vTtNodes; // the node truth tables
};
+// DSD network
struct Dsd_Ntk_t_
{
unsigned char nVars; // at most 16 (perhaps 18?)
@@ -59,15 +58,36 @@ struct Dsd_Ntk_t_
Dsd_Obj_t * pNodes[0]; // the nodes
};
-static inline unsigned Dsd_ObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
-static inline unsigned * Dsd_ObjTruth( Dsd_Obj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
-static inline Dsd_Obj_t * Dsd_NtkRoot( Dsd_Ntk_t * pNtk ) { return pNtk->pNodes[(pNtk->Root >> 1) - pNtk->nVars]; }
+// DSD node
+struct Dsd_Obj_t_
+{
+ unsigned Id : 6; // the number of this node
+ unsigned Type : 3; // none, const, var, AND, XOR, MUX, PRIME
+ unsigned fMark : 1; // finished checking output
+ unsigned Offset : 8; // offset to the truth table
+ unsigned nRefs : 8; // offset to the truth table
+ unsigned nFans : 6; // the number of fanins of this node
+ unsigned char pFans[0]; // the fanin literals
+};
-#define Dsd_NtkForEachObj( pNtk, pObj, i ) \
+static inline int Dsd_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
+static inline int Dsd_Lit2Var( int Lit ) { return Lit >> 1; }
+static inline int Dsd_LitIsCompl( int Lit ) { return Lit & 1; }
+static inline int Dsd_LitNot( int Lit ) { return Lit ^ 1; }
+static inline int Dsd_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
+static inline int Dsd_LitRegular( int Lit ) { return Lit & 0xfe; }
+
+static inline unsigned Dsd_ObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
+static inline unsigned * Dsd_ObjTruth( Dsd_Obj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
+static inline Dsd_Obj_t * Dsd_NtkObj( Dsd_Ntk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
+static inline Dsd_Obj_t * Dsd_NtkRoot( Dsd_Ntk_t * pNtk ) { return Dsd_NtkObj( pNtk, Dsd_Lit2Var(pNtk->Root) ); }
+
+#define Dsd_NtkForEachObj( pNtk, pObj, i ) \
for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
-#define Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i ) \
- for ( i = 0; (i < (pObj)->nFans) && (((pFanin) = ((pObj)->pFans[i] < 2*pNtk->nVars)? NULL: (pNtk)->pNodes[((pObj)->pFans[i]>>1) - pNtk->nVars]), 1) && ((iVar) = (pObj)->pFans[i], 1); i++ )
+#define Dsd_ObjForEachFanin( pNtk, pObj, iLit, i ) \
+ for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
+extern unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_t * pNtk );
extern void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk );
extern Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk );
@@ -78,6 +98,47 @@ extern void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk );
/**Function*************************************************************
+ Synopsis [Allocates the DSD manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dsd_Man_t * Dsd_ManAlloc( int nVars )
+{
+ Dsd_Man_t * p;
+ p = ALLOC( Dsd_Man_t, 1 );
+ memset( p, 0, sizeof(Dsd_Man_t) );
+ p->nVars = nVars;
+ p->nWords = Kit_TruthWordNum( p->nVars );
+ p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
+ p->vTtNodes = Vec_PtrAllocSimInfo( 64, p->nWords );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates the DSD manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dsd_ManFree( Dsd_Man_t * p )
+{
+ Vec_PtrFree( p->vTtElems );
+ Vec_PtrFree( p->vTtNodes );
+ free( p );
+}
+
+/**Function*************************************************************
+
Synopsis [Allocates the DSD node.]
Description []
@@ -130,7 +191,7 @@ void Dsd_ObjFree( Dsd_Ntk_t * p, Dsd_Obj_t * pObj )
SeeAlso []
***********************************************************************/
-Dsd_Ntk_t * Kit_DsdNtkAlloc( unsigned * pTruth, int nVars )
+Dsd_Ntk_t * Kit_DsdNtkAlloc( int nVars )
{
Dsd_Ntk_t * pNtk;
int nSize = sizeof(Dsd_Ntk_t) + sizeof(void *) * nVars;
@@ -200,12 +261,20 @@ void Kit_DsdPrintHex( FILE * pFile, unsigned * pTruth, int nFans )
SeeAlso []
***********************************************************************/
-void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
+void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, int Id )
{
- Dsd_Obj_t * pFanin;
- unsigned iVar, i;
+ Dsd_Obj_t * pObj;
+ unsigned iLit, i;
char Symbol;
+ pObj = Dsd_NtkObj( pNtk, Id );
+ if ( pObj == NULL )
+ {
+ assert( Id < pNtk->nVars );
+ fprintf( pFile, "%c", 'a' + Id );
+ return;
+ }
+
if ( pObj->Type == KIT_DSD_CONST1 )
{
assert( pObj->nFans == 0 );
@@ -223,20 +292,15 @@ void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
else
Symbol = ',';
- if ( pObj->Type == KIT_DSD_MUX )
- fprintf( pFile, "CA" );
- else if ( pObj->Type == KIT_DSD_PRIME )
+ if ( pObj->Type == KIT_DSD_PRIME )
Kit_DsdPrintHex( stdout, Dsd_ObjTruth(pObj), pObj->nFans );
fprintf( pFile, "(" );
- Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i )
+ Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
{
- if ( iVar & 1 )
+ if ( Dsd_LitIsCompl(iLit) )
fprintf( pFile, "!" );
- if ( pFanin )
- Kit_DsdPrint_rec( pFile, pNtk, pFanin );
- else
- fprintf( pFile, "%c", 'a' + (pNtk->nVars - 1 - (iVar >> 1)) );
+ Kit_DsdPrint_rec( pFile, pNtk, Dsd_Lit2Var(iLit) );
if ( i < pObj->nFans - 1 )
fprintf( pFile, "%c", Symbol );
}
@@ -257,14 +321,301 @@ void Kit_DsdPrint_rec( FILE * pFile, Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk )
{
fprintf( pFile, "F = " );
- if ( pNtk->Root & 1 )
+ if ( Dsd_LitIsCompl(pNtk->Root) )
fprintf( pFile, "!" );
- Kit_DsdPrint_rec( pFile, pNtk, Dsd_NtkRoot(pNtk) );
+ Kit_DsdPrint_rec( pFile, pNtk, Dsd_Lit2Var(pNtk->Root) );
fprintf( pFile, "\n" );
}
/**Function*************************************************************
+ Synopsis [Derives the truth table of the DSD node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Kit_DsdTruthComputeNode_rec( Dsd_Man_t * p, Dsd_Ntk_t * pNtk, int Id )
+{
+ Dsd_Obj_t * pObj;
+ unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16];
+ unsigned i, m, iLit, nMints, fCompl;
+
+ // get the node with this ID
+ pObj = Dsd_NtkObj( 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, Dsd_Lit2Var(iLit) );
+ if ( Dsd_LitIsCompl(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
+ Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
+ pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Dsd_Lit2Var(iLit) );
+ // create the truth table
+
+ // simple gates
+ if ( pObj->Type == KIT_DSD_AND )
+ {
+ Kit_TruthFill( pTruthRes, pNtk->nVars );
+ Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
+ Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Dsd_LitIsCompl(iLit) );
+ return pTruthRes;
+ }
+ if ( pObj->Type == KIT_DSD_XOR )
+ {
+ Kit_TruthClear( pTruthRes, pNtk->nVars );
+ fCompl = 0;
+ Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
+ {
+ Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars );
+ fCompl ^= Dsd_LitIsCompl(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 = Dsd_ObjTruth( 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 );
+ Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
+ Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, Dsd_LitIsCompl(iLit) );
+ Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars );
+ }
+ return pTruthRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives the truth table of the DSD network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+unsigned * Kit_DsdTruthCompute( Dsd_Man_t * p, Dsd_Ntk_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, Dsd_Lit2Var(pNtk->Root) );
+ // complement the truth table if needed
+ if ( Dsd_LitIsCompl(pNtk->Root) )
+ Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars );
+ return pTruthRes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Expands the node.]
+
+ Description [Returns the new literal.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdExpandCollectAnd_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int * nLitsNew )
+{
+ Dsd_Obj_t * pObj;
+ unsigned i, iLitFanin;
+ // check the end of the supergate
+ pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) );
+ if ( Dsd_LitIsCompl(iLit) || Dsd_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_AND )
+ {
+ piLitsNew[(*nLitsNew)++] = iLit;
+ return;
+ }
+ // iterate through the fanins
+ Dsd_ObjForEachFanin( p, pObj, iLitFanin, i )
+ Kit_DsdExpandCollectAnd_rec( p, iLitFanin, piLitsNew, nLitsNew );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Expands the node.]
+
+ Description [Returns the new literal.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Kit_DsdExpandCollectXor_rec( Dsd_Ntk_t * p, int iLit, int * piLitsNew, int * nLitsNew )
+{
+ Dsd_Obj_t * pObj;
+ unsigned i, iLitFanin;
+ // check the end of the supergate
+ pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) );
+ if ( Dsd_Lit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_XOR )
+ {
+ piLitsNew[(*nLitsNew)++] = iLit;
+ return;
+ }
+ // iterate through the fanins
+ pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) );
+ Dsd_ObjForEachFanin( p, pObj, iLitFanin, i )
+ Kit_DsdExpandCollectXor_rec( p, iLitFanin, piLitsNew, nLitsNew );
+ // if the literal was complemented, pass the complemented attribute somewhere
+ if ( Dsd_LitIsCompl(iLit) )
+ piLitsNew[0] = Dsd_LitNot( piLitsNew[0] );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Expands the node.]
+
+ Description [Returns the new literal.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DsdExpandNode_rec( Dsd_Ntk_t * pNew, Dsd_Ntk_t * p, int iLit )
+{
+ unsigned * pTruth, * pTruthNew;
+ unsigned i, fCompl, iLitFanin, piLitsNew[16], nLitsNew = 0;
+ Dsd_Obj_t * pObj, * pObjNew;
+
+ // remember the complement
+ fCompl = Dsd_LitIsCompl(iLit);
+ iLit = Dsd_LitRegular(iLit);
+ assert( !Dsd_LitIsCompl(iLit) );
+
+ // consider the case of simple gate
+ pObj = Dsd_NtkObj( p, Dsd_Lit2Var(iLit) );
+ if ( pObj->Type == KIT_DSD_AND )
+ {
+ Kit_DsdExpandCollectAnd_rec( p, iLit, piLitsNew, &nLitsNew );
+ pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_AND, nLitsNew );
+ for ( i = 0; i < pObjNew->nFans; i++ )
+ pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] );
+ return Dsd_Var2Lit( pObjNew->Id, fCompl );
+ }
+ if ( pObj->Type == KIT_DSD_XOR )
+ {
+ Kit_DsdExpandCollectXor_rec( p, iLit, piLitsNew, &nLitsNew );
+ pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_XOR, nLitsNew );
+ for ( i = 0; i < pObjNew->nFans; i++ )
+ {
+ pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, Dsd_LitRegular(piLitsNew[i]) );
+ fCompl ^= Dsd_LitIsCompl(piLitsNew[i]);
+ }
+ return Dsd_Var2Lit( pObjNew->Id, fCompl );
+ }
+ assert( pObj->Type == KIT_DSD_PRIME );
+
+ // create new PRIME node
+ pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans );
+ // copy the truth table
+ pTruth = Dsd_ObjTruth( pObj );
+ pTruthNew = Dsd_ObjTruth( pObjNew );
+ Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans );
+ // create fanins
+ Dsd_ObjForEachFanin( pNtk, pObj, iLitFanin, i )
+ {
+ pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, iLitFanin );
+ // complement the corresponding inputs of the truth table
+ if ( Dsd_LitIsCompl(pObjNew->pFans[i]) )
+ {
+ pObjNew->pFans[i] = Dsd_LitRegular(pObjNew->pFans[i]);
+ Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i );
+ }
+ }
+ // if the incoming phase is complemented, absorb it into the prime node
+ if ( fCompl )
+ Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans );
+ return Dsd_Var2Lit( pObjNew->Id, 0 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Expands the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dsd_Ntk_t * Kit_DsdExpand( Dsd_Ntk_t * p )
+{
+ Dsd_Ntk_t * pNew;
+ Dsd_Obj_t * pObjNew;
+ assert( p->nVars <= 16 );
+ // create a new network
+ pNew = Kit_DsdNtkAlloc( p->nVars );
+ // consider simple special cases
+ if ( Dsd_NtkRoot(p)->Type == KIT_DSD_CONST1 )
+ {
+ pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_CONST1, 0 );
+ pNew->Root = Dsd_Var2Lit( pObjNew->Id, Dsd_LitIsCompl(p->Root) );
+ return pNew;
+ }
+ if ( Dsd_NtkRoot(p)->Type == KIT_DSD_VAR )
+ {
+ pObjNew = Dsd_ObjAlloc( pNew, KIT_DSD_VAR, 1 );
+ pObjNew->pFans[0] = Dsd_NtkRoot(p)->pFans[0];
+ pNew->Root = Dsd_Var2Lit( pObjNew->Id, Dsd_LitIsCompl(p->Root) );
+ return pNew;
+ }
+ // convert the root node
+ pNew->Root = Kit_DsdExpandNode_rec( pNew, p, p->Root );
+ return pNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if there is a component with more than 3 inputs.]
Description []
@@ -274,16 +625,16 @@ void Kit_DsdPrint( FILE * pFile, Dsd_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj )
+int Kit_DsdFindLargeBox( Dsd_Ntk_t * pNtk, int Id )
{
- Dsd_Obj_t * pFanin;
- unsigned iVar, i, RetValue;
+ Dsd_Obj_t * pObj;
+ unsigned iLit, i, RetValue;
+ pObj = Dsd_NtkObj( pNtk, Id );
if ( pObj->nFans > 3 )
return 1;
RetValue = 0;
- Dsd_ObjForEachFanin( pNtk, pObj, pFanin, iVar, i )
- if ( pFanin )
- RetValue |= Kit_DsdFindLargeBox( pNtk, pFanin );
+ Dsd_ObjForEachFanin( pNtk, pObj, iLit, i )
+ RetValue |= Kit_DsdFindLargeBox( pNtk, Dsd_Lit2Var(iLit) );
return RetValue;
}
@@ -305,7 +656,7 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
unsigned * pTruth = Dsd_ObjTruth(pObj);
unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords };
unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} };
- int i, iVar0, iVar1, nFans0, nFans1, nPairs;
+ int i, iLit0, iLit1, nFans0, nFans1, nPairs;
int fEquals[2][2], fOppos, fPairs[4][4];
unsigned j, k, nFansNew, uSupp0, uSupp1;
@@ -331,12 +682,12 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
{
pObj->Type = KIT_DSD_NONE;
if ( pTruth[0] == 0x55555555 )
- pObj->pFans[0] ^= 1;
+ pObj->pFans[0] = Dsd_LitNot(pObj->pFans[0]);
else
assert( pTruth[0] == 0xAAAAAAAA );
// update the parent pointer
-// assert( !((*pPar) & 1) );
- *pPar = pObj->pFans[0] ^ ((*pPar) & 1);
+// assert( !Dsd_LitIsCompl(*pPar) );
+ *pPar = Dsd_LitNotCond( pObj->pFans[0], Dsd_LitIsCompl(*pPar) );
return;
}
@@ -375,13 +726,14 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
Kit_TruthCopy( Dsd_ObjTruth(pRes0), pCofs2[0], pObj->nFans );
Kit_TruthCopy( Dsd_ObjTruth(pRes1), pCofs2[1], pObj->nFans );
// update the current one
- pObj->Type = KIT_DSD_MUX;
+ assert( pObj->Type == KIT_DSD_PRIME );
+ pTruth[0] = 0xCACACACA;
pObj->nFans = 3;
- pObj->pFans[0] = pObj->pFans[i];
+ pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++;
pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++;
- pObj->pFans[2] = 2*pRes0->Id; pRes0->nRefs++;
+ pObj->pFans[2] = pObj->pFans[i];
// call recursively
- Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 2 );
+ Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0 );
Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1 );
return;
}
@@ -402,20 +754,20 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
}
else if ( fEquals[0][1] )
{
- pRes->pFans[0] ^= 1;
+ pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]);
Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
}
else if ( fEquals[1][0] )
{
- *pPar ^= 1;
- pRes->pFans[1] ^= 1;
+ *pPar = Dsd_LitNot(*pPar);
+ pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]);
Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans );
}
else if ( fEquals[1][1] )
{
- *pPar ^= 1;
- pRes->pFans[0] ^= 1;
- pRes->pFans[1] ^= 1;
+ *pPar = Dsd_LitNot(*pPar);
+ pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]);
+ pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]);
Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans );
}
else if ( fOppos )
@@ -457,13 +809,13 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
if ( nFans0 == 1 && nFans1 == 1 )
{
// get the cofactors w.r.t. the unique variables
- iVar0 = Kit_WordFindFirstBit( uSupp0 & ~uSupp1 );
- iVar1 = Kit_WordFindFirstBit( uSupp1 & ~uSupp0 );
+ iLit0 = Kit_WordFindFirstBit( uSupp0 & ~uSupp1 );
+ iLit1 = Kit_WordFindFirstBit( uSupp1 & ~uSupp0 );
// get four cofactors
- Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, iVar0 );
- Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, iVar0 );
- Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, iVar1 );
- Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, iVar1 );
+ Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, iLit0 );
+ Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, iLit0 );
+ Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, iLit1 );
+ Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, iLit1 );
// check existence conditions
fEquals[0][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans );
fEquals[0][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans );
@@ -472,12 +824,13 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) )
{
// construct the MUX
- pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_MUX, 3 );
+ pRes = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, 3 );
+ Dsd_ObjTruth(pRes)[0] = 0xCACACACA;
pRes->nRefs++;
pRes->nFans = 3;
- pRes->pFans[0] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support
- pRes->pFans[1] = pObj->pFans[iVar1]; pObj->pFans[iVar1] = 127; uSupp &= ~(1 << iVar1);
- pRes->pFans[2] = pObj->pFans[iVar0]; pObj->pFans[iVar0] = 127; uSupp &= ~(1 << iVar0);
+ pRes->pFans[0] = pObj->pFans[iLit0]; pObj->pFans[iLit0] = 127; uSupp &= ~(1 << iLit0);
+ pRes->pFans[1] = pObj->pFans[iLit1]; pObj->pFans[iLit1] = 127; uSupp &= ~(1 << iLit1);
+ pRes->pFans[2] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support
// update the node
if ( fEquals[0][0] && fEquals[0][1] )
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i );
@@ -516,18 +869,18 @@ void Kit_DsdDecompose_rec( Dsd_Ntk_t * pNtk, Dsd_Obj_t * pObj, unsigned uSupp, u
pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i);
if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00
{
- pRes->pFans[0] ^= 1;
- pRes->pFans[1] ^= 1;
+ pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]);
+ pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]);
Kit_TruthMux( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k );
}
else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01
{
- pRes->pFans[0] ^= 1;
+ pRes->pFans[0] = Dsd_LitNot(pRes->pFans[0]);
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k );
}
else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10
{
- pRes->pFans[1] ^= 1;
+ pRes->pFans[1] = Dsd_LitNot(pRes->pFans[1]);
Kit_TruthMux( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k );
}
else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11
@@ -572,13 +925,13 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
unsigned uSupp;
int i, nVarsReal;
assert( nVars <= 16 );
- pNtk = Kit_DsdNtkAlloc( pTruth, nVars );
- pNtk->Root = 2*pNtk->nVars;
+ pNtk = Kit_DsdNtkAlloc( nVars );
+ pNtk->Root = Dsd_Var2Lit( pNtk->nVars, 0 );
// create the first node
pObj = Dsd_ObjAlloc( pNtk, KIT_DSD_PRIME, nVars );
- pNtk->pNodes[0] = pObj;
+ assert( pNtk->pNodes[0] == pObj );
for ( i = 0; i < nVars; i++ )
- pObj->pFans[i] = 2*i;
+ pObj->pFans[i] = Dsd_Var2Lit( i, 0 );
Kit_TruthCopy( Dsd_ObjTruth(pObj), pTruth, nVars );
uSupp = Kit_TruthSupport( pTruth, nVars );
// consider special cases
@@ -587,15 +940,15 @@ Dsd_Ntk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars )
{
pObj->Type = KIT_DSD_CONST1;
pObj->nFans = 0;
- pNtk->Root ^= (pTruth[0] == 0);
+ if ( pTruth[0] == 0 )
+ pNtk->Root = Dsd_LitNot(pNtk->Root);
return pNtk;
}
if ( nVarsReal == 1 )
{
pObj->Type = KIT_DSD_VAR;
pObj->nFans = 1;
- pObj->pFans[0] = 2 * Kit_WordFindFirstBit( uSupp );
- pObj->pFans[0] ^= (pTruth[0] & 1);
+ pObj->pFans[0] = Dsd_Var2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) );
return pNtk;
}
Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root );
@@ -674,7 +1027,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
Dsd_Ntk_t * pNtk;
pNtk = Kit_DsdDecompose( pTruth, nVars );
-// if ( Kit_DsdFindLargeBox(pNtk, Dsd_NtkRoot(pNtk)) )
+// if ( Kit_DsdFindLargeBox(pNtk, Dsd_Lit2Var(pNtk->Root)) )
// Kit_DsdPrint( stdout, pNtk );
// if ( Dsd_NtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 )
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 16:05:49 +0000