src/aig/kit/kitDsd.c File Reference
#include "kit.h"
Include dependency graph for kitDsd.c:
Go to the source code of this file.
Functions | |
| Kit_DsdMan_t * | Kit_DsdManAlloc (int nVars, int nNodes) |
| void | Kit_DsdManFree (Kit_DsdMan_t *p) |
| Kit_DsdObj_t * | Kit_DsdObjAlloc (Kit_DsdNtk_t *pNtk, Kit_Dsd_t Type, int nFans) |
| void | Kit_DsdObjFree (Kit_DsdNtk_t *p, Kit_DsdObj_t *pObj) |
| Kit_DsdNtk_t * | Kit_DsdNtkAlloc (int nVars) |
| void | Kit_DsdNtkFree (Kit_DsdNtk_t *pNtk) |
| void | Kit_DsdPrintHex (FILE *pFile, unsigned *pTruth, int nFans) |
| void | Kit_DsdPrint_rec (FILE *pFile, Kit_DsdNtk_t *pNtk, int Id) |
| void | Kit_DsdPrint (FILE *pFile, Kit_DsdNtk_t *pNtk) |
| void | Kit_DsdPrintExpanded (Kit_DsdNtk_t *pNtk) |
| void | Kit_DsdPrintFromTruth (unsigned *pTruth, int nVars) |
| unsigned * | Kit_DsdTruthComputeNode_rec (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id) |
| unsigned * | Kit_DsdTruthCompute (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk) |
| unsigned * | Kit_DsdTruthComputeNodeOne_rec (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id, unsigned uSupp) |
| unsigned * | Kit_DsdTruthComputeOne (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp) |
| unsigned * | Kit_DsdTruthComputeNodeTwo_rec (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, int Id, unsigned uSupp, int iVar, unsigned *pTruthDec) |
| unsigned * | Kit_DsdTruthComputeTwo (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthDec) |
| void | Kit_DsdTruth (Kit_DsdNtk_t *pNtk, unsigned *pTruthRes) |
| void | Kit_DsdTruthPartialTwo (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned uSupp, int iVar, unsigned *pTruthCo, unsigned *pTruthDec) |
| void | Kit_DsdTruthPartial (Kit_DsdMan_t *p, Kit_DsdNtk_t *pNtk, unsigned *pTruthRes, unsigned uSupp) |
| int | Kit_DsdCountLuts_rec (Kit_DsdNtk_t *pNtk, int nLutSize, int Id, int *pCounter) |
| int | Kit_DsdCountLuts (Kit_DsdNtk_t *pNtk, int nLutSize) |
| int | Kit_DsdNonDsdSizeMax (Kit_DsdNtk_t *pNtk) |
| unsigned | Kit_DsdNonDsdSupports (Kit_DsdNtk_t *pNtk) |
| void | Kit_DsdExpandCollectAnd_rec (Kit_DsdNtk_t *p, int iLit, int *piLitsNew, int *nLitsNew) |
| void | Kit_DsdExpandCollectXor_rec (Kit_DsdNtk_t *p, int iLit, int *piLitsNew, int *nLitsNew) |
| int | Kit_DsdExpandNode_rec (Kit_DsdNtk_t *pNew, Kit_DsdNtk_t *p, int iLit) |
| Kit_DsdNtk_t * | Kit_DsdExpand (Kit_DsdNtk_t *p) |
| void | Kit_DsdCompSort (int pPrios[], unsigned uSupps[], unsigned char *piLits, int nVars, int piLitsRes[]) |
| int | Kit_DsdShrink_rec (Kit_DsdNtk_t *pNew, Kit_DsdNtk_t *p, int iLit, int pPrios[]) |
| Kit_DsdNtk_t * | Kit_DsdShrink (Kit_DsdNtk_t *p, int pPrios[]) |
| void | Kit_DsdRotate (Kit_DsdNtk_t *p, int pFreqs[]) |
| unsigned | Kit_DsdGetSupports_rec (Kit_DsdNtk_t *p, int iLit) |
| unsigned | Kit_DsdGetSupports (Kit_DsdNtk_t *p) |
| int | Kit_DsdFindLargeBox_rec (Kit_DsdNtk_t *pNtk, int Id, int Size) |
| int | Kit_DsdFindLargeBox (Kit_DsdNtk_t *pNtk, int Size) |
| int | Kit_DsdRootNodeHasCommonVars (Kit_DsdObj_t *pObj0, Kit_DsdObj_t *pObj1) |
| int | Kit_DsdCheckVar4Dec2 (Kit_DsdNtk_t *pNtk0, Kit_DsdNtk_t *pNtk1) |
| void | Kit_DsdDecompose_rec (Kit_DsdNtk_t *pNtk, Kit_DsdObj_t *pObj, unsigned uSupp, unsigned char *pPar, int nDecMux) |
| Kit_DsdNtk_t * | Kit_DsdDecomposeInt (unsigned *pTruth, int nVars, int nDecMux) |
| Kit_DsdNtk_t * | Kit_DsdDecompose (unsigned *pTruth, int nVars) |
| Kit_DsdNtk_t * | Kit_DsdDecomposeExpand (unsigned *pTruth, int nVars) |
| Kit_DsdNtk_t * | Kit_DsdDecomposeMux (unsigned *pTruth, int nVars, int nDecMux) |
| int | Kit_DsdTestCofs (Kit_DsdNtk_t *pNtk, unsigned *pTruthInit) |
| int | Kit_DsdEval (unsigned *pTruth, int nVars, int nLutSize) |
| void | Kit_DsdVerify (Kit_DsdNtk_t *pNtk, unsigned *pTruth, int nVars) |
| void | Kit_DsdTest (unsigned *pTruth, int nVars) |
| void | Kit_DsdPrecompute4Vars () |
| int | Kit_DsdCofactoringGetVars (Kit_DsdNtk_t **ppNtk, int nSize, int *pVars) |
| int | Kit_DsdCofactoring (unsigned *pTruth, int nVars, int *pCofVars, int nLimit, int fVerbose) |
| void | Kit_DsdPrintCofactors (unsigned *pTruth, int nVars, int nCofLevel, int fVerbose) |
Function Documentation
| int Kit_DsdCheckVar4Dec2 | ( | Kit_DsdNtk_t * | pNtk0, | |
| Kit_DsdNtk_t * | pNtk1 | |||
| ) |
Function*************************************************************
Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
Description []
SideEffects []
SeeAlso []
Definition at line 1557 of file kitDsd.c.
01558 { 01559 assert( pNtk0->nVars == 4 ); 01560 assert( pNtk1->nVars == 4 ); 01561 if ( Kit_DsdFindLargeBox(pNtk0, 2) ) 01562 return 0; 01563 if ( Kit_DsdFindLargeBox(pNtk1, 2) ) 01564 return 0; 01565 return Kit_DsdRootNodeHasCommonVars( Kit_DsdNtkRoot(pNtk0), Kit_DsdNtkRoot(pNtk1) ); 01566 }
| int Kit_DsdCofactoring | ( | unsigned * | pTruth, | |
| int | nVars, | |||
| int * | pCofVars, | |||
| int | nLimit, | |||
| int | fVerbose | |||
| ) |
Function*************************************************************
Synopsis [Canonical decomposition into completely DSD-structure.]
Description [Returns the number of cofactoring steps. Also returns the cofactoring variables in pVars.]
SideEffects []
SeeAlso []
Definition at line 2266 of file kitDsd.c.
02267 { 02268 Kit_DsdNtk_t * ppNtks[5][16] = {0}, * pTemp; 02269 unsigned * ppCofs[5][16]; 02270 int pTryVars[16], nTryVars; 02271 int nPrimeSizeMin, nPrimeSizeMax, nPrimeSizeCur; 02272 int nSuppSizeMin, nSuppSizeMax, iVarBest; 02273 int i, k, v, nStep, nSize, nMemSize; 02274 assert( nLimit < 5 ); 02275 02276 // allocate storage for cofactors 02277 nMemSize = Kit_TruthWordNum(nVars); 02278 ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize ); 02279 nSize = 0; 02280 for ( i = 0; i < 5; i++ ) 02281 for ( k = 0; k < 16; k++ ) 02282 ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++; 02283 assert( nSize == 80 ); 02284 02285 // copy the function 02286 Kit_TruthCopy( ppCofs[0][0], pTruth, nVars ); 02287 ppNtks[0][0] = Kit_DsdDecompose( ppCofs[0][0], nVars ); 02288 02289 if ( fVerbose ) 02290 printf( "\nProcessing prime function with %d support variables:\n", nVars ); 02291 02292 // perform recursive cofactoring 02293 for ( nStep = 0; nStep < nLimit; nStep++ ) 02294 { 02295 nSize = (1 << nStep); 02296 // find the variables to use in the cofactoring step 02297 nTryVars = Kit_DsdCofactoringGetVars( ppNtks[nStep], nSize, pTryVars ); 02298 if ( nTryVars == 0 ) 02299 break; 02300 // cofactor w.r.t. the above variables 02301 iVarBest = -1; 02302 nPrimeSizeMin = 10000; 02303 nSuppSizeMin = 10000; 02304 for ( v = 0; v < nTryVars; v++ ) 02305 { 02306 nPrimeSizeMax = 0; 02307 nSuppSizeMax = 0; 02308 for ( i = 0; i < nSize; i++ ) 02309 { 02310 // cofactor and decompose cofactors 02311 Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, pTryVars[v] ); 02312 Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, pTryVars[v] ); 02313 ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars ); 02314 ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars ); 02315 // compute the largest non-decomp block 02316 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+0]); 02317 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); 02318 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[nStep+1][2*i+1]); 02319 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); 02320 // compute the sum total of supports 02321 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+0], nVars ); 02322 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nStep+1][2*i+1], nVars ); 02323 // free the networks 02324 Kit_DsdNtkFree( ppNtks[nStep+1][2*i+0] ); 02325 Kit_DsdNtkFree( ppNtks[nStep+1][2*i+1] ); 02326 } 02327 // find the min max support size of the prime component 02328 if ( nPrimeSizeMin > nPrimeSizeMax || (nPrimeSizeMin == nPrimeSizeMax && nSuppSizeMin > nSuppSizeMax) ) 02329 { 02330 nPrimeSizeMin = nPrimeSizeMax; 02331 nSuppSizeMin = nSuppSizeMax; 02332 iVarBest = pTryVars[v]; 02333 } 02334 } 02335 assert( iVarBest != -1 ); 02336 // save the variable 02337 if ( pCofVars ) 02338 pCofVars[nStep] = iVarBest; 02339 // cofactor w.r.t. the best 02340 for ( i = 0; i < nSize; i++ ) 02341 { 02342 Kit_TruthCofactor0New( ppCofs[nStep+1][2*i+0], ppCofs[nStep][i], nVars, iVarBest ); 02343 Kit_TruthCofactor1New( ppCofs[nStep+1][2*i+1], ppCofs[nStep][i], nVars, iVarBest ); 02344 ppNtks[nStep+1][2*i+0] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+0], nVars ); 02345 ppNtks[nStep+1][2*i+1] = Kit_DsdDecompose( ppCofs[nStep+1][2*i+1], nVars ); 02346 if ( fVerbose ) 02347 { 02348 ppNtks[nStep+1][2*i+0] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+0] ); 02349 Kit_DsdNtkFree( pTemp ); 02350 ppNtks[nStep+1][2*i+1] = Kit_DsdExpand( pTemp = ppNtks[nStep+1][2*i+1] ); 02351 Kit_DsdNtkFree( pTemp ); 02352 02353 printf( "Cof%d%d: ", nStep+1, 2*i+0 ); 02354 Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] ); 02355 printf( "Cof%d%d: ", nStep+1, 2*i+1 ); 02356 Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] ); 02357 } 02358 } 02359 } 02360 02361 // free the networks 02362 for ( i = 0; i < 5; i++ ) 02363 for ( k = 0; k < 16; k++ ) 02364 if ( ppNtks[i][k] ) 02365 Kit_DsdNtkFree( ppNtks[i][k] ); 02366 free( ppCofs[0][0] ); 02367 02368 assert( nStep <= nLimit ); 02369 return nStep; 02370 }
| int Kit_DsdCofactoringGetVars | ( | Kit_DsdNtk_t ** | ppNtk, | |
| int | nSize, | |||
| int * | pVars | |||
| ) |
Function*************************************************************
Synopsis [Returns the set of cofactoring variables.]
Description [If there is no DSD components returns 0.]
SideEffects []
SeeAlso []
Definition at line 2220 of file kitDsd.c.
02221 { 02222 Kit_DsdObj_t * pObj; 02223 unsigned m; 02224 int i, k, v, Var, nVars, iFaninLit; 02225 // go through all the networks 02226 nVars = 0; 02227 for ( i = 0; i < nSize; i++ ) 02228 { 02229 // go through the prime objects of each networks 02230 Kit_DsdNtkForEachObj( ppNtk[i], pObj, k ) 02231 { 02232 if ( pObj->Type != KIT_DSD_PRIME ) 02233 continue; 02234 if ( pObj->nFans == 3 ) 02235 continue; 02236 // collect direct fanin variables 02237 Kit_DsdObjForEachFanin( ppNtk[i], pObj, iFaninLit, m ) 02238 { 02239 if ( !Kit_DsdLitIsLeaf(ppNtk[i], iFaninLit) ) 02240 continue; 02241 // add it to the array 02242 Var = Kit_DsdLit2Var( iFaninLit ); 02243 for ( v = 0; v < nVars; v++ ) 02244 if ( pVars[v] == Var ) 02245 break; 02246 if ( v == nVars ) 02247 pVars[nVars++] = Var; 02248 } 02249 } 02250 } 02251 return nVars; 02252 }
| void Kit_DsdCompSort | ( | int | pPrios[], | |
| unsigned | uSupps[], | |||
| unsigned char * | piLits, | |||
| int | nVars, | |||
| int | piLitsRes[] | |||
| ) |
Function*************************************************************
Synopsis [Sorts the literals by their support.]
Description []
SideEffects []
SeeAlso []
Definition at line 1182 of file kitDsd.c.
01183 { 01184 int nSuppSizes[16], Priority[16], pOrder[16]; 01185 int i, k, iVarBest, SuppMax, PrioMax; 01186 // compute support sizes and priorities of the components 01187 for ( i = 0; i < nVars; i++ ) 01188 { 01189 assert( uSupps[i] ); 01190 pOrder[i] = i; 01191 Priority[i] = KIT_INFINITY; 01192 for ( k = 0; k < 16; k++ ) 01193 if ( uSupps[i] & (1 << k) ) 01194 Priority[i] = KIT_MIN( Priority[i], pPrios[k] ); 01195 assert( Priority[i] != 16 ); 01196 nSuppSizes[i] = Kit_WordCountOnes(uSupps[i]); 01197 } 01198 // sort the components by pririty 01199 Extra_BubbleSort( pOrder, Priority, nVars, 0 ); 01200 // find the component by with largest size and lowest priority 01201 iVarBest = -1; 01202 SuppMax = 0; 01203 PrioMax = 0; 01204 for ( i = 0; i < nVars; i++ ) 01205 { 01206 if ( SuppMax < nSuppSizes[i] || (SuppMax == nSuppSizes[i] && PrioMax < Priority[i]) ) 01207 { 01208 SuppMax = nSuppSizes[i]; 01209 PrioMax = Priority[i]; 01210 iVarBest = i; 01211 } 01212 } 01213 assert( iVarBest != -1 ); 01214 // copy the resulting literals 01215 k = 0; 01216 piLitsRes[k++] = piLits[iVarBest]; 01217 for ( i = 0; i < nVars; i++ ) 01218 { 01219 if ( pOrder[i] == iVarBest ) 01220 continue; 01221 piLitsRes[k++] = piLits[pOrder[i]]; 01222 } 01223 assert( k == nVars ); 01224 }
| int Kit_DsdCountLuts | ( | Kit_DsdNtk_t * | pNtk, | |
| int | nLutSize | |||
| ) |
Function*************************************************************
Synopsis [Counts the number of blocks of the given number of inputs.]
Description []
SideEffects []
SeeAlso []
Definition at line 945 of file kitDsd.c.
00946 { 00947 int Counter = 0; 00948 if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_CONST1 ) 00949 return 0; 00950 if ( Kit_DsdNtkRoot(pNtk)->Type == KIT_DSD_VAR ) 00951 return 0; 00952 Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pNtk->Root), &Counter ); 00953 if ( Counter >= 1000 ) 00954 return -1; 00955 return Counter; 00956 }
| int Kit_DsdCountLuts_rec | ( | Kit_DsdNtk_t * | pNtk, | |
| int | nLutSize, | |||
| int | Id, | |||
| int * | pCounter | |||
| ) |
Function*************************************************************
Synopsis [Counts the number of blocks of the given number of inputs.]
Description []
SideEffects []
SeeAlso []
Definition at line 901 of file kitDsd.c.
00902 { 00903 Kit_DsdObj_t * pObj; 00904 unsigned iLit, i, Res0, Res1; 00905 pObj = Kit_DsdNtkObj( pNtk, Id ); 00906 if ( pObj == NULL ) 00907 return 0; 00908 if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR ) 00909 { 00910 assert( pObj->nFans == 2 ); 00911 Res0 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pObj->pFans[0]), pCounter ); 00912 Res1 = Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(pObj->pFans[1]), pCounter ); 00913 if ( Res0 == 0 && Res1 > 0 ) 00914 return Res1 - 1; 00915 if ( Res0 > 0 && Res1 == 0 ) 00916 return Res0 - 1; 00917 (*pCounter)++; 00918 return nLutSize - 2; 00919 } 00920 assert( pObj->Type == KIT_DSD_PRIME ); 00921 if ( (int)pObj->nFans > nLutSize ) //+ 1 ) 00922 { 00923 *pCounter = 1000; 00924 return 0; 00925 } 00926 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00927 Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(iLit), pCounter ); 00928 (*pCounter)++; 00929 // if ( (int)pObj->nFans == nLutSize + 1 ) 00930 // (*pCounter)++; 00931 return nLutSize - pObj->nFans; 00932 }
| Kit_DsdNtk_t* Kit_DsdDecompose | ( | unsigned * | pTruth, | |
| int | nVars | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
Definition at line 1923 of file kitDsd.c.
01924 { 01925 return Kit_DsdDecomposeInt( pTruth, nVars, 0 ); 01926 }
| void Kit_DsdDecompose_rec | ( | Kit_DsdNtk_t * | pNtk, | |
| Kit_DsdObj_t * | pObj, | |||
| unsigned | uSupp, | |||
| unsigned char * | pPar, | |||
| int | nDecMux | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the node.]
Description []
SideEffects []
SeeAlso []
Definition at line 1579 of file kitDsd.c.
01580 { 01581 Kit_DsdObj_t * pRes, * pRes0, * pRes1; 01582 int nWords = Kit_TruthWordNum(pObj->nFans); 01583 unsigned * pTruth = Kit_DsdObjTruth(pObj); 01584 unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + nWords }; 01585 unsigned * pCofs4[2][2] = { {pNtk->pMem + 2 * nWords, pNtk->pMem + 3 * nWords}, {pNtk->pMem + 4 * nWords, pNtk->pMem + 5 * nWords} }; 01586 int i, iLit0, iLit1, nFans0, nFans1, nPairs; 01587 int fEquals[2][2], fOppos, fPairs[4][4]; 01588 unsigned j, k, nFansNew, uSupp0, uSupp1; 01589 01590 assert( pObj->nFans > 0 ); 01591 assert( pObj->Type == KIT_DSD_PRIME ); 01592 assert( uSupp == (uSupp0 = (unsigned)Kit_TruthSupport(pTruth, pObj->nFans)) ); 01593 01594 // compress the truth table 01595 if ( uSupp != Kit_BitMask(pObj->nFans) ) 01596 { 01597 nFansNew = Kit_WordCountOnes(uSupp); 01598 Kit_TruthShrink( pNtk->pMem, pTruth, nFansNew, pObj->nFans, uSupp, 1 ); 01599 for ( j = k = 0; j < pObj->nFans; j++ ) 01600 if ( uSupp & (1 << j) ) 01601 pObj->pFans[k++] = pObj->pFans[j]; 01602 assert( k == nFansNew ); 01603 pObj->nFans = k; 01604 uSupp = Kit_BitMask(pObj->nFans); 01605 } 01606 01607 // consider the single variable case 01608 if ( pObj->nFans == 1 ) 01609 { 01610 pObj->Type = KIT_DSD_NONE; 01611 if ( pTruth[0] == 0x55555555 ) 01612 pObj->pFans[0] = Kit_DsdLitNot(pObj->pFans[0]); 01613 else 01614 assert( pTruth[0] == 0xAAAAAAAA ); 01615 // update the parent pointer 01616 *pPar = Kit_DsdLitNotCond( pObj->pFans[0], Kit_DsdLitIsCompl(*pPar) ); 01617 return; 01618 } 01619 01620 // decompose the output 01621 if ( !pObj->fMark ) 01622 for ( i = pObj->nFans - 1; i >= 0; i-- ) 01623 { 01624 // get the two-variable cofactors 01625 Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i ); 01626 Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i ); 01627 // assert( !Kit_TruthVarInSupport( pCofs2[0], pObj->nFans, i) ); 01628 // assert( !Kit_TruthVarInSupport( pCofs2[1], pObj->nFans, i) ); 01629 // get the constant cofs 01630 fEquals[0][0] = Kit_TruthIsConst0( pCofs2[0], pObj->nFans ); 01631 fEquals[0][1] = Kit_TruthIsConst0( pCofs2[1], pObj->nFans ); 01632 fEquals[1][0] = Kit_TruthIsConst1( pCofs2[0], pObj->nFans ); 01633 fEquals[1][1] = Kit_TruthIsConst1( pCofs2[1], pObj->nFans ); 01634 fOppos = Kit_TruthIsOpposite( pCofs2[0], pCofs2[1], pObj->nFans ); 01635 assert( !Kit_TruthIsEqual(pCofs2[0], pCofs2[1], pObj->nFans) ); 01636 if ( fEquals[0][0] + fEquals[0][1] + fEquals[1][0] + fEquals[1][1] + fOppos == 0 ) 01637 { 01638 // check the MUX decomposition 01639 uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans ); 01640 uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans ); 01641 assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) ); 01642 if ( uSupp0 & uSupp1 ) 01643 continue; 01644 // perform MUX decomposition 01645 pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans ); 01646 pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans ); 01647 for ( k = 0; k < pObj->nFans; k++ ) 01648 { 01649 pRes0->pFans[k] = (uSupp0 & (1 << k))? pObj->pFans[k] : 127; 01650 pRes1->pFans[k] = (uSupp1 & (1 << k))? pObj->pFans[k] : 127; 01651 } 01652 Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans ); 01653 Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans ); 01654 // update the current one 01655 assert( pObj->Type == KIT_DSD_PRIME ); 01656 pTruth[0] = 0xCACACACA; 01657 pObj->nFans = 3; 01658 pObj->pFans[2] = pObj->pFans[i]; 01659 pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++; 01660 pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++; 01661 // call recursively 01662 Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux ); 01663 Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux ); 01664 return; 01665 } 01666 01667 // create the new node 01668 pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 ); 01669 pRes->nRefs++; 01670 pRes->nFans = 2; 01671 pRes->pFans[0] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i); 01672 pRes->pFans[1] = 2*pObj->Id; 01673 // update the parent pointer 01674 *pPar = Kit_DsdLitNotCond( 2 * pRes->Id, Kit_DsdLitIsCompl(*pPar) ); 01675 // consider different decompositions 01676 if ( fEquals[0][0] ) 01677 { 01678 Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans ); 01679 } 01680 else if ( fEquals[0][1] ) 01681 { 01682 pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]); 01683 Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans ); 01684 } 01685 else if ( fEquals[1][0] ) 01686 { 01687 *pPar = Kit_DsdLitNot(*pPar); 01688 pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]); 01689 Kit_TruthCopy( pTruth, pCofs2[1], pObj->nFans ); 01690 } 01691 else if ( fEquals[1][1] ) 01692 { 01693 *pPar = Kit_DsdLitNot(*pPar); 01694 pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]); 01695 pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]); 01696 Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans ); 01697 } 01698 else if ( fOppos ) 01699 { 01700 pRes->Type = KIT_DSD_XOR; 01701 Kit_TruthCopy( pTruth, pCofs2[0], pObj->nFans ); 01702 } 01703 else 01704 assert( 0 ); 01705 // decompose the remainder 01706 assert( Kit_DsdObjTruth(pObj) == pTruth ); 01707 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pRes->pFans + 1, nDecMux ); 01708 return; 01709 } 01710 pObj->fMark = 1; 01711 01712 // decompose the input 01713 for ( i = pObj->nFans - 1; i >= 0; i-- ) 01714 { 01715 assert( Kit_TruthVarInSupport( pTruth, pObj->nFans, i ) ); 01716 // get the single variale cofactors 01717 Kit_TruthCofactor0New( pCofs2[0], pTruth, pObj->nFans, i ); 01718 Kit_TruthCofactor1New( pCofs2[1], pTruth, pObj->nFans, i ); 01719 // check the existence of MUX decomposition 01720 uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans ); 01721 uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans ); 01722 assert( uSupp == (uSupp0 | uSupp1 | (1<<i)) ); 01723 // if one of the cofs is a constant, it is time to check the output again 01724 if ( uSupp0 == 0 || uSupp1 == 0 ) 01725 { 01726 pObj->fMark = 0; 01727 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux ); 01728 return; 01729 } 01730 assert( uSupp0 && uSupp1 ); 01731 // get the number of unique variables 01732 nFans0 = Kit_WordCountOnes( uSupp0 & ~uSupp1 ); 01733 nFans1 = Kit_WordCountOnes( uSupp1 & ~uSupp0 ); 01734 if ( nFans0 == 1 && nFans1 == 1 ) 01735 { 01736 // get the cofactors w.r.t. the unique variables 01737 iLit0 = Kit_WordFindFirstBit( uSupp0 & ~uSupp1 ); 01738 iLit1 = Kit_WordFindFirstBit( uSupp1 & ~uSupp0 ); 01739 // get four cofactors 01740 Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, iLit0 ); 01741 Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, iLit0 ); 01742 Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, iLit1 ); 01743 Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, iLit1 ); 01744 // check existence conditions 01745 fEquals[0][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans ); 01746 fEquals[0][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans ); 01747 fEquals[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans ); 01748 fEquals[1][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans ); 01749 if ( (fEquals[0][0] && fEquals[0][1]) || (fEquals[1][0] && fEquals[1][1]) ) 01750 { 01751 // construct the MUX 01752 pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, 3 ); 01753 Kit_DsdObjTruth(pRes)[0] = 0xCACACACA; 01754 pRes->nRefs++; 01755 pRes->nFans = 3; 01756 pRes->pFans[0] = pObj->pFans[iLit0]; pObj->pFans[iLit0] = 127; uSupp &= ~(1 << iLit0); 01757 pRes->pFans[1] = pObj->pFans[iLit1]; pObj->pFans[iLit1] = 127; uSupp &= ~(1 << iLit1); 01758 pRes->pFans[2] = pObj->pFans[i]; pObj->pFans[i] = 2 * pRes->Id; // remains in support 01759 // update the node 01760 // if ( fEquals[0][0] && fEquals[0][1] ) 01761 // Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, i ); 01762 // else 01763 // Kit_TruthMuxVar( pTruth, pCofs4[0][1], pCofs4[0][0], pObj->nFans, i ); 01764 Kit_TruthMuxVar( pTruth, pCofs4[1][0], pCofs4[1][1], pObj->nFans, i ); 01765 if ( fEquals[1][0] && fEquals[1][1] ) 01766 pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]); 01767 // decompose the remainder 01768 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux ); 01769 return; 01770 } 01771 } 01772 01773 // try other inputs 01774 for ( k = i+1; k < pObj->nFans; k++ ) 01775 { 01776 // get four cofactors ik 01777 Kit_TruthCofactor0New( pCofs4[0][0], pCofs2[0], pObj->nFans, k ); // 00 01778 Kit_TruthCofactor1New( pCofs4[0][1], pCofs2[0], pObj->nFans, k ); // 01 01779 Kit_TruthCofactor0New( pCofs4[1][0], pCofs2[1], pObj->nFans, k ); // 10 01780 Kit_TruthCofactor1New( pCofs4[1][1], pCofs2[1], pObj->nFans, k ); // 11 01781 // compare equal pairs 01782 fPairs[0][1] = fPairs[1][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[0][1], pObj->nFans ); 01783 fPairs[0][2] = fPairs[2][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][0], pObj->nFans ); 01784 fPairs[0][3] = fPairs[3][0] = Kit_TruthIsEqual( pCofs4[0][0], pCofs4[1][1], pObj->nFans ); 01785 fPairs[1][2] = fPairs[2][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][0], pObj->nFans ); 01786 fPairs[1][3] = fPairs[3][1] = Kit_TruthIsEqual( pCofs4[0][1], pCofs4[1][1], pObj->nFans ); 01787 fPairs[2][3] = fPairs[3][2] = Kit_TruthIsEqual( pCofs4[1][0], pCofs4[1][1], pObj->nFans ); 01788 nPairs = fPairs[0][1] + fPairs[0][2] + fPairs[0][3] + fPairs[1][2] + fPairs[1][3] + fPairs[2][3]; 01789 if ( nPairs != 3 && nPairs != 2 ) 01790 continue; 01791 01792 // decomposition exists 01793 pRes = Kit_DsdObjAlloc( pNtk, KIT_DSD_AND, 2 ); 01794 pRes->nRefs++; 01795 pRes->nFans = 2; 01796 pRes->pFans[0] = pObj->pFans[k]; pObj->pFans[k] = 2 * pRes->Id; // remains in support 01797 pRes->pFans[1] = pObj->pFans[i]; pObj->pFans[i] = 127; uSupp &= ~(1 << i); 01798 if ( !fPairs[0][1] && !fPairs[0][2] && !fPairs[0][3] ) // 00 01799 { 01800 pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]); 01801 pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]); 01802 Kit_TruthMuxVar( pTruth, pCofs4[1][1], pCofs4[0][0], pObj->nFans, k ); 01803 } 01804 else if ( !fPairs[1][0] && !fPairs[1][2] && !fPairs[1][3] ) // 01 01805 { 01806 pRes->pFans[1] = Kit_DsdLitNot(pRes->pFans[1]); 01807 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k ); 01808 } 01809 else if ( !fPairs[2][0] && !fPairs[2][1] && !fPairs[2][3] ) // 10 01810 { 01811 pRes->pFans[0] = Kit_DsdLitNot(pRes->pFans[0]); 01812 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][0], pObj->nFans, k ); 01813 } 01814 else if ( !fPairs[3][0] && !fPairs[3][1] && !fPairs[3][2] ) // 11 01815 { 01816 // unsigned uSupp0 = Kit_TruthSupport(pCofs4[0][0], pObj->nFans); 01817 // unsigned uSupp1 = Kit_TruthSupport(pCofs4[1][1], pObj->nFans); 01818 // unsigned uSupp; 01819 // Extra_PrintBinary( stdout, &uSupp0, pObj->nFans ); printf( "\n" ); 01820 // Extra_PrintBinary( stdout, &uSupp1, pObj->nFans ); printf( "\n" ); 01821 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[1][1], pObj->nFans, k ); 01822 // uSupp = Kit_TruthSupport(pTruth, pObj->nFans); 01823 // Extra_PrintBinary( stdout, &uSupp, pObj->nFans ); printf( "\n" ); printf( "\n" ); 01824 } 01825 else 01826 { 01827 assert( fPairs[0][3] && fPairs[1][2] ); 01828 pRes->Type = KIT_DSD_XOR;; 01829 Kit_TruthMuxVar( pTruth, pCofs4[0][0], pCofs4[0][1], pObj->nFans, k ); 01830 } 01831 // decompose the remainder 01832 Kit_DsdDecompose_rec( pNtk, pObj, uSupp, pPar, nDecMux ); 01833 return; 01834 } 01835 } 01836 /* 01837 // if all decomposition methods failed and we are still above the limit, perform MUX-decomposition 01838 if ( nDecMux > 0 && (int)pObj->nFans > nDecMux ) 01839 { 01840 int iBestVar = Kit_TruthBestCofVar( pTruth, pObj->nFans, pCofs2[0], pCofs2[1] ); 01841 uSupp0 = Kit_TruthSupport( pCofs2[0], pObj->nFans ); 01842 uSupp1 = Kit_TruthSupport( pCofs2[1], pObj->nFans ); 01843 // perform MUX decomposition 01844 pRes0 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans ); 01845 pRes1 = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, pObj->nFans ); 01846 for ( k = 0; k < pObj->nFans; k++ ) 01847 pRes0->pFans[k] = pRes1->pFans[k] = pObj->pFans[k]; 01848 Kit_TruthCopy( Kit_DsdObjTruth(pRes0), pCofs2[0], pObj->nFans ); 01849 Kit_TruthCopy( Kit_DsdObjTruth(pRes1), pCofs2[1], pObj->nFans ); 01850 // update the current one 01851 assert( pObj->Type == KIT_DSD_PRIME ); 01852 pTruth[0] = 0xCACACACA; 01853 pObj->nFans = 3; 01854 pObj->pFans[0] = 2*pRes0->Id; pRes0->nRefs++; 01855 pObj->pFans[1] = 2*pRes1->Id; pRes1->nRefs++; 01856 pObj->pFans[2] = pObj->pFans[iBestVar]; 01857 // call recursively 01858 Kit_DsdDecompose_rec( pNtk, pRes0, uSupp0, pObj->pFans + 0, nDecMux ); 01859 Kit_DsdDecompose_rec( pNtk, pRes1, uSupp1, pObj->pFans + 1, nDecMux ); 01860 } 01861 */ 01862 }
| Kit_DsdNtk_t* Kit_DsdDecomposeExpand | ( | unsigned * | pTruth, | |
| int | nVars | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
Definition at line 1939 of file kitDsd.c.
01940 { 01941 Kit_DsdNtk_t * pNtk, * pTemp; 01942 pNtk = Kit_DsdDecomposeInt( pTruth, nVars, 0 ); 01943 pNtk = Kit_DsdExpand( pTemp = pNtk ); 01944 Kit_DsdNtkFree( pTemp ); 01945 return pNtk; 01946 }
| Kit_DsdNtk_t* Kit_DsdDecomposeInt | ( | unsigned * | pTruth, | |
| int | nVars, | |||
| int | nDecMux | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
Definition at line 1875 of file kitDsd.c.
01876 { 01877 Kit_DsdNtk_t * pNtk; 01878 Kit_DsdObj_t * pObj; 01879 unsigned uSupp; 01880 int i, nVarsReal; 01881 assert( nVars <= 16 ); 01882 pNtk = Kit_DsdNtkAlloc( nVars ); 01883 pNtk->Root = Kit_DsdVar2Lit( pNtk->nVars, 0 ); 01884 // create the first node 01885 pObj = Kit_DsdObjAlloc( pNtk, KIT_DSD_PRIME, nVars ); 01886 assert( pNtk->pNodes[0] == pObj ); 01887 for ( i = 0; i < nVars; i++ ) 01888 pObj->pFans[i] = Kit_DsdVar2Lit( i, 0 ); 01889 Kit_TruthCopy( Kit_DsdObjTruth(pObj), pTruth, nVars ); 01890 uSupp = Kit_TruthSupport( pTruth, nVars ); 01891 // consider special cases 01892 nVarsReal = Kit_WordCountOnes( uSupp ); 01893 if ( nVarsReal == 0 ) 01894 { 01895 pObj->Type = KIT_DSD_CONST1; 01896 pObj->nFans = 0; 01897 if ( pTruth[0] == 0 ) 01898 pNtk->Root = Kit_DsdLitNot(pNtk->Root); 01899 return pNtk; 01900 } 01901 if ( nVarsReal == 1 ) 01902 { 01903 pObj->Type = KIT_DSD_VAR; 01904 pObj->nFans = 1; 01905 pObj->pFans[0] = Kit_DsdVar2Lit( Kit_WordFindFirstBit(uSupp), (pTruth[0] & 1) ); 01906 return pNtk; 01907 } 01908 Kit_DsdDecompose_rec( pNtk, pNtk->pNodes[0], uSupp, &pNtk->Root, nDecMux ); 01909 return pNtk; 01910 }
| Kit_DsdNtk_t* Kit_DsdDecomposeMux | ( | unsigned * | pTruth, | |
| int | nVars, | |||
| int | nDecMux | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description [Uses MUXes to break-down large prime nodes.]
SideEffects []
SeeAlso []
Definition at line 1959 of file kitDsd.c.
01960 { 01961 return Kit_DsdDecomposeInt( pTruth, nVars, nDecMux ); 01962 }
| int Kit_DsdEval | ( | unsigned * | pTruth, | |
| int | nVars, | |||
| int | nLutSize | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
Definition at line 2044 of file kitDsd.c.
02045 { 02046 Kit_DsdMan_t * p; 02047 Kit_DsdNtk_t * pNtk; 02048 unsigned * pTruthC; 02049 int Result; 02050 02051 // decompose the function 02052 pNtk = Kit_DsdDecompose( pTruth, nVars ); 02053 Result = Kit_DsdCountLuts( pNtk, nLutSize ); 02054 // printf( "\n" ); 02055 // Kit_DsdPrint( stdout, pNtk ); 02056 // printf( "Eval = %d.\n", Result ); 02057 02058 // recompute the truth table 02059 p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) ); 02060 pTruthC = Kit_DsdTruthCompute( p, pNtk ); 02061 if ( !Kit_TruthIsEqual( pTruth, pTruthC, nVars ) ) 02062 printf( "Verification failed.\n" ); 02063 Kit_DsdManFree( p ); 02064 02065 Kit_DsdNtkFree( pNtk ); 02066 return Result; 02067 }
| Kit_DsdNtk_t* Kit_DsdExpand | ( | Kit_DsdNtk_t * | p | ) |
Function*************************************************************
Synopsis [Expands the network.]
Description []
SideEffects []
SeeAlso []
Definition at line 1145 of file kitDsd.c.
01146 { 01147 Kit_DsdNtk_t * pNew; 01148 Kit_DsdObj_t * pObjNew; 01149 assert( p->nVars <= 16 ); 01150 // create a new network 01151 pNew = Kit_DsdNtkAlloc( p->nVars ); 01152 // consider simple special cases 01153 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 ) 01154 { 01155 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 ); 01156 pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) ); 01157 return pNew; 01158 } 01159 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR ) 01160 { 01161 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 ); 01162 pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0]; 01163 pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) ); 01164 return pNew; 01165 } 01166 // convert the root node 01167 pNew->Root = Kit_DsdExpandNode_rec( pNew, p, p->Root ); 01168 return pNew; 01169 }
| void Kit_DsdExpandCollectAnd_rec | ( | Kit_DsdNtk_t * | p, | |
| int | iLit, | |||
| int * | piLitsNew, | |||
| int * | nLitsNew | |||
| ) |
Function*************************************************************
Synopsis [Expands the node.]
Description [Returns the new literal.]
SideEffects []
SeeAlso []
Definition at line 1021 of file kitDsd.c.
01022 { 01023 Kit_DsdObj_t * pObj; 01024 unsigned i, iLitFanin; 01025 // check the end of the supergate 01026 pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); 01027 if ( Kit_DsdLitIsCompl(iLit) || Kit_DsdLit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_AND ) 01028 { 01029 piLitsNew[(*nLitsNew)++] = iLit; 01030 return; 01031 } 01032 // iterate through the fanins 01033 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) 01034 Kit_DsdExpandCollectAnd_rec( p, iLitFanin, piLitsNew, nLitsNew ); 01035 }
| void Kit_DsdExpandCollectXor_rec | ( | Kit_DsdNtk_t * | p, | |
| int | iLit, | |||
| int * | piLitsNew, | |||
| int * | nLitsNew | |||
| ) |
Function*************************************************************
Synopsis [Expands the node.]
Description [Returns the new literal.]
SideEffects []
SeeAlso []
Definition at line 1048 of file kitDsd.c.
01049 { 01050 Kit_DsdObj_t * pObj; 01051 unsigned i, iLitFanin; 01052 // check the end of the supergate 01053 pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); 01054 if ( Kit_DsdLit2Var(iLit) < p->nVars || pObj->Type != KIT_DSD_XOR ) 01055 { 01056 piLitsNew[(*nLitsNew)++] = iLit; 01057 return; 01058 } 01059 // iterate through the fanins 01060 pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); 01061 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) 01062 Kit_DsdExpandCollectXor_rec( p, iLitFanin, piLitsNew, nLitsNew ); 01063 // if the literal was complemented, pass the complemented attribute somewhere 01064 if ( Kit_DsdLitIsCompl(iLit) ) 01065 piLitsNew[0] = Kit_DsdLitNot( piLitsNew[0] ); 01066 }
| int Kit_DsdExpandNode_rec | ( | Kit_DsdNtk_t * | pNew, | |
| Kit_DsdNtk_t * | p, | |||
| int | iLit | |||
| ) |
Function*************************************************************
Synopsis [Expands the node.]
Description [Returns the new literal.]
SideEffects []
SeeAlso []
Definition at line 1079 of file kitDsd.c.
01080 { 01081 unsigned * pTruth, * pTruthNew; 01082 unsigned i, iLitFanin, piLitsNew[16], nLitsNew = 0; 01083 Kit_DsdObj_t * pObj, * pObjNew; 01084 01085 // consider the case of simple gate 01086 pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); 01087 if ( pObj == NULL ) 01088 return iLit; 01089 if ( pObj->Type == KIT_DSD_AND ) 01090 { 01091 Kit_DsdExpandCollectAnd_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew ); 01092 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, nLitsNew ); 01093 for ( i = 0; i < pObjNew->nFans; i++ ) 01094 pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, piLitsNew[i] ); 01095 return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) ); 01096 } 01097 if ( pObj->Type == KIT_DSD_XOR ) 01098 { 01099 int fCompl = Kit_DsdLitIsCompl(iLit); 01100 Kit_DsdExpandCollectXor_rec( p, Kit_DsdLitRegular(iLit), piLitsNew, &nLitsNew ); 01101 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, nLitsNew ); 01102 for ( i = 0; i < pObjNew->nFans; i++ ) 01103 { 01104 pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, Kit_DsdLitRegular(piLitsNew[i]) ); 01105 fCompl ^= Kit_DsdLitIsCompl(piLitsNew[i]); 01106 } 01107 return Kit_DsdVar2Lit( pObjNew->Id, fCompl ); 01108 } 01109 assert( pObj->Type == KIT_DSD_PRIME ); 01110 01111 // create new PRIME node 01112 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans ); 01113 // copy the truth table 01114 pTruth = Kit_DsdObjTruth( pObj ); 01115 pTruthNew = Kit_DsdObjTruth( pObjNew ); 01116 Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans ); 01117 // create fanins 01118 Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i ) 01119 { 01120 pObjNew->pFans[i] = Kit_DsdExpandNode_rec( pNew, p, iLitFanin ); 01121 // complement the corresponding inputs of the truth table 01122 if ( Kit_DsdLitIsCompl(pObjNew->pFans[i]) ) 01123 { 01124 pObjNew->pFans[i] = Kit_DsdLitRegular(pObjNew->pFans[i]); 01125 Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i ); 01126 } 01127 } 01128 // if the incoming phase is complemented, absorb it into the prime node 01129 if ( Kit_DsdLitIsCompl(iLit) ) 01130 Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans ); 01131 return Kit_DsdVar2Lit( pObjNew->Id, 0 ); 01132 }
| int Kit_DsdFindLargeBox | ( | Kit_DsdNtk_t * | pNtk, | |
| int | Size | |||
| ) |
Function*************************************************************
Synopsis [Returns 1 if there is a component with more than 3 inputs.]
Description []
SideEffects []
SeeAlso []
Definition at line 1516 of file kitDsd.c.
01517 { 01518 return Kit_DsdFindLargeBox_rec( pNtk, Kit_DsdLit2Var(pNtk->Root), Size ); 01519 }
| int Kit_DsdFindLargeBox_rec | ( | Kit_DsdNtk_t * | pNtk, | |
| int | Id, | |||
| int | Size | |||
| ) |
Function*************************************************************
Synopsis [Returns 1 if there is a component with more than 3 inputs.]
Description []
SideEffects []
SeeAlso []
Definition at line 1490 of file kitDsd.c.
01491 { 01492 Kit_DsdObj_t * pObj; 01493 unsigned iLit, i, RetValue; 01494 pObj = Kit_DsdNtkObj( pNtk, Id ); 01495 if ( pObj == NULL ) 01496 return 0; 01497 if ( pObj->Type == KIT_DSD_PRIME && (int)pObj->nFans > Size ) 01498 return 1; 01499 RetValue = 0; 01500 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 01501 RetValue |= Kit_DsdFindLargeBox_rec( pNtk, Kit_DsdLit2Var(iLit), Size ); 01502 return RetValue; 01503 }
| unsigned Kit_DsdGetSupports | ( | Kit_DsdNtk_t * | p | ) |
Function*************************************************************
Synopsis [Compute the support.]
Description []
SideEffects []
SeeAlso []
Definition at line 1455 of file kitDsd.c.
01456 { 01457 Kit_DsdObj_t * pRoot; 01458 unsigned uSupport; 01459 assert( p->pSupps == NULL ); 01460 p->pSupps = ALLOC( unsigned, p->nNodes ); 01461 // consider simple special cases 01462 pRoot = Kit_DsdNtkRoot(p); 01463 if ( pRoot->Type == KIT_DSD_CONST1 ) 01464 { 01465 assert( p->nNodes == 1 ); 01466 uSupport = p->pSupps[0] = 0; 01467 } 01468 if ( pRoot->Type == KIT_DSD_VAR ) 01469 { 01470 assert( p->nNodes == 1 ); 01471 uSupport = p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] ); 01472 } 01473 else 01474 uSupport = Kit_DsdGetSupports_rec( p, p->Root ); 01475 assert( uSupport <= 0xFFFF ); 01476 return uSupport; 01477 }
| unsigned Kit_DsdGetSupports_rec | ( | Kit_DsdNtk_t * | p, | |
| int | iLit | |||
| ) |
Function*************************************************************
Synopsis [Compute the support.]
Description []
SideEffects []
SeeAlso []
Definition at line 1428 of file kitDsd.c.
01429 { 01430 Kit_DsdObj_t * pObj; 01431 unsigned uSupport, k; 01432 int iFaninLit; 01433 pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); 01434 if ( pObj == NULL ) 01435 return Kit_DsdLitSupport( p, iLit ); 01436 uSupport = 0; 01437 Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k ) 01438 uSupport |= Kit_DsdGetSupports_rec( p, iFaninLit ); 01439 p->pSupps[pObj->Id - p->nVars] = uSupport; 01440 assert( uSupport <= 0xFFFF ); 01441 return uSupport; 01442 }
| Kit_DsdMan_t* Kit_DsdManAlloc | ( | int | nVars, | |
| int | nNodes | |||
| ) |
CFile****************************************************************
FileName [kitDsd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Computation kit.]
Synopsis [Performs disjoint-support decomposition based on truth tables.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Dec 6, 2006.]
Revision [
- Id
- kitDsd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp
] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************
Synopsis [Allocates the DSD manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 42 of file kitDsd.c.
00043 { 00044 Kit_DsdMan_t * p; 00045 p = ALLOC( Kit_DsdMan_t, 1 ); 00046 memset( p, 0, sizeof(Kit_DsdMan_t) ); 00047 p->nVars = nVars; 00048 p->nWords = Kit_TruthWordNum( p->nVars ); 00049 p->vTtElems = Vec_PtrAllocTruthTables( p->nVars ); 00050 p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords ); 00051 p->dd = Cloud_Init( 16, 14 ); 00052 p->vTtBdds = Vec_PtrAllocSimInfo( (1<<12), p->nWords ); 00053 p->vNodes = Vec_IntAlloc( 512 ); 00054 return p; 00055 }
| void Kit_DsdManFree | ( | Kit_DsdMan_t * | p | ) |
Function*************************************************************
Synopsis [Deallocates the DSD manager.]
Description []
SideEffects []
SeeAlso []
Definition at line 68 of file kitDsd.c.
00069 { 00070 Cloud_Quit( p->dd ); 00071 Vec_IntFree( p->vNodes ); 00072 Vec_PtrFree( p->vTtBdds ); 00073 Vec_PtrFree( p->vTtElems ); 00074 Vec_PtrFree( p->vTtNodes ); 00075 free( p ); 00076 }
| int Kit_DsdNonDsdSizeMax | ( | Kit_DsdNtk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Counts the number of blocks of the given number of inputs.]
Description []
SideEffects []
SeeAlso []
Definition at line 969 of file kitDsd.c.
00970 { 00971 Kit_DsdObj_t * pObj; 00972 unsigned i, nSizeMax = 0; 00973 Kit_DsdNtkForEachObj( pNtk, pObj, i ) 00974 { 00975 if ( pObj->Type != KIT_DSD_PRIME ) 00976 continue; 00977 if ( nSizeMax < pObj->nFans ) 00978 nSizeMax = pObj->nFans; 00979 } 00980 return nSizeMax; 00981 }
| unsigned Kit_DsdNonDsdSupports | ( | Kit_DsdNtk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Finds the union of supports of the non-DSD blocks.]
Description []
SideEffects []
SeeAlso []
Definition at line 994 of file kitDsd.c.
00995 { 00996 Kit_DsdObj_t * pObj; 00997 unsigned i, uSupport = 0; 00998 // FREE( pNtk->pSupps ); 00999 Kit_DsdGetSupports( pNtk ); 01000 Kit_DsdNtkForEachObj( pNtk, pObj, i ) 01001 { 01002 if ( pObj->Type != KIT_DSD_PRIME ) 01003 continue; 01004 uSupport |= Kit_DsdLitSupport( pNtk, Kit_DsdVar2Lit(pObj->Id,0) ); 01005 } 01006 return uSupport; 01007 }
| Kit_DsdNtk_t* Kit_DsdNtkAlloc | ( | int | nVars | ) |
Function*************************************************************
Synopsis [Allocates the DSD network.]
Description []
SideEffects []
SeeAlso []
Definition at line 137 of file kitDsd.c.
00138 { 00139 Kit_DsdNtk_t * pNtk; 00140 pNtk = ALLOC( Kit_DsdNtk_t, 1 ); 00141 memset( pNtk, 0, sizeof(Kit_DsdNtk_t) ); 00142 pNtk->pNodes = ALLOC( Kit_DsdObj_t *, nVars ); 00143 pNtk->nVars = nVars; 00144 pNtk->nNodesAlloc = nVars; 00145 pNtk->pMem = ALLOC( unsigned, 6 * Kit_TruthWordNum(nVars) ); 00146 return pNtk; 00147 }
| void Kit_DsdNtkFree | ( | Kit_DsdNtk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Deallocate the DSD network.]
Description []
SideEffects []
SeeAlso []
Definition at line 160 of file kitDsd.c.
00161 { 00162 Kit_DsdObj_t * pObj; 00163 unsigned i; 00164 Kit_DsdNtkForEachObj( pNtk, pObj, i ) 00165 free( pObj ); 00166 FREE( pNtk->pSupps ); 00167 free( pNtk->pNodes ); 00168 free( pNtk->pMem ); 00169 free( pNtk ); 00170 }
| Kit_DsdObj_t* Kit_DsdObjAlloc | ( | Kit_DsdNtk_t * | pNtk, | |
| Kit_Dsd_t | Type, | |||
| int | nFans | |||
| ) |
Function*************************************************************
Synopsis [Allocates the DSD node.]
Description []
SideEffects []
SeeAlso []
Definition at line 89 of file kitDsd.c.
00090 { 00091 Kit_DsdObj_t * pObj; 00092 int nSize = sizeof(Kit_DsdObj_t) + sizeof(unsigned) * (Kit_DsdObjOffset(nFans) + (Type == KIT_DSD_PRIME) * Kit_TruthWordNum(nFans)); 00093 pObj = (Kit_DsdObj_t *)ALLOC( char, nSize ); 00094 memset( pObj, 0, nSize ); 00095 pObj->Id = pNtk->nVars + pNtk->nNodes; 00096 pObj->Type = Type; 00097 pObj->nFans = nFans; 00098 pObj->Offset = Kit_DsdObjOffset( nFans ); 00099 // add the object 00100 if ( pNtk->nNodes == pNtk->nNodesAlloc ) 00101 { 00102 pNtk->nNodesAlloc *= 2; 00103 pNtk->pNodes = REALLOC( Kit_DsdObj_t *, pNtk->pNodes, pNtk->nNodesAlloc ); 00104 } 00105 assert( pNtk->nNodes < pNtk->nNodesAlloc ); 00106 pNtk->pNodes[pNtk->nNodes++] = pObj; 00107 return pObj; 00108 }
| void Kit_DsdObjFree | ( | Kit_DsdNtk_t * | p, | |
| Kit_DsdObj_t * | pObj | |||
| ) |
| void Kit_DsdPrecompute4Vars | ( | ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
Definition at line 2153 of file kitDsd.c.
02154 { 02155 Kit_DsdMan_t * p; 02156 Kit_DsdNtk_t * pNtk, * pTemp; 02157 FILE * pFile; 02158 unsigned uTruth; 02159 unsigned * pTruthC; 02160 char Buffer[256]; 02161 int i, RetValue; 02162 int Counter1 = 0, Counter2 = 0; 02163 02164 pFile = fopen( "5npn/npn4.txt", "r" ); 02165 for ( i = 0; fgets( Buffer, 100, pFile ); i++ ) 02166 { 02167 Buffer[6] = 0; 02168 Extra_ReadHexadecimal( &uTruth, Buffer+2, 4 ); 02169 uTruth = ((uTruth & 0xffff) << 16) | (uTruth & 0xffff); 02170 pNtk = Kit_DsdDecompose( &uTruth, 4 ); 02171 02172 pNtk = Kit_DsdExpand( pTemp = pNtk ); 02173 Kit_DsdNtkFree( pTemp ); 02174 02175 02176 if ( Kit_DsdFindLargeBox(pNtk, 3) ) 02177 { 02178 // RetValue = 0; 02179 RetValue = Kit_DsdTestCofs( pNtk, &uTruth ); 02180 printf( "\n" ); 02181 printf( "%3d : Non-DSD function %s %s\n", i, Buffer + 2, RetValue? "implementable" : "" ); 02182 Kit_DsdPrint( stdout, pNtk ); 02183 02184 Counter1++; 02185 Counter2 += RetValue; 02186 } 02187 02188 /* 02189 printf( "%3d : Function %s ", i, Buffer + 2 ); 02190 if ( !Kit_DsdFindLargeBox(pNtk, 3) ) 02191 Kit_DsdPrint( stdout, pNtk ); 02192 else 02193 printf( "\n" ); 02194 */ 02195 02196 p = Kit_DsdManAlloc( 4, Kit_DsdNtkObjNum(pNtk) ); 02197 pTruthC = Kit_DsdTruthCompute( p, pNtk ); 02198 if ( !Extra_TruthIsEqual( &uTruth, pTruthC, 4 ) ) 02199 printf( "Verification failed.\n" ); 02200 Kit_DsdManFree( p ); 02201 02202 Kit_DsdNtkFree( pNtk ); 02203 } 02204 fclose( pFile ); 02205 printf( "non-DSD = %d implementable = %d\n", Counter1, Counter2 ); 02206 }
| void Kit_DsdPrint | ( | FILE * | pFile, | |
| Kit_DsdNtk_t * | pNtk | |||
| ) |
Function*************************************************************
Synopsis [Print the DSD formula.]
Description []
SideEffects []
SeeAlso []
Definition at line 265 of file kitDsd.c.
00266 { 00267 fprintf( pFile, "F = " ); 00268 if ( Kit_DsdLitIsCompl(pNtk->Root) ) 00269 fprintf( pFile, "!" ); 00270 Kit_DsdPrint_rec( pFile, pNtk, Kit_DsdLit2Var(pNtk->Root) ); 00271 fprintf( pFile, "\n" ); 00272 }
| void Kit_DsdPrint_rec | ( | FILE * | pFile, | |
| Kit_DsdNtk_t * | pNtk, | |||
| int | Id | |||
| ) |
Function*************************************************************
Synopsis [Recursively print the DSD formula.]
Description []
SideEffects []
SeeAlso []
Definition at line 208 of file kitDsd.c.
00209 { 00210 Kit_DsdObj_t * pObj; 00211 unsigned iLit, i; 00212 char Symbol; 00213 00214 pObj = Kit_DsdNtkObj( pNtk, Id ); 00215 if ( pObj == NULL ) 00216 { 00217 assert( Id < pNtk->nVars ); 00218 fprintf( pFile, "%c", 'a' + Id ); 00219 return; 00220 } 00221 00222 if ( pObj->Type == KIT_DSD_CONST1 ) 00223 { 00224 assert( pObj->nFans == 0 ); 00225 fprintf( pFile, "Const1" ); 00226 return; 00227 } 00228 00229 if ( pObj->Type == KIT_DSD_VAR ) 00230 assert( pObj->nFans == 1 ); 00231 00232 if ( pObj->Type == KIT_DSD_AND ) 00233 Symbol = '*'; 00234 else if ( pObj->Type == KIT_DSD_XOR ) 00235 Symbol = '+'; 00236 else 00237 Symbol = ','; 00238 00239 if ( pObj->Type == KIT_DSD_PRIME ) 00240 Kit_DsdPrintHex( stdout, Kit_DsdObjTruth(pObj), pObj->nFans ); 00241 00242 fprintf( pFile, "(" ); 00243 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00244 { 00245 if ( Kit_DsdLitIsCompl(iLit) ) 00246 fprintf( pFile, "!" ); 00247 Kit_DsdPrint_rec( pFile, pNtk, Kit_DsdLit2Var(iLit) ); 00248 if ( i < pObj->nFans - 1 ) 00249 fprintf( pFile, "%c", Symbol ); 00250 } 00251 fprintf( pFile, ")" ); 00252 }
| void Kit_DsdPrintCofactors | ( | unsigned * | pTruth, | |
| int | nVars, | |||
| int | nCofLevel, | |||
| int | fVerbose | |||
| ) |
Function*************************************************************
Synopsis [Canonical decomposition into completely DSD-structure.]
Description [Returns the number of cofactoring steps. Also returns the cofactoring variables in pVars.]
SideEffects []
SeeAlso []
Definition at line 2384 of file kitDsd.c.
02385 { 02386 Kit_DsdNtk_t * ppNtks[32] = {0}, * pTemp; 02387 unsigned * ppCofs[5][16]; 02388 int piCofVar[5]; 02389 int nPrimeSizeMax, nPrimeSizeCur, nSuppSizeMax; 02390 int i, k, v1, v2, v3, v4, s, nSteps, nSize, nMemSize; 02391 assert( nCofLevel < 5 ); 02392 02393 // print the function 02394 ppNtks[0] = Kit_DsdDecompose( pTruth, nVars ); 02395 ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); 02396 Kit_DsdNtkFree( pTemp ); 02397 if ( fVerbose ) 02398 Kit_DsdPrint( stdout, ppNtks[0] ); 02399 Kit_DsdNtkFree( ppNtks[0] ); 02400 02401 // allocate storage for cofactors 02402 nMemSize = Kit_TruthWordNum(nVars); 02403 ppCofs[0][0] = ALLOC( unsigned, 80 * nMemSize ); 02404 nSize = 0; 02405 for ( i = 0; i < 5; i++ ) 02406 for ( k = 0; k < 16; k++ ) 02407 ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++; 02408 assert( nSize == 80 ); 02409 02410 // copy the function 02411 Kit_TruthCopy( ppCofs[0][0], pTruth, nVars ); 02412 02413 if ( nCofLevel == 1 ) 02414 for ( v1 = 0; v1 < nVars; v1++ ) 02415 { 02416 nSteps = 0; 02417 piCofVar[nSteps++] = v1; 02418 02419 printf( " Variables { " ); 02420 for ( i = 0; i < nSteps; i++ ) 02421 printf( "%c ", 'a' + piCofVar[i] ); 02422 printf( "}\n" ); 02423 02424 // single cofactors 02425 for ( s = 1; s <= nSteps; s++ ) 02426 { 02427 for ( k = 0; k < s; k++ ) 02428 { 02429 nSize = (1 << k); 02430 for ( i = 0; i < nSize; i++ ) 02431 { 02432 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); 02433 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); 02434 } 02435 } 02436 } 02437 // compute DSD networks 02438 nSize = (1 << nSteps); 02439 nPrimeSizeMax = 0; 02440 nSuppSizeMax = 0; 02441 for ( i = 0; i < nSize; i++ ) 02442 { 02443 ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars ); 02444 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); 02445 Kit_DsdNtkFree( pTemp ); 02446 if ( fVerbose ) 02447 { 02448 printf( "Cof%d%d: ", nSteps, i ); 02449 Kit_DsdPrint( stdout, ppNtks[i] ); 02450 } 02451 // compute the largest non-decomp block 02452 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]); 02453 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); 02454 Kit_DsdNtkFree( ppNtks[i] ); 02455 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars ); 02456 } 02457 printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax ); 02458 } 02459 02460 if ( nCofLevel == 2 ) 02461 for ( v1 = 0; v1 < nVars; v1++ ) 02462 for ( v2 = v1+1; v2 < nVars; v2++ ) 02463 { 02464 nSteps = 0; 02465 piCofVar[nSteps++] = v1; 02466 piCofVar[nSteps++] = v2; 02467 02468 printf( " Variables { " ); 02469 for ( i = 0; i < nSteps; i++ ) 02470 printf( "%c ", 'a' + piCofVar[i] ); 02471 printf( "}\n" ); 02472 02473 // single cofactors 02474 for ( s = 1; s <= nSteps; s++ ) 02475 { 02476 for ( k = 0; k < s; k++ ) 02477 { 02478 nSize = (1 << k); 02479 for ( i = 0; i < nSize; i++ ) 02480 { 02481 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); 02482 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); 02483 } 02484 } 02485 } 02486 // compute DSD networks 02487 nSize = (1 << nSteps); 02488 nPrimeSizeMax = 0; 02489 nSuppSizeMax = 0; 02490 for ( i = 0; i < nSize; i++ ) 02491 { 02492 ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars ); 02493 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); 02494 Kit_DsdNtkFree( pTemp ); 02495 if ( fVerbose ) 02496 { 02497 printf( "Cof%d%d: ", nSteps, i ); 02498 Kit_DsdPrint( stdout, ppNtks[i] ); 02499 } 02500 // compute the largest non-decomp block 02501 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]); 02502 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); 02503 Kit_DsdNtkFree( ppNtks[i] ); 02504 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars ); 02505 } 02506 printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax ); 02507 } 02508 02509 if ( nCofLevel == 3 ) 02510 for ( v1 = 0; v1 < nVars; v1++ ) 02511 for ( v2 = v1+1; v2 < nVars; v2++ ) 02512 for ( v3 = v2+1; v3 < nVars; v3++ ) 02513 { 02514 nSteps = 0; 02515 piCofVar[nSteps++] = v1; 02516 piCofVar[nSteps++] = v2; 02517 piCofVar[nSteps++] = v3; 02518 02519 printf( " Variables { " ); 02520 for ( i = 0; i < nSteps; i++ ) 02521 printf( "%c ", 'a' + piCofVar[i] ); 02522 printf( "}\n" ); 02523 02524 // single cofactors 02525 for ( s = 1; s <= nSteps; s++ ) 02526 { 02527 for ( k = 0; k < s; k++ ) 02528 { 02529 nSize = (1 << k); 02530 for ( i = 0; i < nSize; i++ ) 02531 { 02532 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); 02533 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); 02534 } 02535 } 02536 } 02537 // compute DSD networks 02538 nSize = (1 << nSteps); 02539 nPrimeSizeMax = 0; 02540 nSuppSizeMax = 0; 02541 for ( i = 0; i < nSize; i++ ) 02542 { 02543 ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars ); 02544 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); 02545 Kit_DsdNtkFree( pTemp ); 02546 if ( fVerbose ) 02547 { 02548 printf( "Cof%d%d: ", nSteps, i ); 02549 Kit_DsdPrint( stdout, ppNtks[i] ); 02550 } 02551 // compute the largest non-decomp block 02552 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]); 02553 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); 02554 Kit_DsdNtkFree( ppNtks[i] ); 02555 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars ); 02556 } 02557 printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax ); 02558 } 02559 02560 if ( nCofLevel == 4 ) 02561 for ( v1 = 0; v1 < nVars; v1++ ) 02562 for ( v2 = v1+1; v2 < nVars; v2++ ) 02563 for ( v3 = v2+1; v3 < nVars; v3++ ) 02564 for ( v4 = v3+1; v4 < nVars; v4++ ) 02565 { 02566 nSteps = 0; 02567 piCofVar[nSteps++] = v1; 02568 piCofVar[nSteps++] = v2; 02569 piCofVar[nSteps++] = v3; 02570 piCofVar[nSteps++] = v4; 02571 02572 printf( " Variables { " ); 02573 for ( i = 0; i < nSteps; i++ ) 02574 printf( "%c ", 'a' + piCofVar[i] ); 02575 printf( "}\n" ); 02576 02577 // single cofactors 02578 for ( s = 1; s <= nSteps; s++ ) 02579 { 02580 for ( k = 0; k < s; k++ ) 02581 { 02582 nSize = (1 << k); 02583 for ( i = 0; i < nSize; i++ ) 02584 { 02585 Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); 02586 Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); 02587 } 02588 } 02589 } 02590 // compute DSD networks 02591 nSize = (1 << nSteps); 02592 nPrimeSizeMax = 0; 02593 nSuppSizeMax = 0; 02594 for ( i = 0; i < nSize; i++ ) 02595 { 02596 ppNtks[i] = Kit_DsdDecompose( ppCofs[nSteps][i], nVars ); 02597 ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); 02598 Kit_DsdNtkFree( pTemp ); 02599 if ( fVerbose ) 02600 { 02601 printf( "Cof%d%d: ", nSteps, i ); 02602 Kit_DsdPrint( stdout, ppNtks[i] ); 02603 } 02604 // compute the largest non-decomp block 02605 nPrimeSizeCur = Kit_DsdNonDsdSizeMax(ppNtks[i]); 02606 nPrimeSizeMax = KIT_MAX( nPrimeSizeMax, nPrimeSizeCur ); 02607 Kit_DsdNtkFree( ppNtks[i] ); 02608 nSuppSizeMax += Kit_TruthSupportSize( ppCofs[nSteps][i], nVars ); 02609 } 02610 printf( "Max = %2d. Supps = %2d.\n", nPrimeSizeMax, nSuppSizeMax ); 02611 } 02612 02613 02614 free( ppCofs[0][0] ); 02615 }
| void Kit_DsdPrintExpanded | ( | Kit_DsdNtk_t * | pNtk | ) |
Function*************************************************************
Synopsis [Print the DSD formula.]
Description []
SideEffects []
SeeAlso []
Definition at line 285 of file kitDsd.c.
00286 { 00287 Kit_DsdNtk_t * pTemp; 00288 pTemp = Kit_DsdExpand( pNtk ); 00289 Kit_DsdPrint( stdout, pTemp ); 00290 Kit_DsdNtkFree( pTemp ); 00291 }
| void Kit_DsdPrintFromTruth | ( | unsigned * | pTruth, | |
| int | nVars | |||
| ) |
Function*************************************************************
Synopsis [Print the DSD formula.]
Description []
SideEffects []
SeeAlso []
Definition at line 304 of file kitDsd.c.
00305 { 00306 Kit_DsdNtk_t * pTemp; 00307 pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 ); 00308 Kit_DsdVerify( pTemp, pTruth, nVars ); 00309 Kit_DsdPrintExpanded( pTemp ); 00310 Kit_DsdNtkFree( pTemp ); 00311 }
| void Kit_DsdPrintHex | ( | FILE * | pFile, | |
| unsigned * | pTruth, | |||
| int | nFans | |||
| ) |
Function*************************************************************
Synopsis [Prints the hex unsigned into a file.]
Description []
SideEffects []
SeeAlso []
Definition at line 183 of file kitDsd.c.
00184 { 00185 int nDigits, Digit, k; 00186 nDigits = (1 << nFans) / 4; 00187 for ( k = nDigits - 1; k >= 0; k-- ) 00188 { 00189 Digit = ((pTruth[k/8] >> ((k%8) * 4)) & 15); 00190 if ( Digit < 10 ) 00191 fprintf( pFile, "%d", Digit ); 00192 else 00193 fprintf( pFile, "%c", 'A' + Digit-10 ); 00194 } 00195 }
| int Kit_DsdRootNodeHasCommonVars | ( | Kit_DsdObj_t * | pObj0, | |
| Kit_DsdObj_t * | pObj1 | |||
| ) |
Function*************************************************************
Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
Description []
SideEffects []
SeeAlso []
Definition at line 1532 of file kitDsd.c.
01533 { 01534 unsigned i, k; 01535 for ( i = 0; i < pObj0->nFans; i++ ) 01536 { 01537 if ( Kit_DsdLit2Var(pObj0->pFans[i]) >= 4 ) 01538 continue; 01539 for ( k = 0; k < pObj1->nFans; k++ ) 01540 if ( Kit_DsdLit2Var(pObj0->pFans[i]) == Kit_DsdLit2Var(pObj1->pFans[k]) ) 01541 return 1; 01542 } 01543 return 0; 01544 }
| void Kit_DsdRotate | ( | Kit_DsdNtk_t * | p, | |
| int | pFreqs[] | |||
| ) |
Function*************************************************************
Synopsis [Rotates the network.]
Description [Transforms prime nodes to have the fanin with the highest frequency of supports go first.]
SideEffects []
SeeAlso []
Definition at line 1364 of file kitDsd.c.
01365 { 01366 Kit_DsdObj_t * pObj; 01367 unsigned * pIn, * pOut, * pTemp, k; 01368 int i, v, Temp, uSuppFanin, iFaninLit, WeightMax, FaninMax, nSwaps; 01369 int Weights[16]; 01370 // go through the prime nodes 01371 Kit_DsdNtkForEachObj( p, pObj, i ) 01372 { 01373 if ( pObj->Type != KIT_DSD_PRIME ) 01374 continue; 01375 // count the fanin frequencies 01376 Kit_DsdObjForEachFanin( p, pObj, iFaninLit, k ) 01377 { 01378 uSuppFanin = Kit_DsdLitSupport( p, iFaninLit ); 01379 Weights[k] = 0; 01380 for ( v = 0; v < 16; v++ ) 01381 if ( uSuppFanin & (1 << v) ) 01382 Weights[k] += pFreqs[v] - 1; 01383 } 01384 // find the most frequent fanin 01385 WeightMax = 0; 01386 FaninMax = -1; 01387 for ( k = 0; k < pObj->nFans; k++ ) 01388 if ( WeightMax < Weights[k] ) 01389 { 01390 WeightMax = Weights[k]; 01391 FaninMax = k; 01392 } 01393 // no need to reorder if there are no frequent fanins 01394 if ( FaninMax == -1 ) 01395 continue; 01396 // move the fanins number k to the first place 01397 nSwaps = 0; 01398 pIn = Kit_DsdObjTruth(pObj); 01399 pOut = p->pMem; 01400 // for ( v = FaninMax; v < ((int)pObj->nFans)-1; v++ ) 01401 for ( v = FaninMax-1; v >= 0; v-- ) 01402 { 01403 // swap the fanins 01404 Temp = pObj->pFans[v]; 01405 pObj->pFans[v] = pObj->pFans[v+1]; 01406 pObj->pFans[v+1] = Temp; 01407 // swap the truth table variables 01408 Kit_TruthSwapAdjacentVars( pOut, pIn, pObj->nFans, v ); 01409 pTemp = pIn; pIn = pOut; pOut = pTemp; 01410 nSwaps++; 01411 } 01412 if ( nSwaps & 1 ) 01413 Kit_TruthCopy( pOut, pIn, pObj->nFans ); 01414 } 01415 }
| Kit_DsdNtk_t* Kit_DsdShrink | ( | Kit_DsdNtk_t * | p, | |
| int | pPrios[] | |||
| ) |
Function*************************************************************
Synopsis [Shrinks the network.]
Description [Transforms the network to have two-input nodes so that the higher-ordered nodes were decomposed out first.]
SideEffects []
SeeAlso []
Definition at line 1326 of file kitDsd.c.
01327 { 01328 Kit_DsdNtk_t * pNew; 01329 Kit_DsdObj_t * pObjNew; 01330 assert( p->nVars <= 16 ); 01331 // create a new network 01332 pNew = Kit_DsdNtkAlloc( p->nVars ); 01333 // consider simple special cases 01334 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 ) 01335 { 01336 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_CONST1, 0 ); 01337 pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) ); 01338 return pNew; 01339 } 01340 if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR ) 01341 { 01342 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_VAR, 1 ); 01343 pObjNew->pFans[0] = Kit_DsdNtkRoot(p)->pFans[0]; 01344 pNew->Root = Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(p->Root) ); 01345 return pNew; 01346 } 01347 // convert the root node 01348 pNew->Root = Kit_DsdShrink_rec( pNew, p, p->Root, pPrios ); 01349 return pNew; 01350 }
| int Kit_DsdShrink_rec | ( | Kit_DsdNtk_t * | pNew, | |
| Kit_DsdNtk_t * | p, | |||
| int | iLit, | |||
| int | pPrios[] | |||
| ) |
Function*************************************************************
Synopsis [Shrinks multi-input nodes.]
Description [Takes the array of variable priorities pPrios.]
SideEffects []
SeeAlso []
Definition at line 1237 of file kitDsd.c.
01238 { 01239 Kit_DsdObj_t * pObj, * pObjNew; 01240 unsigned * pTruth, * pTruthNew; 01241 unsigned i, piLitsNew[16], uSupps[16]; 01242 int iLitFanin, iLitNew; 01243 01244 // consider the case of simple gate 01245 pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); 01246 if ( pObj == NULL ) 01247 return iLit; 01248 if ( pObj->Type == KIT_DSD_AND ) 01249 { 01250 // get the supports 01251 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) 01252 uSupps[i] = Kit_DsdLitSupport( p, iLitFanin ); 01253 // put the largest component last 01254 // sort other components in the decreasing order of priority of their vars 01255 Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew ); 01256 // construct the two-input node network 01257 iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios ); 01258 for ( i = 1; i < pObj->nFans; i++ ) 01259 { 01260 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_AND, 2 ); 01261 pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios ); 01262 pObjNew->pFans[1] = iLitNew; 01263 iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 ); 01264 } 01265 return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) ); 01266 } 01267 if ( pObj->Type == KIT_DSD_XOR ) 01268 { 01269 // get the supports 01270 Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) 01271 { 01272 assert( !Kit_DsdLitIsCompl(iLitFanin) ); 01273 uSupps[i] = Kit_DsdLitSupport( p, iLitFanin ); 01274 } 01275 // put the largest component last 01276 // sort other components in the decreasing order of priority of their vars 01277 Kit_DsdCompSort( pPrios, uSupps, pObj->pFans, pObj->nFans, piLitsNew ); 01278 // construct the two-input node network 01279 iLitNew = Kit_DsdShrink_rec( pNew, p, piLitsNew[0], pPrios ); 01280 for ( i = 1; i < pObj->nFans; i++ ) 01281 { 01282 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_XOR, 2 ); 01283 pObjNew->pFans[0] = Kit_DsdShrink_rec( pNew, p, piLitsNew[i], pPrios ); 01284 pObjNew->pFans[1] = iLitNew; 01285 iLitNew = Kit_DsdVar2Lit( pObjNew->Id, 0 ); 01286 } 01287 return Kit_DsdVar2Lit( pObjNew->Id, Kit_DsdLitIsCompl(iLit) ); 01288 } 01289 assert( pObj->Type == KIT_DSD_PRIME ); 01290 01291 // create new PRIME node 01292 pObjNew = Kit_DsdObjAlloc( pNew, KIT_DSD_PRIME, pObj->nFans ); 01293 // copy the truth table 01294 pTruth = Kit_DsdObjTruth( pObj ); 01295 pTruthNew = Kit_DsdObjTruth( pObjNew ); 01296 Kit_TruthCopy( pTruthNew, pTruth, pObj->nFans ); 01297 // create fanins 01298 Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i ) 01299 { 01300 pObjNew->pFans[i] = Kit_DsdShrink_rec( pNew, p, iLitFanin, pPrios ); 01301 // complement the corresponding inputs of the truth table 01302 if ( Kit_DsdLitIsCompl(pObjNew->pFans[i]) ) 01303 { 01304 pObjNew->pFans[i] = Kit_DsdLitRegular(pObjNew->pFans[i]); 01305 Kit_TruthChangePhase( pTruthNew, pObjNew->nFans, i ); 01306 } 01307 } 01308 // if the incoming phase is complemented, absorb it into the prime node 01309 if ( Kit_DsdLitIsCompl(iLit) ) 01310 Kit_TruthNot( pTruthNew, pTruthNew, pObj->nFans ); 01311 return Kit_DsdVar2Lit( pObjNew->Id, 0 ); 01312 }
| void Kit_DsdTest | ( | unsigned * | pTruth, | |
| int | nVars | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
Definition at line 2102 of file kitDsd.c.
02103 { 02104 Kit_DsdMan_t * p; 02105 unsigned * pTruthC; 02106 Kit_DsdNtk_t * pNtk, * pTemp; 02107 pNtk = Kit_DsdDecompose( pTruth, nVars ); 02108 02109 // if ( Kit_DsdFindLargeBox(pNtk, Kit_DsdLit2Var(pNtk->Root)) ) 02110 // Kit_DsdPrint( stdout, pNtk ); 02111 02112 // if ( Kit_DsdNtkRoot(pNtk)->nFans == (unsigned)nVars && nVars == 6 ) 02113 02114 printf( "\n" ); 02115 Kit_DsdPrint( stdout, pNtk ); 02116 02117 pNtk = Kit_DsdExpand( pTemp = pNtk ); 02118 Kit_DsdNtkFree( pTemp ); 02119 02120 Kit_DsdPrint( stdout, pNtk ); 02121 02122 // if ( Kit_DsdFindLargeBox(pNtk, Kit_DsdLit2Var(pNtk->Root)) ) 02123 // Kit_DsdTestCofs( pNtk, pTruth ); 02124 02125 // recompute the truth table 02126 p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) ); 02127 pTruthC = Kit_DsdTruthCompute( p, pNtk ); 02128 // Extra_PrintBinary( stdout, pTruth, 1 << nVars ); printf( "\n" ); 02129 // Extra_PrintBinary( stdout, pTruthC, 1 << nVars ); printf( "\n" ); 02130 if ( Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) 02131 { 02132 // printf( "Verification is okay.\n" ); 02133 } 02134 else 02135 printf( "Verification failed.\n" ); 02136 Kit_DsdManFree( p ); 02137 02138 02139 Kit_DsdNtkFree( pNtk ); 02140 }
| int Kit_DsdTestCofs | ( | Kit_DsdNtk_t * | pNtk, | |
| unsigned * | pTruthInit | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
Definition at line 1975 of file kitDsd.c.
01976 { 01977 Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp; 01978 // Kit_DsdObj_t * pRoot; 01979 unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) }; 01980 unsigned i, * pTruth; 01981 int fVerbose = 1; 01982 int RetValue = 0; 01983 01984 pTruth = pTruthInit; 01985 // pRoot = Kit_DsdNtkRoot(pNtk); 01986 // pTruth = Kit_DsdObjTruth(pRoot); 01987 // assert( pRoot->nFans == pNtk->nVars ); 01988 01989 if ( fVerbose ) 01990 { 01991 printf( "Function: " ); 01992 // Extra_PrintBinary( stdout, pTruth, (1 << pNtk->nVars) ); 01993 Extra_PrintHexadecimal( stdout, pTruth, pNtk->nVars ); 01994 printf( "\n" ); 01995 Kit_DsdPrint( stdout, pNtk ); 01996 } 01997 for ( i = 0; i < pNtk->nVars; i++ ) 01998 { 01999 Kit_TruthCofactor0New( pCofs2[0], pTruth, pNtk->nVars, i ); 02000 pNtk0 = Kit_DsdDecompose( pCofs2[0], pNtk->nVars ); 02001 pNtk0 = Kit_DsdExpand( pTemp = pNtk0 ); 02002 Kit_DsdNtkFree( pTemp ); 02003 02004 if ( fVerbose ) 02005 { 02006 printf( "Cof%d0: ", i ); 02007 Kit_DsdPrint( stdout, pNtk0 ); 02008 } 02009 02010 Kit_TruthCofactor1New( pCofs2[1], pTruth, pNtk->nVars, i ); 02011 pNtk1 = Kit_DsdDecompose( pCofs2[1], pNtk->nVars ); 02012 pNtk1 = Kit_DsdExpand( pTemp = pNtk1 ); 02013 Kit_DsdNtkFree( pTemp ); 02014 02015 if ( fVerbose ) 02016 { 02017 printf( "Cof%d1: ", i ); 02018 Kit_DsdPrint( stdout, pNtk1 ); 02019 } 02020 02021 // if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) ) 02022 // RetValue = 1; 02023 02024 Kit_DsdNtkFree( pNtk0 ); 02025 Kit_DsdNtkFree( pNtk1 ); 02026 } 02027 if ( fVerbose ) 02028 printf( "\n" ); 02029 02030 return RetValue; 02031 }
| void Kit_DsdTruth | ( | Kit_DsdNtk_t * | pNtk, | |
| unsigned * | pTruthRes | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
Definition at line 826 of file kitDsd.c.
00827 { 00828 Kit_DsdMan_t * p; 00829 unsigned * pTruth; 00830 p = Kit_DsdManAlloc( pNtk->nVars, Kit_DsdNtkObjNum(pNtk) ); 00831 pTruth = Kit_DsdTruthCompute( p, pNtk ); 00832 Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars ); 00833 Kit_DsdManFree( p ); 00834 }
| unsigned* Kit_DsdTruthCompute | ( | Kit_DsdMan_t * | p, | |
| Kit_DsdNtk_t * | pNtk | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
Definition at line 425 of file kitDsd.c.
00426 { 00427 unsigned * pTruthRes; 00428 int i; 00429 // assign elementary truth ables 00430 assert( pNtk->nVars <= p->nVars ); 00431 for ( i = 0; i < (int)pNtk->nVars; i++ ) 00432 Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars ); 00433 // compute truth table for each node 00434 pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root) ); 00435 // complement the truth table if needed 00436 if ( Kit_DsdLitIsCompl(pNtk->Root) ) 00437 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); 00438 return pTruthRes; 00439 }
| unsigned* Kit_DsdTruthComputeNode_rec | ( | Kit_DsdMan_t * | p, | |
| Kit_DsdNtk_t * | pNtk, | |||
| int | Id | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD node.]
Description []
SideEffects []
SeeAlso []
Definition at line 324 of file kitDsd.c.
00325 { 00326 Kit_DsdObj_t * pObj; 00327 unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp; 00328 unsigned i, iLit, fCompl; 00329 // unsigned m, nMints, * pTruthPrime, * pTruthMint; 00330 00331 // get the node with this ID 00332 pObj = Kit_DsdNtkObj( pNtk, Id ); 00333 pTruthRes = Vec_PtrEntry( p->vTtNodes, Id ); 00334 00335 // special case: literal of an internal node 00336 if ( pObj == NULL ) 00337 { 00338 assert( Id < pNtk->nVars ); 00339 return pTruthRes; 00340 } 00341 00342 // constant node 00343 if ( pObj->Type == KIT_DSD_CONST1 ) 00344 { 00345 assert( pObj->nFans == 0 ); 00346 Kit_TruthFill( pTruthRes, pNtk->nVars ); 00347 return pTruthRes; 00348 } 00349 00350 // elementary variable node 00351 if ( pObj->Type == KIT_DSD_VAR ) 00352 { 00353 assert( pObj->nFans == 1 ); 00354 iLit = pObj->pFans[0]; 00355 pTruthFans[0] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) ); 00356 if ( Kit_DsdLitIsCompl(iLit) ) 00357 Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars ); 00358 else 00359 Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars ); 00360 return pTruthRes; 00361 } 00362 00363 // collect the truth tables of the fanins 00364 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00365 pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit) ); 00366 // create the truth table 00367 00368 // simple gates 00369 if ( pObj->Type == KIT_DSD_AND ) 00370 { 00371 Kit_TruthFill( pTruthRes, pNtk->nVars ); 00372 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00373 Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); 00374 return pTruthRes; 00375 } 00376 if ( pObj->Type == KIT_DSD_XOR ) 00377 { 00378 Kit_TruthClear( pTruthRes, pNtk->nVars ); 00379 fCompl = 0; 00380 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00381 { 00382 Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); 00383 fCompl ^= Kit_DsdLitIsCompl(iLit); 00384 } 00385 if ( fCompl ) 00386 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); 00387 return pTruthRes; 00388 } 00389 assert( pObj->Type == KIT_DSD_PRIME ); 00390 /* 00391 // get the truth table of the prime node 00392 pTruthPrime = Kit_DsdObjTruth( pObj ); 00393 // get storage for the temporary minterm 00394 pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes); 00395 00396 // go through the minterms 00397 nMints = (1 << pObj->nFans); 00398 Kit_TruthClear( pTruthRes, pNtk->nVars ); 00399 for ( m = 0; m < nMints; m++ ) 00400 { 00401 if ( !Kit_TruthHasBit(pTruthPrime, m) ) 00402 continue; 00403 Kit_TruthFill( pTruthMint, pNtk->nVars ); 00404 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00405 Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) ); 00406 Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars ); 00407 } 00408 */ 00409 pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes ); 00410 Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars ); 00411 return pTruthRes; 00412 }
| unsigned* Kit_DsdTruthComputeNodeOne_rec | ( | Kit_DsdMan_t * | p, | |
| Kit_DsdNtk_t * | pNtk, | |||
| int | Id, | |||
| unsigned | uSupp | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD node.]
Description []
SideEffects []
SeeAlso []
Definition at line 452 of file kitDsd.c.
00453 { 00454 Kit_DsdObj_t * pObj; 00455 unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp; 00456 unsigned i, iLit, fCompl, nPartial = 0; 00457 // unsigned m, nMints, * pTruthPrime, * pTruthMint; 00458 00459 // get the node with this ID 00460 pObj = Kit_DsdNtkObj( pNtk, Id ); 00461 pTruthRes = Vec_PtrEntry( p->vTtNodes, Id ); 00462 00463 // special case: literal of an internal node 00464 if ( pObj == NULL ) 00465 { 00466 assert( Id < pNtk->nVars ); 00467 assert( !uSupp || uSupp != (uSupp & ~(1<<Id)) ); 00468 return pTruthRes; 00469 } 00470 00471 // constant node 00472 if ( pObj->Type == KIT_DSD_CONST1 ) 00473 { 00474 assert( pObj->nFans == 0 ); 00475 Kit_TruthFill( pTruthRes, pNtk->nVars ); 00476 return pTruthRes; 00477 } 00478 00479 // elementary variable node 00480 if ( pObj->Type == KIT_DSD_VAR ) 00481 { 00482 assert( pObj->nFans == 1 ); 00483 iLit = pObj->pFans[0]; 00484 assert( Kit_DsdLitIsLeaf( pNtk, iLit ) ); 00485 pTruthFans[0] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); 00486 if ( Kit_DsdLitIsCompl(iLit) ) 00487 Kit_TruthNot( pTruthRes, pTruthFans[0], pNtk->nVars ); 00488 else 00489 Kit_TruthCopy( pTruthRes, pTruthFans[0], pNtk->nVars ); 00490 return pTruthRes; 00491 } 00492 00493 // collect the truth tables of the fanins 00494 if ( uSupp ) 00495 { 00496 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00497 if ( uSupp != (uSupp & ~Kit_DsdLitSupport(pNtk, iLit)) ) 00498 pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); 00499 else 00500 { 00501 pTruthFans[i] = NULL; 00502 nPartial = 1; 00503 } 00504 } 00505 else 00506 { 00507 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00508 pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp ); 00509 } 00510 // create the truth table 00511 00512 // simple gates 00513 if ( pObj->Type == KIT_DSD_AND ) 00514 { 00515 Kit_TruthFill( pTruthRes, pNtk->nVars ); 00516 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00517 if ( pTruthFans[i] ) 00518 Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); 00519 return pTruthRes; 00520 } 00521 if ( pObj->Type == KIT_DSD_XOR ) 00522 { 00523 Kit_TruthClear( pTruthRes, pNtk->nVars ); 00524 fCompl = 0; 00525 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00526 { 00527 if ( pTruthFans[i] ) 00528 { 00529 Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); 00530 fCompl ^= Kit_DsdLitIsCompl(iLit); 00531 } 00532 } 00533 if ( fCompl ) 00534 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); 00535 return pTruthRes; 00536 } 00537 assert( pObj->Type == KIT_DSD_PRIME ); 00538 00539 if ( uSupp && nPartial ) 00540 { 00541 // find the only non-empty component 00542 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00543 if ( pTruthFans[i] ) 00544 break; 00545 assert( i < pObj->nFans ); 00546 return pTruthFans[i]; 00547 } 00548 /* 00549 // get the truth table of the prime node 00550 pTruthPrime = Kit_DsdObjTruth( pObj ); 00551 // get storage for the temporary minterm 00552 pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes); 00553 00554 // go through the minterms 00555 nMints = (1 << pObj->nFans); 00556 Kit_TruthClear( pTruthRes, pNtk->nVars ); 00557 for ( m = 0; m < nMints; m++ ) 00558 { 00559 if ( !Kit_TruthHasBit(pTruthPrime, m) ) 00560 continue; 00561 Kit_TruthFill( pTruthMint, pNtk->nVars ); 00562 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00563 Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) ); 00564 Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars ); 00565 } 00566 */ 00567 pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes ); 00568 Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars ); 00569 return pTruthRes; 00570 }
| unsigned* Kit_DsdTruthComputeNodeTwo_rec | ( | Kit_DsdMan_t * | p, | |
| Kit_DsdNtk_t * | pNtk, | |||
| int | Id, | |||
| unsigned | uSupp, | |||
| int | iVar, | |||
| unsigned * | pTruthDec | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD node.]
Description []
SideEffects []
SeeAlso []
Definition at line 613 of file kitDsd.c.
00614 { 00615 Kit_DsdObj_t * pObj; 00616 int pfBoundSet[16]; 00617 unsigned * pTruthRes, * pTruthFans[16], * pTruthTemp; 00618 unsigned i, iLit, fCompl, nPartial, uSuppFan, uSuppCur; 00619 // unsigned m, nMints, * pTruthPrime, * pTruthMint; 00620 assert( uSupp > 0 ); 00621 00622 // get the node with this ID 00623 pObj = Kit_DsdNtkObj( pNtk, Id ); 00624 pTruthRes = Vec_PtrEntry( p->vTtNodes, Id ); 00625 if ( pObj == NULL ) 00626 { 00627 assert( Id < pNtk->nVars ); 00628 return pTruthRes; 00629 } 00630 assert( pObj->Type != KIT_DSD_CONST1 ); 00631 assert( pObj->Type != KIT_DSD_VAR ); 00632 00633 // count the number of intersecting fanins 00634 // collect the total support of the intersecting fanins 00635 nPartial = 0; 00636 uSuppFan = 0; 00637 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00638 { 00639 uSuppCur = Kit_DsdLitSupport(pNtk, iLit); 00640 if ( uSupp & uSuppCur ) 00641 { 00642 nPartial++; 00643 uSuppFan |= uSuppCur; 00644 } 00645 } 00646 00647 // if there is no intersection, or full intersection, use simple procedure 00648 if ( nPartial == 0 || nPartial == pObj->nFans ) 00649 return Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Id, 0 ); 00650 00651 // if support of the component includes some other variables 00652 // we need to continue constructing it as usual by the two-function procedure 00653 if ( uSuppFan != (uSuppFan & uSupp) ) 00654 { 00655 assert( nPartial == 1 ); 00656 // return Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Id, uSupp, iVar, pTruthDec ); 00657 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00658 { 00659 if ( uSupp & Kit_DsdLitSupport(pNtk, iLit) ) 00660 pTruthFans[i] = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp, iVar, pTruthDec ); 00661 else 00662 pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 ); 00663 } 00664 00665 // create composition/decomposition functions 00666 if ( pObj->Type == KIT_DSD_AND ) 00667 { 00668 Kit_TruthFill( pTruthRes, pNtk->nVars ); 00669 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00670 Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); 00671 return pTruthRes; 00672 } 00673 if ( pObj->Type == KIT_DSD_XOR ) 00674 { 00675 Kit_TruthClear( pTruthRes, pNtk->nVars ); 00676 fCompl = 0; 00677 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00678 { 00679 fCompl ^= Kit_DsdLitIsCompl(iLit); 00680 Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); 00681 } 00682 if ( fCompl ) 00683 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); 00684 return pTruthRes; 00685 } 00686 assert( pObj->Type == KIT_DSD_PRIME ); 00687 } 00688 else 00689 { 00690 assert( uSuppFan == (uSuppFan & uSupp) ); 00691 assert( nPartial < pObj->nFans ); 00692 // the support of the insecting component(s) is contained in the bound-set 00693 // and yet there are components that are not contained in the bound set 00694 00695 // solve the fanins and collect info, which components belong to the bound set 00696 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00697 { 00698 pTruthFans[i] = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 ); 00699 pfBoundSet[i] = (int)((uSupp & Kit_DsdLitSupport(pNtk, iLit)) > 0); 00700 } 00701 00702 // create composition/decomposition functions 00703 if ( pObj->Type == KIT_DSD_AND ) 00704 { 00705 Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar ); 00706 Kit_TruthFill( pTruthDec, pNtk->nVars ); 00707 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00708 if ( pfBoundSet[i] ) 00709 Kit_TruthAndPhase( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); 00710 else 00711 Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); 00712 return pTruthRes; 00713 } 00714 if ( pObj->Type == KIT_DSD_XOR ) 00715 { 00716 Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar ); 00717 Kit_TruthClear( pTruthDec, pNtk->nVars ); 00718 fCompl = 0; 00719 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00720 { 00721 fCompl ^= Kit_DsdLitIsCompl(iLit); 00722 if ( pfBoundSet[i] ) 00723 Kit_TruthXor( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars ); 00724 else 00725 Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); 00726 } 00727 if ( fCompl ) 00728 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); 00729 return pTruthRes; 00730 } 00731 assert( pObj->Type == KIT_DSD_PRIME ); 00732 assert( nPartial == 1 ); 00733 00734 // find the only non-empty component 00735 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00736 if ( pfBoundSet[i] ) 00737 break; 00738 assert( i < pObj->nFans ); 00739 00740 // save this component as the decomposed function 00741 Kit_TruthCopy( pTruthDec, pTruthFans[i], pNtk->nVars ); 00742 // set the corresponding component to be the new variable 00743 Kit_TruthIthVar( pTruthFans[i], pNtk->nVars, iVar ); 00744 } 00745 /* 00746 // get the truth table of the prime node 00747 pTruthPrime = Kit_DsdObjTruth( pObj ); 00748 // get storage for the temporary minterm 00749 pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes); 00750 00751 // go through the minterms 00752 nMints = (1 << pObj->nFans); 00753 Kit_TruthClear( pTruthRes, pNtk->nVars ); 00754 for ( m = 0; m < nMints; m++ ) 00755 { 00756 if ( !Kit_TruthHasBit(pTruthPrime, m) ) 00757 continue; 00758 Kit_TruthFill( pTruthMint, pNtk->nVars ); 00759 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00760 Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) ); 00761 Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars ); 00762 } 00763 */ 00764 Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) 00765 assert( !Kit_DsdLitIsCompl(iLit) ); 00766 pTruthTemp = Kit_TruthCompose( p->dd, Kit_DsdObjTruth(pObj), pObj->nFans, pTruthFans, pNtk->nVars, p->vTtBdds, p->vNodes ); 00767 Kit_TruthCopy( pTruthRes, pTruthTemp, pNtk->nVars ); 00768 return pTruthRes; 00769 }
| unsigned* Kit_DsdTruthComputeOne | ( | Kit_DsdMan_t * | p, | |
| Kit_DsdNtk_t * | pNtk, | |||
| unsigned | uSupp | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
Definition at line 583 of file kitDsd.c.
00584 { 00585 unsigned * pTruthRes; 00586 int i; 00587 // if support is specified, request that supports are available 00588 if ( uSupp ) 00589 Kit_DsdGetSupports( pNtk ); 00590 // assign elementary truth tables 00591 assert( pNtk->nVars <= p->nVars ); 00592 for ( i = 0; i < (int)pNtk->nVars; i++ ) 00593 Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars ); 00594 // compute truth table for each node 00595 pTruthRes = Kit_DsdTruthComputeNodeOne_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp ); 00596 // complement the truth table if needed 00597 if ( Kit_DsdLitIsCompl(pNtk->Root) ) 00598 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); 00599 return pTruthRes; 00600 }
| unsigned* Kit_DsdTruthComputeTwo | ( | Kit_DsdMan_t * | p, | |
| Kit_DsdNtk_t * | pNtk, | |||
| unsigned | uSupp, | |||
| int | iVar, | |||
| unsigned * | pTruthDec | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
Definition at line 782 of file kitDsd.c.
00783 { 00784 unsigned * pTruthRes, uSuppAll; 00785 int i; 00786 assert( uSupp > 0 ); 00787 assert( pNtk->nVars <= p->nVars ); 00788 // compute support of all nodes 00789 uSuppAll = Kit_DsdGetSupports( pNtk ); 00790 // consider special case - there is no overlap 00791 if ( (uSupp & uSuppAll) == 0 ) 00792 { 00793 Kit_TruthClear( pTruthDec, pNtk->nVars ); 00794 return Kit_DsdTruthCompute( p, pNtk ); 00795 } 00796 // consider special case - support is fully contained 00797 if ( (uSupp & uSuppAll) == uSuppAll ) 00798 { 00799 pTruthRes = Kit_DsdTruthCompute( p, pNtk ); 00800 Kit_TruthCopy( pTruthDec, pTruthRes, pNtk->nVars ); 00801 Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar ); 00802 return pTruthRes; 00803 } 00804 // assign elementary truth tables 00805 for ( i = 0; i < (int)pNtk->nVars; i++ ) 00806 Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars ); 00807 // compute truth table for each node 00808 pTruthRes = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp, iVar, pTruthDec ); 00809 // complement the truth table if needed 00810 if ( Kit_DsdLitIsCompl(pNtk->Root) ) 00811 Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); 00812 return pTruthRes; 00813 }
| void Kit_DsdTruthPartial | ( | Kit_DsdMan_t * | p, | |
| Kit_DsdNtk_t * | pNtk, | |||
| unsigned * | pTruthRes, | |||
| unsigned | uSupp | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
Definition at line 865 of file kitDsd.c.
00866 { 00867 unsigned * pTruth = Kit_DsdTruthComputeOne( p, pNtk, uSupp ); 00868 Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars ); 00869 /* 00870 // verification 00871 { 00872 // compute the same function using different procedure 00873 unsigned * pTruthTemp = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes + 1); 00874 pNtk->pSupps = NULL; 00875 Kit_DsdTruthComputeTwo( p, pNtk, uSupp, -1, pTruthTemp ); 00876 // if ( !Kit_TruthIsEqual( pTruthTemp, pTruthRes, pNtk->nVars ) ) 00877 if ( !Kit_TruthIsEqualWithPhase( pTruthTemp, pTruthRes, pNtk->nVars ) ) 00878 { 00879 printf( "Verification FAILED!\n" ); 00880 Kit_DsdPrint( stdout, pNtk ); 00881 Kit_DsdPrintFromTruth( pTruthRes, pNtk->nVars ); 00882 Kit_DsdPrintFromTruth( pTruthTemp, pNtk->nVars ); 00883 } 00884 // else 00885 // printf( "Verification successful.\n" ); 00886 } 00887 */ 00888 }
| void Kit_DsdTruthPartialTwo | ( | Kit_DsdMan_t * | p, | |
| Kit_DsdNtk_t * | pNtk, | |||
| unsigned | uSupp, | |||
| int | iVar, | |||
| unsigned * | pTruthCo, | |||
| unsigned * | pTruthDec | |||
| ) |
Function*************************************************************
Synopsis [Derives the truth table of the DSD network.]
Description []
SideEffects []
SeeAlso []
Definition at line 847 of file kitDsd.c.
00848 { 00849 unsigned * pTruth = Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar, pTruthDec ); 00850 if ( pTruthCo ) 00851 Kit_TruthCopy( pTruthCo, pTruth, pNtk->nVars ); 00852 }
| void Kit_DsdVerify | ( | Kit_DsdNtk_t * | pNtk, | |
| unsigned * | pTruth, | |||
| int | nVars | |||
| ) |
Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
Definition at line 2080 of file kitDsd.c.
02081 { 02082 Kit_DsdMan_t * p; 02083 unsigned * pTruthC; 02084 p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 ); 02085 pTruthC = Kit_DsdTruthCompute( p, pNtk ); 02086 if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) 02087 printf( "Verification failed.\n" ); 02088 Kit_DsdManFree( p ); 02089 }
