diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-06-24 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-06-24 08:01:00 -0700 |
commit | d6804597a397379f826810a736ccbe99bf56c497 (patch) | |
tree | 9ead35b5d0dd58628c773576765b249c87c71dda /src/aig/dar/darTruth.c | |
parent | d47752011d94805850f8713258634d1bde5e639f (diff) | |
download | abc-d6804597a397379f826810a736ccbe99bf56c497.tar.gz abc-d6804597a397379f826810a736ccbe99bf56c497.tar.bz2 abc-d6804597a397379f826810a736ccbe99bf56c497.zip |
Version abc70624
Diffstat (limited to 'src/aig/dar/darTruth.c')
-rw-r--r-- | src/aig/dar/darTruth.c | 350 |
1 files changed, 350 insertions, 0 deletions
diff --git a/src/aig/dar/darTruth.c b/src/aig/dar/darTruth.c new file mode 100644 index 00000000..16b9f62a --- /dev/null +++ b/src/aig/dar/darTruth.c @@ -0,0 +1,350 @@ +/**CFile**************************************************************** + + FileName [darTruth.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting.] + + Synopsis [Computes the truth table of a cut.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: darTruth.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dar.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManCollectCut_rec( Dar_Man_t * p, Dar_Obj_t * pNode, Vec_Int_t * vNodes ) +{ + if ( pNode->fMarkA ) + return; + pNode->fMarkA = 1; + assert( Dar_ObjIsAnd(pNode) || Dar_ObjIsExor(pNode) ); + Dar_ManCollectCut_rec( p, Dar_ObjFanin0(pNode), vNodes ); + Dar_ManCollectCut_rec( p, Dar_ObjFanin1(pNode), vNodes ); + Vec_IntPush( vNodes, pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [Does not modify the array of leaves. Uses array vTruth to store + temporary truth tables. The returned pointer should be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManCollectCut( Dar_Man_t * p, Dar_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) +{ + int i, Leaf; + // collect and mark the leaves + Vec_IntClear( vNodes ); + Vec_IntForEachEntry( vLeaves, Leaf, i ) + { + Vec_IntPush( vNodes, Leaf ); + Dar_ManObj(p, Leaf)->fMarkA = 1; + } + // collect and mark the nodes + Dar_ManCollectCut_rec( p, pRoot, vNodes ); + // clean the nodes + Vec_IntForEachEntry( vNodes, Leaf, i ) + Dar_ManObj(p, Leaf)->fMarkA = 0; +} + +/**Function************************************************************* + + Synopsis [Returns the pointer to the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Dar_ObjGetTruthStore( int ObjNum, Vec_Int_t * vTruth ) +{ + return ((unsigned *)Vec_IntArray(vTruth)) + 8 * ObjNum; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManCutTruthOne( Dar_Man_t * p, Dar_Obj_t * pNode, Vec_Int_t * vTruth, int nWords ) +{ + unsigned * pTruth, * pTruth0, * pTruth1; + int i; + pTruth = Dar_ObjGetTruthStore( pNode->Level, vTruth ); + pTruth0 = Dar_ObjGetTruthStore( Dar_ObjFanin0(pNode)->Level, vTruth ); + pTruth1 = Dar_ObjGetTruthStore( Dar_ObjFanin1(pNode)->Level, vTruth ); + if ( Dar_ObjIsExor(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] ^ pTruth1[i]; + else if ( !Dar_ObjFaninC0(pNode) && !Dar_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & pTruth1[i]; + else if ( !Dar_ObjFaninC0(pNode) && Dar_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = pTruth0[i] & ~pTruth1[i]; + else if ( Dar_ObjFaninC0(pNode) && !Dar_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & pTruth1[i]; + else // if ( Dar_ObjFaninC0(pNode) && Dar_ObjFaninC1(pNode) ) + for ( i = 0; i < nWords; i++ ) + pTruth[i] = ~pTruth0[i] & ~pTruth1[i]; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [Does not modify the array of leaves. Uses array vTruth to store + temporary truth tables. The returned pointer should be used immediately.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Dar_ManCutTruth( Dar_Man_t * p, Dar_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, Vec_Int_t * vTruth ) +{ + static unsigned uTruths[8][8] = { // elementary truth tables + { 0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA,0xAAAAAAAA }, + { 0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC,0xCCCCCCCC }, + { 0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0,0xF0F0F0F0 }, + { 0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00,0xFF00FF00 }, + { 0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000,0xFFFF0000 }, + { 0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF,0x00000000,0xFFFFFFFF }, + { 0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF }, + { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } + }; + int i, Leaf; + // collect the cut +// Dar_ManCollectCut( p, pRoot, vLeaves, vNodes ); + // set the node numbers + Vec_IntForEachEntry( vNodes, Leaf, i ) + Dar_ManObj(p, Leaf)->Level = i; + // alloc enough memory + Vec_IntClear( vTruth ); + Vec_IntGrow( vTruth, 8 * Vec_IntSize(vNodes) ); + // set the elementary truth tables + Vec_IntForEachEntry( vLeaves, Leaf, i ) + memcpy( Dar_ObjGetTruthStore(i, vTruth), uTruths[i], 8 * sizeof(unsigned) ); + // compute truths for other nodes + Vec_IntForEachEntryStart( vNodes, Leaf, i, Vec_IntSize(vLeaves) ) + Dar_ManCutTruthOne( p, Dar_ManObj(p, Leaf), vTruth, 8 ); + return Dar_ObjGetTruthStore( pRoot->Level, vTruth ); +} + +static inline int Kit_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } +static inline void Kit_TruthNot( unsigned * pOut, unsigned * pIn, int nVars ) +{ + int w; + for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~pIn[w]; +} + +/**Function************************************************************* + + Synopsis [Computes the cost based on two ISOPs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManLargeCutEvalIsop( unsigned * pTruth, int nVars, Vec_Int_t * vMemory ) +{ + extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth ); + int RetValue, nClauses; + // compute ISOP for the positive phase + RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 ); + if ( RetValue == -1 ) + return DAR_INFINITY; + assert( RetValue == 0 || RetValue == 1 ); + nClauses = Vec_IntSize( vMemory ); + // compute ISOP for the negative phase + Kit_TruthNot( pTruth, pTruth, nVars ); + RetValue = Kit_TruthIsop( pTruth, nVars, vMemory, 0 ); + if ( RetValue == -1 ) + return DAR_INFINITY; + Kit_TruthNot( pTruth, pTruth, nVars ); + assert( RetValue == 0 || RetValue == 1 ); + nClauses += Vec_IntSize( vMemory ); + return nClauses; +} + +/**Function************************************************************* + + Synopsis [Computes truth table of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManLargeCutCollect_rec( Dar_Man_t * p, Dar_Obj_t * pNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) +{ + if ( Dar_ObjIsTravIdCurrent(p, pNode) ) + return; + if ( Dar_ObjIsTravIdPrevious(p, pNode) ) + { + Vec_IntPush( vLeaves, pNode->Id ); +// Vec_IntPush( vNodes, pNode->Id ); + Dar_ObjSetTravIdCurrent( p, pNode ); + return; + } + assert( Dar_ObjIsAnd(pNode) || Dar_ObjIsExor(pNode) ); + Dar_ObjSetTravIdCurrent( p, pNode ); + Dar_ManLargeCutCollect_rec( p, Dar_ObjFanin0(pNode), vLeaves, vNodes ); + Dar_ManLargeCutCollect_rec( p, Dar_ObjFanin1(pNode), vLeaves, vNodes ); + Vec_IntPush( vNodes, pNode->Id ); +} + +/**Function************************************************************* + + Synopsis [Collect leaves and nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManLargeCutCollect( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf, + Vec_Int_t * vLeaves, Vec_Int_t * vNodes ) +{ + Vec_Int_t * vTemp; + Dar_Obj_t * pObj; + int Node, i; + + Dar_ManIncrementTravId( p ); + Dar_CutForEachLeaf( p, pCutR, pObj, i ) + if ( pObj->Id != Leaf ) + Dar_ObjSetTravIdCurrent( p, pObj ); + Dar_CutForEachLeaf( p, pCutL, pObj, i ) + Dar_ObjSetTravIdCurrent( p, pObj ); + + // collect the internal nodes and leaves + Dar_ManIncrementTravId( p ); + vTemp = Vec_IntAlloc( 100 ); + Dar_ManLargeCutCollect_rec( p, pRoot, vLeaves, vTemp ); + + Vec_IntForEachEntry( vLeaves, Node, i ) + Vec_IntPush( vNodes, Node ); + Vec_IntForEachEntry( vTemp, Node, i ) + Vec_IntPush( vNodes, Node ); + + Vec_IntFree( vTemp ); + +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManLargeCutEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCutR, Dar_Cut_t * pCutL, int Leaf ) +{ + Vec_Int_t * vLeaves, * vNodes, * vTruth, * vMemory; + unsigned * pTruth; + int RetValue; +// Dar_Obj_t * pObj; + + vMemory = Vec_IntAlloc( 1 << 16 ); + vTruth = Vec_IntAlloc( 1 << 16 ); + vLeaves = Vec_IntAlloc( 100 ); + vNodes = Vec_IntAlloc( 100 ); + + Dar_ManLargeCutCollect( p, pRoot, pCutR, pCutL, Leaf, vLeaves, vNodes ); +/* + // collect the nodes + Dar_CutForEachLeaf( p, pCutR, pObj, i ) + { + if ( pObj->Id == Leaf ) + continue; + if ( pObj->fMarkA ) + continue; + pObj->fMarkA = 1; + Vec_IntPush( vLeaves, pObj->Id ); + Vec_IntPush( vNodes, pObj->Id ); + } + Dar_CutForEachLeaf( p, pCutL, pObj, i ) + { + if ( pObj->fMarkA ) + continue; + pObj->fMarkA = 1; + Vec_IntPush( vLeaves, pObj->Id ); + Vec_IntPush( vNodes, pObj->Id ); + } + // collect and mark the nodes + Dar_ManCollectCut_rec( p, pRoot, vNodes ); + // clean the nodes + Vec_IntForEachEntry( vNodes, Leaf, i ) + Dar_ManObj(p, Leaf)->fMarkA = 0; +*/ + + pTruth = Dar_ManCutTruth( p, pRoot, vLeaves, vNodes, vTruth ); + RetValue = Dar_ManLargeCutEvalIsop( pTruth, Vec_IntSize(vLeaves), vMemory ); + + Vec_IntFree( vLeaves ); + Vec_IntFree( vNodes ); + Vec_IntFree( vTruth ); + Vec_IntFree( vMemory ); + + return RetValue; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |