diff options
Diffstat (limited to 'src/opt/kit/kitDsd.c')
| -rw-r--r-- | src/opt/kit/kitDsd.c | 503 |
1 files changed, 428 insertions, 75 deletions
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 ) |