/**CFile****************************************************************
FileName [saigSimSeq.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Fast sequential AIG simulator.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigSimSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
#include "proof/ssw/ssw.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// combinational simulation manager
typedef struct Raig_Man_t_ Raig_Man_t;
struct Raig_Man_t_
{
// parameters
Aig_Man_t * pAig; // the AIG to be used for simulation
int nWords; // the number of words to simulate
// AIG representation
int nPis; // the number of primary inputs
int nPos; // the number of primary outputs
int nCis; // the number of combinational inputs
int nCos; // the number of combinational outputs
int nNodes; // the number of internal nodes
int nObjs; // nCis + nNodes + nCos + 2
int * pFans0; // fanin0 for all objects
int * pFans1; // fanin1 for all objects
Vec_Int_t * vCis2Ids; // mapping of CIs into their PI ids
Vec_Int_t * vLos; // register outputs
Vec_Int_t * vLis; // register inputs
// simulation info
int * pRefs; // reference counter for each node
unsigned * pSims; // simlulation information for each node
// recycable memory
unsigned * pMems; // allocated simulaton memory
int nWordsAlloc; // the number of allocated entries
int nMems; // the number of used entries
int nMemsMax; // the max number of used entries
int MemFree; // next free entry
};
static inline int Raig_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Raig_Lit2Var( int Lit ) { return Lit >> 1; }
static inline int Raig_LitIsCompl( int Lit ) { return Lit & 1; }
static inline int Raig_LitNot( int Lit ) { return Lit ^ 1; }
static inline int Raig_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
static inline int Raig_LitRegular( int Lit ) { return Lit & ~01; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Find the PO corresponding to the PO driver.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Raig_ManFindPo( Aig_Man_t * pAig, int iNode )
{
Aig_Obj_t * pObj;
int i;
Saig_ManForEachPo( pAig, pObj, i )
if ( pObj->iData == iNode )
return i;
return -1;
}
/**Function*************************************************************
Synopsis [Creates fast simulation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Raig_ManCreate_rec( Raig_Man_t * p, Aig_Obj_t * pObj )
{
int iFan0, iFan1;
assert( !Aig_IsComplement(pObj) );
if ( pObj->iData )
return pObj->iData;
assert( !Aig_ObjIsConst1(pObj) );
if ( Aig_ObjIsNode(pObj) )
{
iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
iFan1 = Raig_ManCreate_rec( p, Aig_ObjFanin1(pObj) );
iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj);
}
else if ( Aig_ObjIsCo(pObj) )
{
iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) );
iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj);
iFan1 = 0;
}
else
{
iFan0 = iFan1 = 0;
Vec_IntPush( p->vCis2Ids, Aig_ObjCioId(pObj) );
}
p->pFans0[p->nObjs] = iFan0;
p->pFans1[p->nObjs] = iFan1;
p->pRefs[p->nObjs] = Aig_ObjRefs(pObj);
return pObj->iData = p->nObjs++;
}
/**Function*************************************************************
Synopsis [Creates fast simulation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig )
{
Raig_Man_t * p;
Aig_Obj_t * pObj;
int i, nObjs;
Aig_ManCleanData( pAig );
p = (Raig_Man_t *)ABC_ALLOC( Raig_Man_t, 1 );
memset( p, 0, sizeof(Raig_Man_t) );
p->pAig = pAig;
p->nPis = Saig_ManPiNum(pAig);
p->nPos = Saig_ManPoNum(pAig);
p->nCis = Aig_ManCiNum(pAig);
p->nCos = Aig_ManCoNum(pAig);
p->nNodes = Aig_ManNodeNum(pAig);
nObjs = p->nCis + p->nCos + p->nNodes + 2;
p->pFans0 = ABC_ALLOC( int, nObjs );
p->pFans1 = ABC_ALLOC( int, nObjs );
p->pRefs = ABC_ALLOC( int, nObjs );
p->pSims = ABC_CALLOC( unsigned, nObjs );
p->vCis2Ids = Vec_IntAlloc( Aig_ManCiNum(pAig) );
// add objects (0=unused; 1=const1)
p->nObjs = 2;
pObj = Aig_ManConst1( pAig );
pObj->iData = 1;
Aig_ManForEachCi( pAig, pObj, i )
if ( Aig_ObjRefs(pObj) == 0 )
Raig_ManCreate_rec( p, pObj );
Aig_ManForEachCo( pAig, pObj, i )
Raig_ManCreate_rec( p, pObj );
assert( Vec_IntSize(p->vCis2Ids) == Aig_ManCiNum(pAig) );
assert( p->nObjs == nObjs );
// collect flop outputs
p->vLos = Vec_IntAlloc( Aig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
Vec_IntPush( p->vLos, pObj->iData );
// collect flop inputs
p->vLis = Vec_IntAlloc( Aig_ManRegNum(pAig) );
Saig_ManForEachLi( pAig, pObj, i )
{
Vec_IntPush( p->vLis, pObj->iData );
assert( p->pRefs[ pObj->iData ] == 0 );
p->pRefs[ pObj->iData ]++;
}
return p;
}
/**Function*************************************************************
Synopsis [Creates fast simulation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Raig_ManDelete( Raig_Man_t * p )
{
Vec_IntFree( p->vCis2Ids );
Vec_IntFree( p->vLos );
Vec_IntFree( p->vLis );
ABC_FREE( p->pFans0 );
ABC_FREE( p->pFans1 );
ABC_FREE( p->pRefs );
ABC_FREE( p->pSims );
ABC_FREE( p->pMems );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [References simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Raig_ManSimRef( Raig_Man_t * p, int i )
{
unsigned * pSim;
assert( i > 1 );
assert( p->pSims[i] == 0 );
if ( p->MemFree == 0 )
{
unsigned * pPlace, Ent;
if ( p->nWordsAlloc == 0 )
{
assert( p->pMems == NULL );
p->nWordsAlloc = (1<<17); // -> 1Mb
p->nMems = 1;
}
p->nWordsAlloc *= 2;
p->pMems = ABC_REALLOC( unsigned, p->pMems, p->nWordsAlloc );
memset( p->pMems, 0xff, sizeof(unsigned) * (p->nWords + 1) );
pPlace = (unsigned *)&p->MemFree;
for ( Ent = p->nMems * (p->nWords + 1);
Ent + p->nWords + 1 < (unsigned)p->nWordsAlloc;
Ent += p->nWords + 1 )
{
*pPlace = Ent;
pPlace = p->pMems + Ent;
}
*pPlace = 0;
}
p->pSims[i] = p->MemFree;
pSim = p->pMems + p->MemFree;
p->MemFree = pSim[0];
pSim[0] = p->pRefs[i];
p->nMems++;
if ( p->nMemsMax < p->nMems )
p->nMemsMax = p->nMems;
return pSim;
}
/**Function*************************************************************
Synopsis [Dereference simulaton info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Raig_ManSimDeref( Raig_Man_t * p, int i )
{
unsigned * pSim;
assert( i );
if ( i == 1 ) // const 1
return p->pMems;
assert( p->pSims[i] > 0 );
pSim = p->pMems + p->pSims[i];
if ( --pSim[0] == 0 )
{
pSim[0] = p->MemFree;
p->MemFree = p->pSims[i];
p->pSims[i] = 0;
p->nMems--;
}
return pSim;
}
/**Function*************************************************************
Synopsis [Simulates one round.]
Description [Returns the number of PO entry if failed; 0 otherwise.]
SideEffects []
SeeAlso []
***********************************************************************/
int Raig_ManSimulateRound( Raig_Man_t * p, int fMiter, int fFirst, int * piPat )
{
unsigned * pRes0, * pRes1, * pRes;
int i, w, nCis, nCos, iFan0, iFan1, iPioNum;
// nove the values to the register outputs
Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
{
if ( iPioNum < p->nPis )
continue;
pRes = Raig_ManSimRef( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
if ( fFirst )
memset( pRes + 1, 0, sizeof(unsigned) * p->nWords );
else
{
pRes0 = Raig_ManSimDeref( p, Vec_IntEntry(p->vLis, iPioNum-p->nPis) );
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = pRes0[w];
}
// handle unused PIs
if ( pRes[0] == 0 )
{
pRes[0] = 1;
Raig_ManSimDeref( p, Vec_IntEntry(p->vLos, iPioNum-p->nPis) );
}
}
// simulate the logic
nCis = nCos = 0;
for ( i = 2; i < p->nObjs; i++ )
{
if ( p->pFans0[i] == 0 ) // ci always has zero first fanin
{
iPioNum = Vec_IntEntry( p->vCis2Ids, nCis );
if ( iPioNum < p->nPis )
{
pRes = Raig_ManSimRef( p, i );
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = Aig_ManRandom( 0 );
// handle unused PIs
if ( pRes[0] == 0 )
{
pRes[0] = 1;
Raig_ManSimDeref( p, i );
}
}
else
assert( Vec_IntEntry(p->vLos, iPioNum-p->nPis) == i );
nCis++;
continue;
}
if ( p->pFans1[i] == 0 ) // co always has non-zero 1st fanin and zero 2nd fanin
{
pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
if ( nCos < p->nPos && fMiter )
{
unsigned Const = Raig_LitIsCompl(p->pFans0[i])? ~0 : 0;
for ( w = 1; w <= p->nWords; w++ )
if ( pRes0[w] != Const )
{
*piPat = 32*(w-1) + Aig_WordFindFirstBit( pRes0[w] ^ Const );
return i;
}
}
else
{
pRes = Raig_ManSimRef( p, i );
assert( pRes[0] == 1 );
if ( Raig_LitIsCompl(p->pFans0[i]) )
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = ~pRes0[w];
else
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = pRes0[w];
}
nCos++;
continue;
}
pRes = Raig_ManSimRef( p, i );
assert( pRes[0] > 0 );
iFan0 = p->pFans0[i];
iFan1 = p->pFans1[i];
pRes0 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans0[i]) );
pRes1 = Raig_ManSimDeref( p, Raig_Lit2Var(p->pFans1[i]) );
if ( Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = ~(pRes0[w] | pRes1[w]);
else if ( Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = ~pRes0[w] & pRes1[w];
else if ( !Raig_LitIsCompl(iFan0) && Raig_LitIsCompl(iFan1) )
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = pRes0[w] & ~pRes1[w];
else if ( !Raig_LitIsCompl(iFan0) && !Raig_LitIsCompl(iFan1) )
for ( w = 1; w <= p->nWords; w++ )
pRes[w] = pRes0[w] & pRes1[w];
}
assert( nCis == p->nCis );
assert( nCos == p->nCos );
assert( p->nMems == 1 + Vec_IntSize(p->vLis) );
return 0;
}
/**Function*************************************************************
Synopsis [Returns the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t * vCis2Ids )
{
Abc_Cex_t * p;
unsigned * pData;
int f, i, w, iPioId, Counter;
p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
p->iFrame = iFrame;
p->iPo = iOut;
// fill in the binary data
Aig_ManRandom( 1 );
Counter = p->nRegs;
pData = ABC_ALLOC( unsigned, nWords );
for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
for ( i = 0; i < Aig_ManCiNum(pAig); i++ )
{
iPioId = Vec_IntEntry( vCis2Ids, i );
if ( iPioId >= p->nPis )
continue;
for ( w = 0; w < nWords; w++ )
pData[w] = Aig_ManRandom( 0 );
if ( Abc_InfoHasBit( pData, iPat ) )
Abc_InfoSetBit( p->pData, Counter + iPioId );
}
ABC_FREE( pData );
return p;
}
/**Function*************************************************************
Synopsis [Returns 1 if the bug is detected, 0 otherwise.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Raig_ManSimulate( Aig_Man_t * pAig, int nWords, int nIters, int TimeLimit, int fMiter, int fVerbose )
{
Raig_Man_t * p;
Sec_MtrStatus_t Status;
int i, iPat, RetValue = 0;
abctime clk, clkTotal = Abc_Clock();
assert( Aig_ManRegNum(pAig) > 0 );
Status = Sec_MiterStatus( pAig );
if ( Status.nSat > 0 )
{
printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
return 1;
}
if ( Status.nUndec == 0 )
{
printf( "Miter is trivially unsatisfiable.\n" );
return 0;
}
Aig_ManRandom( 1 );
p = Raig_ManCreate( pAig );
p->nWords = nWords;
// iterate through objects
for ( i = 0; i < nIters; i++ )
{
clk = Abc_Clock();
RetValue = Raig_ManSimulateRound( p, fMiter, i==0, &iPat );
if ( fVerbose )
{
printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, nIters, TimeLimit );
printf("Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC);
}
if ( RetValue > 0 )
{
int iOut = Raig_ManFindPo(p->pAig, RetValue);
assert( pAig->pSeqModel == NULL );
pAig->pSeqModel = Raig_ManGenerateCounter( pAig, i, iOut, nWords, iPat, p->vCis2Ids );
if ( fVerbose )
printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
break;
}
if ( (Abc_Clock() - clk)/CLOCKS_PER_SEC >= TimeLimit )
{
printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, TimeLimit );
break;
}
}
if ( fVerbose )
{
printf( "Maxcut = %8d. AigMem = %7.2f MB. SimMem = %7.2f MB. ",
p->nMemsMax,
1.0*(p->nObjs * 16)/(1<<20),
1.0*(p->nMemsMax * 4 * (nWords+1))/(1<<20) );
ABC_PRT( "Total time", Abc_Clock() - clkTotal );
}
Raig_ManDelete( p );
return RetValue > 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END