/**CFile****************************************************************
FileName [sswRarity.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [Rarity-driven refinement of equivalence classes.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswRarity.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
#include "aig/gia/giaAig.h"
#include "base/main/main.h"
#include "sat/bmc/bmc.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Ssw_RarMan_t_ Ssw_RarMan_t;
struct Ssw_RarMan_t_
{
// parameters
Ssw_RarPars_t* pPars;
int nGroups; // the number of flop groups
int nWordsReg; // the number of words in the registers
// internal data
Aig_Man_t * pAig; // AIG with equivalence classes
Ssw_Cla_t * ppClasses; // equivalence classes
Vec_Int_t * vInits; // initial state
// simulation data
word * pObjData; // simulation info for each obj
word * pPatData; // pattern data for each reg
// candidates to update
Vec_Ptr_t * vUpdConst; // constant 1 candidates
Vec_Ptr_t * vUpdClass; // class representatives
// rarity data
int * pRarity; // occur counts for patterns in groups
double * pPatCosts; // pattern costs
// best patterns
Vec_Int_t * vPatBests; // best patterns
int iFailPo; // failed primary output
int iFailPat; // failed pattern
// counter-examples
Vec_Ptr_t * vCexes;
};
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
return p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat];
}
static inline void Ssw_RarSetBinPat( Ssw_RarMan_t * p, int iBin, int iPat, int Value )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat] = Value;
}
static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->pPars->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->pPars->nBinSize) );
p->pRarity[iBin * (1 << p->pPars->nBinSize) + iPat]++;
}
static inline int Ssw_RarBitWordNum( int nBits ) { return (nBits>>6) + ((nBits&63) > 0); }
static inline word * Ssw_RarObjSim( Ssw_RarMan_t * p, int Id ) { assert( Id < Aig_ManObjNumMax(p->pAig) ); return p->pObjData + p->pPars->nWords * Id; }
static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->pPars->nWords ); return p->pPatData + p->nWordsReg * Id; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarSetDefaultParams( Ssw_RarPars_t * p )
{
memset( p, 0, sizeof(Ssw_RarPars_t) );
p->nFrames = 20;
p->nWords = 50;
p->nBinSize = 8;
p->nRounds = 0;
p->nRestart = 0;
p->nRandSeed = 0;
p->TimeOut = 0;
p->TimeOutGap = 0;
p->fSolveAll = 0;
p->fDropSatOuts = 0;
p->fSetLastState = 0;
p->fVerbose = 0;
p->fNotVerbose = 0;
}
/**Function*************************************************************
Synopsis [Prepares random number generator.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManPrepareRandom( int nRandSeed )
{
int i;
Aig_ManRandom( 1 );
for ( i = 0; i < nRandSeed; i++ )
Aig_ManRandom( 0 );
}
/**Function*************************************************************
Synopsis [Initializes random primary inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManAssingRandomPis( Ssw_RarMan_t * p )
{
word * pSim;
Aig_Obj_t * pObj;
int w, i;
Saig_ManForEachPi( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = Aig_ManRandom64(0);
// pSim[0] <<= 1;
// pSim[0] = (pSim[0] << 2) | 2;
pSim[0] = (pSim[0] << 4) | ((i & 1) ? 0xA : 0xC);
}
}
/**Function*************************************************************
Synopsis [Derives the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Ssw_RarDeriveCex( Ssw_RarMan_t * p, int iFrame, int iPo, int iPatFinal, int fVerbose )
{
Abc_Cex_t * pCex;
Aig_Obj_t * pObj;
Vec_Int_t * vTrace;
word * pSim;
int i, r, f, iBit, iPatThis;
// compute the pattern sequence
iPatThis = iPatFinal;
vTrace = Vec_IntStartFull( iFrame / p->pPars->nFrames + 1 );
Vec_IntWriteEntry( vTrace, iFrame / p->pPars->nFrames, iPatThis );
for ( r = iFrame / p->pPars->nFrames - 1; r >= 0; r-- )
{
iPatThis = Vec_IntEntry( p->vPatBests, r * p->pPars->nWords + iPatThis / 64 );
Vec_IntWriteEntry( vTrace, r, iPatThis );
}
// create counter-example
pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), iFrame+1 );
pCex->iFrame = iFrame;
pCex->iPo = iPo;
// insert the bits
iBit = Aig_ManRegNum(p->pAig);
for ( f = 0; f <= iFrame; f++ )
{
Ssw_RarManAssingRandomPis( p );
iPatThis = Vec_IntEntry( vTrace, f / p->pPars->nFrames );
Saig_ManForEachPi( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
if ( Abc_InfoHasBit( (unsigned *)pSim, iPatThis ) )
Abc_InfoSetBit( pCex->pData, iBit );
iBit++;
}
}
Vec_IntFree( vTrace );
assert( iBit == pCex->nBits );
// verify the counter example
if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
{
Abc_Print( 1, "Ssw_RarDeriveCex(): Counter-example is invalid.\n" );
// Abc_CexFree( pCex );
// pCex = NULL;
}
else
{
// Abc_Print( 1, "Counter-example verification is successful.\n" );
}
return pCex;
}
/**Function*************************************************************
Synopsis [Transposing 32-bit matrix.]
Description [Borrowed from "Hacker's Delight", by Henry Warren.]
SideEffects []
SeeAlso []
***********************************************************************/
void transpose32( unsigned A[32] )
{
int j, k;
unsigned t, m = 0x0000FFFF;
for ( j = 16; j != 0; j = j >> 1, m = m ^ (m << j) )
{
for ( k = 0; k < 32; k = (k + j + 1) & ~j )
{
t = (A[k] ^ (A[k+j] >> j)) & m;
A[k] = A[k] ^ t;
A[k+j] = A[k+j] ^ (t << j);
}
}
}
/**Function*************************************************************
Synopsis [Transposing 64-bit matrix.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void transpose64( word A[64] )
{
int j, k;
word t, m = 0x00000000FFFFFFFF;
for ( j = 32; j != 0; j = j >> 1, m = m ^ (m << j) )
{
for ( k = 0; k < 64; k = (k + j + 1) & ~j )
{
t = (A[k] ^ (A[k+j] >> j)) & m;
A[k] = A[k] ^ t;
A[k+j] = A[k+j] ^ (t << j);
}
}
}
/**Function*************************************************************
Synopsis [Transposing 64-bit matrix.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void transpose64Simple( word A[64], word B[64] )
{
int i, k;
for ( i = 0; i < 64; i++ )
B[i] = 0;
for ( i = 0; i < 64; i++ )
for ( k = 0; k < 64; k++ )
if ( (A[i] >> k) & 1 )
B[k] |= ((word)1 << (63-i));
}
/**Function*************************************************************
Synopsis [Testing the transposing code.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void TransposeTest()
{
word M[64], N[64];
int i;
abctime clk;
Aig_ManRandom64( 1 );
// for ( i = 0; i < 64; i++ )
// M[i] = Aig_ManRandom64( 0 );
for ( i = 0; i < 64; i++ )
M[i] = i? (word)0 : ~(word)0;
// for ( i = 0; i < 64; i++ )
// Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
clk = Abc_Clock();
for ( i = 0; i < 100001; i++ )
transpose64Simple( M, N );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
clk = Abc_Clock();
for ( i = 0; i < 100001; i++ )
transpose64( M );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
for ( i = 0; i < 64; i++ )
if ( M[i] != N[i] )
Abc_Print( 1, "Mismatch\n" );
/*
Abc_Print( 1, "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), Abc_Print( 1, "\n" );
Abc_Print( 1, "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), Abc_Print( 1, "\n" );
*/
}
/**Function*************************************************************
Synopsis [Transposing pObjData[ nRegs x nWords ] -> pPatData[ nWords x nRegs ].]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarTranspose( Ssw_RarMan_t * p )
{
Aig_Obj_t * pObj;
word M[64];
int w, r, i;
for ( w = 0; w < p->pPars->nWords; w++ )
for ( r = 0; r < p->nWordsReg; r++ )
{
// save input
for ( i = 0; i < 64; i++ )
{
if ( r*64 + 63-i < Aig_ManRegNum(p->pAig) )
{
pObj = Saig_ManLi( p->pAig, r*64 + 63-i );
M[i] = Ssw_RarObjSim( p, Aig_ObjId(pObj) )[w];
}
else
M[i] = 0;
}
// transpose
transpose64( M );
// save output
for ( i = 0; i < 64; i++ )
Ssw_RarPatSim( p, w*64 + 63-i )[r] = M[i];
}
/*
Saig_ManForEachLi( p->pAig, pObj, i )
{
word * pBitData = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
Extra_PrintBinary( stdout, (unsigned *)pBitData, 64*p->pPars->nWords ); Abc_Print( 1, "\n" );
}
Abc_Print( 1, "\n" );
for ( i = 0; i < p->pPars->nWords*64; i++ )
{
word * pBitData = Ssw_RarPatSim( p, i );
Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); Abc_Print( 1, "\n" );
}
Abc_Print( 1, "\n" );
*/
}
/**Function*************************************************************
Synopsis [Sets random inputs and specialied flop outputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManInitialize( Ssw_RarMan_t * p, Vec_Int_t * vInit )
{
Aig_Obj_t * pObj, * pObjLi;
word * pSim, * pSimLi;
int w, i;
// constant
pObj = Aig_ManConst1( p->pAig );
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = ~(word)0;
// primary inputs
Ssw_RarManAssingRandomPis( p );
// flop outputs
if ( vInit )
{
assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->pPars->nWords );
Saig_ManForEachLo( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = Vec_IntEntry(vInit, w * Saig_ManRegNum(p->pAig) + i) ? ~(word)0 : (word)0;
}
}
else
{
Saig_ManForEachLiLo( p->pAig, pObjLi, pObj, i )
{
pSimLi = Ssw_RarObjSim( p, Aig_ObjId(pObjLi) );
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = pSimLi[w];
}
}
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManPoIsConst0( void * pMan, Aig_Obj_t * pObj )
{
Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
int w;
for ( w = 0; w < p->pPars->nWords; w++ )
if ( pSim[w] )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjIsConst( void * pMan, Aig_Obj_t * pObj )
{
Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = pObj->fPhase ? ~(word)0 : 0;
int w;
for ( w = 0; w < p->pPars->nWords; w++ )
if ( pSim[w] ^ Flip )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation infos are equal.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjsAreEqual( void * pMan, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
word * pSim0 = Ssw_RarObjSim( p, pObj0->Id );
word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~(word)0 : 0;
int w;
for ( w = 0; w < p->pPars->nWords; w++ )
if ( pSim0[w] ^ pSim1[w] ^ Flip )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Computes hash value of the node using its simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned Ssw_RarManObjHashWord( void * pMan, Aig_Obj_t * pObj )
{
Ssw_RarMan_t * p = (Ssw_RarMan_t *)pMan;
static int s_SPrimes[128] = {
1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
};
unsigned * pSims;
unsigned uHash;
int i;
uHash = 0;
pSims = (unsigned *)Ssw_RarObjSim( p, pObj->Id );
for ( i = 0; i < 2 * p->pPars->nWords; i++ )
uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
return uHash;
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
{
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = 0;//pObj->fPhase ? ~(word)0 : 0; // bug fix!
int w, i;
for ( w = 0; w < p->pPars->nWords; w++ )
if ( pSim[w] ^ Flip )
{
for ( i = 0; i < 64; i++ )
if ( ((pSim[w] ^ Flip) >> i) & 1 )
break;
assert( i < 64 );
return w * 64 + i;
}
return -1;
}
/**Function*************************************************************
Synopsis [Check if any of the POs becomes non-constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int iFrame, abctime Time )
{
Aig_Obj_t * pObj;
int i;
p->iFailPo = -1;
p->iFailPat = -1;
Saig_ManForEachPo( p->pAig, pObj, i )
{
if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
break;
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
if ( Ssw_RarManPoIsConst0(p, pObj) )
continue;
p->iFailPo = i;
p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
if ( !p->pPars->fSolveAll )
break;
// remember the one solved
p->pPars->nSolved++;
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, i) == NULL );
Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(i, NULL) )
return 2; // quitting due to callback
// print final report
if ( !p->pPars->fNotVerbose )
{
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs). ",
nOutDigits, p->iFailPo, iFrame,
nOutDigits, p->pPars->nSolved,
nOutDigits, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Time );
}
}
if ( p->iFailPo >= 0 ) // found CEX
return 1;
else
return 0;
}
/**Function*************************************************************
Synopsis [Performs one round of simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_RarManSimulate( Ssw_RarMan_t * p, Vec_Int_t * vInit, int fUpdate, int fFirst )
{
Aig_Obj_t * pObj, * pRepr;
word * pSim, * pSim0, * pSim1;
word Flip, Flip0, Flip1;
int w, i;
// initialize
Ssw_RarManInitialize( p, vInit );
Vec_PtrClear( p->vUpdConst );
Vec_PtrClear( p->vUpdClass );
Aig_ManIncrementTravId( p->pAig );
// check comb inputs
if ( fUpdate )
Aig_ManForEachCi( p->pAig, pObj, i )
{
pRepr = Aig_ObjRepr(p->pAig, pObj);
if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
continue;
if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
continue;
// save for update
if ( pRepr == Aig_ManConst1(p->pAig) )
Vec_PtrPush( p->vUpdConst, pObj );
else
{
Vec_PtrPush( p->vUpdClass, pRepr );
Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
}
}
// simulate
Aig_ManForEachNode( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
pSim1 = Ssw_RarObjSim( p, Aig_ObjFaninId1(pObj) );
Flip0 = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0;
Flip1 = Aig_ObjFaninC1(pObj) ? ~(word)0 : 0;
for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = (Flip0 ^ pSim0[w]) & (Flip1 ^ pSim1[w]);
if ( !fUpdate )
continue;
// check classes
pRepr = Aig_ObjRepr(p->pAig, pObj);
if ( pRepr == NULL || Aig_ObjIsTravIdCurrent( p->pAig, pRepr ) )
continue;
if ( Ssw_RarManObjsAreEqual( p, pObj, pRepr ) )
continue;
// save for update
if ( pRepr == Aig_ManConst1(p->pAig) )
Vec_PtrPush( p->vUpdConst, pObj );
else
{
Vec_PtrPush( p->vUpdClass, pRepr );
Aig_ObjSetTravIdCurrent( p->pAig, pRepr );
}
}
// transfer to POs
Aig_ManForEachCo( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
Flip = Aig_ObjFaninC0(pObj) ? ~(word)0 : 0;
for ( w = 0; w < p->pPars->nWords; w++ )
pSim[w] = Flip ^ pSim0[w];
}
// refine classes
if ( fUpdate )
{
if ( fFirst )
{
Vec_Ptr_t * vCands = Vec_PtrAlloc( 1000 );
Aig_ManForEachObj( p->pAig, pObj, i )
if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
Vec_PtrPush( vCands, pObj );
assert( Vec_PtrSize(vCands) == Ssw_ClassesCand1Num(p->ppClasses) );
Ssw_ClassesPrepareRehash( p->ppClasses, vCands, 0 );
Vec_PtrFree( vCands );
}
else
{
Ssw_ClassesRefineConst1Group( p->ppClasses, p->vUpdConst, 1 );
Ssw_ClassesRefineGroup( p->ppClasses, p->vUpdClass, 1 );
}
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
{
Ssw_RarMan_t * p;
// if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
// return NULL;
p = ABC_CALLOC( Ssw_RarMan_t, 1 );
p->pAig = pAig;
p->pPars = pPars;
p->nGroups = Aig_ManRegNum(pAig) / pPars->nBinSize;
p->pRarity = ABC_CALLOC( int, (1 << pPars->nBinSize) * p->nGroups );
p->pPatCosts = ABC_CALLOC( double, p->pPars->nWords * 64 );
p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->pPars->nWords );
p->pPatData = ABC_ALLOC( word, 64 * p->pPars->nWords * p->nWordsReg );
p->vUpdConst = Vec_PtrAlloc( 100 );
p->vUpdClass = Vec_PtrAlloc( 100 );
p->vPatBests = Vec_IntAlloc( 100 );
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ssw_RarManStop( Ssw_RarMan_t * p )
{
// Vec_PtrFreeP( &p->vCexes );
if ( p->vCexes )
{
assert( p->pAig->vSeqModelVec == NULL );
p->pAig->vSeqModelVec = p->vCexes;
p->vCexes = NULL;
}
if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
Vec_IntFreeP( &p->vInits );
Vec_IntFreeP( &p->vPatBests );
Vec_PtrFreeP( &p->vUpdConst );
Vec_PtrFreeP( &p->vUpdClass );
ABC_FREE( p->pObjData );
ABC_FREE( p->pPatData );
ABC_FREE( p->pPatCosts );
ABC_FREE( p->pRarity );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Select best patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
{
// Aig_Obj_t * pObj;
unsigned char * pData;
unsigned * pPattern;
int i, k, Value;
// more data from regs to pats
Ssw_RarTranspose( p );
// update counters
for ( k = 0; k < p->pPars->nWords * 64; k++ )
{
pData = (unsigned char *)Ssw_RarPatSim( p, k );
for ( i = 0; i < p->nGroups; i++ )
Ssw_RarAddToBinPat( p, i, pData[i] );
}
// for each pattern
for ( k = 0; k < p->pPars->nWords * 64; k++ )
{
pData = (unsigned char *)Ssw_RarPatSim( p, k );
// find the cost of its values
p->pPatCosts[k] = 0.0;
for ( i = 0; i < p->nGroups; i++ )
{
Value = Ssw_RarGetBinPat( p, i, pData[i] );
assert( Value > 0 );
p->pPatCosts[k] += 1.0/(Value*Value);
}
// print the result
//Abc_Print( 1, "%3d : %9.6f\n", k, p->pPatCosts[k] );
}
// choose as many as there are words
Vec_IntClear( vInits );
for ( i = 0; i < p->pPars->nWords; i++ )
{
// select the best
int iPatBest = -1;
double iCostBest = -ABC_INFINITY;
for ( k = 0; k < p->pPars->nWords * 64; k++ )
if ( iCostBest < p->pPatCosts[k] )
{
iCostBest = p->pPatCosts[k];
iPatBest = k;
}
// remove from costs
assert( iPatBest >= 0 );
p->pPatCosts[iPatBest] = -ABC_INFINITY;
// set the flops
pPattern = (unsigned *)Ssw_RarPatSim( p, iPatBest );
for ( k = 0; k < Aig_ManRegNum(p->pAig); k++ )
Vec_IntPush( vInits, Abc_InfoHasBit(pPattern, k) );
//Abc_Print( 1, "Best pattern %5d\n", iPatBest );
Vec_IntPush( p->vPatBests, iPatBest );
}
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->pPars->nWords );
}
/**Function*************************************************************
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
Vec_Int_t * vInit;
Aig_Obj_t * pObj, * pObjLi;
int f, i, iBit;
// assign register outputs
Saig_ManForEachLi( pAig, pObj, i )
pObj->fMarkB = Abc_InfoHasBit( pCex->pData, i );
// simulate the timeframes
iBit = pCex->nRegs;
for ( f = 0; f <= pCex->iFrame; f++ )
{
// set the PI simulation information
Aig_ManConst1(pAig)->fMarkB = 1;
Saig_ManForEachPi( pAig, pObj, i )
pObj->fMarkB = Abc_InfoHasBit( pCex->pData, iBit++ );
Saig_ManForEachLiLo( pAig, pObjLi, pObj, i )
pObj->fMarkB = pObjLi->fMarkB;
// simulate internal nodes
Aig_ManForEachNode( pAig, pObj, i )
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
& ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
// assign the COs
Aig_ManForEachCo( pAig, pObj, i )
pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) );
}
assert( iBit == pCex->nBits );
// check that the output failed as expected -- cannot check because it is not an SRM!
// pObj = Aig_ManCo( pAig, pCex->iPo );
// if ( pObj->fMarkB != 1 )
// Abc_Print( 1, "The counter-example does not refine the output.\n" );
// record the new pattern
vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
{
//Abc_Print( 1, "%d", pObj->fMarkB );
Vec_IntPush( vInit, pObj->fMarkB );
}
//Abc_Print( 1, "\n" );
Aig_ManCleanMarkB( pAig );
return vInit;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
{
Aig_Obj_t * pObj;
int i;
Saig_ManForEachPo( pAig, pObj, i )
{
if ( pAig->nConstrs && i >= Saig_ManPoNum(pAig) - pAig->nConstrs )
return 0;
if ( pObj->fPhase )
{
ABC_FREE( pAig->pSeqModel );
pAig->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), 1 );
pAig->pSeqModel->iPo = i;
if ( fVerbose )
Abc_Print( 1, "Output %d is trivally SAT in frame 0. \n", i );
return 1;
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Perform sequential simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
{
int fTryBmc = 0;
int fMiter = 1;
Ssw_RarMan_t * p;
int r, f = -1;
abctime clk, clkTotal = Abc_Clock();
abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
abctime timeLastSolved = 0;
int nNumRestart = 0;
int nSavedSeed = pPars->nRandSeed;
int RetValue = -1;
int iFrameFail = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
ABC_FREE( pAig->pSeqModel );
// consider the case of empty AIG
// if ( Aig_ManNodeNum(pAig) == 0 )
// return -1;
// check trivially SAT miters
// if ( fMiter && Ssw_RarCheckTrivial( pAig, fVerbose ) )
// return 0;
if ( pPars->fVerbose )
Abc_Print( 1, "Rarity simulation with %d words, %d frames, %d rounds, %d restart, %d seed, and %d sec timeout.\n",
pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRestart, pPars->nRandSeed, pPars->TimeOut );
// reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed );
// create manager
p = Ssw_RarManStart( pAig, pPars );
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * pPars->nWords );
// perform simulation rounds
pPars->nSolved = 0;
timeLastSolved = Abc_Clock();
for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
{
clk = Abc_Clock();
if ( fTryBmc )
{
Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0, 0 );
// if ( pNewAig->pSeqModel != NULL )
// Abc_Print( 1, "BMC has found a counter-example in frame %d.\n", iFrameFail );
Aig_ManStop( pNewAig );
}
// simulate
for ( f = 0; f < pPars->nFrames; f++ )
{
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
if ( fMiter )
{
int Status = Ssw_RarManCheckNonConstOutputs(p, r * p->pPars->nFrames + f, Abc_Clock() - clkTotal);
if ( Status == 2 )
{
Abc_Print( 1, "Quitting due to callback on fail.\n" );
goto finish;
}
if ( Status == 1 ) // found CEX
{
RetValue = 0;
if ( !pPars->fSolveAll )
{
if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
Ssw_RarManPrepareRandom( nSavedSeed );
if ( pPars->fVerbose )
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, pPars->fVerbose );
// print final report
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
goto finish;
}
timeLastSolved = Abc_Clock();
}
// else - did not find a counter example
}
// check timeout
if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
{
if ( !pPars->fSilent )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
}
goto finish;
}
if ( pPars->TimeOutGap && timeLastSolved && Abc_Clock() > timeLastSolved + pPars->TimeOutGap * CLOCKS_PER_SEC )
{
if ( !pPars->fSilent )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts and solved %d outputs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved );
Abc_Print( 1, "Reached gap timeout (%d sec).\n", pPars->TimeOutGap );
}
goto finish;
}
// check if all outputs are solved by now
if ( pPars->fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 )
goto finish;
}
// get initialization patterns
if ( pPars->nRestart && r == pPars->nRestart )
{
r = -1;
nSavedSeed = (nSavedSeed + 1) % 1000;
Ssw_RarManPrepareRandom( nSavedSeed );
Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
nNumRestart++;
Vec_IntClear( p->vPatBests );
// clean rarity info
// memset( p->pRarity, 0, sizeof(int) * (1 << nBinSize) * p->nGroups );
}
else
Ssw_RarTransferPatterns( p, p->vInits );
// printout
if ( pPars->fVerbose )
{
if ( pPars->fSolveAll )
{
Abc_Print( 1, "Starts =%6d ", nNumRestart );
Abc_Print( 1, "Rounds =%6d ", nNumRestart * pPars->nRestart + ((r==-1)?0:r) );
Abc_Print( 1, "Frames =%6d ", (nNumRestart * pPars->nRestart + r) * pPars->nFrames );
Abc_Print( 1, "CEX =%6d (%6.2f %%) ", pPars->nSolved, 100.0*pPars->nSolved/Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
else
Abc_Print( 1, "." );
}
}
finish:
if ( pPars->fSetLastState && p->vInits )
{
assert( Vec_IntSize(p->vInits) % Aig_ManRegNum(pAig) == 0 );
Vec_IntShrink( p->vInits, Aig_ManRegNum(pAig) );
pAig->pData = p->vInits; p->vInits = NULL;
}
if ( pPars->nSolved )
{
/*
if ( !pPars->fSilent )
{
if ( pPars->fVerbose && !pPars->fSolveAll ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart, pPars->nSolved, Saig_ManPoNum(p->pAig) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
*/
}
else if ( r == pPars->nRounds && f == pPars->nFrames )
{
if ( !pPars->fSilent )
{
if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
}
// cleanup
Ssw_RarManStop( p );
return RetValue;
}
/**Function*************************************************************
Synopsis [Derive random flop permutation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Ssw_RarRandomPermFlop( int nFlops, int nUnused )
{
Vec_Int_t * vPerm;
int i, k, * pArray;
srand( 1 );
printf( "Generating random permutation of %d flops.\n", nFlops );
vPerm = Vec_IntStartNatural( nFlops );
pArray = Vec_IntArray( vPerm );
for ( i = 0; i < nFlops; i++ )
{
k = rand() % nFlops;
ABC_SWAP( int, pArray[i], pArray[k] );
}
printf( "Randomly adding %d unused flops.\n", nUnused );
for ( i = 0; i < nUnused; i++ )
{
k = rand() % Vec_IntSize(vPerm);
Vec_IntPush( vPerm, -1 );
pArray = Vec_IntArray( vPerm );
ABC_SWAP( int, pArray[Vec_IntSize(vPerm)-1], pArray[k] );
}
// Vec_IntPrint(vPerm);
return vPerm;
}
/**Function*************************************************************
Synopsis [Perform sequential simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
{
Aig_Man_t * pAig;
int RetValue;
if ( pPars->fUseFfGrouping )
{
Vec_Int_t * vPerm = Ssw_RarRandomPermFlop( Gia_ManRegNum(p), 10 );
Gia_Man_t * pTemp = Gia_ManDupPermFlopGap( p, vPerm );
Vec_IntFree( vPerm );
pAig = Gia_ManToAigSimple( pTemp );
Gia_ManStop( pTemp );
}
else
pAig = Gia_ManToAigSimple( p );
RetValue = Ssw_RarSimulate( pAig, pPars );
// save counter-example
Abc_CexFree( p->pCexSeq );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
return RetValue;
}
/**Function*************************************************************
Synopsis [Filter equivalence classes of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSignalFilter( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
{
Ssw_RarMan_t * p;
int r, f = -1, i, k;
abctime clkTotal = Abc_Clock();
abctime nTimeToStop = pPars->TimeOut ? pPars->TimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
int nNumRestart = 0;
int nSavedSeed = pPars->nRandSeed;
int RetValue = -1;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManConstrNum(pAig) == 0 );
// consider the case of empty AIG
if ( Aig_ManNodeNum(pAig) == 0 )
return -1;
// check trivially SAT miters
if ( pPars->fMiter && Ssw_RarCheckTrivial( pAig, 1 ) )
return 0;
if ( pPars->fVerbose )
Abc_Print( 1, "Rarity equiv filtering with %d words, %d frames, %d rounds, %d seed, and %d sec timeout.\n",
pPars->nWords, pPars->nFrames, pPars->nRounds, pPars->nRandSeed, pPars->TimeOut );
// reset random numbers
Ssw_RarManPrepareRandom( nSavedSeed );
// create manager
p = Ssw_RarManStart( pAig, pPars );
// compute starting state if needed
assert( p->vInits == NULL );
if ( pPars->pCex )
{
p->vInits = Ssw_RarFindStartingState( pAig, pPars->pCex );
Abc_Print( 1, "Beginning simulation from the state derived using the counter-example.\n" );
}
else
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
// duplicate the array
for ( i = 1; i < pPars->nWords; i++ )
for ( k = 0; k < Aig_ManRegNum(pAig); k++ )
Vec_IntPush( p->vInits, Vec_IntEntry(p->vInits, k) );
assert( Vec_IntSize(p->vInits) == Aig_ManRegNum(pAig) * pPars->nWords );
// create trivial equivalence classes with all nodes being candidates for constant 1
if ( pAig->pReprs == NULL )
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchOnly, 0 );
else
p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
Ssw_ClassesSetData( p->ppClasses, p, Ssw_RarManObjHashWord, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
// print the stats
if ( pPars->fVerbose )
{
Abc_Print( 1, "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// refine classes using BMC
for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
{
// start filtering equivalence classes
if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
{
Abc_Print( 1, "All equivalences are refined away.\n" );
break;
}
// simulate
for ( f = 0; f < pPars->nFrames; f++ )
{
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
if ( pPars->fMiter && Ssw_RarManCheckNonConstOutputs(p, -1, 0) )
{
if ( !pPars->fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
// Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * pPars->nFrames, (r+1) * pPars->nFrames );
if ( pPars->fVerbose )
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Ssw_RarManPrepareRandom( nSavedSeed );
Abc_CexFree( pAig->pSeqModel );
pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->pPars->nFrames + f, p->iFailPo, p->iFailPat, 1 );
// print final report
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
RetValue = 0;
goto finish;
}
// check timeout
if ( pPars->TimeOut && Abc_Clock() > nTimeToStop )
{
if ( pPars->fVerbose ) Abc_Print( 1, "\n" );
Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_Print( 1, "Reached timeout (%d sec).\n", pPars->TimeOut );
goto finish;
}
}
// get initialization patterns
if ( pPars->pCex == NULL && pPars->nRestart && r == pPars->nRestart )
{
r = -1;
nSavedSeed = (nSavedSeed + 1) % 1000;
Ssw_RarManPrepareRandom( nSavedSeed );
Vec_IntFill( p->vInits, Aig_ManRegNum(pAig) * pPars->nWords, 0 );
nNumRestart++;
Vec_IntClear( p->vPatBests );
// clean rarity info
// memset( p->pRarity, 0, sizeof(int) * (1 << nBinSize) * p->nGroups );
}
else
Ssw_RarTransferPatterns( p, p->vInits );
// printout
if ( pPars->fVerbose )
{
Abc_Print( 1, "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
else
{
Abc_Print( 1, "." );
}
}
finish:
// report
if ( r == pPars->nRounds && f == pPars->nFrames )
{
if ( !pPars->fVerbose )
Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts did not assert POs. ", pPars->nFrames, nNumRestart * pPars->nRestart + r, nNumRestart );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
return RetValue;
}
/**Function*************************************************************
Synopsis [Filter equivalence classes of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSignalFilterGia( Gia_Man_t * p, Ssw_RarPars_t * pPars )
{
Aig_Man_t * pAig;
int RetValue;
pAig = Gia_ManToAigSimple( p );
if ( p->pReprs != NULL )
{
Gia_ManReprToAigRepr2( pAig, p );
ABC_FREE( p->pReprs );
ABC_FREE( p->pNexts );
}
RetValue = Ssw_RarSignalFilter( pAig, pPars );
Gia_ManReprFromAigRepr( pAig, p );
// save counter-example
Abc_CexFree( p->pCexSeq );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END