diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-01-30 08:01:00 -0800 |
commit | 4d30a1e4f1edecff86d5066ce4653a370e59e5e1 (patch) | |
tree | 366355938a4af0a92f848841ac65374f338d691b /src/aig/cnf/cnfCut.c | |
parent | 6537f941887b06e588d3acfc97b5fdf48875cc4e (diff) | |
download | abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.tar.gz abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.tar.bz2 abc-4d30a1e4f1edecff86d5066ce4653a370e59e5e1.zip |
Version abc80130
Diffstat (limited to 'src/aig/cnf/cnfCut.c')
-rw-r--r-- | src/aig/cnf/cnfCut.c | 371 |
1 files changed, 0 insertions, 371 deletions
diff --git a/src/aig/cnf/cnfCut.c b/src/aig/cnf/cnfCut.c deleted file mode 100644 index 17ab0c78..00000000 --- a/src/aig/cnf/cnfCut.c +++ /dev/null @@ -1,371 +0,0 @@ -/**CFile**************************************************************** - - FileName [cnfCut.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [AIG-to-CNF conversion.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - April 28, 2007.] - - Revision [$Id: cnfCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "cnf.h" -#include "kit.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates cut of the given size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Cut_t * Cnf_CutAlloc( Cnf_Man_t * p, int nLeaves ) -{ - Cnf_Cut_t * pCut; - int nSize = sizeof(Cnf_Cut_t) + sizeof(int) * nLeaves + sizeof(unsigned) * Aig_TruthWordNum(nLeaves); - pCut = (Cnf_Cut_t *)Aig_MmFlexEntryFetch( p->pMemCuts, nSize ); - pCut->nFanins = nLeaves; - pCut->nWords = Aig_TruthWordNum(nLeaves); - pCut->vIsop[0] = pCut->vIsop[1] = NULL; - return pCut; -} - -/**Function************************************************************* - - Synopsis [Deallocates cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_CutFree( Cnf_Cut_t * pCut ) -{ - if ( pCut->vIsop[0] ) - Vec_IntFree( pCut->vIsop[0] ); - if ( pCut->vIsop[1] ) - Vec_IntFree( pCut->vIsop[1] ); -} - -/**Function************************************************************* - - Synopsis [Creates cut for the given node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Cut_t * Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj ) -{ - Dar_Cut_t * pCutBest; - Cnf_Cut_t * pCut; - unsigned * pTruth; - assert( Aig_ObjIsNode(pObj) ); - pCutBest = Dar_ObjBestCut( pObj ); - assert( pCutBest != NULL ); - assert( pCutBest->nLeaves <= 4 ); - pCut = Cnf_CutAlloc( p, pCutBest->nLeaves ); - memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves ); - pTruth = Cnf_CutTruth(pCut); - *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth; - pCut->Cost = Cnf_CutSopCost( p, pCutBest ); - return pCut; -} - -/**Function************************************************************* - - Synopsis [Deallocates cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_CutPrint( Cnf_Cut_t * pCut ) -{ - int i; - printf( "{" ); - for ( i = 0; i < pCut->nFanins; i++ ) - printf( "%d ", pCut->pFanins[i] ); - printf( " } " ); -} - -/**Function************************************************************* - - Synopsis [Allocates cut of the given size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_CutDeref( Cnf_Man_t * p, Cnf_Cut_t * pCut ) -{ - Aig_Obj_t * pObj; - int i; - Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i ) - { - assert( pObj->nRefs > 0 ); - pObj->nRefs--; - } -} - -/**Function************************************************************* - - Synopsis [Allocates cut of the given size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_CutRef( Cnf_Man_t * p, Cnf_Cut_t * pCut ) -{ - Aig_Obj_t * pObj; - int i; - Cnf_CutForEachLeaf( p->pManAig, pCut, pObj, i ) - { - pObj->nRefs++; - } -} - -/**Function************************************************************* - - Synopsis [Allocates cut of the given size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes ) -{ - Cnf_CutDeref( p, pCut ); - Cnf_CutDeref( p, pCutFan ); - Cnf_CutRef( p, pCutRes ); -} - -/**Function************************************************************* - - Synopsis [Merges two arrays of integers.] - - Description [Returns the number of items.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Cnf_CutMergeLeaves( Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int * pFanins ) -{ - int i, k, nFanins = 0; - for ( i = k = 0; i < pCut->nFanins && k < pCutFan->nFanins; ) - { - if ( pCut->pFanins[i] == pCutFan->pFanins[k] ) - pFanins[nFanins++] = pCut->pFanins[i], i++, k++; - else if ( pCut->pFanins[i] < pCutFan->pFanins[k] ) - pFanins[nFanins++] = pCut->pFanins[i], i++; - else - pFanins[nFanins++] = pCutFan->pFanins[k], k++; - } - for ( ; i < pCut->nFanins; i++ ) - pFanins[nFanins++] = pCut->pFanins[i]; - for ( ; k < pCutFan->nFanins; k++ ) - pFanins[nFanins++] = pCutFan->pFanins[k]; - return nFanins; -} - -/**Function************************************************************* - - Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline unsigned Cnf_TruthPhase( Cnf_Cut_t * pCut, Cnf_Cut_t * pCut1 ) -{ - unsigned uPhase = 0; - int i, k; - for ( i = k = 0; i < pCut->nFanins; i++ ) - { - if ( k == pCut1->nFanins ) - break; - if ( pCut->pFanins[i] < pCut1->pFanins[k] ) - continue; - assert( pCut->pFanins[i] == pCut1->pFanins[k] ); - uPhase |= (1 << i); - k++; - } - return uPhase; -} - -/**Function************************************************************* - - Synopsis [Removes the fanin variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_CutRemoveIthVar( Cnf_Cut_t * pCut, int iVar, int iFan ) -{ - int i; - assert( pCut->pFanins[iVar] == iFan ); - pCut->nFanins--; - for ( i = iVar; i < pCut->nFanins; i++ ) - pCut->pFanins[i] = pCut->pFanins[i+1]; -} - -/**Function************************************************************* - - Synopsis [Inserts the fanin variable.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Cnf_CutInsertIthVar( Cnf_Cut_t * pCut, int iVar, int iFan ) -{ - int i; - for ( i = pCut->nFanins; i > iVar; i-- ) - pCut->pFanins[i] = pCut->pFanins[i-1]; - pCut->pFanins[iVar] = iFan; - pCut->nFanins++; -} - -/**Function************************************************************* - - Synopsis [Merges two cuts.] - - Description [Returns NULL of the cuts cannot be merged.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Cnf_Cut_t * Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan ) -{ - Cnf_Cut_t * pCutRes; - static int pFanins[32]; - unsigned * pTruth, * pTruthFan, * pTruthRes; - unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3]; - unsigned uPhase, uPhaseFan; - int i, iVar, nFanins, RetValue; - - // make sure the second cut is the fanin of the first - for ( iVar = 0; iVar < pCut->nFanins; iVar++ ) - if ( pCut->pFanins[iVar] == iFan ) - break; - assert( iVar < pCut->nFanins ); - // remove this variable - Cnf_CutRemoveIthVar( pCut, iVar, iFan ); - // merge leaves of the cuts - nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins ); - if ( nFanins+1 > p->nMergeLimit ) - { - Cnf_CutInsertIthVar( pCut, iVar, iFan ); - return NULL; - } - // create new cut - pCutRes = Cnf_CutAlloc( p, nFanins ); - memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins ); - assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins ); - - // derive its truth table - // get the truth tables in the composition space - pTruth = Cnf_CutTruth(pCut); - pTruthFan = Cnf_CutTruth(pCutFan); - pTruthRes = Cnf_CutTruth(pCutRes); - for ( i = 0; i < 2*pCutRes->nWords; i++ ) - pTop[i] = pTruth[i % pCut->nWords]; - for ( i = 0; i < pCutRes->nWords; i++ ) - pFan[i] = pTruthFan[i % pCutFan->nWords]; - // move the variable to the end - uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar); - Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 ); - // compute the phases - uPhase = Cnf_TruthPhase( pCutRes, pCut ) | (1 << pCutRes->nFanins); - uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan ); - // permute truth-tables to the common support - Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1, pCutRes->nFanins+1, uPhase, 1 ); - Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins, uPhaseFan, 1 ); - // perform Boolean operation - Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins ); - // return the cut to its original condition - Cnf_CutInsertIthVar( pCut, iVar, iFan ); - // consider the simple case - if ( pCutRes->nFanins < 5 ) - { - pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes]; - return pCutRes; - } - - // derive ISOP for positive phase - RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 ); - pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory ); - // derive ISOP for negative phase - Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins ); - RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 ); - pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory ); - Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins ); - - // compute the cut cost - if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL ) - pCutRes->Cost = 127; - else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 ) - pCutRes->Cost = 127; - else - pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]); - return pCutRes; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |