From 53adc97675511f41fd9c40c31dcb9b3506f75daf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 27 Nov 2016 11:56:40 -0800 Subject: New SAT-based optimization package. --- src/opt/sbd/sbdCore.c | 93 ++++++++++----- src/opt/sbd/sbdSim.c | 310 ++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 376 insertions(+), 27 deletions(-) create mode 100644 src/opt/sbd/sbdSim.c diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c index 2120a8f9..6b311e01 100644 --- a/src/opt/sbd/sbdCore.c +++ b/src/opt/sbd/sbdCore.c @@ -48,6 +48,7 @@ struct Sbd_Man_t_ Vec_Int_t * vTfo; // TFO (excludes node, includes roots) Vec_Int_t * vLeaves; // leaves (TFI leaves + extended leaves) Vec_Int_t * vTfi; // TFI (TFI + node + extended TFI) + Vec_Int_t * vDivs; // divisors Vec_Int_t * vCounts[2]; // counters of zeros and ones }; @@ -76,7 +77,7 @@ void Sbd_ParSetDefault( Sbd_Par_t * pPars ) { memset( pPars, 0, sizeof(Sbd_Par_t) ); pPars->nLutSize = 4; // target LUT size - pPars->nTfoLevels = 4; // the number of TFO levels (windowing) + pPars->nTfoLevels = 3; // the number of TFO levels (windowing) pPars->nTfoFanMax = 4; // the max number of fanouts (windowing) pPars->nWinSizeMax = 0; // maximum window size (windowing) pPars->nBTLimit = 0; // maximum number of SAT conflicts @@ -102,6 +103,7 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax ) Vec_Wec_t * vTfos = Vec_WecStart( Gia_ManObjNum(p) ); // TFO nodes with roots marked Vec_Wec_t * vTemp = Vec_WecStart( Gia_ManObjNum(p) ); // storage Vec_Int_t * vNodes, * vNodes0, * vNodes1; + Vec_Bit_t * vPoDrivers = Vec_BitStart( Gia_ManObjNum(p) ); int i, k, k2, Id, Fan; Gia_ManLevelNum( p ); Gia_ManCreateRefs( p ); @@ -112,13 +114,15 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax ) Vec_IntGrow( vNodes, 1 ); Vec_IntPush( vNodes, Id ); } + Gia_ManForEachCoDriverId( p, Id, i ) + Vec_BitWriteEntry( vPoDrivers, Id, 1 ); Gia_ManForEachAndId( p, Id ) { - int fAlwaysRoot = Gia_ObjRefNumId(p, Id) >= nTfoFanMax; + int fAlwaysRoot = Vec_BitEntry(vPoDrivers, Id) || (Gia_ObjRefNumId(p, Id) >= nTfoFanMax); vNodes0 = Vec_WecEntry( vTemp, Gia_ObjFaninId0(Gia_ManObj(p, Id), Id) ); vNodes1 = Vec_WecEntry( vTemp, Gia_ObjFaninId1(Gia_ManObj(p, Id), Id) ); vNodes = Vec_WecEntry( vTemp, Id ); - Vec_IntTwoMerge2( vNodes, vNodes0, vNodes1 ); + Vec_IntTwoMerge2( vNodes0, vNodes1, vNodes ); k2 = 0; Vec_IntForEachEntry( vNodes, Fan, k ) { @@ -127,10 +131,16 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax ) if ( !fRoot ) Vec_IntWriteEntry( vNodes, k2++, Fan ); } Vec_IntShrink( vNodes, k2 ); - Vec_IntPush( vNodes, Id ); + if ( fAlwaysRoot ) + Vec_WecPush( vTfos, Id, Abc_Var2Lit(Id, 1) ); + else + Vec_IntPush( vNodes, Id ); } Vec_WecFree( vTemp ); + Vec_BitFree( vPoDrivers ); + // print the results + if ( 1 ) Vec_WecForEachLevel( vTfos, vNodes, i ) { if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) ) @@ -139,8 +149,8 @@ Vec_Wec_t * Sbd_ManWindowRoots( Gia_Man_t * p, int nTfoLevels, int nTfoFanMax ) Vec_IntForEachEntry( vNodes, Fan, k ) printf( "%d%s ", Abc_Lit2Var(Fan), Abc_LitIsCompl(Fan)? "*":"" ); printf( "\n" ); - } + return vTfos; } @@ -171,6 +181,7 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars ) p->vCover = Vec_IntStart( 100 ); p->vLeaves = Vec_IntAlloc( Gia_ManCiNum(pGia) ); p->vTfi = Vec_IntAlloc( Gia_ManAndNum(pGia) ); + p->vDivs = Vec_IntAlloc( Gia_ManObjNum(pGia) ); p->vCounts[0] = Vec_IntAlloc( 100 ); p->vCounts[1] = Vec_IntAlloc( 100 ); // start input cuts @@ -199,8 +210,10 @@ void Sbd_ManStop( Sbd_Man_t * p ) Vec_IntFree( p->vCover ); Vec_IntFree( p->vLeaves ); Vec_IntFree( p->vTfi ); + Vec_IntFree( p->vDivs ); Vec_IntFree( p->vCounts[0] ); Vec_IntFree( p->vCounts[1] ); + ABC_FREE( p ); } @@ -234,20 +247,38 @@ void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int Node ) Sbd_ManWindowSim_rec( p, Gia_ObjFaninId1(pObj, Node) ); Vec_IntPush( p->vTfi, Node ); // simulate - Abc_TtAndCompl( Sbd_ObjSim0(p, Node), - Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), - Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), - p->pPars->nWords ); - if ( pObj->fMark0 ) - Abc_TtAndCompl( Sbd_ObjSim1(p, Node), - Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), - Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), + if ( Gia_ObjIsXor(pObj) ) + { + Abc_TtXor( Sbd_ObjSim0(p, Node), + Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), + Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), + p->pPars->nWords, + Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) ); + if ( pObj->fMark0 ) + Abc_TtXor( Sbd_ObjSim1(p, Node), + Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), + Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), + p->pPars->nWords, + Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) ); + } + else + { + Abc_TtAndCompl( Sbd_ObjSim0(p, Node), + Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), + Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), p->pPars->nWords ); + if ( pObj->fMark0 ) + Abc_TtAndCompl( Sbd_ObjSim1(p, Node), + Gia_ObjFanin0(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId0(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId0(pObj, Node)), Gia_ObjFaninC0(pObj), + Gia_ObjFanin1(pObj)->fMark0 ? Sbd_ObjSim1(p, Gia_ObjFaninId1(pObj, Node)) : Sbd_ObjSim0(p, Gia_ObjFaninId1(pObj, Node)), Gia_ObjFaninC1(pObj), + p->pPars->nWords ); + } } void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node ) { - int iObj0 = Gia_ObjFaninId0(Gia_ManObj(p->pGia, Node), Node); - int iObj1 = Gia_ObjFaninId1(Gia_ManObj(p->pGia, Node), Node); + Gia_Obj_t * pNode = Gia_ManObj(p->pGia, Node); + int iObj0 = Gia_ObjFaninId0(pNode, Node); + int iObj1 = Gia_ObjFaninId1(pNode, Node); word * pCtrl = Sbd_ObjSim2(p, Node); word * pCtrl0 = Sbd_ObjSim2(p, iObj0); word * pCtrl1 = Sbd_ObjSim2(p, iObj1); @@ -255,10 +286,13 @@ void Sbd_ManPropagateControl( Sbd_Man_t * p, int Node ) word * pSims0 = Sbd_ObjSim0(p, iObj0); word * pSims1 = Sbd_ObjSim0(p, iObj1); int w; +// printf( "Node %2d : %d %d\n", Node, (int)(pSims[0] & 1), (int)(pCtrl[0] & 1) ); for ( w = 0; w < p->pPars->nWords; w++ ) { - pCtrl0[w] = pCtrl[w] & (pSims[w] | pSims1[w]); - pCtrl1[w] = pCtrl[w] & (pSims[w] | pSims0[w] | (~pSims0[w] & ~pSims1[w])); + word Sim0 = Gia_ObjFaninC0(pNode) ? ~pSims0[w] : pSims0[w]; + word Sim1 = Gia_ObjFaninC1(pNode) ? ~pSims1[w] : pSims1[w]; + pCtrl0[w] = pCtrl[w] & (pSims[w] | Sim1 | (~Sim0 & ~Sim1)); + pCtrl1[w] = pCtrl[w] & (pSims[w] | Sim0); } } void Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) @@ -269,11 +303,14 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) p->vTfo = Vec_WecEntry( p->vTfos, Pivot ); Vec_IntClear( p->vLeaves ); Vec_IntClear( p->vTfi ); + Vec_IntClear( p->vDivs ); // simulate TFI cone Gia_ManIncrementTravId( p->pGia ); Sbd_ManWindowSim_rec( p, Pivot ); p->nTfiLeaves = Vec_IntSize( p->vLeaves ); p->nTfiNodes = Vec_IntSize( p->vTfi ); + Vec_IntAppend( p->vDivs, p->vLeaves ); + Vec_IntAppend( p->vDivs, p->vTfi ); // simulate node Gia_ManObj(p->pGia, Pivot)->fMark0 = 1; Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 ); @@ -282,7 +319,7 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) { Gia_ManObj(p->pGia, Abc_Lit2Var(Node))->fMark0 = 1; if ( Abc_LitIsCompl(Node) ) - Sbd_ManWindowSim_rec( p, Node ); + Sbd_ManWindowSim_rec( p, Abc_Lit2Var(Node) ); } // remove marks Gia_ManObj(p->pGia, Pivot)->fMark0 = 0; @@ -292,9 +329,9 @@ void Sbd_ManWindow( Sbd_Man_t * p, int Pivot ) Abc_TtClear( Sbd_ObjSim2(p, Pivot), p->pPars->nWords ); Vec_IntForEachEntry( p->vTfo, Node, i ) if ( Abc_LitIsCompl(Node) ) // root - Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Node), Sbd_ObjSim1(p, Node), p->pPars->nWords ); - // propagate controlability to TFI - for ( i = p->nTfiNodes; i >= 0 && (Node = Vec_IntEntry(p->vTfi, i)); i-- ) + Abc_TtOrXor( Sbd_ObjSim2(p, Pivot), Sbd_ObjSim0(p, Abc_Lit2Var(Node)), Sbd_ObjSim1(p, Abc_Lit2Var(Node)), p->pPars->nWords ); + // propagate controlability to fanins for the TFI nodes starting from the pivot + for ( i = p->nTfiLeaves + p->nTfiNodes - 1; i >= p->nTfiLeaves && ((Node = Vec_IntEntry(p->vDivs, i)), 1); i-- ) Sbd_ManPropagateControl( p, Node ); } @@ -319,11 +356,11 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot ) for ( k = 0; k < p->pPars->nWords * 64; k++ ) { printf( "%3d : ", k ); - Vec_IntForEachEntry( p->vTfi, Id, i ) + Vec_IntForEachEntry( p->vDivs, Id, i ) { word * pSims = Sbd_ObjSim0( p, Id ); word * pCtrl = Sbd_ObjSim2( p, Id ); - if ( i == Vec_IntSize(p->vTfi)-1 ) + if ( i == Vec_IntSize(p->vDivs)-1 ) { if ( Abc_TtGetBit(pCtrl, k) ) Vec_IntPush( p->vCounts[Abc_TtGetBit(pSims, k)], k ); @@ -335,15 +372,15 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot ) } // covering table printf( "Exploring %d x %d covering table.\n", Vec_IntSize(p->vCounts[0]), Vec_IntSize(p->vCounts[1]) ); - Vec_IntForEachEntry( p->vCounts[0], Bit0, k0 ) - Vec_IntForEachEntry( p->vCounts[1], Bit1, k1 ) + Vec_IntForEachEntryStop( p->vCounts[0], Bit0, k0, 5 ) + Vec_IntForEachEntryStop( p->vCounts[1], Bit1, k1, 5 ) { printf( "%3d %3d : ", Bit0, Bit1 ); - Vec_IntForEachEntry( p->vTfi, Id, i ) + Vec_IntForEachEntry( p->vDivs, Id, i ) { word * pSims = Sbd_ObjSim0( p, Id ); word * pCtrl = Sbd_ObjSim2( p, Id ); - if ( i == Vec_IntSize(p->vTfi)-1 ) + if ( i == Vec_IntSize(p->vDivs)-1 ) printf( " " ); printf( "%c", (Abc_TtGetBit(pCtrl, Bit0) && Abc_TtGetBit(pCtrl, Bit1) && Abc_TtGetBit(pSims, Bit0) != Abc_TtGetBit(pSims, Bit1)) ? '1' : '.' ); } @@ -512,9 +549,11 @@ Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars ) { if ( Sbd_ManComputeCut( p, Pivot ) ) continue; + printf( "Looking at node %d\n", Pivot ); Sbd_ManWindow( p, Pivot ); if ( Sbd_ManExplore( p, Pivot, pCut, &Truth ) ) Sbd_ManImplement( p, Pivot, pCut, Truth ); + break; } pNew = Sbd_ManDerive( pGia, p->vMirrors ); Sbd_ManStop( p ); diff --git a/src/opt/sbd/sbdSim.c b/src/opt/sbd/sbdSim.c new file mode 100644 index 00000000..3bb44159 --- /dev/null +++ b/src/opt/sbd/sbdSim.c @@ -0,0 +1,310 @@ +/**CFile**************************************************************** + + FileName [sbdSim.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based optimization using internal don't-cares.] + + Synopsis [Simulation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: sbdSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "sbdInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline word * Sbd_ObjSims( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims, p->iPatsPi * i ); } +static inline word * Sbd_ObjCtrl( Gia_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSimsPi, p->iPatsPi * i ); } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [This does not work.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sbd_GiaSimRoundBack2( Gia_Man_t * p ) +{ + int nWords = p->iPatsPi; + Gia_Obj_t * pObj; + int w, i, Id; + // init primary outputs + Gia_ManForEachCoId( p, Id, i ) + for ( w = 0; w < nWords; w++ ) + Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0); + // transfer to nodes + Gia_ManForEachCo( p, pObj, i ) + { + word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj)); + Abc_TtCopy( Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), pSims, nWords, Gia_ObjFaninC0(pObj) ); + } + // simulate nodes + Gia_ManForEachAndReverse( p, pObj, i ) + { + word * pSims = Sbd_ObjSims(p, i); + word * pSims0 = Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)); + word * pSims1 = Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)); + word Rand = Gia_ManRandomW(0); + for ( w = 0; w < nWords; w++ ) + { + pSims0[w] = pSims[w] | Rand; + pSims1[w] = pSims[w] | ~Rand; + } + if ( Gia_ObjFaninC0(pObj) ) Abc_TtNot( pSims0, nWords ); + if ( Gia_ObjFaninC1(pObj) ) Abc_TtNot( pSims1, nWords ); + } + // primary inputs are initialized +} + + +/**Function************************************************************* + + Synopsis [Tries to falsify a sequence of two-literal SAT problems.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Sbd_GiaSatOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, int Value, int fFirst, int iPat ) +{ + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return (int)pObj->fMark0 == Value; + Gia_ObjSetTravIdCurrent(p, pObj); + pObj->fMark0 = Value; + if ( Gia_ObjIsCi(pObj) ) + { + word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj)); + if ( Abc_TtGetBit( pSims, iPat ) != Value ) + Abc_TtXorBit( pSims, iPat ); + return 1; + } + assert( Gia_ObjIsAnd(pObj) ); + assert( !Gia_ObjIsXor(pObj) ); + if ( Value ) + return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), !Gia_ObjFaninC0(pObj), fFirst, iPat ) && + Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), !Gia_ObjFaninC1(pObj), fFirst, iPat ); + if ( fFirst ) + return Sbd_GiaSatOne_rec( p, Gia_ObjFanin0(pObj), Gia_ObjFaninC0(pObj), fFirst, iPat ); + else + return Sbd_GiaSatOne_rec( p, Gia_ObjFanin1(pObj), Gia_ObjFaninC1(pObj), fFirst, iPat ); +} +int Sbd_GiaSatOne( Gia_Man_t * p, Vec_Int_t * vPairs ) +{ + int k, n, Var1, Var2, iPat = 0; + //Gia_ManSetPhase( p ); + Vec_IntForEachEntryDouble( vPairs, Var1, Var2, k ) + { + Gia_Obj_t * pObj1 = Gia_ManObj( p, Var1 ); + Gia_Obj_t * pObj2 = Gia_ManObj( p, Var2 ); + assert( Var2 > 0 ); + if ( Var1 == 0 ) + { + for ( n = 0; n < 2; n++ ) + { + Gia_ManIncrementTravId( p ); + if ( Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) ) + { + iPat++; + break; + } + } + printf( "%c", n == 2 ? '.' : 'c' ); + } + else + { + for ( n = 0; n < 2; n++ ) + { + Gia_ManIncrementTravId( p ); + if ( Sbd_GiaSatOne_rec(p, pObj1, !pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, pObj2->fPhase, n, iPat) ) + { + iPat++; + break; + } + Gia_ManIncrementTravId( p ); + if ( Sbd_GiaSatOne_rec(p, pObj1, pObj1->fPhase, n, iPat) && Sbd_GiaSatOne_rec(p, pObj2, !pObj2->fPhase, n, iPat) ) + { + iPat++; + break; + } + } + printf( "%c", n == 2 ? '.' : 'e' ); + } + if ( iPat == 64 * p->iPatsPi - 1 ) + break; + } + printf( "\n" ); + return iPat; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sbd_GiaSimRoundBack( Gia_Man_t * p ) +{ + extern void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap ); + Vec_Int_t * vReprs = Vec_IntStart( Gia_ManObjNum(p) ); + Vec_Int_t * vPairs = Vec_IntAlloc( 1000 ); + Vec_Int_t * vMap; // maps each node into its class + int i, nConsts = 0, nClasses = 0, nPats; + Sbd_GiaSimRound( p, 0, &vMap ); + Gia_ManForEachAndId( p, i ) + { + if ( Vec_IntEntry(vMap, i) == 0 ) + Vec_IntPushTwo( vPairs, 0, i ), nConsts++; + else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) == 0 ) + Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), i ); + else if ( Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)) != -1 ) + { + Vec_IntPushTwo( vPairs, Vec_IntEntry(vReprs, Vec_IntEntry(vMap, i)), i ); + Vec_IntWriteEntry( vReprs, Vec_IntEntry(vMap, i), -1 ); + nClasses++; + } + } + Vec_IntFree( vMap ); + Vec_IntFree( vReprs ); + printf( "Constants = %d. Classes = %d.\n", nConsts, nClasses ); + + nPats = Sbd_GiaSatOne( p, vPairs ); + Vec_IntFree( vPairs ); + + printf( "Generated %d patterns.\n", nPats ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sbd_GiaSimRound( Gia_Man_t * p, int fTry, Vec_Int_t ** pvMap ) +{ + int nWords = p->iPatsPi; + Vec_Mem_t * vStore; + Gia_Obj_t * pObj; + Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(p) ); + int w, i, Id, fCompl, RetValue; + // init primary inputs + if ( fTry ) + { + Sbd_GiaSimRoundBack( p ); + Gia_ManForEachCiId( p, Id, i ) + Sbd_ObjSims(p, Id)[0] <<= 1; + } + else + { + Gia_ManForEachCiId( p, Id, i ) + for ( w = 0; w < nWords; w++ ) + Sbd_ObjSims(p, Id)[w] = Gia_ManRandomW(0) << !w; + } + // simulate internal nodes + vStore = Vec_MemAlloc( nWords, 16 ); // 2^12 N-word entries per page + Vec_MemHashAlloc( vStore, 1 << 16 ); + RetValue = Vec_MemHashInsert( vStore, Sbd_ObjSims(p, 0) ); // const zero + assert( RetValue == 0 ); + Gia_ManForEachAnd( p, pObj, i ) + { + word * pSims = Sbd_ObjSims(p, i); + if ( Gia_ObjIsXor(pObj) ) + Abc_TtXor( pSims, + Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), + Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), + nWords, + Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) ); + else + Abc_TtAndCompl( pSims, + Sbd_ObjSims(p, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj), + Sbd_ObjSims(p, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj), + nWords ); + // hash sim info + fCompl = (int)(pSims[0] & 1); + if ( fCompl ) Abc_TtNot( pSims, nWords ); + Vec_IntWriteEntry( vMap, i, Vec_MemHashInsert(vStore, pSims) ); + if ( fCompl ) Abc_TtNot( pSims, nWords ); + } + Gia_ManForEachCo( p, pObj, i ) + { + word * pSims = Sbd_ObjSims(p, Gia_ObjId(p, pObj)); + Abc_TtCopy( pSims, Sbd_ObjSims(p, Gia_ObjFaninId0p(p, pObj)), nWords, Gia_ObjFaninC0(pObj) ); +// printf( "%d ", Abc_TtCountOnesVec(pSims, nWords) ); + assert( Gia_ObjPhase(pObj) == (int)(pSims[0] & 1) ); + } +// printf( "\n" ); + Vec_MemHashFree( vStore ); + Vec_MemFree( vStore ); + printf( "Objects = %6d. Unique = %6d.\n", Gia_ManAndNum(p), Vec_IntCountUnique(vMap) ); + if ( pvMap ) + *pvMap = vMap; + else + Vec_IntFree( vMap ); +} +void Sbd_GiaSimTest( Gia_Man_t * pGia ) +{ + Gia_ManSetPhase( pGia ); + + // allocate simulation info + pGia->iPatsPi = 32; + pGia->vSims = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi ); + pGia->vSimsPi = Vec_WrdStart( Gia_ManObjNum(pGia) * pGia->iPatsPi ); + + Gia_ManRandom( 1 ); + + Sbd_GiaSimRound( pGia, 0, NULL ); + Sbd_GiaSimRound( pGia, 0, NULL ); + Sbd_GiaSimRound( pGia, 0, NULL ); + + printf( "\n" ); + Sbd_GiaSimRound( pGia, 1, NULL ); + printf( "\n" ); + Sbd_GiaSimRound( pGia, 1, NULL ); + printf( "\n" ); + Sbd_GiaSimRound( pGia, 1, NULL ); + + Vec_WrdFreeP( &pGia->vSims ); + Vec_WrdFreeP( &pGia->vSimsPi ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3