From 028138a76eb74eee80f1d9592f43bdbe0d4c3d6c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 30 Mar 2007 08:01:00 -0700 Subject: Version abc70330 --- abc.dsp | 4 + src/base/abc/abc.h | 14 ++ src/base/abc/abcSop.c | 4 +- src/base/abci/abc.c | 117 ++++++++++ src/base/abci/abcDsdRes.c | 563 ++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/module.make | 1 + src/base/cmd/cmd.c | 6 + src/base/io/io.c | 6 +- src/misc/vec/vecPtr.h | 39 ++++ src/opt/kit/kit.h | 6 + src/opt/kit/kitDsd.c | 503 +++++++++++++++++++++++++++++++++++------ 11 files changed, 1183 insertions(+), 80 deletions(-) create mode 100644 src/base/abci/abcDsdRes.c diff --git a/abc.dsp b/abc.dsp index 7d5e9e58..1e4f44a1 100644 --- a/abc.dsp +++ b/abc.dsp @@ -226,6 +226,10 @@ SOURCE=.\src\base\abci\abcDsd.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcDsdRes.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcEspresso.c # End Source File # Begin Source File 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 ] [-Q ] [-S ] [-vwh]\n" ); + fprintf( pErr, "\t performs \"rewriting\" for LUT networks\n" ); + fprintf( pErr, "\t-N : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax ); + fprintf( pErr, "\t-Q : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver ); + fprintf( pErr, "\t-S : the max number of LUT inputs shared (0 <= num) [default = %d]\n", pPars->nVarsShared ); + fprintf( pErr, "\t-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 @@ -175,6 +175,45 @@ static inline Vec_Ptr_t * Vec_PtrAllocSimInfo( int nEntries, int nWords ) return Vec_PtrAllocArray( pMemory, nEntries ); } +/**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.] 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 ); @@ -76,6 +96,47 @@ extern void Kit_DsdNtkFree( Dsd_Ntk_t * pNtk ); /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**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.] @@ -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,12 +321,299 @@ 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.] @@ -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 ) -- cgit v1.2.3