Skip to content

A
abc
Commit 2adf8dc2 by Alan Mishchenko
Options

Sequential cleanup with symbolic/ternary simulation.

parent df6d5090
Showing with 226 additions and 25 deletions
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 ///
////////////////////////////////////////////////////////////////////////
......
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_IntPush( vConst0, k );
else
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) + k, Aig_ManConst0(p->pAig) );
Vec_PtrWriteEntry( vMap, Saig_ManPiNum(p->pAig) + FlopK, Aig_ManConst0(p->pAig) );
Counter1++;
}
else
Vec_IntPush( vBinValued, k );
}
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 )
......
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:
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment