luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Changes to enable smarter simulation.

This commit is contained in:
Alan Mishchenko 2011-07-29 14:20:41 +07:00
parent 9e6d0664cb
commit 581daaeade
6 changed files with 982 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/aig/aigUtil.c
View File

@ -1217,8 +1217,8 @@ unsigned Aig_ManRandom( int fReset )
***********************************************************************/
word Aig_ManRandom64( int fReset )
{
word Res = ((word)Aig_ManRandom(fReset)) << 32;
return Res | (word)Aig_ManRandom(0);
word Res = (word)Aig_ManRandom(fReset);
return Res | ((word)Aig_ManRandom(0) << 32);
}

3
src/aig/ssw/ssw.h
View File

@ -118,6 +118,9 @@ extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars
/*=== sswRarity.c ===================================================*/
extern int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
extern int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose );
/*=== sswRarity2.c ===================================================*/
extern int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
extern int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose );
/*=== sswSim.c ===================================================*/
extern Ssw_Sml_t * Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );

20
src/aig/ssw/sswClass.c
View File

@ -1039,6 +1039,26 @@ int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive )
return nRefis;
}
/**Function*************************************************************
Synopsis [Refines the classes after simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive )
{
Aig_Obj_t * pObj;
int i, nRefis = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vReprs, pObj, i )
nRefis += Ssw_ClassesRefineOneClass( p, pObj, fRecursive );
return nRefis;
}
/**Function*************************************************************
Synopsis [Refine the group of constant 1 nodes.]

1
src/aig/ssw/sswInt.h
View File

@ -226,6 +226,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
extern Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
extern Ssw_Cla_t * Ssw_ClassesPreparePairsSimple( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
extern int Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
extern int Ssw_ClassesRefineGroup( Ssw_Cla_t * p, Vec_Ptr_t * vReprs, int fRecursive );
extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );

168
src/aig/ssw/sswRarity.c
View File

@ -84,7 +84,7 @@ static inline void Ssw_RarAddToBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
SeeAlso []
***********************************************************************/
Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int nBinSize, int fVerbose )
{
Ssw_RarMan_t * p;
if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
@ -115,7 +115,7 @@ Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames, int n
SeeAlso []
***********************************************************************/
void Ssw_RarManStop( Ssw_RarMan_t * p )
static void Ssw_RarManStop( Ssw_RarMan_t * p )
{
if ( p->pSml ) Ssw_SmlStop( p->pSml );
if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
@ -139,7 +139,7 @@ void Ssw_RarManStop( Ssw_RarMan_t * p )
SeeAlso []
***********************************************************************/
void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
static void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
{
Aig_Obj_t * pObj;
unsigned * pData;
@ -185,7 +185,7 @@ void Ssw_RarUpdateCounters( Ssw_RarMan_t * p )
SeeAlso []
***********************************************************************/
void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
static void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
{
Aig_Obj_t * pObj;
unsigned * pData;
@ -214,7 +214,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
}
// printf( "\n" );
// print the result
// printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
}
// choose as many as there are words
@ -239,8 +239,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
pData = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjId(pObj) ) + p->nWords * (p->nFrames - 1);
Vec_IntPush( vInits, Aig_InfoHasBit(pData, iPatBest) );
}
//printf( "Best pattern %5d\n", iPatBest );
printf( "Best pattern %5d\n", iPatBest );
}
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->nWords );
}
@ -257,7 +256,7 @@ void Ssw_RarTransferPatterns( Ssw_RarMan_t * p, Vec_Int_t * vInits )
SeeAlso []
***********************************************************************/
Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
{
Vec_Int_t * vInit;
Aig_Obj_t * pObj, * pObjLi;
@ -295,6 +294,84 @@ Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex )
return vInit;
}
/**Function*************************************************************
Synopsis [Perform sequential simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
{
int fMiter = 1;
Ssw_RarMan_t * p;
int r, clk, clkTotal = clock();
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;
if ( fVerbose )
printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers
Aig_ManRandom( 1 );
// create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// perform simulation rounds
for ( r = 0; r < nRounds; r++ )
{
clk = clock();
// simulate
Ssw_SmlSimulateOne( p->pSml );
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
RetValue = 0;
break;
}
// get initialization patterns
Ssw_RarUpdateCounters( p );
Ssw_RarTransferPatterns( p, p->vInits );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// printout
if ( fVerbose )
{
// printf( "Round %3d: ", r );
// Abc_PrintTime( 1, "Time", clock() - clk );
printf( "." );
}
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
break;
}
}
if ( r == nRounds )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
return RetValue;
}
/**Function*************************************************************
Synopsis [Filter equivalence classes of nodes.]
@ -430,81 +507,6 @@ int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize
/**Function*************************************************************
Synopsis [Perform sequential simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
{
int fMiter = 1;
Ssw_RarMan_t * p;
int r, clk, clkTotal = clock();
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;
if ( fVerbose )
printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers
Aig_ManRandom( 1 );
// create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// perform simulation rounds
for ( r = 0; r < nRounds; r++ )
{
clk = clock();
// simulate
Ssw_SmlSimulateOne( p->pSml );
if ( fMiter && Ssw_SmlCheckNonConstOutputs(p->pSml) )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
RetValue = 0;
break;
}
// get initialization patterns
Ssw_RarUpdateCounters( p );
Ssw_RarTransferPatterns( p, p->vInits );
Ssw_SmlInitializeSpecial( p->pSml, p->vInits );
// printout
if ( fVerbose )
{
// printf( "Round %3d: ", r );
// Abc_PrintTime( 1, "Time", clock() - clk );
printf( "." );
}
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
break;
}
}
if ( r == nRounds )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

871
src/aig/ssw/sswRarity2.c Normal file
View File

@ -0,0 +1,871 @@
/**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 "giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Ssw_RarMan_t_ Ssw_RarMan_t;
struct Ssw_RarMan_t_
{
// parameters
int nWords; // the number of words to simulate
int nFrames; // the number of frames to simulate
int nBinSize; // the number of flops in one group
int fVerbose; // the verbosiness flag
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
};
static inline int Ssw_RarGetBinPat( Ssw_RarMan_t * p, int iBin, int iPat )
{
assert( iBin >= 0 && iBin < Aig_ManRegNum(p->pAig) / p->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
return p->pRarity[iBin * (1 << p->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->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
p->pRarity[iBin * (1 << p->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->nBinSize );
assert( iPat >= 0 && iPat < (1 << p->nBinSize) );
p->pRarity[iBin * (1 << p->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->nWords * Id; }
static inline word * Ssw_RarPatSim( Ssw_RarMan_t * p, int Id ) { assert( Id < 64 * p->nWords ); return p->pPatData + p->nWordsReg * Id; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**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, 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 ), printf( "\n" );
clk = clock();
for ( i = 0; i < 100001; i++ )
transpose64Simple( M, N );
Abc_PrintTime( 1, "Time", clock() - clk );
clk = clock();
for ( i = 0; i < 100001; i++ )
transpose64( M );
Abc_PrintTime( 1, "Time", clock() - clk );
for ( i = 0; i < 64; i++ )
if ( M[i] != N[i] )
printf( "Mismatch\n" );
/*
printf( "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&M[i], 64 ), printf( "\n" );
printf( "\n" );
for ( i = 0; i < 64; i++ )
Extra_PrintBinary( stdout, (unsigned *)&N[i], 64 ), printf( "\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->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->nWords ); printf( "\n" );
}
printf( "\n" );
for ( i = 0; i < p->nWords*64; i++ )
{
word * pBitData = Ssw_RarPatSim( p, i );
Extra_PrintBinary( stdout, (unsigned *)pBitData, Aig_ManRegNum(p->pAig) ); printf( "\n" );
}
printf( "\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->nWords; w++ )
pSim[w] = ~(word)0;
// primary inputs
Saig_ManForEachPi( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->nWords; w++ )
pSim[w] = Aig_ManRandom64(0);
}
// flop outputs
if ( vInit )
{
assert( Vec_IntSize(vInit) == Saig_ManRegNum(p->pAig) * p->nWords );
Saig_ManForEachLo( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
for ( w = 0; w < p->nWords; w++ )
pSim[w] = Vec_IntEntry( vInit, w * Saig_ManRegNum(p->pAig) + i );
}
}
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->nWords; w++ )
pSim[w] = pSimLi[w];
}
}
}
/**Function*************************************************************
Synopsis [Returns 1 if simulation info is composed of all zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManObjIsConst( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
{
word * pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
word Flip = pObj->fPhase ? ~0 : 0;
int w;
for ( w = 0; w < p->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( Ssw_RarMan_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
{
word * pSim0 = Ssw_RarObjSim( p, pObj0->Id );
word * pSim1 = Ssw_RarObjSim( p, pObj1->Id );
word Flip = (pObj0->fPhase != pObj1->fPhase) ? ~0 : 0;
int w;
for ( w = 0; w < p->nWords; w++ )
if ( pSim0[w] ^ pSim1[w] ^ Flip )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Check if any of the POs becomes non-constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
{
Aig_Obj_t * pObj;
int i;
Saig_ManForEachPo( p->pAig, pObj, i )
{
if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
return 0;
if ( !Ssw_RarManObjIsConst(p, pObj) )
return 1;
}
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 )
{
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_ManForEachPi( 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) ? ~0 : 0;
Flip1 = Aig_ObjFaninC1(pObj) ? ~0 : 0;
for ( w = 0; w < p->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_ManForEachPo( p->pAig, pObj, i )
{
pSim = Ssw_RarObjSim( p, Aig_ObjId(pObj) );
pSim0 = Ssw_RarObjSim( p, Aig_ObjFaninId0(pObj) );
Flip = Aig_ObjFaninC0(pObj) ? ~0 : 0;
for ( w = 0; w < p->nWords; w++ )
pSim[w] = Flip ^ pSim0[w];
}
// refine classes
if ( fUpdate )
{
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, int nWords, int nFrames, int nBinSize, int fVerbose )
{
Ssw_RarMan_t * p;
if ( Aig_ManRegNum(pAig) < nBinSize || nBinSize <= 0 )
return NULL;
p = ABC_CALLOC( Ssw_RarMan_t, 1 );
p->pAig = pAig;
p->nWords = nWords;
p->nFrames = nFrames;
p->nBinSize = nBinSize;
p->fVerbose = fVerbose;
p->nGroups = Aig_ManRegNum(pAig) / nBinSize;
p->pRarity = ABC_CALLOC( int, (1 << nBinSize) * p->nGroups );
p->pPatCosts = ABC_CALLOC( double, p->nWords * 64 );
p->nWordsReg = Ssw_RarBitWordNum( Aig_ManRegNum(pAig) );
p->pObjData = ABC_ALLOC( word, Aig_ManObjNumMax(pAig) * p->nWords );
p->pPatData = ABC_ALLOC( word, 64 * p->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 )
{
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->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->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);
// printf( "%d ", Value );
}
// printf( "\n" );
// print the result
printf( "%3d : %9.6f\n", k, p->pPatCosts[k] );
}
// choose as many as there are words
Vec_IntClear( vInits );
for ( i = 0; i < p->nWords; i++ )
{
// select the best
int iPatBest = -1;
double iCostBest = -ABC_INFINITY;
for ( k = 0; k < p->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, Aig_InfoHasBit(pPattern, k) );
printf( "Best pattern %5d\n", iPatBest );
Vec_IntPush( p->vPatBests, iPatBest );
}
assert( Vec_IntSize(vInits) == Aig_ManRegNum(p->pAig) * p->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 = 0;
// 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 = Aig_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_ManForEachPo( 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_ManPo( pAig, pCex->iPo );
// if ( pObj->fMarkB != 1 )
// printf( "The counter-example does not refine the output.\n" );
// record the new pattern
vInit = Vec_IntAlloc( Saig_ManRegNum(pAig) );
Saig_ManForEachLo( pAig, pObj, i )
Vec_IntPush( vInit, pObj->fMarkB );
return vInit;
}
/**Function*************************************************************
Synopsis [Perform sequential simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSimulate2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, int fVerbose )
{
int fMiter = 1;
Ssw_RarMan_t * p;
int r, f, clk, clkTotal = clock();
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;
if ( fVerbose )
printf( "Simulating %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers
Aig_ManRandom( 1 );
// create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) * nWords );
// perform simulation rounds
for ( r = 0; r < nRounds; r++ )
{
clk = clock();
// simulate
for ( f = 0; f < nFrames; f++ )
{
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0 );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
RetValue = 0;
goto finish;
}
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
goto finish;
}
}
// get initialization patterns
Ssw_RarTransferPatterns( p, p->vInits );
// printout
if ( fVerbose )
{
// printf( "Round %3d: ", r );
// Abc_PrintTime( 1, "Time", clock() - clk );
printf( "." );
}
}
finish:
if ( r == nRounds )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
return RetValue;
}
/**Function*************************************************************
Synopsis [Filter equivalence classes of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSignalFilter2( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{
int fMiter = 0;
Ssw_RarMan_t * p;
int r, f, i, k, clkTotal = clock();
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;
if ( fVerbose )
printf( "Filtering equivs with %d words through %d frames with %d binsize, %d rounds, and %d sec timeout.\n",
nWords, nFrames, nBinSize, nRounds, TimeOut );
// reset random numbers
Aig_ManRandom( 1 );
// create manager
p = Ssw_RarManStart( pAig, nWords, nFrames, nBinSize, fVerbose );
// compute starting state if needed
assert( p->vInits == NULL );
if ( pCex )
p->vInits = Ssw_RarFindStartingState( pAig, pCex );
else
p->vInits = Vec_IntStart( Aig_ManRegNum(pAig) );
// duplicate the array
for ( i = 1; i < 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) * nWords );
// create trivial equivalence classes with all nodes being candidates for constant 1
if ( pAig->pReprs == NULL )
p->ppClasses = Ssw_ClassesPrepareSimple( pAig, fLatchOnly, 0 );
else
p->ppClasses = Ssw_ClassesPrepareFromReprs( pAig );
Ssw_ClassesSetData( p->ppClasses, p, NULL, Ssw_RarManObjIsConst, Ssw_RarManObjsAreEqual );
// print the stats
if ( fVerbose )
{
printf( "Initial : " );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// refine classes using BMC
for ( r = 0; r < nRounds; r++ )
{
// start filtering equivalence classes
if ( Ssw_ClassesCand1Num(p->ppClasses) == 0 && Ssw_ClassesClassNum(p->ppClasses) == 0 )
{
printf( "All equivalences are refined away.\n" );
break;
}
// simulate
for ( f = 0; f < nFrames; f++ )
{
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1 );
if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
{
if ( fVerbose ) printf( "\n" );
printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
RetValue = 0;
goto finish;
}
// check timeout
if ( TimeOut && ((float)TimeOut <= (float)(clock()-clkTotal)/(float)(CLOCKS_PER_SEC)) )
{
if ( fVerbose ) printf( "\n" );
printf( "Reached timeout (%d seconds).\n", TimeOut );
goto finish;
}
}
// printout
if ( fVerbose )
{
printf( "Round %3d: ", r );
Ssw_ClassesPrint( p->ppClasses, 0 );
}
// get initialization patterns
Ssw_RarTransferPatterns( p, p->vInits );
}
finish:
// report
if ( r == nRounds )
{
printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames );
Abc_PrintTime( 1, "Time", clock() - clkTotal );
}
// cleanup
Ssw_RarManStop( p );
return -1;
}
/**Function*************************************************************
Synopsis [Filter equivalence classes of nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose )
{
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_RarSignalFilter2( pAig, nFrames, nWords, nBinSize, nRounds, TimeOut, pCex, fLatchOnly, fVerbose );
Gia_ManReprFromAigRepr( pAig, p );
Aig_ManStop( pAig );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END