/**CFile****************************************************************
FileName [saigPhase.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Sequential AIG package.]
Synopsis [Automated phase abstraction.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: saigPhase.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "saig.h"
ABC_NAMESPACE_IMPL_START
/*
The algorithm is described in the paper: Per Bjesse and Jim Kukula,
"Automatic Phase Abstraction for Formal Verification", ICCAD 2005
http://www.iccad.com/data2/iccad/iccad_05acceptedpapers.nsf/9cfb1ebaaf59043587256a6a00031f78/1701ecf34b149e958725702f00708828?OpenDocument
*/
// the maximum number of cycles of termiry simulation
#define TSIM_MAX_ROUNDS 10000
#define TSIM_ONE_SERIES 3000
#define SAIG_XVS0 1
#define SAIG_XVS1 2
#define SAIG_XVSX 3
static inline int Saig_XsimConvertValue( int v ) { return v == 0? SAIG_XVS0 : (v == 1? SAIG_XVS1 : (v == 2? SAIG_XVSX : -1)); }
static inline void Saig_ObjSetXsim( Aig_Obj_t * pObj, int Value ) { pObj->nCuts = Value; }
static inline int Saig_ObjGetXsim( Aig_Obj_t * pObj ) { return pObj->nCuts; }
static inline int Saig_XsimInv( int Value )
{
if ( Value == SAIG_XVS0 )
return SAIG_XVS1;
if ( Value == SAIG_XVS1 )
return SAIG_XVS0;
assert( Value == SAIG_XVSX );
return SAIG_XVSX;
}
static inline int Saig_XsimAnd( int Value0, int Value1 )
{
if ( Value0 == SAIG_XVS0 || Value1 == SAIG_XVS0 )
return SAIG_XVS0;
if ( Value0 == SAIG_XVSX || Value1 == SAIG_XVSX )
return SAIG_XVSX;
assert( Value0 == SAIG_XVS1 && Value1 == SAIG_XVS1 );
return SAIG_XVS1;
}
static inline int Saig_XsimRand2()
{
return (Aig_ManRandom(0) & 1) ? SAIG_XVS1 : SAIG_XVS0;
}
static inline int Saig_XsimRand3()
{
int RetValue;
do {
RetValue = Aig_ManRandom(0) & 3;
} while ( RetValue == 0 );
return RetValue;
}
static inline int Saig_ObjGetXsimFanin0( Aig_Obj_t * pObj )
{
int RetValue;
RetValue = Saig_ObjGetXsim(Aig_ObjFanin0(pObj));
return Aig_ObjFaninC0(pObj)? Saig_XsimInv(RetValue) : RetValue;
}
static inline int Saig_ObjGetXsimFanin1( Aig_Obj_t * pObj )
{
int RetValue;
RetValue = Saig_ObjGetXsim(Aig_ObjFanin1(pObj));
return Aig_ObjFaninC1(pObj)? Saig_XsimInv(RetValue) : RetValue;
}
static inline void Saig_XsimPrint( FILE * pFile, int Value )
{
if ( Value == SAIG_XVS0 )
{
fprintf( pFile, "0" );
return;
}
if ( Value == SAIG_XVS1 )
{
fprintf( pFile, "1" );
return;
}
assert( Value == SAIG_XVSX );
fprintf( pFile, "x" );
}
// simulation manager
typedef struct Saig_Tsim_t_ Saig_Tsim_t;
struct Saig_Tsim_t_
{
Aig_Man_t * pAig; // the original AIG manager
int nWords; // the number of words in the states
// ternary state representation
Vec_Ptr_t * vStates; // the collection of ternary states
Aig_MmFixed_t * pMem; // memory for ternary states
int nPrefix; // prefix of the ternary state space
int nCycle; // cycle of the ternary state space
int nNonXRegs; // the number of candidate registers
Vec_Int_t * vNonXRegs; // the candidate registers
// hash table for terminary states
unsigned ** pBins;
int nBins;
};
static inline unsigned * Saig_TsiNext( unsigned * pState, int nWords ) { return *((unsigned **)(pState + nWords)); }
static inline void Saig_TsiSetNext( unsigned * pState, int nWords, unsigned * pNext ) { *((unsigned **)(pState + nWords)) = pNext; }
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Allocates simulation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Saig_Tsim_t * Saig_TsiStart( Aig_Man_t * pAig )
{
Saig_Tsim_t * p;
p = (Saig_Tsim_t *)ABC_ALLOC( char, sizeof(Saig_Tsim_t) );
memset( p, 0, sizeof(Saig_Tsim_t) );
p->pAig = pAig;
p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) );
p->vStates = Vec_PtrAlloc( 1000 );
p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 );
p->nBins = Aig_PrimeCudd(TSIM_MAX_ROUNDS/2);
p->pBins = ABC_ALLOC( unsigned *, p->nBins );
memset( p->pBins, 0, sizeof(unsigned *) * p->nBins );
return p;
}
/**Function*************************************************************
Synopsis [Deallocates simulation manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_TsiStop( Saig_Tsim_t * p )
{
if ( p->vNonXRegs )
Vec_IntFree( p->vNonXRegs );
Aig_MmFixedStop( p->pMem, 0 );
Vec_PtrFree( p->vStates );
ABC_FREE( p->pBins );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis [Computes hash value of the node using its simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
{
static int s_FPrimes[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 uHash;
int i;
uHash = 0;
for ( i = 0; i < nWords; i++ )
uHash ^= pState[i] * s_FPrimes[i & 0x7F];
return uHash % nTableSize;
}
/**Function*************************************************************
Synopsis [Count non-X-valued registers in the simulation data.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nPref )
{
unsigned * pState;
int nRegs = p->pAig->nRegs;
int Value, i, k;
assert( p->vNonXRegs == NULL );
p->vNonXRegs = Vec_IntAlloc( 10 );
for ( i = 0; i < nRegs; i++ )
{
Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, nPref )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
assert( Value != 0 );
if ( Value == SAIG_XVSX )
break;
}
if ( k == Vec_PtrSize(p->vStates) )
Vec_IntPush( p->vNonXRegs, i );
}
return Vec_IntSize(p->vNonXRegs);
}
/**Function*************************************************************
Synopsis [Computes flops that are stuck-at constant.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_TsiComputeTransient( Saig_Tsim_t * p, int nPref )
{
Vec_Int_t * vCounters;
unsigned * pState;
int ValueThis, ValuePrev = -1, StepPrev = -1;
int i, k, nRegs = p->pAig->nRegs;
vCounters = Vec_IntStart( nPref );
for ( i = 0; i < nRegs; i++ )
{
Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
{
ValueThis = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
//printf( "%s", (ValueThis == 1)? "0" : ((ValueThis == 2)? "1" : "x") );
assert( ValueThis != 0 );
if ( ValuePrev != ValueThis )
{
ValuePrev = ValueThis;
StepPrev = k;
}
}
//printf( "\n" );
if ( ValueThis == SAIG_XVSX )
continue;
if ( StepPrev >= nPref )
continue;
Vec_IntAddToEntry( vCounters, StepPrev, 1 );
}
Vec_IntForEachEntry( vCounters, ValueThis, i )
{
if ( ValueThis == 0 )
continue;
// printf( "%3d : %3d\n", i, ValueThis );
}
return vCounters;
}
/**Function*************************************************************
Synopsis [Count non-X-valued registers in the simulation data.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix, int nLoop )
{
unsigned * pState;
int nRegs = p->pAig->nRegs;
int Value, i, k, Counter = 0;
printf( "Ternary traces for each flop:\n" );
printf( " : " );
for ( i = 0; i < Vec_PtrSize(p->vStates) - nLoop - 1; i++ )
printf( "%d", i%10 );
printf( " " );
for ( i = 0; i < nLoop; i++ )
printf( "%d", i%10 );
printf( "\n" );
for ( i = 0; i < nRegs; i++ )
{
/*
Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
if ( Value == SAIG_XVSX )
break;
}
if ( k == Vec_PtrSize(p->vStates) )
Counter++;
else
continue;
*/
// print trace
// printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
printf( "%5d : ", Counter++ );
Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
if ( Value == SAIG_XVS0 )
printf( "0" );
else if ( Value == SAIG_XVS1 )
printf( "1" );
else if ( Value == SAIG_XVSX )
printf( "x" );
else
assert( 0 );
if ( k == nPrefix - 1 )
printf( " " );
}
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Returns the number of the state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_TsiComputePrefix( Saig_Tsim_t * p, unsigned * pState, int nWords )
{
unsigned * pEntry, * pPrev;
int Hash, i;
Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) )
if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
{
Vec_PtrForEachEntry( unsigned *, p->vStates, pPrev, i )
{
if ( pPrev == pEntry )
return i;
}
assert( 0 );
return -1;
}
return -1;
}
/**Function*************************************************************
Synopsis [Checks if the value exists in the table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_TsiStateLookup( Saig_Tsim_t * p, unsigned * pState, int nWords )
{
unsigned * pEntry;
int Hash;
Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
for ( pEntry = p->pBins[Hash]; pEntry; pEntry = Saig_TsiNext(pEntry, nWords) )
if ( !memcmp( pEntry, pState, sizeof(unsigned) * nWords ) )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis [Inserts value into the table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_TsiStateInsert( Saig_Tsim_t * p, unsigned * pState, int nWords )
{
int Hash = Saig_TsiStateHash( pState, nWords, p->nBins );
assert( !Saig_TsiStateLookup( p, pState, nWords ) );
Saig_TsiSetNext( pState, nWords, p->pBins[Hash] );
p->pBins[Hash] = pState;
}
/**Function*************************************************************
Synopsis [Inserts value into the table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Saig_TsiStateNew( Saig_Tsim_t * p )
{
unsigned * pState;
pState = (unsigned *)Aig_MmFixedEntryFetch( p->pMem );
memset( pState, 0, sizeof(unsigned) * p->nWords );
Vec_PtrPush( p->vStates, pState );
return pState;
}
/**Function*************************************************************
Synopsis [Inserts value into the table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_TsiStatePrint( Saig_Tsim_t * p, unsigned * pState )
{
int i, Value, nZeros = 0, nOnes = 0, nDcs = 0;
for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
if ( Value == SAIG_XVS0 )
printf( "0" ), nZeros++;
else if ( Value == SAIG_XVS1 )
printf( "1" ), nOnes++;
else if ( Value == SAIG_XVSX )
printf( "x" ), nDcs++;
else
assert( 0 );
}
printf( " (0=%5d, 1=%5d, x=%5d)\n", nZeros, nOnes, nDcs );
}
/**Function*************************************************************
Synopsis [Count constant values in the state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_TsiStateCount( Saig_Tsim_t * p, unsigned * pState )
{
Aig_Obj_t * pObjLi, * pObjLo;
int i, Value, nCounter = 0;
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
nCounter += (Value == SAIG_XVS0 || Value == SAIG_XVS1);
}
return nCounter;
}
/**Function*************************************************************
Synopsis [Count constant values in the state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_TsiStateOrAll( Saig_Tsim_t * pTsi, unsigned * pState )
{
unsigned * pPrev;
int i, k;
Vec_PtrForEachEntry( unsigned *, pTsi->vStates, pPrev, i )
{
for ( k = 0; k < pTsi->nWords; k++ )
pState[k] |= pPrev[k];
}
}
/**Function*************************************************************
Synopsis [Cycles the circuit to create a new initial state.]
Description [Simulates the circuit with random input for the given
number of timeframes to get a better initial state.]
SideEffects []
SeeAlso []
***********************************************************************/
Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int fVerbose )
{
Saig_Tsim_t * pTsi;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
unsigned * pState;
int i, f, Value, nCounter;
// allocate the simulation manager
pTsi = Saig_TsiStart( p );
// initialize the values
Saig_ObjSetXsim( Aig_ManConst1(p), SAIG_XVS1 );
Saig_ManForEachPi( p, pObj, i )
Saig_ObjSetXsim( pObj, SAIG_XVSX );
if ( vInits )
{
Saig_ManForEachLo( p, pObj, i )
Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) );
}
else
{
Saig_ManForEachLo( p, pObj, i )
Saig_ObjSetXsim( pObj, SAIG_XVS0 );
}
// simulate for the given number of timeframes
for ( f = 0; f < TSIM_MAX_ROUNDS; f++ )
{
// collect this state
pState = Saig_TsiStateNew( pTsi );
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
{
Value = Saig_ObjGetXsim(pObjLo);
if ( Value & 1 )
Aig_InfoSetBit( pState, 2 * i );
if ( Value & 2 )
Aig_InfoSetBit( pState, 2 * i + 1 );
}
// printf( "%d ", Saig_TsiStateCount(pTsi, pState) );
// Saig_TsiStatePrint( pTsi, pState );
// check if this state exists
if ( Saig_TsiStateLookup( pTsi, pState, pTsi->nWords ) )
{
if ( fVerbose )
printf( "Ternary simulation converged after %d iterations.\n", f );
return pTsi;
}
// insert this state
Saig_TsiStateInsert( pTsi, pState, pTsi->nWords );
// simulate internal nodes
Aig_ManForEachNode( p, pObj, i )
Saig_ObjSetXsim( pObj, Saig_XsimAnd(Saig_ObjGetXsimFanin0(pObj), Saig_ObjGetXsimFanin1(pObj)) );
// transfer the latch values
Saig_ManForEachLi( p, pObj, i )
Saig_ObjSetXsim( pObj, Saig_ObjGetXsimFanin0(pObj) );
nCounter = 0;
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
{
if ( f < TSIM_ONE_SERIES )
Saig_ObjSetXsim( pObjLo, Saig_ObjGetXsim(pObjLi) );
else
{
if ( Saig_ObjGetXsim(pObjLi) != Saig_ObjGetXsim(pObjLo) )
Saig_ObjSetXsim( pObjLo, SAIG_XVSX );
}
nCounter += (Saig_ObjGetXsim(pObjLo) == SAIG_XVS0);
}
}
printf( "Saig_ManReachableTernary(): Did not reach a fixed point after %d iterations (not a bug).\n", TSIM_MAX_ROUNDS );
Saig_TsiStop( pTsi );
return NULL;
}
/**Function*************************************************************
Synopsis [Analize initial value of the selected register.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg )
{
Aig_Obj_t * pObj, * pReg, * pCtrl, * pAnd;
int i;
pReg = Saig_ManLo( p, Reg );
pCtrl = Saig_ManLo( p, Saig_ManRegNum(p)-1 );
assert( pReg->Id < pCtrl->Id );
// find a node pointing to both
pAnd = NULL;
Aig_ManForEachNode( p, pObj, i )
{
if ( Aig_ObjFanin0(pObj) == pReg && Aig_ObjFanin1(pObj) == pCtrl )
{
pAnd = pObj;
break;
}
}
if ( pAnd == NULL )
{
printf( "Register is not found.\n" );
return;
}
printf( "Clock-like register: \n" );
Aig_ObjPrint( p, pReg );
printf( "\n" );
printf( "Control register: \n" );
Aig_ObjPrint( p, pCtrl );
printf( "\n" );
printf( "Their fanout: \n" );
Aig_ObjPrint( p, pAnd );
printf( "\n" );
// find the fanouts of pAnd
printf( "Fanouts of the fanout: \n" );
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjFanin0(pObj) == pAnd || Aig_ObjFanin1(pObj) == pAnd )
{
Aig_ObjPrint( p, pObj );
printf( "\n" );
}
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Finds the registers to phase-abstract.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose )
{
int Values[257] = {0};
unsigned * pState;
int r, i, k, Reg, Value;
int nTests = pTsi->nPrefix + 2 * pTsi->nCycle;
assert( nFrames <= 256 );
r = 0;
Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
{
for ( k = 0; k < nTests; k++ )
{
if ( k < pTsi->nPrefix + pTsi->nCycle )
pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, k );
else
pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, k - pTsi->nCycle );
Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg );
assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
if ( k < nFrames || (fIgnore && k == nFrames) )
Values[k % nFrames] = Value;
else if ( Values[k % nFrames] != Value )
break;
}
if ( k < nTests )
continue;
// skip stuck at
if ( fIgnore )
{
for ( k = 1; k < nFrames; k++ )
if ( Values[k] != Values[0] )
break;
if ( k == nFrames )
continue;
}
// report useful register
Vec_IntWriteEntry( pTsi->vNonXRegs, r++, Reg );
if ( fVerbose )
{
printf( "Register %5d has generator: [", Reg );
for ( k = 0; k < nFrames; k++ )
Saig_XsimPrint( stdout, Values[k] );
printf( "]\n" );
if ( fVerbose )
Saig_ManAnalizeControl( pTsi->pAig, Reg );
}
}
Vec_IntShrink( pTsi->vNonXRegs, r );
if ( fVerbose )
printf( "Found %3d useful registers.\n", Vec_IntSize(pTsi->vNonXRegs) );
return Vec_IntSize(pTsi->vNonXRegs);
}
/**Function*************************************************************
Synopsis [Mapping of AIG nodes into frames nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Aig_Obj_t * Saig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; }
static inline void Saig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
static inline Aig_Obj_t * Saig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Saig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Saig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
/**Function*************************************************************
Synopsis [Performs phase abstraction by unrolling the circuit.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVerbose )
{
Aig_Man_t * pFrames, * pAig = pTsi->pAig;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
Aig_Obj_t ** pObjMap;
unsigned * pState;
int i, f, Reg, Value;
assert( Vec_IntSize(pTsi->vNonXRegs) > 0 );
// create mapping for the frames nodes
pObjMap = ABC_ALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
memset( pObjMap, 0, sizeof(Aig_Obj_t *) * nFrames * Aig_ManObjNumMax(pAig) );
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
pFrames->pName = Aig_UtilStrsav( pAig->pName );
pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
// map constant nodes
for ( f = 0; f < nFrames; f++ )
Saig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
// create PI nodes for the frames
for ( f = 0; f < nFrames; f++ )
Aig_ManForEachPiSeq( pAig, pObj, i )
Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
// create the latches
Aig_ManForEachLoSeq( pAig, pObj, i )
Saig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
// add timeframes
for ( f = 0; f < nFrames; f++ )
{
// replace abstracted registers by constants
Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
{
pObj = Saig_ManLo( pAig, Reg );
pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, f );
Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg );
assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
pObjNew = (Value == SAIG_XVS1)? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames);
Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
}
// add internal nodes of this frame
Aig_ManForEachNode( pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Saig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
}
// set the latch inputs and copy them into the latch outputs of the next frame
Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
{
pObjNew = Saig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
if ( f < nFrames - 1 )
Saig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
}
}
for ( f = 0; f < nFrames; f++ )
{
Aig_ManForEachPoSeq( pAig, pObj, i )
{
pObjNew = Aig_ObjCreatePo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,f) );
Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
}
}
pFrames->nRegs = pAig->nRegs;
pFrames->nTruePis = Aig_ManPiNum(pFrames) - Aig_ManRegNum(pFrames);
pFrames->nTruePos = Aig_ManPoNum(pFrames) - Aig_ManRegNum(pFrames);
Aig_ManForEachLiSeq( pAig, pObj, i )
{
pObjNew = Aig_ObjCreatePo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,nFrames-1) );
Saig_ObjSetFrames( pObjMap, nFrames, pObj, nFrames-1, pObjNew );
}
//Aig_ManPrintStats( pFrames );
Aig_ManSeqCleanup( pFrames );
//Aig_ManPrintStats( pFrames );
// Aig_ManPiCleanup( pFrames );
//Aig_ManPrintStats( pFrames );
ABC_FREE( pObjMap );
return pFrames;
}
/**Function*************************************************************
Synopsis [Performs automated phase abstraction.]
Description [Takes the AIG manager and the array of initial states.]
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits )
{
Saig_Tsim_t * pTsi;
int nFrames, nPrefix;
assert( Saig_ManRegNum(p) );
assert( Saig_ManPiNum(p) );
assert( Saig_ManPoNum(p) );
// perform terminary simulation
pTsi = Saig_ManReachableTernary( p, vInits, 0 );
if ( pTsi == NULL )
return 1;
// derive information
nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
Saig_TsiStop( pTsi );
// potentially, may need to reduce nFrames if nPrefix is less than nFrames
return nFrames;
}
/**Function*************************************************************
Synopsis [Performs automated phase abstraction.]
Description [Takes the AIG manager and the array of initial states.]
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans )
{
Saig_Tsim_t * pTsi;
int nFrames, nPrefix, nNonXRegs;
assert( Saig_ManRegNum(p) );
assert( Saig_ManPiNum(p) );
assert( Saig_ManPoNum(p) );
// perform terminary simulation
pTsi = Saig_ManReachableTernary( p, NULL, 0 );
if ( pTsi == NULL )
return 0;
// derive information
nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, nPrefix );
if ( pvTrans )
*pvTrans = Saig_TsiComputeTransient( pTsi, nPrefix );
// print statistics
if ( fVerbose )
printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs );
if ( fVeryVerbose )
Saig_TsiPrintTraces( pTsi, pTsi->nWords, nPrefix, nFrames );
Saig_TsiStop( pTsi );
// potentially, may need to reduce nFrames if nPrefix is less than nFrames
return nPrefix;
}
/**Function*************************************************************
Synopsis [Performs automated phase abstraction.]
Description [Takes the AIG manager and the array of initial states.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose )
{
Aig_Man_t * pNew = NULL;
Saig_Tsim_t * pTsi;
assert( Saig_ManRegNum(p) );
assert( Saig_ManPiNum(p) );
assert( Saig_ManPoNum(p) );
// perform terminary simulation
pTsi = Saig_ManReachableTernary( p, vInits, fVerbose );
if ( pTsi == NULL )
return NULL;
// derive information
pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, ABC_MIN(pTsi->nPrefix,nPref));
// print statistics
if ( fVerbose )
{
printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
}
if ( fPrint )
printf( "Print-out finished. Phase assignment is not performed.\n" );
else if ( nFrames < 2 )
printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
else if ( nFrames > 256 )
printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
else if ( pTsi->nCycle == 1 )
printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
else if ( pTsi->nCycle % nFrames != 0 )
printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
else if ( pTsi->nNonXRegs == 0 )
printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
else if ( !Saig_ManFindRegisters( pTsi, nFrames, fIgnore, fVerbose ) )
printf( "There is no registers to abstract with %d frames.\n", nFrames );
else
pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
Saig_TsiStop( pTsi );
return pNew;
}
/**Function*************************************************************
Synopsis [Performs automated phase abstraction.]
Description [Takes the AIG manager and the array of initial states.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
{
Aig_Man_t * pNew = NULL;
Saig_Tsim_t * pTsi;
int fPrint = 0;
int nFrames;
assert( Saig_ManRegNum(p) );
assert( Saig_ManPiNum(p) );
assert( Saig_ManPoNum(p) );
// perform terminary simulation
pTsi = Saig_ManReachableTernary( p, NULL, fVerbose );
if ( pTsi == NULL )
return NULL;
// derive information
pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, 0);
// print statistics
if ( fVerbose )
{
printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
}
nFrames = pTsi->nCycle;
if ( fPrint )
{
printf( "Print-out finished. Phase assignment is not performed.\n" );
}
else if ( nFrames < 2 )
{
// printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
}
else if ( nFrames > 256 )
{
// printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
}
else if ( pTsi->nCycle == 1 )
{
// printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
}
else if ( pTsi->nCycle % nFrames != 0 )
{
// printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
}
else if ( pTsi->nNonXRegs == 0 )
{
// printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
}
else if ( !Saig_ManFindRegisters( pTsi, nFrames, 0, fVerbose ) )
{
// printf( "There is no registers to abstract with %d frames.\n", nFrames );
}
else
pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
Saig_TsiStop( pTsi );
if ( pNew == NULL )
pNew = Aig_ManDupSimple( p );
if ( Aig_ManPiNum(pNew) == Aig_ManRegNum(pNew) )
{
Aig_ManStop( pNew);
pNew = Aig_ManDupSimple( p );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Derives CEX for the original AIG from CEX of the unrolled AIG.]
Description [The number of PIs of the given CEX should divide by the number
of PIs of the original AIG without a remainder.]
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Cex_t * Saig_PhaseTranslateCex( Aig_Man_t * p, Abc_Cex_t * pCex )
{
Abc_Cex_t * pNew;
int i, k, iFrame, nFrames;
// make sure the PI count of the AIG is a multiple of the PI count of the CEX
// if this is not true, the CEX is not derived as the result of unrolling of pAig
// or the unrolled CEX went through transformations that change the PI count
if ( pCex->nPis % Saig_ManPiNum(p) != 0 )
{
printf( "The PI count in the AIG and in the CEX do not match.\n" );
return NULL;
}
// get the number of unrolled frames
nFrames = pCex->nPis / Saig_ManPiNum(p);
// get the frame where it fails
iFrame = pCex->iFrame * nFrames + pCex->iPo / Saig_ManPoNum(p);
// start a new CEX (assigns: p->nRegs, p->nPis, p->nBits)
pNew = Abc_CexAlloc( Saig_ManRegNum(p), Saig_ManPiNum(p), iFrame+1 );
assert( pNew->nBits == pNew->nPis * (iFrame + 1) + pNew->nRegs );
// now assign the failed frame and the failed PO (p->iFrame and p->iPo)
pNew->iFrame = iFrame;
pNew->iPo = pCex->iPo % Saig_ManPoNum(p);
// copy the bit data
for ( i = pCex->nRegs, k = pNew->nRegs; k < pNew->nBits; k++, i++ )
if ( Aig_InfoHasBit( pCex->pData, i ) )
Aig_InfoSetBit( pNew->pData, k );
assert( i <= pCex->nBits );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END