From 2adf8dc2fd13d2eb77f48afd2fe33f7d7230527c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 25 Aug 2011 17:21:17 +0700 Subject: Sequential cleanup with symbolic/ternary simulation. --- src/aig/bdc/bdcSpfd.c | 55 +++++++++++++- src/aig/saig/saigSimMv.c | 194 +++++++++++++++++++++++++++++++++++++++++------ src/base/abci/abc.c | 4 +- 3 files changed, 227 insertions(+), 26 deletions(-) (limited to 'src') diff --git a/src/aig/bdc/bdcSpfd.c b/src/aig/bdc/bdcSpfd.c index cd94e66b..d9f0c7d6 100644 --- a/src/aig/bdc/bdcSpfd.c +++ b/src/aig/bdc/bdcSpfd.c @@ -897,7 +897,7 @@ int Bdc_SpfdDecomposeTestOne( word t, Vec_Wrd_t * vDivs, Vec_Int_t * vWeights ) SeeAlso [] ***********************************************************************/ -void Bdc_SpfdDecomposeTest() +void Bdc_SpfdDecomposeTest44() { // word t = 0x5052585a0002080a; @@ -1114,6 +1114,59 @@ Abc_Show6VarFunc( 0, (FuncBest ^ t) ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bdc_SpfdDecomposeTest() +{ + int nSizeM = (1 << 26); // big array size + int nSizeK = (1 << 3); // small array size + Vec_Wrd_t * v1M, * v1K; + int EntryM, EntryK; + int i, k, Counter, clk; + + Aig_ManRandom64( 1 ); + + v1M = Vec_WrdAlloc( nSizeM ); + for ( i = 0; i < nSizeM; i++ ) + Vec_WrdPush( v1M, Aig_ManRandom64(0) ); + + v1K = Vec_WrdAlloc( nSizeK ); + for ( i = 0; i < nSizeK; i++ ) + Vec_WrdPush( v1K, Aig_ManRandom64(0) ); + + clk = clock(); + Counter = 0; +// for ( i = 0; i < nSizeM; i++ ) +// for ( k = 0; k < nSizeK; k++ ) +// Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]); + Vec_WrdForEachEntry( v1M, EntryM, i ) + Vec_WrdForEachEntry( v1K, EntryK, k ) + Counter += ((EntryM & EntryK) == EntryK); + printf( "Total = %8d. ", Counter ); + Abc_PrintTime( 1, "Time", clock() - clk ); + + clk = clock(); + Counter = 0; +// for ( k = 0; k < nSizeK; k++ ) +// for ( i = 0; i < nSizeM; i++ ) +// Counter += ((v1M->pArray[i] & v1K->pArray[k]) == v1K->pArray[k]); + Vec_WrdForEachEntry( v1K, EntryK, k ) + Vec_WrdForEachEntry( v1M, EntryM, i ) + Counter += ((EntryM & EntryK) == EntryK); + printf( "Total = %8d. ", Counter ); + Abc_PrintTime( 1, "Time", clock() - clk ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c index 995d425a..95cc01b7 100644 --- a/src/aig/saig/saigSimMv.c +++ b/src/aig/saig/saigSimMv.c @@ -658,7 +658,7 @@ Vec_Int_t * Saig_MvManFindXFlops( Saig_MvMan_t * p ) /**Function************************************************************* - Synopsis [Finds equivalent flops.] + Synopsis [Checks if the flop is an oscilator.] Description [] @@ -667,19 +667,69 @@ Vec_Int_t * Saig_MvManFindXFlops( Saig_MvMan_t * p ) SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Saig_MvManDeriveMap( Saig_MvMan_t * p, int fVerbose ) +int Saig_MvManCheckOscilator( Saig_MvMan_t * p, int iFlop ) { - Vec_Int_t * vBinValued; - Vec_Ptr_t * vMap = NULL; - Aig_Obj_t * pObj; + Vec_Int_t * vValues; unsigned * pState; - int i, k, j, FlopK, FlopJ, fConst0, Counter1 = 0, Counter2 = 0; - // prepare CI map - vMap = Vec_PtrAlloc( Aig_ManPiNum(p->pAig) ); - Aig_ManForEachPi( p->pAig, pObj, i ) - Vec_PtrPush( vMap, pObj ); + int k, Per, Entry; + // collect values of this flop + vValues = Vec_IntAlloc( 100 ); + Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, 1 ) + { + Vec_IntPush( vValues, pState[iFlop+1] ); +//printf( "%d ", pState[iFlop+1] ); + } +//printf( "\n" ); + assert( Saig_MvIsConst0( Vec_IntEntry(vValues,0) ) ); + // look for constants + for ( Per = 0; Per < Vec_IntSize(vValues)/2; Per++ ) + { + // find the first non-const0 + Vec_IntForEachEntryStart( vValues, Entry, Per, Per ) + if ( !Saig_MvIsConst0(Entry) ) + break; + if ( Per == Vec_IntSize(vValues) ) + break; + // find the first const0 + Vec_IntForEachEntryStart( vValues, Entry, Per, Per ) + if ( Saig_MvIsConst0(Entry) ) + break; + if ( Per == Vec_IntSize(vValues) ) + break; + // try to determine period + assert( Saig_MvIsConst0( Vec_IntEntry(vValues,Per) ) ); + for ( k = Per; k < Vec_IntSize(vValues); k++ ) + if ( Vec_IntEntry(vValues, k-Per) != Vec_IntEntry(vValues, k) ) + break; + if ( k < Vec_IntSize(vValues) ) + continue; + Vec_IntFree( vValues ); +//printf( "Period = %d\n", Per ); + return Per; + } + Vec_IntFree( vValues ); + return 0; +} + +/**Function************************************************************* + + Synopsis [Returns const0 and binary flops.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_MvManFindConstBinaryFlops( Saig_MvMan_t * p, Vec_Int_t ** pvBinary ) +{ + unsigned * pState; + Vec_Int_t * vBinary, * vConst0; + int i, k, fConst0; // detect constant flops - vBinValued = Vec_IntAlloc( p->nFlops ); + vConst0 = Vec_IntAlloc( p->nFlops ); + vBinary = Vec_IntAlloc( p->nFlops ); for ( k = 0; k < p->nFlops; k++ ) { // check if this flop is constant 0 in all states @@ -695,16 +745,106 @@ Vec_Ptr_t * Saig_MvManDeriveMap( Saig_MvMan_t * p, int fVerbose ) continue; // the flop is binary-valued if ( fConst0 ) - { - Vec_PtrWriteEntry( vMap, Saig_ManPiNum(p->pAig) + k, Aig_ManConst0(p->pAig) ); - Counter1++; - } + Vec_IntPush( vConst0, k ); else - Vec_IntPush( vBinValued, k ); + Vec_IntPush( vBinary, k ); + } + *pvBinary = vBinary; + return vConst0; +} + +/**Function************************************************************* + + Synopsis [Find oscilators.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_MvManFindOscilators( Saig_MvMan_t * p, Vec_Int_t ** pvConst0 ) +{ + Vec_Int_t * vBinary, * vOscils; + int Entry, i; + // detect constant flops + *pvConst0 = Saig_MvManFindConstBinaryFlops( p, &vBinary ); + // check binary flops + vOscils = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vBinary, Entry, i ) + if ( Saig_MvManCheckOscilator( p, Entry ) ) + Vec_IntPush( vOscils, Entry ); + Vec_IntFree( vBinary ); + return vOscils; +} + +/**Function************************************************************* + + Synopsis [Find constants and oscilators.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Saig_MvManCreateNextSkip( Saig_MvMan_t * p ) +{ + Vec_Int_t * vConst0, * vOscils, * vXFlops; + int i, Entry; + vOscils = Saig_MvManFindOscilators( p, &vConst0 ); +//printf( "Found %d constants and %d oscilators.\n", Vec_IntSize(vConst0), Vec_IntSize(vOscils) ); + vXFlops = Vec_IntAlloc( p->nFlops ); + Vec_IntFill( vXFlops, p->nFlops, 1 ); + Vec_IntForEachEntry( vConst0, Entry, i ) + Vec_IntWriteEntry( vXFlops, Entry, 0 ); + Vec_IntForEachEntry( vOscils, Entry, i ) + Vec_IntWriteEntry( vXFlops, Entry, 0 ); + Vec_IntFree( vOscils ); + Vec_IntFree( vConst0 ); + return vXFlops; +} + +/**Function************************************************************* + + Synopsis [Finds equivalent flops.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Saig_MvManDeriveMap( Saig_MvMan_t * p, int fVerbose ) +{ + Vec_Int_t * vConst0, * vBinValued; + Vec_Ptr_t * vMap = NULL; + Aig_Obj_t * pObj; + unsigned * pState; + int i, k, j, FlopK, FlopJ; + int Counter1 = 0, Counter2 = 0; + // prepare CI map + vMap = Vec_PtrAlloc( Aig_ManPiNum(p->pAig) ); + Aig_ManForEachPi( p->pAig, pObj, i ) + Vec_PtrPush( vMap, pObj ); + // detect constant flops + vConst0 = Saig_MvManFindConstBinaryFlops( p, &vBinValued ); + // set constants + Vec_IntForEachEntry( vConst0, FlopK, k ) + { + Vec_PtrWriteEntry( vMap, Saig_ManPiNum(p->pAig) + FlopK, Aig_ManConst0(p->pAig) ); + Counter1++; } + Vec_IntFree( vConst0 ); + // detect equivalent (non-ternary flops) Vec_IntForEachEntry( vBinValued, FlopK, k ) + if ( FlopK >= 0 ) Vec_IntForEachEntryStart( vBinValued, FlopJ, j, k+1 ) + if ( FlopJ >= 0 ) { // check if they are equal Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, i, 1 ) @@ -714,6 +854,7 @@ Vec_Ptr_t * Saig_MvManDeriveMap( Saig_MvMan_t * p, int fVerbose ) continue; // set the equivalence Vec_PtrWriteEntry( vMap, Saig_ManPiNum(p->pAig) + FlopJ, Saig_ManLo(p->pAig, FlopK) ); + Vec_IntWriteEntry( vBinValued, FlopJ, -1 ); Counter2++; } if ( fVerbose ) @@ -758,6 +899,20 @@ ABC_PRT( "Constructing the problem", clock() - clk ); clk = clock(); for ( f = 0; ; f++ ) { + if ( f == nFramesSatur ) + { + if ( fVerbose ) + printf( "Begining to saturate simulation after %d frames\n", f ); + // find all flops that have at least one X value in the past and set them to X forever + p->vXFlops = Saig_MvManFindXFlops( p ); + } + if ( f == 2 * nFramesSatur ) + { + if ( fVerbose ) + printf( "Agressively saturating simulation after %d frames\n", f ); + Vec_IntFree( p->vXFlops ); + p->vXFlops = Saig_MvManCreateNextSkip( p ); + } // retire some flops if ( p->vXFlops ) { @@ -778,13 +933,6 @@ ABC_PRT( "Constructing the problem", clock() - clk ); // printf( "Total number of PIs = %d. AND nodes = %d.\n", p->nPis, p->nObjs - p->nPis ); break; } - if ( f == nFramesSatur ) - { - if ( fVerbose ) - printf( "Begining to saturate simulation after %d frames\n", f+1 ); - // find all flops that have at least one X value in the past and set them to X forever - p->vXFlops = Saig_MvManFindXFlops( p ); - } } // printf( "Coverged after %d frames.\n", f ); if ( fVerbose ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 39a6aacb..1802f24a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8854,8 +8854,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) */ { -// void Bdc_SpfdDecomposeTest(); -// Bdc_SpfdDecomposeTest(); + void Bdc_SpfdDecomposeTest(); + Bdc_SpfdDecomposeTest(); } return 0; usage: -- cgit v1.2.3