mirror of https://github.com/YosysHQ/abc.git
New code since Dec 2010.
This commit is contained in:
Alan Mishchenko
parent
ab80b015a4
commit
624af674a0
|
|
@ -0,0 +1,705 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [giaSim.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Scalable AIG package.]
|
||||
|
||||
Synopsis [Fast sequential simulator.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "gia.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct Gia_Sim2_t_ Gia_Sim2_t;
|
||||
struct Gia_Sim2_t_
|
||||
{
|
||||
Gia_Man_t * pAig;
|
||||
Gia_ParSim_t * pPars;
|
||||
int nWords;
|
||||
unsigned * pDataSim;
|
||||
Vec_Int_t * vClassOld;
|
||||
Vec_Int_t * vClassNew;
|
||||
};
|
||||
|
||||
static inline unsigned * Gia_Sim2Data( Gia_Sim2_t * p, int i ) { return p->pDataSim + i * p->nWords; }
|
||||
|
||||
extern void Gia_ManResetRandom( Gia_ParSim_t * pPars );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_Sim2Delete( Gia_Sim2_t * p )
|
||||
{
|
||||
Vec_IntFreeP( &p->vClassOld );
|
||||
Vec_IntFreeP( &p->vClassNew );
|
||||
ABC_FREE( p->pDataSim );
|
||||
ABC_FREE( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates fast simulation manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Gia_Sim2_t * Gia_Sim2Create( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
|
||||
{
|
||||
Gia_Sim2_t * p;
|
||||
Gia_Obj_t * pObj;
|
||||
int i;
|
||||
p = ABC_CALLOC( Gia_Sim2_t, 1 );
|
||||
p->pAig = pAig;
|
||||
p->pPars = pPars;
|
||||
p->nWords = pPars->nWords;
|
||||
p->pDataSim = ABC_ALLOC( unsigned, p->nWords * Gia_ManObjNum(p->pAig) );
|
||||
if ( !p->pDataSim )
|
||||
{
|
||||
Abc_Print( 1, "Simulator could not allocate %.2f Gb for simulation info.\n",
|
||||
4.0 * p->nWords * Gia_ManObjNum(p->pAig) / (1<<30) );
|
||||
Gia_Sim2Delete( p );
|
||||
return NULL;
|
||||
}
|
||||
p->vClassOld = Vec_IntAlloc( 100 );
|
||||
p->vClassNew = Vec_IntAlloc( 100 );
|
||||
if ( pPars->fVerbose )
|
||||
Abc_Print( 1, "Memory: AIG = %7.2f Mb. SimInfo = %7.2f Mb.\n",
|
||||
12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*Gia_ManObjNum(p->pAig)/(1<<20) );
|
||||
// prepare AIG
|
||||
Gia_ManSetPhase( pAig );
|
||||
Gia_ManForEachObj( pAig, pObj, i )
|
||||
pObj->Value = i;
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_Sim2InfoRandom( Gia_Sim2_t * p, unsigned * pInfo )
|
||||
{
|
||||
int w;
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = Gia_ManRandom( 0 );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_Sim2InfoZero( Gia_Sim2_t * p, unsigned * pInfo )
|
||||
{
|
||||
int w;
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = 0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_Sim2InfoOne( Gia_Sim2_t * p, unsigned * pInfo )
|
||||
{
|
||||
int w;
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = ~0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_Sim2InfoCopy( Gia_Sim2_t * p, unsigned * pInfo, unsigned * pInfo0 )
|
||||
{
|
||||
int w;
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = pInfo0[w];
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_Sim2SimulateCo( Gia_Sim2_t * p, Gia_Obj_t * pObj )
|
||||
{
|
||||
unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
|
||||
unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
|
||||
int w;
|
||||
if ( Gia_ObjFaninC0(pObj) )
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = ~pInfo0[w];
|
||||
else
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = pInfo0[w];
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_Sim2SimulateNode( Gia_Sim2_t * p, Gia_Obj_t * pObj )
|
||||
{
|
||||
unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
|
||||
unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
|
||||
unsigned * pInfo1 = Gia_Sim2Data( p, Gia_ObjFaninId1(pObj, Gia_ObjValue(pObj)) );
|
||||
int w;
|
||||
if ( Gia_ObjFaninC0(pObj) )
|
||||
{
|
||||
if ( Gia_ObjFaninC1(pObj) )
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
|
||||
else
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = ~pInfo0[w] & pInfo1[w];
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( Gia_ObjFaninC1(pObj) )
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = pInfo0[w] & ~pInfo1[w];
|
||||
else
|
||||
for ( w = p->nWords-1; w >= 0; w-- )
|
||||
pInfo[w] = pInfo0[w] & pInfo1[w];
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_Sim2InfoTransfer( Gia_Sim2_t * p )
|
||||
{
|
||||
Gia_Obj_t * pObjRo, * pObjRi;
|
||||
unsigned * pInfo0, * pInfo1;
|
||||
int i;
|
||||
Gia_ManForEachRiRo( p->pAig, pObjRi, pObjRo, i )
|
||||
{
|
||||
pInfo0 = Gia_Sim2Data( p, Gia_ObjValue(pObjRo) );
|
||||
pInfo1 = Gia_Sim2Data( p, Gia_ObjValue(pObjRi) );
|
||||
Gia_Sim2InfoCopy( p, pInfo0, pInfo1 );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Gia_Sim2SimulateRound( Gia_Sim2_t * p )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i;
|
||||
pObj = Gia_ManConst0(p->pAig);
|
||||
assert( Gia_ObjValue(pObj) == 0 );
|
||||
Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
|
||||
Gia_ManForEachPi( p->pAig, pObj, i )
|
||||
Gia_Sim2InfoRandom( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
|
||||
Gia_ManForEachAnd( p->pAig, pObj, i )
|
||||
{
|
||||
assert( Gia_ObjValue(pObj) == i );
|
||||
Gia_Sim2SimulateNode( p, pObj );
|
||||
}
|
||||
Gia_ManForEachCo( p->pAig, pObj, i )
|
||||
Gia_Sim2SimulateCo( p, pObj );
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Compares simulation info of two nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_Sim2CompareEqual( unsigned * p0, unsigned * p1, int nWords, int fCompl )
|
||||
{
|
||||
int w;
|
||||
if ( !fCompl )
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
if ( p0[w] != p1[w] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
if ( p0[w] != ~p1[w] )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Compares simulation info of one node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_Sim2CompareZero( unsigned * p0, int nWords, int fCompl )
|
||||
{
|
||||
int w;
|
||||
if ( !fCompl )
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
if ( p0[w] != 0 )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
else
|
||||
{
|
||||
for ( w = 0; w < nWords; w++ )
|
||||
if ( p0[w] != ~0 )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates equivalence class.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_Sim2ClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
|
||||
{
|
||||
int Repr = GIA_VOID, EntPrev = -1, Ent, i;
|
||||
assert( Vec_IntSize(vClass) > 0 );
|
||||
Vec_IntForEachEntry( vClass, Ent, i )
|
||||
{
|
||||
if ( i == 0 )
|
||||
{
|
||||
Repr = Ent;
|
||||
Gia_ObjSetRepr( p, Ent, GIA_VOID );
|
||||
EntPrev = Ent;
|
||||
}
|
||||
else
|
||||
{
|
||||
assert( Repr < Ent );
|
||||
Gia_ObjSetRepr( p, Ent, Repr );
|
||||
Gia_ObjSetNext( p, EntPrev, Ent );
|
||||
EntPrev = Ent;
|
||||
}
|
||||
}
|
||||
Gia_ObjSetNext( p, EntPrev, 0 );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Refines one equivalence class.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_Sim2ClassRefineOne( Gia_Sim2_t * p, int i )
|
||||
{
|
||||
Gia_Obj_t * pObj0, * pObj1;
|
||||
unsigned * pSim0, * pSim1;
|
||||
int Ent;
|
||||
Vec_IntClear( p->vClassOld );
|
||||
Vec_IntClear( p->vClassNew );
|
||||
Vec_IntPush( p->vClassOld, i );
|
||||
pObj0 = Gia_ManObj( p->pAig, i );
|
||||
pSim0 = Gia_Sim2Data( p, i );
|
||||
Gia_ClassForEachObj1( p->pAig, i, Ent )
|
||||
{
|
||||
pObj1 = Gia_ManObj( p->pAig, Ent );
|
||||
pSim1 = Gia_Sim2Data( p, Ent );
|
||||
if ( Gia_Sim2CompareEqual( pSim0, pSim1, p->nWords, Gia_ObjPhase(pObj0) ^ Gia_ObjPhase(pObj1) ) )
|
||||
Vec_IntPush( p->vClassOld, Ent );
|
||||
else
|
||||
Vec_IntPush( p->vClassNew, Ent );
|
||||
}
|
||||
if ( Vec_IntSize( p->vClassNew ) == 0 )
|
||||
return 0;
|
||||
Gia_Sim2ClassCreate( p->pAig, p->vClassOld );
|
||||
Gia_Sim2ClassCreate( p->pAig, p->vClassNew );
|
||||
if ( Vec_IntSize(p->vClassNew) > 1 )
|
||||
return 1 + Gia_Sim2ClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes hash key of the simuation info.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_Sim2HashKey( unsigned * pSim, int nWords, int nTableSize )
|
||||
{
|
||||
static int s_Primes[16] = {
|
||||
1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
|
||||
4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
|
||||
unsigned uHash = 0;
|
||||
int i;
|
||||
if ( pSim[0] & 1 )
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
uHash ^= ~pSim[i] * s_Primes[i & 0xf];
|
||||
else
|
||||
for ( i = 0; i < nWords; i++ )
|
||||
uHash ^= pSim[i] * s_Primes[i & 0xf];
|
||||
return (int)(uHash % nTableSize);
|
||||
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Refines nodes belonging to candidate constant class.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_Sim2ProcessRefined( Gia_Sim2_t * p, Vec_Int_t * vRefined )
|
||||
{
|
||||
unsigned * pSim;
|
||||
int * pTable, nTableSize, i, k, Key;
|
||||
if ( Vec_IntSize(vRefined) == 0 )
|
||||
return;
|
||||
nTableSize = Gia_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
|
||||
pTable = ABC_CALLOC( int, nTableSize );
|
||||
Vec_IntForEachEntry( vRefined, i, k )
|
||||
{
|
||||
pSim = Gia_Sim2Data( p, i );
|
||||
Key = Gia_Sim2HashKey( pSim, p->nWords, nTableSize );
|
||||
if ( pTable[Key] == 0 )
|
||||
{
|
||||
assert( Gia_ObjRepr(p->pAig, i) == 0 );
|
||||
assert( Gia_ObjNext(p->pAig, i) == 0 );
|
||||
Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
|
||||
}
|
||||
else
|
||||
{
|
||||
Gia_ObjSetNext( p->pAig, pTable[Key], i );
|
||||
Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
|
||||
if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
|
||||
Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
|
||||
assert( Gia_ObjRepr(p->pAig, i) > 0 );
|
||||
}
|
||||
pTable[Key] = i;
|
||||
}
|
||||
/*
|
||||
Vec_IntForEachEntry( vRefined, i, k )
|
||||
{
|
||||
if ( Gia_ObjIsHead( p->pAig, i ) )
|
||||
Gia_Sim2ClassRefineOne( p, i );
|
||||
}
|
||||
*/
|
||||
ABC_FREE( pTable );
|
||||
}
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Refines equivalences after one simulation round.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Gia_Sim2InfoRefineEquivs( Gia_Sim2_t * p )
|
||||
{
|
||||
Vec_Int_t * vRefined;
|
||||
Gia_Obj_t * pObj;
|
||||
unsigned * pSim;
|
||||
int i, Count = 0;
|
||||
// process constant candidates
|
||||
vRefined = Vec_IntAlloc( 100 );
|
||||
Gia_ManForEachObj1( p->pAig, pObj, i )
|
||||
{
|
||||
if ( !Gia_ObjIsConst(p->pAig, i) )
|
||||
continue;
|
||||
pSim = Gia_Sim2Data( p, i );
|
||||
//Extra_PrintBinary( stdout, pSim, 32 * p->nWords ); printf( "\n" );
|
||||
if ( !Gia_Sim2CompareZero( pSim, p->nWords, Gia_ObjPhase(pObj) ) )
|
||||
{
|
||||
Vec_IntPush( vRefined, i );
|
||||
Count++;
|
||||
}
|
||||
}
|
||||
Gia_Sim2ProcessRefined( p, vRefined );
|
||||
Vec_IntFree( vRefined );
|
||||
// process other classes
|
||||
Gia_ManForEachClass( p->pAig, i )
|
||||
Count += Gia_Sim2ClassRefineOne( p, i );
|
||||
// if ( Count )
|
||||
// printf( "Refined %d times.\n", Count );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns index of the first pattern that failed.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Gia_Sim2InfoIsZero( Gia_Sim2_t * p, unsigned * pInfo )
|
||||
{
|
||||
int w;
|
||||
for ( w = 0; w < p->nWords; w++ )
|
||||
if ( pInfo[w] )
|
||||
return 32*w + Gia_WordFindFirstBit( pInfo[w] );
|
||||
return -1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns index of the PO and pattern that failed it.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Gia_Sim2CheckPos( Gia_Sim2_t * p, int * piPo, int * piPat )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int i, iPat;
|
||||
Gia_ManForEachPo( p->pAig, pObj, i )
|
||||
{
|
||||
iPat = Gia_Sim2InfoIsZero( p, Gia_Sim2Data( p, Gia_ObjValue(pObj) ) );
|
||||
if ( iPat >= 0 )
|
||||
{
|
||||
*piPo = i;
|
||||
*piPat = iPat;
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns the counter-example.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int nWords, int iPat )
|
||||
{
|
||||
Abc_Cex_t * p;
|
||||
unsigned * pData;
|
||||
int f, i, w, Counter;
|
||||
p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
|
||||
p->iFrame = iFrame;
|
||||
p->iPo = iOut;
|
||||
// fill in the binary data
|
||||
Counter = p->nRegs;
|
||||
pData = ABC_ALLOC( unsigned, nWords );
|
||||
for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
|
||||
for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
|
||||
{
|
||||
for ( w = nWords-1; w >= 0; w-- )
|
||||
pData[w] = Gia_ManRandom( 0 );
|
||||
if ( Gia_InfoHasBit( pData, iPat ) )
|
||||
Gia_InfoSetBit( p->pData, Counter + i );
|
||||
}
|
||||
ABC_FREE( pData );
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs simulation to refine equivalence classes.]
|
||||
|
||||
Description [Returns 1 if counter-example is detected.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
|
||||
{
|
||||
Gia_Sim2_t * p;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, clkTotal = clock();
|
||||
int RetValue = 0, iOut, iPat;
|
||||
assert( pAig->pReprs && pAig->pNexts );
|
||||
ABC_FREE( pAig->pCexSeq );
|
||||
p = Gia_Sim2Create( pAig, pPars );
|
||||
Gia_ManResetRandom( pPars );
|
||||
Gia_ManForEachRo( p->pAig, pObj, i )
|
||||
Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
|
||||
for ( i = 0; i < pPars->nIters; i++ )
|
||||
{
|
||||
Gia_Sim2SimulateRound( p );
|
||||
if ( pPars->fVerbose )
|
||||
{
|
||||
Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
|
||||
if ( pAig->pReprs && pAig->pNexts )
|
||||
Abc_Print( 1, "Lits = %4d. ", Gia_ManEquivCountLitsAll(pAig) );
|
||||
Abc_Print( 1, "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
|
||||
}
|
||||
if ( pPars->fCheckMiter && Gia_Sim2CheckPos( p, &iOut, &iPat ) )
|
||||
{
|
||||
Gia_ManResetRandom( pPars );
|
||||
pPars->iOutFail = iOut;
|
||||
pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
|
||||
Abc_Print( 1, "Networks are NOT EQUIVALENT. Output %d was asserted in frame %d. ", iOut, i );
|
||||
if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
|
||||
{
|
||||
// Abc_Print( 1, "\n" );
|
||||
Abc_Print( 1, "\nGenerated counter-example is INVALID. " );
|
||||
// Abc_Print( 1, "\n" );
|
||||
}
|
||||
else
|
||||
{
|
||||
// Abc_Print( 1, "\n" );
|
||||
// if ( pPars->fVerbose )
|
||||
// Abc_Print( 1, "\nGenerated counter-example is verified correctly. " );
|
||||
// Abc_Print( 1, "\n" );
|
||||
}
|
||||
RetValue = 1;
|
||||
break;
|
||||
}
|
||||
if ( pAig->pReprs && pAig->pNexts )
|
||||
Gia_Sim2InfoRefineEquivs( p );
|
||||
if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
|
||||
{
|
||||
i++;
|
||||
break;
|
||||
}
|
||||
if ( i < pPars->nIters - 1 )
|
||||
Gia_Sim2InfoTransfer( p );
|
||||
}
|
||||
Gia_Sim2Delete( p );
|
||||
if ( pAig->pCexSeq == NULL )
|
||||
Abc_Print( 1, "No bug detected after simulating %d frames with %d words. ", i, pPars->nWords );
|
||||
Abc_PrintTime( 1, "Time", clock() - clkTotal );
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,199 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [saigTempor.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Sequential AIG package.]
|
||||
|
||||
Synopsis [Temporal decomposition.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - June 20, 2005.]
|
||||
|
||||
Revision [$Id: saigTempor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "saig.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates initialized timeframes for temporal decomposition.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames )
|
||||
{
|
||||
Aig_Man_t * pFrames;
|
||||
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
|
||||
int i, f;
|
||||
// start the frames package
|
||||
Aig_ManCleanData( pAig );
|
||||
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
|
||||
pFrames->pName = Aig_UtilStrsav( pAig->pName );
|
||||
// initiliaze the flops
|
||||
Saig_ManForEachLo( pAig, pObj, i )
|
||||
pObj->pData = Aig_ManConst0(pFrames);
|
||||
// for each timeframe
|
||||
for ( f = 0; f < nFrames; f++ )
|
||||
{
|
||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
|
||||
Saig_ManForEachPi( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi(pFrames);
|
||||
Aig_ManForEachNode( pAig, pObj, i )
|
||||
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
Aig_ManForEachPo( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjChild0Copy(pObj);
|
||||
Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
|
||||
pObjLo->pData = pObjLi->pData;
|
||||
}
|
||||
// create POs for the flop inputs
|
||||
Saig_ManForEachLi( pAig, pObj, i )
|
||||
Aig_ObjCreatePo( pFrames, pObj->pData );
|
||||
Aig_ManCleanup( pFrames );
|
||||
return pFrames;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
|
||||
{
|
||||
Aig_Man_t * pAigNew, * pFrames;
|
||||
Aig_Obj_t * pObj, * pReset;
|
||||
int i;
|
||||
if ( pAig->nConstrs > 0 )
|
||||
{
|
||||
printf( "The AIG manager should have no constraints.\n" );
|
||||
return NULL;
|
||||
}
|
||||
// create initialized timeframes
|
||||
pFrames = Saig_ManTemporFrames( pAig, nFrames );
|
||||
assert( Aig_ManPoNum(pFrames) == Aig_ManRegNum(pAig) );
|
||||
|
||||
// start the new manager
|
||||
Aig_ManCleanData( pAig );
|
||||
pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
|
||||
pAigNew->pName = Aig_UtilStrsav( pAig->pName );
|
||||
// map the constant node and primary inputs
|
||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
|
||||
Saig_ManForEachPi( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pAigNew );
|
||||
|
||||
// insert initialization logic
|
||||
Aig_ManConst1(pFrames)->pData = Aig_ManConst1( pAigNew );
|
||||
Aig_ManForEachPi( pFrames, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi( pAigNew );
|
||||
Aig_ManForEachNode( pFrames, pObj, i )
|
||||
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
Aig_ManForEachPo( pFrames, pObj, i )
|
||||
pObj->pData = Aig_ObjChild0Copy(pObj);
|
||||
|
||||
// create reset latch (the first one among the latches)
|
||||
pReset = Aig_ObjCreatePi( pAigNew );
|
||||
|
||||
// create flop output values
|
||||
Saig_ManForEachLo( pAig, pObj, i )
|
||||
pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreatePi(pAigNew), Aig_ManPo(pFrames, i)->pData );
|
||||
Aig_ManStop( pFrames );
|
||||
|
||||
// add internal nodes of this frame
|
||||
Aig_ManForEachNode( pAig, pObj, i )
|
||||
pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
// create primary outputs
|
||||
Saig_ManForEachPo( pAig, pObj, i )
|
||||
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
|
||||
|
||||
// create reset latch (the first one among the latches)
|
||||
Aig_ObjCreatePo( pAigNew, Aig_ManConst1(pAigNew) );
|
||||
// create latch inputs
|
||||
Saig_ManForEachLi( pAig, pObj, i )
|
||||
Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
|
||||
|
||||
// finalize
|
||||
Aig_ManCleanup( pAigNew );
|
||||
Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); // + reset latch (011111...)
|
||||
return pAigNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose )
|
||||
{
|
||||
extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose );
|
||||
int RetValue, nFramesFinished = -1;
|
||||
assert( nFrames >= 0 );
|
||||
if ( nFrames == 0 )
|
||||
{
|
||||
nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose );
|
||||
if ( nFrames == 1 )
|
||||
{
|
||||
printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" );
|
||||
return NULL;
|
||||
}
|
||||
Abc_Print( 1, "Using computed frame number (%d).\n", nFrames );
|
||||
}
|
||||
else
|
||||
Abc_Print( 1, "Using user-given frame number (%d).\n", nFrames );
|
||||
// run BMC2
|
||||
if ( fUseBmc )
|
||||
{
|
||||
RetValue = Saig_BmcPerform( pAig, 0, nFrames, 5000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
|
||||
if ( RetValue == 0 )
|
||||
{
|
||||
printf( "A cex found in the first %d frames.\n", nFrames );
|
||||
return NULL;
|
||||
}
|
||||
if ( nFramesFinished < nFrames )
|
||||
{
|
||||
printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
|
||||
return NULL;
|
||||
}
|
||||
}
|
||||
return Saig_ManTemporDecompose( pAig, nFrames );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
SRC += src/sat/pdr/pdr.c \
|
||||
src/sat/pdr/pdrCnf.c \
|
||||
src/sat/pdr/pdrCore.c \
|
||||
src/sat/pdr/pdrInv.c \
|
||||
src/sat/pdr/pdrMan.c \
|
||||
src/sat/pdr/pdrSat.c \
|
||||
src/sat/pdr/pdrTsim.c \
|
||||
src/sat/pdr/pdrUtil.c
|
||||
|
|
@ -0,0 +1,53 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdr.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis []
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,77 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdr.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [External declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdr.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __PDR_H__
|
||||
#define __PDR_H__
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct Pdr_Par_t_ Pdr_Par_t;
|
||||
struct Pdr_Par_t_
|
||||
{
|
||||
int iOutput; // zero-based number of primary output to solve
|
||||
int nRecycle; // limit on vars for recycling
|
||||
int nFrameMax; // limit on frame count
|
||||
int nConfLimit; // limit on SAT solver conflicts
|
||||
int nTimeOut; // timeout in seconds
|
||||
int fTwoRounds; // use two rounds for generalization
|
||||
int fMonoCnf; // monolythic CNF
|
||||
int fDumpInv; // dump inductive invariant
|
||||
int fShortest; // forces bug traces to be shortest
|
||||
int fVerbose; // verbose output
|
||||
int fVeryVerbose; // very verbose output
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== pdrCore.c ==========================================================*/
|
||||
extern void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
|
||||
extern int Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
|
||||
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,223 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrClass.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [Equivalence classes of register outputs.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrClass.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs duplication with the variable map.]
|
||||
|
||||
Description [Var map contains -1 if const0 and <reg_num> otherwise.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap )
|
||||
{
|
||||
Aig_Man_t * pFrames;
|
||||
Aig_Obj_t * pObj;
|
||||
int i, iReg;
|
||||
assert( Vec_IntSize(vMap) == Aig_ManRegNum(pAig) );
|
||||
// start the fraig package
|
||||
pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) );
|
||||
pFrames->pName = Aig_UtilStrsav( pAig->pName );
|
||||
pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
|
||||
// create CI mapping
|
||||
Aig_ManCleanData( pAig );
|
||||
Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
|
||||
Aig_ManForEachPi( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePi(pFrames);
|
||||
Saig_ManForEachLo( pAig, pObj, i )
|
||||
{
|
||||
iReg = Vec_IntEntry(vMap, i);
|
||||
if ( iReg == -1 )
|
||||
pObj->pData = Aig_ManConst0(pFrames);
|
||||
else
|
||||
pObj->pData = Saig_ManLo(pAig, iReg)->pData;
|
||||
}
|
||||
// add internal nodes of this frame
|
||||
Aig_ManForEachNode( pAig, pObj, i )
|
||||
pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
|
||||
// add output nodes
|
||||
Aig_ManForEachPo( pAig, pObj, i )
|
||||
pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
|
||||
// finish off
|
||||
Aig_ManCleanup( pFrames );
|
||||
Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) );
|
||||
return pFrames;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates mapping of registers.]
|
||||
|
||||
Description [Var map contains -1 if const0 and <reg_num> otherwise.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Pdr_ManCreateMap( Aig_Man_t * p )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
Vec_Int_t * vMap;
|
||||
int * pLit2Id, Lit, i;
|
||||
pLit2Id = ABC_ALLOC( int, Aig_ManObjNumMax(p) * 2 );
|
||||
for ( i = 0; i < Aig_ManObjNumMax(p) * 2; i++ )
|
||||
pLit2Id[i] = -1;
|
||||
vMap = Vec_IntAlloc( Aig_ManRegNum(p) );
|
||||
Saig_ManForEachLi( p, pObj, i )
|
||||
{
|
||||
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p) )
|
||||
{
|
||||
Vec_IntPush( vMap, -1 );
|
||||
continue;
|
||||
}
|
||||
Lit = 2 * Aig_ObjFaninId0(pObj) + Aig_ObjFaninC0(pObj);
|
||||
if ( pLit2Id[Lit] < 0 ) // the first time
|
||||
pLit2Id[Lit] = i;
|
||||
Vec_IntPush( vMap, pLit2Id[Lit] );
|
||||
}
|
||||
ABC_FREE( pLit2Id );
|
||||
return vMap;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Counts reduced registers.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManCountMap( Vec_Int_t * vMap )
|
||||
{
|
||||
int i, Entry, Counter = 0;
|
||||
Vec_IntForEachEntry( vMap, Entry, i )
|
||||
if ( Entry != i )
|
||||
Counter++;
|
||||
return Counter;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Counts reduced registers.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManPrintMap( Vec_Int_t * vMap )
|
||||
{
|
||||
Vec_Int_t * vMarks;
|
||||
int f, i, iClass, Entry, Counter = 0;
|
||||
printf( " Consts: " );
|
||||
Vec_IntForEachEntry( vMap, Entry, i )
|
||||
if ( Entry == -1 )
|
||||
printf( "%d ", i );
|
||||
printf( "\n" );
|
||||
vMarks = Vec_IntAlloc( 100 );
|
||||
Vec_IntForEachEntry( vMap, iClass, f )
|
||||
{
|
||||
if ( iClass == -1 )
|
||||
continue;
|
||||
if ( iClass == f )
|
||||
continue;
|
||||
// check previous classes
|
||||
if ( Vec_IntFind( vMarks, iClass ) >= 0 )
|
||||
continue;
|
||||
Vec_IntPush( vMarks, iClass );
|
||||
// print class
|
||||
printf( " Class %d : ", iClass );
|
||||
Vec_IntForEachEntry( vMap, Entry, i )
|
||||
if ( Entry == iClass )
|
||||
printf( "%d ", i );
|
||||
printf( "\n" );
|
||||
}
|
||||
Vec_IntFree( vMarks );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManEquivClasses( Aig_Man_t * pAig )
|
||||
{
|
||||
Vec_Int_t * vMap;
|
||||
Aig_Man_t * pTemp;
|
||||
int f, nFrames = 100;
|
||||
assert( Saig_ManRegNum(pAig) > 0 );
|
||||
// start the map
|
||||
vMap = Vec_IntAlloc( 0 );
|
||||
Vec_IntFill( vMap, Aig_ManRegNum(pAig), -1 );
|
||||
// iterate and print changes
|
||||
for ( f = 0; f < nFrames; f++ )
|
||||
{
|
||||
// implement variable map
|
||||
pTemp = Pdr_ManRehashWithMap( pAig, vMap );
|
||||
// report the result
|
||||
printf( "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n",
|
||||
f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap),
|
||||
Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" );
|
||||
// recreate the map
|
||||
Pdr_ManPrintMap( vMap );
|
||||
Vec_IntFree( vMap );
|
||||
vMap = Pdr_ManCreateMap( pTemp );
|
||||
Aig_ManStop( pTemp );
|
||||
if ( Pdr_ManCountMap(vMap) == 0 )
|
||||
break;
|
||||
}
|
||||
Vec_IntFree( vMap );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,354 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrCnf.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [CNF computation on demand.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrCnf.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*
|
||||
The CNF (p->pCnf2) is expressed in terms of object IDs.
|
||||
Each node in the CNF is marked if it has clauses (p->pCnf2->pObj2Count[Id] > 0).
|
||||
Each node in the CNF has the first clause (p->pCnf2->pObj2Clause)
|
||||
and the number of clauses (p->pCnf2->pObj2Count).
|
||||
Each node used in a CNF of any timeframe has its SAT var recorded.
|
||||
Each frame has a reserve mapping of SAT variables into ObjIds.
|
||||
*/
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns SAT variable of the given object.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Pdr_ObjSatVar1( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
|
||||
{
|
||||
return p->pCnf1->pVarNums[ Aig_ObjId(pObj) ];
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns SAT variable of the given object.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Pdr_ObjSatVar2FindOrAdd( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
|
||||
{
|
||||
assert( p->pCnf2->pObj2Count[Aig_ObjId(pObj)] >= 0 );
|
||||
if ( p->pvId2Vars[Aig_ObjId(pObj)] == NULL )
|
||||
p->pvId2Vars[Aig_ObjId(pObj)] = Vec_IntStart( 16 );
|
||||
if ( Vec_IntGetEntry( p->pvId2Vars[Aig_ObjId(pObj)], k ) == 0 )
|
||||
{
|
||||
sat_solver * pSat = Pdr_ManSolver(p, k);
|
||||
Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
|
||||
int iVarNew = Vec_IntSize( vVar2Ids );
|
||||
assert( iVarNew > 0 );
|
||||
Vec_IntPush( vVar2Ids, Aig_ObjId(pObj) );
|
||||
Vec_IntWriteEntry( p->pvId2Vars[Aig_ObjId(pObj)], k, iVarNew );
|
||||
sat_solver_setnvars( pSat, iVarNew + 1 );
|
||||
if ( k == 0 && Saig_ObjIsLo(p->pAig, pObj) ) // initialize the register output
|
||||
{
|
||||
int Lit = toLitCond( iVarNew, 1 );
|
||||
int RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
|
||||
assert( RetValue == 1 );
|
||||
sat_solver_compress( pSat );
|
||||
}
|
||||
}
|
||||
return Vec_IntEntry( p->pvId2Vars[Aig_ObjId(pObj)], k );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Recursively adds CNF for the given object.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Vec_Int_t * vLits;
|
||||
Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
|
||||
int nVarCount = Vec_IntSize(vVar2Ids);
|
||||
int iVarThis = Pdr_ObjSatVar2FindOrAdd( p, k, pObj );
|
||||
int * pLit, i, iVar, nClauses, iFirstClause, RetValue;
|
||||
if ( nVarCount == Vec_IntSize(vVar2Ids) )
|
||||
return iVarThis;
|
||||
assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) );
|
||||
if ( Aig_ObjIsPi(pObj) )
|
||||
return iVarThis;
|
||||
nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)];
|
||||
iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)];
|
||||
assert( nClauses > 0 );
|
||||
pSat = Pdr_ManSolver(p, k);
|
||||
vLits = Vec_IntAlloc( 16 );
|
||||
for ( i = iFirstClause; i < iFirstClause + nClauses; i++ )
|
||||
{
|
||||
Vec_IntClear( vLits );
|
||||
for ( pLit = p->pCnf2->pClauses[i]; pLit < p->pCnf2->pClauses[i+1]; pLit++ )
|
||||
{
|
||||
iVar = Pdr_ObjSatVar2( p, k, Aig_ManObj(p->pAig, lit_var(*pLit)) );
|
||||
Vec_IntPush( vLits, toLitCond( iVar, lit_sign(*pLit) ) );
|
||||
}
|
||||
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits)+Vec_IntSize(vLits) );
|
||||
assert( RetValue );
|
||||
}
|
||||
Vec_IntFree( vLits );
|
||||
return iVarThis;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns SAT variable of the given object.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj )
|
||||
{
|
||||
if ( p->pPars->fMonoCnf )
|
||||
return Pdr_ObjSatVar1( p, k, pObj );
|
||||
else
|
||||
return Pdr_ObjSatVar2( p, k, pObj );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns register number for the given SAT variable.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Pdr_ObjRegNum1( Pdr_Man_t * p, int k, int iSatVar )
|
||||
{
|
||||
int RegId;
|
||||
assert( iSatVar >= 0 );
|
||||
// consider the case of auxiliary variable
|
||||
if ( iSatVar >= p->pCnf1->nVars )
|
||||
return -1;
|
||||
// consider the case of register output
|
||||
RegId = Vec_IntEntry( p->vVar2Reg, iSatVar );
|
||||
assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
|
||||
return RegId;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns register number for the given SAT variable.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int ObjId;
|
||||
Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry(p->vVar2Ids, k);
|
||||
assert( iSatVar > 0 && iSatVar < Vec_IntSize(vVar2Ids) );
|
||||
ObjId = Vec_IntEntry( vVar2Ids, iSatVar );
|
||||
if ( ObjId == -1 ) // activation variable
|
||||
return -1;
|
||||
pObj = Aig_ManObj( p->pAig, ObjId );
|
||||
if ( Saig_ObjIsLi( p->pAig, pObj ) )
|
||||
return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig);
|
||||
assert( 0 ); // should be called for register inputs only
|
||||
return -1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns register number for the given SAT variable.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar )
|
||||
{
|
||||
if ( p->pPars->fMonoCnf )
|
||||
return Pdr_ObjRegNum1( p, k, iSatVar );
|
||||
else
|
||||
return Pdr_ObjRegNum2( p, k, iSatVar );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns the index of unused SAT variable.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManFreeVar( Pdr_Man_t * p, int k )
|
||||
{
|
||||
if ( p->pPars->fMonoCnf )
|
||||
return sat_solver_nvars( Pdr_ManSolver(p, k) );
|
||||
else
|
||||
{
|
||||
Vec_Int_t * vVar2Ids = (Vec_Int_t *)Vec_PtrEntry( p->vVar2Ids, k );
|
||||
Vec_IntPush( vVar2Ids, -1 );
|
||||
return Vec_IntSize( vVar2Ids ) - 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline sat_solver * Pdr_ManNewSolver1( Pdr_Man_t * p, int k, int fInit )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
if ( p->pCnf1 == NULL )
|
||||
{
|
||||
int nRegs = p->pAig->nRegs;
|
||||
p->pAig->nRegs = Aig_ManPoNum(p->pAig);
|
||||
p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManPoNum(p->pAig) );
|
||||
p->pAig->nRegs = nRegs;
|
||||
assert( p->vVar2Reg == NULL );
|
||||
p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars );
|
||||
Saig_ManForEachLi( p->pAig, pObj, i )
|
||||
Vec_IntWriteEntry( p->vVar2Reg, Pdr_ObjSatVar(p, k, pObj), i );
|
||||
}
|
||||
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf1, 1, fInit );
|
||||
return pSat;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline sat_solver * Pdr_ManNewSolver2( Pdr_Man_t * p, int k, int fInit )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Vec_Int_t * vVar2Ids;
|
||||
int i, Entry;
|
||||
if ( p->pCnf2 == NULL )
|
||||
{
|
||||
p->pCnf2 = Cnf_DeriveOther( p->pAig );
|
||||
p->pvId2Vars = ABC_CALLOC( Vec_Int_t *, Aig_ManObjNumMax(p->pAig) );
|
||||
p->vVar2Ids = Vec_PtrAlloc( 256 );
|
||||
}
|
||||
// update the variable mapping
|
||||
vVar2Ids = (Vec_Int_t *)Vec_PtrGetEntry( p->vVar2Ids, k );
|
||||
if ( vVar2Ids == NULL )
|
||||
{
|
||||
vVar2Ids = Vec_IntAlloc( 500 );
|
||||
Vec_PtrWriteEntry( p->vVar2Ids, k, vVar2Ids );
|
||||
}
|
||||
Vec_IntForEachEntry( vVar2Ids, Entry, i )
|
||||
{
|
||||
if ( Entry == -1 )
|
||||
continue;
|
||||
assert( Vec_IntEntry( p->pvId2Vars[Entry], k ) > 0 );
|
||||
Vec_IntWriteEntry( p->pvId2Vars[Entry], k, 0 );
|
||||
}
|
||||
Vec_IntClear( vVar2Ids );
|
||||
Vec_IntPush( vVar2Ids, -1 );
|
||||
// start the SAT solver
|
||||
pSat = sat_solver_new();
|
||||
sat_solver_setnvars( pSat, 500 );
|
||||
return pSat;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
sat_solver * Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit )
|
||||
{
|
||||
if ( p->pPars->fMonoCnf )
|
||||
return Pdr_ManNewSolver1( p, k, fInit );
|
||||
else
|
||||
return Pdr_ManNewSolver2( p, k, fInit );
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,692 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrCore.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [Core procedures.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrCore.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if the state could be blocked.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
|
||||
{
|
||||
memset( pPars, 0, sizeof(Pdr_Par_t) );
|
||||
pPars->iOutput = -1; // zero-based output number
|
||||
pPars->nRecycle = 300; // limit on vars for recycling
|
||||
pPars->nFrameMax = 5000; // limit on number of timeframes
|
||||
pPars->nTimeOut = 0; // timeout in seconds
|
||||
pPars->nConfLimit = 100000; // limit on SAT solver conflicts
|
||||
pPars->fTwoRounds = 0; // use two rounds for generalization
|
||||
pPars->fMonoCnf = 0; // monolythic CNF
|
||||
pPars->fDumpInv = 0; // dump inductive invariant
|
||||
pPars->fShortest = 0; // forces bug traces to be shortest
|
||||
pPars->fVerbose = 0; // verbose output
|
||||
pPars->fVeryVerbose = 0; // very verbose output
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Reduces clause using analyzeFinal.]
|
||||
|
||||
Description [Assumes that the SAT solver just terminated an UNSAT call.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Set_t * Pdr_ManReduceClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
|
||||
{
|
||||
Pdr_Set_t * pCubeMin;
|
||||
Vec_Int_t * vLits;
|
||||
int i, Entry, nCoreLits, * pCoreLits;
|
||||
// get relevant SAT literals
|
||||
nCoreLits = sat_solver_final(Pdr_ManSolver(p, k), &pCoreLits);
|
||||
// translate them into register literals and remove auxiliary
|
||||
vLits = Pdr_ManLitsToCube( p, k, pCoreLits, nCoreLits );
|
||||
// skip if there is no improvement
|
||||
if ( Vec_IntSize(vLits) == pCube->nLits )
|
||||
return NULL;
|
||||
assert( Vec_IntSize(vLits) < pCube->nLits );
|
||||
// if the cube overlaps with init, add any literal
|
||||
Vec_IntForEachEntry( vLits, Entry, i )
|
||||
if ( lit_sign(Entry) == 0 ) // positive literal
|
||||
break;
|
||||
if ( i == Vec_IntSize(vLits) ) // only negative literals
|
||||
{
|
||||
// add the first positive literal
|
||||
for ( i = 0; i < pCube->nLits; i++ )
|
||||
if ( lit_sign(pCube->Lits[i]) == 0 ) // positive literal
|
||||
{
|
||||
Vec_IntPush( vLits, pCube->Lits[i] );
|
||||
break;
|
||||
}
|
||||
assert( i < pCube->nLits );
|
||||
}
|
||||
// generate a starting cube
|
||||
pCubeMin = Pdr_SetCreateSubset( pCube, Vec_IntArray(vLits), Vec_IntSize(vLits) );
|
||||
assert( !Pdr_SetIsInit(pCubeMin, -1) );
|
||||
/*
|
||||
// make sure the cube works
|
||||
{
|
||||
int RetValue;
|
||||
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
|
||||
assert( RetValue );
|
||||
}
|
||||
*/
|
||||
return pCubeMin;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if the state could be blocked.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManPushClauses( Pdr_Man_t * p )
|
||||
{
|
||||
Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
|
||||
Vec_Ptr_t * vArrayK, * vArrayK1;
|
||||
int i, j, k, m, RetValue = 0, kMax = Vec_PtrSize(p->vSolvers)-1;
|
||||
int Counter = 0;
|
||||
int clk = clock();
|
||||
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax-1 )
|
||||
{
|
||||
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
|
||||
vArrayK1 = (Vec_Ptr_t *)Vec_VecEntry( p->vClauses, k+1 );
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
|
||||
{
|
||||
Counter++;
|
||||
|
||||
// remove cubes in the same frame that are contained by pCubeK
|
||||
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
|
||||
{
|
||||
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
|
||||
continue;
|
||||
Pdr_SetDeref( pTemp );
|
||||
Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
|
||||
Vec_PtrPop(vArrayK);
|
||||
m--;
|
||||
}
|
||||
|
||||
// check if the clause can be moved to the next frame
|
||||
if ( !Pdr_ManCheckCube( p, k, pCubeK, NULL, 0 ) )
|
||||
continue;
|
||||
|
||||
{
|
||||
Pdr_Set_t * pCubeMin;
|
||||
pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
|
||||
if ( pCubeMin != NULL )
|
||||
{
|
||||
// printf( "%d ", pCubeK->nLits - pCubeMin->nLits );
|
||||
Pdr_SetDeref( pCubeK );
|
||||
pCubeK = pCubeMin;
|
||||
}
|
||||
}
|
||||
|
||||
// if it can be moved, add it to the next frame
|
||||
Pdr_ManSolverAddClause( p, k+1, pCubeK );
|
||||
// check if the clause subsumes others
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
|
||||
{
|
||||
if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
|
||||
continue;
|
||||
Pdr_SetDeref( pCubeK1 );
|
||||
Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
|
||||
Vec_PtrPop(vArrayK1);
|
||||
i--;
|
||||
}
|
||||
// add the last clause
|
||||
Vec_PtrPush( vArrayK1, pCubeK );
|
||||
Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
|
||||
Vec_PtrPop(vArrayK);
|
||||
j--;
|
||||
}
|
||||
if ( Vec_PtrSize(vArrayK) == 0 )
|
||||
RetValue = 1;
|
||||
}
|
||||
|
||||
// clean up the last one
|
||||
vArrayK = (Vec_Ptr_t *)Vec_VecEntry( p->vClauses, kMax );
|
||||
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
|
||||
{
|
||||
// remove cubes in the same frame that are contained by pCubeK
|
||||
Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
|
||||
{
|
||||
if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
|
||||
continue;
|
||||
/*
|
||||
printf( "===\n" );
|
||||
Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
|
||||
printf( "\n" );
|
||||
Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
|
||||
printf( "\n" );
|
||||
*/
|
||||
Pdr_SetDeref( pTemp );
|
||||
Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
|
||||
Vec_PtrPop(vArrayK);
|
||||
m--;
|
||||
}
|
||||
}
|
||||
p->tPush += clock() - clk;
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if the clause is contained in higher clauses.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManCheckContainment( Pdr_Man_t * p, int k, Pdr_Set_t * pSet )
|
||||
{
|
||||
Pdr_Set_t * pThis;
|
||||
Vec_Ptr_t * vArrayK;
|
||||
int i, j, kMax = Vec_PtrSize(p->vSolvers)-1;
|
||||
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, i, k, kMax )
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pThis, j )
|
||||
if ( Pdr_SetContains( pSet, pThis ) )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Sorts literals by priority.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int * Pdr_ManSortByPriority( Pdr_Man_t * p, Pdr_Set_t * pCube )
|
||||
{
|
||||
int * pPrios = Vec_IntArray(p->vPrio);
|
||||
int * pArray = p->pOrder;
|
||||
int temp, i, j, best_i, nSize = pCube->nLits;
|
||||
// initialize variable order
|
||||
for ( i = 0; i < nSize; i++ )
|
||||
pArray[i] = i;
|
||||
for ( i = 0; i < nSize-1; i++ )
|
||||
{
|
||||
best_i = i;
|
||||
for ( j = i+1; j < nSize; j++ )
|
||||
// if ( pArray[j] < pArray[best_i] )
|
||||
if ( pPrios[pCube->Lits[pArray[j]]>>1] < pPrios[pCube->Lits[pArray[best_i]]>>1] )
|
||||
best_i = j;
|
||||
temp = pArray[i];
|
||||
pArray[i] = pArray[best_i];
|
||||
pArray[best_i] = temp;
|
||||
}
|
||||
/*
|
||||
for ( i = 0; i < pCube->nLits; i++ )
|
||||
printf( "%2d : %5d %5d %5d\n", i, pArray[i], pCube->Lits[pArray[i]]>>1, pPrios[pCube->Lits[pArray[i]]>>1] );
|
||||
printf( "\n" );
|
||||
*/
|
||||
return pArray;
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if the state could be blocked.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, Pdr_Set_t ** ppCubeMin )
|
||||
{
|
||||
Pdr_Set_t * pCubeMin, * pCubeTmp = NULL;
|
||||
int i, j, n, Lit, RetValue, clk = clock();
|
||||
int * pOrder;
|
||||
// if there is no induction, return
|
||||
*ppCubeMin = NULL;
|
||||
RetValue = Pdr_ManCheckCube( p, k, pCube, ppPred, p->pPars->nConfLimit );
|
||||
if ( RetValue == -1 )
|
||||
return -1;
|
||||
if ( RetValue == 0 )
|
||||
{
|
||||
p->tGeneral += clock() - clk;
|
||||
return 0;
|
||||
}
|
||||
// reduce clause using assumptions
|
||||
// pCubeMin = Pdr_SetDup( pCube );
|
||||
pCubeMin = Pdr_ManReduceClause( p, k, pCube );
|
||||
if ( pCubeMin == NULL )
|
||||
pCubeMin = Pdr_SetDup( pCube );
|
||||
|
||||
// sort literals by their occurences
|
||||
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
|
||||
|
||||
// try removing literals
|
||||
for ( j = 0; j < pCubeMin->nLits; j++ )
|
||||
{
|
||||
// use ordering
|
||||
// i = j;
|
||||
i = pOrder[j];
|
||||
|
||||
// check init state
|
||||
assert( pCubeMin->Lits[i] != -1 );
|
||||
if ( Pdr_SetIsInit(pCubeMin, i) )
|
||||
continue;
|
||||
// try removing this literal
|
||||
Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
|
||||
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
|
||||
if ( RetValue == -1 )
|
||||
{
|
||||
Pdr_SetDeref( pCubeMin );
|
||||
return -1;
|
||||
}
|
||||
pCubeMin->Lits[i] = Lit;
|
||||
if ( RetValue == 0 )
|
||||
continue;
|
||||
|
||||
// remove j-th entry
|
||||
for ( n = j; n < pCubeMin->nLits-1; n++ )
|
||||
pOrder[n] = pOrder[n+1];
|
||||
j--;
|
||||
|
||||
// success - update the cube
|
||||
pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
|
||||
Pdr_SetDeref( pCubeTmp );
|
||||
assert( pCubeMin->nLits > 0 );
|
||||
i--;
|
||||
|
||||
// get the ordering by decreasing priorit
|
||||
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
|
||||
}
|
||||
|
||||
if ( p->pPars->fTwoRounds )
|
||||
for ( j = 0; j < pCubeMin->nLits; j++ )
|
||||
{
|
||||
// use ordering
|
||||
// i = j;
|
||||
i = pOrder[j];
|
||||
|
||||
// check init state
|
||||
assert( pCubeMin->Lits[i] != -1 );
|
||||
if ( Pdr_SetIsInit(pCubeMin, i) )
|
||||
continue;
|
||||
// try removing this literal
|
||||
Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1;
|
||||
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
|
||||
if ( RetValue == -1 )
|
||||
{
|
||||
Pdr_SetDeref( pCubeMin );
|
||||
return -1;
|
||||
}
|
||||
pCubeMin->Lits[i] = Lit;
|
||||
if ( RetValue == 0 )
|
||||
continue;
|
||||
|
||||
// remove j-th entry
|
||||
for ( n = j; n < pCubeMin->nLits-1; n++ )
|
||||
pOrder[n] = pOrder[n+1];
|
||||
j--;
|
||||
|
||||
// success - update the cube
|
||||
pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
|
||||
Pdr_SetDeref( pCubeTmp );
|
||||
assert( pCubeMin->nLits > 0 );
|
||||
i--;
|
||||
|
||||
// get the ordering by decreasing priorit
|
||||
pOrder = Pdr_ManSortByPriority( p, pCubeMin );
|
||||
}
|
||||
|
||||
assert( ppCubeMin != NULL );
|
||||
*ppCubeMin = pCubeMin;
|
||||
p->tGeneral += clock() - clk;
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns 1 if the state could be blocked.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
|
||||
{
|
||||
Pdr_Obl_t * pThis;
|
||||
Pdr_Set_t * pPred, * pCubeMin;
|
||||
int i, k, RetValue, Prio = ABC_INFINITY, Counter = 0;
|
||||
int kMax = Vec_PtrSize(p->vSolvers)-1, clk;
|
||||
p->nBlocks++;
|
||||
// create first proof obligation
|
||||
assert( p->pQueue == NULL );
|
||||
pThis = Pdr_OblStart( kMax, Prio--, pCube, NULL ); // consume ref
|
||||
Pdr_QueuePush( p, pThis );
|
||||
// try to solve it recursively
|
||||
while ( !Pdr_QueueIsEmpty(p) )
|
||||
{
|
||||
Counter++;
|
||||
pThis = Pdr_QueueHead( p );
|
||||
if ( pThis->iFrame == 0 )
|
||||
return 0; // SAT
|
||||
pThis = Pdr_QueuePop( p );
|
||||
assert( pThis->iFrame > 0 );
|
||||
assert( !Pdr_SetIsInit(pThis->pState, -1) );
|
||||
|
||||
clk = clock();
|
||||
if ( Pdr_ManCheckContainment( p, pThis->iFrame, pThis->pState ) )
|
||||
{
|
||||
p->tContain += clock() - clk;
|
||||
Pdr_OblDeref( pThis );
|
||||
continue;
|
||||
}
|
||||
p->tContain += clock() - clk;
|
||||
|
||||
// check if the cube is already contained
|
||||
if ( Pdr_ManCheckCubeCs( p, pThis->iFrame, pThis->pState ) ) // cube is blocked by clauses in this frame
|
||||
{
|
||||
Pdr_OblDeref( pThis );
|
||||
continue;
|
||||
}
|
||||
|
||||
// check if the cube holds with relative induction
|
||||
pCubeMin = NULL;
|
||||
RetValue = Pdr_ManGeneralize( p, pThis->iFrame-1, pThis->pState, &pPred, &pCubeMin );
|
||||
if ( RetValue == -1 )
|
||||
{
|
||||
Pdr_OblDeref( pThis );
|
||||
return -1;
|
||||
}
|
||||
if ( RetValue ) // cube is blocked inductively in this frame
|
||||
{
|
||||
assert( pCubeMin != NULL );
|
||||
|
||||
// k is the last frame where pCubeMin holds
|
||||
k = pThis->iFrame;
|
||||
|
||||
// check other frames
|
||||
assert( pPred == NULL );
|
||||
for ( k = pThis->iFrame; k < kMax; k++ )
|
||||
if ( !Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ) )
|
||||
break;
|
||||
|
||||
// add new clause
|
||||
if ( p->pPars->fVeryVerbose )
|
||||
{
|
||||
printf( "Adding cube " );
|
||||
Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
|
||||
printf( " to frame %d.\n", k );
|
||||
}
|
||||
// set priority flops
|
||||
for ( i = 0; i < pCubeMin->nLits; i++ )
|
||||
{
|
||||
assert( pCubeMin->Lits[i] >= 0 );
|
||||
assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
|
||||
Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 );
|
||||
}
|
||||
|
||||
Vec_VecPush( p->vClauses, k, pCubeMin ); // consume ref
|
||||
p->nCubes++;
|
||||
// add clause
|
||||
for ( i = 1; i <= k; i++ )
|
||||
Pdr_ManSolverAddClause( p, i, pCubeMin );
|
||||
// schedule proof obligation
|
||||
if ( k < kMax && !p->pPars->fShortest )
|
||||
{
|
||||
pThis->iFrame = k+1;
|
||||
pThis->prio = Prio--;
|
||||
Pdr_QueuePush( p, pThis );
|
||||
}
|
||||
else
|
||||
{
|
||||
Pdr_OblDeref( pThis );
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
assert( pCubeMin == NULL );
|
||||
assert( pPred != NULL );
|
||||
pThis->prio = Prio--;
|
||||
Pdr_QueuePush( p, pThis );
|
||||
|
||||
pThis = Pdr_OblStart( pThis->iFrame-1, Prio--, pPred, Pdr_OblRef(pThis) );
|
||||
Pdr_QueuePush( p, pThis );
|
||||
}
|
||||
|
||||
// check the timeout
|
||||
if ( p->timeToStop && clock() >= p->timeToStop )
|
||||
return -1;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManSolveInt( Pdr_Man_t * p )
|
||||
{
|
||||
int fPrintClauses = 0;
|
||||
Pdr_Set_t * pCube;
|
||||
int k, RetValue = -1;
|
||||
int clkTotal = clock();
|
||||
int clkStart = clock();
|
||||
p->timeToStop = (p->pPars->nTimeOut == 0) ? 0 : clock() + (CLOCKS_PER_SEC * p->pPars->nTimeOut);
|
||||
assert( Vec_PtrSize(p->vSolvers) == 0 );
|
||||
// create the first timeframe
|
||||
Pdr_ManCreateSolver( p, (k = 0) );
|
||||
while ( 1 )
|
||||
{
|
||||
p->nFrames = k;
|
||||
assert( k == Vec_PtrSize(p->vSolvers)-1 );
|
||||
RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
|
||||
if ( RetValue == -1 )
|
||||
{
|
||||
if ( p->pPars->fVerbose )
|
||||
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
|
||||
printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
|
||||
return -1;
|
||||
}
|
||||
if ( RetValue == 0 )
|
||||
{
|
||||
RetValue = Pdr_ManBlockCube( p, pCube );
|
||||
if ( RetValue == -1 )
|
||||
{
|
||||
if ( p->pPars->fVerbose )
|
||||
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
|
||||
printf( "Reached conflict limit (%d).\n", p->pPars->nConfLimit );
|
||||
return -1;
|
||||
}
|
||||
if ( RetValue == 0 )
|
||||
{
|
||||
if ( fPrintClauses )
|
||||
{
|
||||
printf( "*** Clauses after frame %d:\n", k );
|
||||
Pdr_ManPrintClauses( p, 0 );
|
||||
}
|
||||
if ( p->pPars->fVerbose )
|
||||
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
|
||||
return 0; // SAT
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
// open a new timeframe
|
||||
assert( pCube == NULL );
|
||||
Pdr_ManSetPropertyOutput( p, k );
|
||||
Pdr_ManCreateSolver( p, ++k );
|
||||
if ( fPrintClauses )
|
||||
{
|
||||
printf( "*** Clauses after frame %d:\n", k );
|
||||
Pdr_ManPrintClauses( p, 0 );
|
||||
}
|
||||
if ( p->pPars->fVerbose )
|
||||
Pdr_ManPrintProgress( p, 0, clock() - clkStart );
|
||||
// push clauses into this timeframe
|
||||
if ( Pdr_ManPushClauses( p ) )
|
||||
{
|
||||
if ( p->pPars->fVerbose )
|
||||
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
|
||||
Pdr_ManReportInvariant( p );
|
||||
Pdr_ManVerifyInvariant( p );
|
||||
if ( p->pPars->fDumpInv )
|
||||
Pdr_ManDumpClauses( p, (char *)"inv.pla" );
|
||||
return 1; // UNSAT
|
||||
}
|
||||
if ( p->pPars->fVerbose )
|
||||
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
|
||||
clkStart = clock();
|
||||
}
|
||||
|
||||
// check the timeout
|
||||
if ( p->timeToStop && clock() >= p->timeToStop )
|
||||
{
|
||||
if ( fPrintClauses )
|
||||
{
|
||||
printf( "*** Clauses after frame %d:\n", k );
|
||||
Pdr_ManPrintClauses( p, 0 );
|
||||
}
|
||||
if ( p->pPars->fVerbose )
|
||||
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
|
||||
printf( "Reached timeout (%d seconds).\n", p->pPars->nTimeOut );
|
||||
return -1;
|
||||
}
|
||||
if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
|
||||
{
|
||||
if ( p->pPars->fVerbose )
|
||||
Pdr_ManPrintProgress( p, 1, clock() - clkStart );
|
||||
printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
|
||||
return -1;
|
||||
}
|
||||
}
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, Abc_Cex_t ** ppCex )
|
||||
{
|
||||
Pdr_Man_t * p;
|
||||
int RetValue;
|
||||
int clk = clock();
|
||||
p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
|
||||
RetValue = Pdr_ManSolveInt( p );
|
||||
*ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
|
||||
// if ( *ppCex && pPars->fVerbose )
|
||||
// printf( "Found counter-example in frame %d after exploring %d frames.\n",
|
||||
// (*ppCex)->iFrame, p->nFrames );
|
||||
p->tTotal += clock() - clk;
|
||||
if ( pvPrioInit )
|
||||
{
|
||||
*pvPrioInit = p->vPrio;
|
||||
p->vPrio = NULL;
|
||||
}
|
||||
Pdr_ManStop( p );
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
|
||||
{
|
||||
/*
|
||||
Vec_Int_t * vPrioInit = NULL;
|
||||
int RetValue, nTimeOut;
|
||||
if ( pPars->nTimeOut > 0 )
|
||||
return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
|
||||
nTimeOut = pPars->nTimeOut;
|
||||
pPars->nTimeOut = 10;
|
||||
RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
|
||||
pPars->nTimeOut = nTimeOut;
|
||||
if ( RetValue == -1 )
|
||||
RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
|
||||
Vec_IntFree( vPrioInit );
|
||||
return RetValue;
|
||||
*/
|
||||
return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,187 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrInt.h]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [Internal declarations.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrInt.h,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#ifndef __PDR_INT_H__
|
||||
#define __PDR_INT_H__
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// INCLUDES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#include "saig.h"
|
||||
#include "cnf.h"
|
||||
#include "satSolver.h"
|
||||
#include "pdr.h"
|
||||
|
||||
ABC_NAMESPACE_HEADER_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// PARAMETERS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// BASIC TYPES ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
typedef struct Pdr_Set_t_ Pdr_Set_t;
|
||||
struct Pdr_Set_t_
|
||||
{
|
||||
word Sign; // signature
|
||||
int nRefs; // ref counter
|
||||
short nTotal; // total literals
|
||||
short nLits; // num flop literals
|
||||
int Lits[0];
|
||||
};
|
||||
|
||||
typedef struct Pdr_Obl_t_ Pdr_Obl_t;
|
||||
struct Pdr_Obl_t_
|
||||
{
|
||||
int iFrame; // time frame
|
||||
int prio; // priority
|
||||
int nRefs; // reference counter
|
||||
Pdr_Set_t * pState; // state cube
|
||||
Pdr_Obl_t * pNext; // next one
|
||||
Pdr_Obl_t * pLink; // queue link
|
||||
};
|
||||
|
||||
typedef struct Pdr_Man_t_ Pdr_Man_t;
|
||||
struct Pdr_Man_t_
|
||||
{
|
||||
// input problem
|
||||
Pdr_Par_t * pPars; // parameters
|
||||
Aig_Man_t * pAig; // user's AIG
|
||||
// static CNF representation
|
||||
Cnf_Dat_t * pCnf1; // CNF for this AIG
|
||||
Vec_Int_t * vVar2Reg; // mapping of SAT var into registers
|
||||
// dynamic CNF representation
|
||||
Cnf_Dat_t * pCnf2; // CNF for this AIG
|
||||
Vec_Int_t** pvId2Vars; // for each used ObjId, maps frame into SAT var
|
||||
Vec_Ptr_t * vVar2Ids; // for each used frame, maps SAT var into ObjId
|
||||
// data representation
|
||||
Vec_Ptr_t * vSolvers; // SAT solvers
|
||||
Vec_Vec_t * vClauses; // clauses by timeframe
|
||||
Pdr_Obl_t * pQueue; // proof obligations
|
||||
int * pOrder; // ordering of the lits
|
||||
Vec_Int_t * vActVars; // the counter of activation variables
|
||||
// internal use
|
||||
Vec_Int_t * vPrio; // priority flops
|
||||
Vec_Int_t * vLits; // array of literals
|
||||
Vec_Int_t * vCiObjs; // cone leaves
|
||||
Vec_Int_t * vCoObjs; // cone roots
|
||||
Vec_Int_t * vCiVals; // cone leaf values
|
||||
Vec_Int_t * vCoVals; // cone root values
|
||||
Vec_Int_t * vNodes; // cone nodes
|
||||
Vec_Int_t * vUndo; // cone undos
|
||||
Vec_Int_t * vVisits; // intermediate
|
||||
Vec_Int_t * vCi2Rem; // CIs to be removed
|
||||
Vec_Int_t * vRes; // final result
|
||||
// statistics
|
||||
int nBlocks; // the number of times blockState was called
|
||||
int nObligs; // the number of proof obligations derived
|
||||
int nCubes; // the number of cubes derived
|
||||
int nCalls; // the number of SAT calls
|
||||
int nCallsS; // the number of SAT calls (sat)
|
||||
int nCallsU; // the number of SAT calls (unsat)
|
||||
int nStarts; // the number of SAT solver restarts
|
||||
int nFrames; // frames explored
|
||||
// runtime
|
||||
int timeStart;
|
||||
int timeToStop;
|
||||
// time stats
|
||||
int tSat;
|
||||
int tSatSat;
|
||||
int tSatUnsat;
|
||||
int tGeneral;
|
||||
int tPush;
|
||||
int tTsim;
|
||||
int tContain;
|
||||
int tCnf;
|
||||
int tTotal;
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// MACRO DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
static inline sat_solver * Pdr_ManSolver( Pdr_Man_t * p, int k ) { return (sat_solver *)Vec_PtrEntry(p->vSolvers, k); }
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/*=== pdrCex.c ==========================================================*/
|
||||
extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
|
||||
/*=== pdrCnf.c ==========================================================*/
|
||||
extern int Pdr_ObjSatVar( Pdr_Man_t * p, int k, Aig_Obj_t * pObj );
|
||||
extern int Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
|
||||
extern int Pdr_ManFreeVar( Pdr_Man_t * p, int k );
|
||||
extern sat_solver * Pdr_ManNewSolver( Pdr_Man_t * p, int k, int fInit );
|
||||
/*=== pdrInv.c ==========================================================*/
|
||||
extern void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time );
|
||||
extern void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart );
|
||||
extern void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName );
|
||||
extern void Pdr_ManReportInvariant( Pdr_Man_t * p );
|
||||
extern void Pdr_ManVerifyInvariant( Pdr_Man_t * p );
|
||||
/*=== pdrMan.c ==========================================================*/
|
||||
extern Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
|
||||
extern void Pdr_ManStop( Pdr_Man_t * p );
|
||||
extern Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p );
|
||||
/*=== pdrSat.c ==========================================================*/
|
||||
extern sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
|
||||
extern sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
|
||||
extern void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k );
|
||||
extern Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext );
|
||||
extern Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray );
|
||||
extern void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
|
||||
extern void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues );
|
||||
extern int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
|
||||
extern int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit );
|
||||
/*=== pdrTsim.c ==========================================================*/
|
||||
extern Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube );
|
||||
/*=== pdrUtil.c ==========================================================*/
|
||||
extern Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits );
|
||||
extern Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove );
|
||||
extern Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits );
|
||||
extern Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet );
|
||||
extern Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p );
|
||||
extern void Pdr_SetDeref( Pdr_Set_t * p );
|
||||
extern int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew );
|
||||
extern int Pdr_SetIsInit( Pdr_Set_t * p, int iRemove );
|
||||
extern void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts );
|
||||
extern int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 );
|
||||
extern Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext );
|
||||
extern Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p );
|
||||
extern void Pdr_OblDeref( Pdr_Obl_t * p );
|
||||
extern int Pdr_QueueIsEmpty( Pdr_Man_t * p );
|
||||
extern Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p );
|
||||
extern Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p );
|
||||
extern void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
|
||||
extern void Pdr_QueuePrint( Pdr_Man_t * p );
|
||||
extern void Pdr_QueueStop( Pdr_Man_t * p );
|
||||
|
||||
ABC_NAMESPACE_HEADER_END
|
||||
|
||||
|
||||
#endif
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
@ -0,0 +1,351 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrInv.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [Invariant computation, printing, verification.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrInv.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, int Time )
|
||||
{
|
||||
extern int Extra_Base10Log( unsigned int Num );
|
||||
static int PastSize;
|
||||
Vec_Ptr_t * vVec;
|
||||
int i, ThisSize, Length, LengthStart;
|
||||
if ( Vec_PtrSize(p->vSolvers) < 2 )
|
||||
return;
|
||||
// count the total length of the printout
|
||||
Length = 0;
|
||||
Vec_VecForEachLevel( p->vClauses, vVec, i )
|
||||
Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
|
||||
// determine the starting point
|
||||
LengthStart = ABC_MAX( 0, Length - 70 );
|
||||
printf( "%3d :", Vec_PtrSize(p->vSolvers)-1 );
|
||||
ThisSize = 6;
|
||||
if ( LengthStart > 0 )
|
||||
{
|
||||
printf( " ..." );
|
||||
ThisSize += 4;
|
||||
}
|
||||
Length = 0;
|
||||
Vec_VecForEachLevel( p->vClauses, vVec, i )
|
||||
{
|
||||
if ( Length < LengthStart )
|
||||
{
|
||||
Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
|
||||
continue;
|
||||
}
|
||||
printf( " %d", Vec_PtrSize(vVec) );
|
||||
Length += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
|
||||
ThisSize += 1 + Extra_Base10Log(Vec_PtrSize(vVec)+1);
|
||||
}
|
||||
if ( fClose )
|
||||
{
|
||||
for ( i = 0; i < PastSize - ThisSize; i++ )
|
||||
printf( " " );
|
||||
printf( "\n" );
|
||||
}
|
||||
else
|
||||
{
|
||||
printf( "\r" );
|
||||
PastSize = ThisSize;
|
||||
}
|
||||
// printf(" %.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC));
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Counts how many times each flop appears in the set of cubes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Pdr_ManCountFlops( Pdr_Man_t * p, Vec_Ptr_t * vCubes )
|
||||
{
|
||||
Vec_Int_t * vFlopCount;
|
||||
Pdr_Set_t * pCube;
|
||||
int i, n;
|
||||
vFlopCount = Vec_IntStart( Aig_ManRegNum(p->pAig) );
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
|
||||
for ( n = 0; n < pCube->nLits; n++ )
|
||||
{
|
||||
assert( pCube->Lits[n] >= 0 && pCube->Lits[n] < 2*Aig_ManRegNum(p->pAig) );
|
||||
Vec_IntAddToEntry( vFlopCount, pCube->Lits[n] >> 1, 1 );
|
||||
}
|
||||
return vFlopCount;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManFindInvariantStart( Pdr_Man_t * p )
|
||||
{
|
||||
Vec_Ptr_t * vArrayK;
|
||||
int k, kMax = Vec_PtrSize(p->vSolvers)-1;
|
||||
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, 1, kMax )
|
||||
if ( Vec_PtrSize(vArrayK) == 0 )
|
||||
return k;
|
||||
return -1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Counts the number of variables used in the clauses.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Ptr_t * Pdr_ManCollectCubes( Pdr_Man_t * p, int kStart )
|
||||
{
|
||||
Vec_Ptr_t * vResult;
|
||||
Vec_Ptr_t * vArrayK;
|
||||
Pdr_Set_t * pSet;
|
||||
int i, j;
|
||||
vResult = Vec_PtrAlloc( 100 );
|
||||
Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, kStart )
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pSet, j )
|
||||
Vec_PtrPush( vResult, pSet );
|
||||
return vResult;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Counts the number of variables used in the clauses.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManCountVariables( Pdr_Man_t * p, int kStart )
|
||||
{
|
||||
Vec_Int_t * vFlopCounts;
|
||||
Vec_Ptr_t * vCubes;
|
||||
int i, Entry, Counter = 0;
|
||||
vCubes = Pdr_ManCollectCubes( p, kStart );
|
||||
vFlopCounts = Pdr_ManCountFlops( p, vCubes );
|
||||
Vec_IntForEachEntry( vFlopCounts, Entry, i )
|
||||
Counter += (Entry > 0);
|
||||
Vec_IntFreeP( &vFlopCounts );
|
||||
Vec_PtrFree( vCubes );
|
||||
return Counter;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManPrintClauses( Pdr_Man_t * p, int kStart )
|
||||
{
|
||||
Vec_Ptr_t * vArrayK;
|
||||
Pdr_Set_t * pCube;
|
||||
int i, k, Counter = 0;
|
||||
Vec_VecForEachLevelStart( p->vClauses, vArrayK, k, kStart )
|
||||
{
|
||||
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
|
||||
{
|
||||
printf( "C=%4d. F=%4d ", Counter++, k );
|
||||
Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
|
||||
printf( "\n" );
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManDumpClauses( Pdr_Man_t * p, char * pFileName )
|
||||
{
|
||||
int fUseSupp = 1;
|
||||
FILE * pFile;
|
||||
Vec_Int_t * vFlopCounts;
|
||||
Vec_Ptr_t * vCubes;
|
||||
Pdr_Set_t * pCube;
|
||||
int i, kStart;
|
||||
// create file
|
||||
pFile = fopen( pFileName, "w" );
|
||||
if ( pFile == NULL )
|
||||
{
|
||||
printf( "Cannot open file \"%s\" for writing invariant.\n", pFileName );
|
||||
return;
|
||||
}
|
||||
// collect cubes
|
||||
kStart = Pdr_ManFindInvariantStart( p );
|
||||
vCubes = Pdr_ManCollectCubes( p, kStart );
|
||||
Vec_PtrSort( vCubes, (int (*)(void))Pdr_SetCompare );
|
||||
// collect variable appearances
|
||||
vFlopCounts = fUseSupp ? Pdr_ManCountFlops( p, vCubes ) : NULL;
|
||||
// output the header
|
||||
fprintf( pFile, "# Inductive invariant for \"%s\"\n", p->pAig->pName );
|
||||
fprintf( pFile, "# generated by PDR in ABC on %s\n", Aig_TimeStamp() );
|
||||
fprintf( pFile, ".i %d\n", fUseSupp ? Pdr_ManCountVariables(p, kStart) : Aig_ManRegNum(p->pAig) );
|
||||
fprintf( pFile, ".o 1\n" );
|
||||
fprintf( pFile, ".p %d\n", Vec_PtrSize(vCubes) );
|
||||
// output cubes
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
|
||||
{
|
||||
Pdr_SetPrint( pFile, pCube, Aig_ManRegNum(p->pAig), vFlopCounts );
|
||||
fprintf( pFile, " 1\n" );
|
||||
}
|
||||
fprintf( pFile, ".e\n\n" );
|
||||
fclose( pFile );
|
||||
Vec_IntFreeP( &vFlopCounts );
|
||||
Vec_PtrFree( vCubes );
|
||||
printf( "Inductive invariant was written into file \"%s\".\n", pFileName );
|
||||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManReportInvariant( Pdr_Man_t * p )
|
||||
{
|
||||
Vec_Ptr_t * vCubes;
|
||||
int kStart = Pdr_ManFindInvariantStart( p );
|
||||
vCubes = Pdr_ManCollectCubes( p, kStart );
|
||||
printf( "Invariant F[%d] : %d clauses with %d flops (out of %d)\n",
|
||||
kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) );
|
||||
Vec_PtrFree( vCubes );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Vec_Int_t * vLits;
|
||||
Vec_Ptr_t * vCubes;
|
||||
Pdr_Set_t * pCube;
|
||||
int i, kStart, kThis, RetValue, Counter = 0, clk = clock();
|
||||
// collect cubes used in the inductive invariant
|
||||
kStart = Pdr_ManFindInvariantStart( p );
|
||||
vCubes = Pdr_ManCollectCubes( p, kStart );
|
||||
// create solver with the cubes
|
||||
kThis = Vec_PtrSize(p->vSolvers);
|
||||
pSat = Pdr_ManCreateSolver( p, kThis );
|
||||
// add the property output
|
||||
Pdr_ManSetPropertyOutput( p, kThis );
|
||||
// add the clauses
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
|
||||
{
|
||||
vLits = Pdr_ManCubeToLits( p, kThis, pCube, 1, 0 );
|
||||
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
|
||||
assert( RetValue );
|
||||
sat_solver_compress( pSat );
|
||||
}
|
||||
// check each clause
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
|
||||
{
|
||||
vLits = Pdr_ManCubeToLits( p, kThis, pCube, 0, 1 );
|
||||
RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
|
||||
if ( RetValue != l_False )
|
||||
{
|
||||
printf( "Verification of clause %d failed.\n", i );
|
||||
Counter++;
|
||||
}
|
||||
}
|
||||
if ( Counter )
|
||||
printf( "Verification of %d clauses has failed.\n", Counter );
|
||||
else
|
||||
{
|
||||
printf( "Verification of invariant with %d clauses was successful. ", Vec_PtrSize(vCubes) );
|
||||
Abc_PrintTime( 1, "Time", clock() - clk );
|
||||
}
|
||||
// sat_solver_delete( pSat );
|
||||
Vec_PtrFree( vCubes );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,190 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdr.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [Manager procedures.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdr.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )
|
||||
{
|
||||
Pdr_Man_t * p;
|
||||
p = ABC_CALLOC( Pdr_Man_t, 1 );
|
||||
p->pPars = pPars;
|
||||
p->pAig = pAig;
|
||||
p->vSolvers = Vec_PtrAlloc( 0 );
|
||||
p->vClauses = Vec_VecAlloc( 0 );
|
||||
p->pQueue = NULL;
|
||||
p->pOrder = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
|
||||
p->vActVars = Vec_IntAlloc( 256 );
|
||||
// internal use
|
||||
p->vPrio = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) ); // priority flops
|
||||
p->vLits = Vec_IntAlloc( 100 ); // array of literals
|
||||
p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves
|
||||
p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots
|
||||
p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values
|
||||
p->vCoVals = Vec_IntAlloc( 100 ); // cone root values
|
||||
p->vNodes = Vec_IntAlloc( 100 ); // cone nodes
|
||||
p->vUndo = Vec_IntAlloc( 100 ); // cone undos
|
||||
p->vVisits = Vec_IntAlloc( 100 ); // intermediate
|
||||
p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed
|
||||
p->vRes = Vec_IntAlloc( 100 ); // final result
|
||||
// additional AIG data-members
|
||||
if ( pAig->pFanData == NULL )
|
||||
Aig_ManFanoutStart( pAig );
|
||||
if ( pAig->pTerSimData == NULL )
|
||||
pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
|
||||
p->timeStart = clock();
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Frees manager.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManStop( Pdr_Man_t * p )
|
||||
{
|
||||
Pdr_Set_t * pCla;
|
||||
sat_solver * pSat;
|
||||
int i, k;
|
||||
if ( p->pPars->fVerbose )
|
||||
{
|
||||
printf( "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Start =%4d\n",
|
||||
p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nStarts );
|
||||
ABC_PRTP( "SAT solving", p->tSat, p->tTotal );
|
||||
ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal );
|
||||
ABC_PRTP( " sat ", p->tSatSat, p->tTotal );
|
||||
ABC_PRTP( "Generalize ", p->tGeneral, p->tTotal );
|
||||
ABC_PRTP( "Push clause", p->tPush, p->tTotal );
|
||||
ABC_PRTP( "Ternary sim", p->tTsim, p->tTotal );
|
||||
ABC_PRTP( "Containment", p->tContain, p->tTotal );
|
||||
ABC_PRTP( "CNF compute", p->tCnf, p->tTotal );
|
||||
ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal );
|
||||
}
|
||||
|
||||
Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
|
||||
sat_solver_delete( pSat );
|
||||
Vec_PtrFree( p->vSolvers );
|
||||
Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
|
||||
Pdr_SetDeref( pCla );
|
||||
Vec_VecFree( p->vClauses );
|
||||
Pdr_QueueStop( p );
|
||||
ABC_FREE( p->pOrder );
|
||||
Vec_IntFree( p->vActVars );
|
||||
// static CNF
|
||||
Cnf_DataFree( p->pCnf1 );
|
||||
Vec_IntFreeP( &p->vVar2Reg );
|
||||
// dynamic CNF
|
||||
Cnf_DataFree( p->pCnf2 );
|
||||
if ( p->pvId2Vars )
|
||||
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
|
||||
Vec_IntFreeP( &p->pvId2Vars[i] );
|
||||
ABC_FREE( p->pvId2Vars );
|
||||
Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
|
||||
// internal use
|
||||
Vec_IntFreeP( &p->vPrio ); // priority flops
|
||||
Vec_IntFree( p->vLits ); // array of literals
|
||||
Vec_IntFree( p->vCiObjs ); // cone leaves
|
||||
Vec_IntFree( p->vCoObjs ); // cone roots
|
||||
Vec_IntFree( p->vCiVals ); // cone leaf values
|
||||
Vec_IntFree( p->vCoVals ); // cone root values
|
||||
Vec_IntFree( p->vNodes ); // cone nodes
|
||||
Vec_IntFree( p->vUndo ); // cone undos
|
||||
Vec_IntFree( p->vVisits ); // intermediate
|
||||
Vec_IntFree( p->vCi2Rem ); // CIs to be removed
|
||||
Vec_IntFree( p->vRes ); // final result
|
||||
// additional AIG data-members
|
||||
if ( p->pAig->pFanData != NULL )
|
||||
Aig_ManFanoutStop( p->pAig );
|
||||
if ( p->pAig->pTerSimData != NULL )
|
||||
ABC_FREE( p->pAig->pTerSimData );
|
||||
ABC_FREE( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives counter-example.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
|
||||
{
|
||||
extern Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
|
||||
Abc_Cex_t * pCex;
|
||||
Pdr_Obl_t * pObl;
|
||||
int i, f, Lit, nFrames = 0;
|
||||
// count the number of frames
|
||||
for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
|
||||
nFrames++;
|
||||
// create the counter-example
|
||||
pCex = Gia_ManAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
|
||||
pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
|
||||
pCex->iFrame = nFrames-1;
|
||||
for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
|
||||
for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
|
||||
{
|
||||
Lit = pObl->pState->Lits[i];
|
||||
if ( lit_sign(Lit) )
|
||||
continue;
|
||||
assert( lit_var(Lit) < pCex->nPis );
|
||||
Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
|
||||
}
|
||||
assert( f == nFrames );
|
||||
return pCex;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,351 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrSat.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [SAT solver procedures.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrSat.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Creates new SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
assert( Vec_PtrSize(p->vSolvers) == k );
|
||||
assert( Vec_VecSize(p->vClauses) == k );
|
||||
assert( Vec_IntSize(p->vActVars) == k );
|
||||
// create new solver
|
||||
pSat = Pdr_ManNewSolver( p, k, (int)(k == 0) );
|
||||
Vec_PtrPush( p->vSolvers, pSat );
|
||||
Vec_VecExpand( p->vClauses, k );
|
||||
Vec_IntPush( p->vActVars, 0 );
|
||||
// add property cone
|
||||
Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
|
||||
return pSat;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Returns old or restarted solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Vec_Ptr_t * vArrayK;
|
||||
Pdr_Set_t * pCube;
|
||||
int i, j;
|
||||
pSat = Pdr_ManSolver(p, k);
|
||||
if ( Vec_IntEntry(p->vActVars, k) < p->pPars->nRecycle )
|
||||
return pSat;
|
||||
assert( k < Vec_PtrSize(p->vSolvers) - 1 );
|
||||
p->nStarts++;
|
||||
sat_solver_delete( pSat );
|
||||
// create new SAT solver
|
||||
pSat = Pdr_ManNewSolver( p, k, (int)(k == 0) );
|
||||
// write new SAT solver
|
||||
Vec_PtrWriteEntry( p->vSolvers, k, pSat );
|
||||
Vec_IntWriteEntry( p->vActVars, k, 0 );
|
||||
// set the property output
|
||||
Pdr_ManSetPropertyOutput( p, k );
|
||||
// add the clauses
|
||||
Vec_VecForEachLevelStart( p->vClauses, vArrayK, i, k )
|
||||
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, j )
|
||||
Pdr_ManSolverAddClause( p, k, pCube );
|
||||
return pSat;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Converts SAT variables into register IDs.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Pdr_ManLitsToCube( Pdr_Man_t * p, int k, int * pArray, int nArray )
|
||||
{
|
||||
int i, RegId;
|
||||
Vec_IntClear( p->vLits );
|
||||
for ( i = 0; i < nArray; i++ )
|
||||
{
|
||||
RegId = Pdr_ObjRegNum( p, k, lit_var(pArray[i]) );
|
||||
if ( RegId == -1 )
|
||||
continue;
|
||||
assert( RegId >= 0 && RegId < Aig_ManRegNum(p->pAig) );
|
||||
Vec_IntPush( p->vLits, toLitCond(RegId, !lit_sign(pArray[i])) );
|
||||
}
|
||||
assert( Vec_IntSize(p->vLits) >= 0 && Vec_IntSize(p->vLits) <= nArray );
|
||||
return p->vLits;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Converts the cube in terms of RO numbers into array of CNF literals.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCompl, int fNext )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i, iVar, iVarMax = 0;
|
||||
int clk = clock();
|
||||
Vec_IntClear( p->vLits );
|
||||
for ( i = 0; i < pCube->nLits; i++ )
|
||||
{
|
||||
if ( pCube->Lits[i] == -1 )
|
||||
continue;
|
||||
if ( fNext )
|
||||
pObj = Saig_ManLi( p->pAig, lit_var(pCube->Lits[i]) );
|
||||
else
|
||||
pObj = Saig_ManLo( p->pAig, lit_var(pCube->Lits[i]) );
|
||||
iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
|
||||
iVarMax = ABC_MAX( iVarMax, iVar );
|
||||
Vec_IntPush( p->vLits, toLitCond( iVar, fCompl ^ lit_sign(pCube->Lits[i]) ) );
|
||||
}
|
||||
// sat_solver_setnvars( Pdr_ManSolver(p, k), iVarMax + 1 );
|
||||
p->tCnf += clock() - clk;
|
||||
return p->vLits;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Sets the property output to 0 (sat) forever.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
int Lit, RetValue;
|
||||
pSat = Pdr_ManSolver(p, k);
|
||||
Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
|
||||
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
|
||||
assert( RetValue == 1 );
|
||||
sat_solver_compress( pSat );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Adds one clause in terms of ROs to the k-th SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManSolverAddClause( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Vec_Int_t * vLits;
|
||||
int RetValue;
|
||||
pSat = Pdr_ManSolver(p, k);
|
||||
vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
|
||||
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
|
||||
assert( RetValue == 1 );
|
||||
sat_solver_compress( pSat );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Collects values of the RO/RI variables in k-th SAT solver.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManCollectValues( Pdr_Man_t * p, int k, Vec_Int_t * vObjIds, Vec_Int_t * vValues )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Aig_Obj_t * pObj;
|
||||
int iVar, i;
|
||||
Vec_IntClear( vValues );
|
||||
pSat = Pdr_ManSolver(p, k);
|
||||
Aig_ManForEachNodeVec( p->pAig, vObjIds, pObj, i )
|
||||
{
|
||||
iVar = Pdr_ObjSatVar( p, k, pObj ); assert( iVar >= 0 );
|
||||
Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]
|
||||
|
||||
Description [Return 1/0 if cube or property are proved to hold/fail
|
||||
in k-th timeframe. Returns the predecessor bad state in ppPred.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManCheckCubeCs( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
|
||||
{
|
||||
sat_solver * pSat;
|
||||
Vec_Int_t * vLits;
|
||||
int RetValue;
|
||||
pSat = Pdr_ManFetchSolver( p, k );
|
||||
vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 0 );
|
||||
RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
|
||||
assert( RetValue != l_Undef );
|
||||
return (RetValue == l_False);
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Checks if the cube holds (UNSAT) in the given timeframe.]
|
||||
|
||||
Description [Return 1/0 if cube or property are proved to hold/fail
|
||||
in k-th timeframe. Returns the predecessor bad state in ppPred.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPred, int nConfLimit )
|
||||
{
|
||||
int fUseLit = 1;
|
||||
int fLitUsed = 0;
|
||||
sat_solver * pSat;
|
||||
Vec_Int_t * vLits;
|
||||
int Lit, RetValue, clk;
|
||||
p->nCalls++;
|
||||
pSat = Pdr_ManFetchSolver( p, k );
|
||||
if ( pCube == NULL ) // solve the property
|
||||
{
|
||||
clk = clock();
|
||||
Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
|
||||
RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
|
||||
if ( RetValue == l_Undef )
|
||||
return -1;
|
||||
}
|
||||
else // check relative containment in terms of next states
|
||||
{
|
||||
if ( fUseLit )
|
||||
{
|
||||
fLitUsed = 1;
|
||||
Vec_IntAddToEntry( p->vActVars, k, 1 );
|
||||
// add the cube in terms of current state variables
|
||||
vLits = Pdr_ManCubeToLits( p, k, pCube, 1, 0 );
|
||||
// add activation literal
|
||||
Lit = toLit( Pdr_ManFreeVar(p, k) );
|
||||
// add activation literal
|
||||
Vec_IntPush( vLits, Lit );
|
||||
RetValue = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
|
||||
assert( RetValue == 1 );
|
||||
sat_solver_compress( pSat );
|
||||
// create assumptions
|
||||
vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
|
||||
// add activation literal
|
||||
Vec_IntPush( vLits, lit_neg(Lit) );
|
||||
}
|
||||
else
|
||||
vLits = Pdr_ManCubeToLits( p, k, pCube, 0, 1 );
|
||||
|
||||
// solve
|
||||
clk = clock();
|
||||
RetValue = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nConfLimit, 0, 0, 0 );
|
||||
if ( RetValue == l_Undef )
|
||||
return -1;
|
||||
}
|
||||
clk = clock() - clk;
|
||||
p->tSat += clk;
|
||||
assert( RetValue != l_Undef );
|
||||
if ( RetValue == l_False )
|
||||
{
|
||||
p->tSatUnsat += clk;
|
||||
p->nCallsU++;
|
||||
if ( ppPred )
|
||||
*ppPred = NULL;
|
||||
RetValue = 1;
|
||||
}
|
||||
else // if ( RetValue == l_True )
|
||||
{
|
||||
p->tSatSat += clk;
|
||||
p->nCallsS++;
|
||||
if ( ppPred )
|
||||
*ppPred = Pdr_ManTernarySim( p, k, pCube );
|
||||
RetValue = 0;
|
||||
}
|
||||
|
||||
/* // for some reason, it does not work...
|
||||
if ( fLitUsed )
|
||||
{
|
||||
int RetValue;
|
||||
Lit = lit_neg(Lit);
|
||||
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
|
||||
assert( RetValue == 1 );
|
||||
sat_solver_compress( pSat );
|
||||
}
|
||||
*/
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,450 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrTsim.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [Ternary simulation.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
#define PDR_ZER 1
|
||||
#define PDR_ONE 2
|
||||
#define PDR_UND 3
|
||||
|
||||
static inline int Pdr_ManSimInfoNot( int Value )
|
||||
{
|
||||
if ( Value == PDR_ZER )
|
||||
return PDR_ONE;
|
||||
if ( Value == PDR_ONE )
|
||||
return PDR_ZER;
|
||||
return PDR_UND;
|
||||
}
|
||||
|
||||
static inline int Pdr_ManSimInfoAnd( int Value0, int Value1 )
|
||||
{
|
||||
if ( Value0 == PDR_ZER || Value1 == PDR_ZER )
|
||||
return PDR_ZER;
|
||||
if ( Value0 == PDR_ONE && Value1 == PDR_ONE )
|
||||
return PDR_ONE;
|
||||
return PDR_UND;
|
||||
}
|
||||
|
||||
static inline int Pdr_ManSimInfoGet( Aig_Man_t * p, Aig_Obj_t * pObj )
|
||||
{
|
||||
return 3 & (p->pTerSimData[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
|
||||
}
|
||||
|
||||
static inline void Pdr_ManSimInfoSet( Aig_Man_t * p, Aig_Obj_t * pObj, int Value )
|
||||
{
|
||||
assert( Value >= PDR_ZER && Value <= PDR_UND );
|
||||
Value ^= Pdr_ManSimInfoGet( p, pObj );
|
||||
p->pTerSimData[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Marks the TFI cone and collects CIs and nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
|
||||
{
|
||||
assert( !Aig_IsComplement(pObj) );
|
||||
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
|
||||
return;
|
||||
Aig_ObjSetTravIdCurrent(pAig, pObj);
|
||||
if ( Aig_ObjIsPi(pObj) )
|
||||
{
|
||||
Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
|
||||
return;
|
||||
}
|
||||
Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
|
||||
if ( Aig_ObjIsPo(pObj) )
|
||||
return;
|
||||
Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
|
||||
Vec_IntPush( vNodes, Aig_ObjId(pObj) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Marks the TFI cone and collects CIs and nodes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
Vec_IntClear( vCiObjs );
|
||||
Vec_IntClear( vNodes );
|
||||
Aig_ManIncrementTravId( pAig );
|
||||
Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
|
||||
Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
|
||||
Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs ternary simulation for one node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
|
||||
{
|
||||
int Value0, Value1, Value;
|
||||
Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
|
||||
if ( Aig_ObjFaninC0(pObj) )
|
||||
Value0 = Pdr_ManSimInfoNot( Value0 );
|
||||
if ( Aig_ObjIsPo(pObj) )
|
||||
{
|
||||
Pdr_ManSimInfoSet( pAig, pObj, Value0 );
|
||||
return Value0;
|
||||
}
|
||||
assert( Aig_ObjIsNode(pObj) );
|
||||
Value1 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin1(pObj) );
|
||||
if ( Aig_ObjFaninC1(pObj) )
|
||||
Value1 = Pdr_ManSimInfoNot( Value1 );
|
||||
Value = Pdr_ManSimInfoAnd( Value0, Value1 );
|
||||
Pdr_ManSimInfoSet( pAig, pObj, Value );
|
||||
return Value;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs ternary simulation for one design.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManSimDataInit( Aig_Man_t * pAig,
|
||||
Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
|
||||
Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
// set the CI values
|
||||
Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE );
|
||||
Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
|
||||
Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) );
|
||||
// set the FOs to remove
|
||||
if ( vCi2Rem != NULL )
|
||||
Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
|
||||
Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
|
||||
// perform ternary simulation
|
||||
Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
|
||||
Pdr_ManExtendOneEval( pAig, pObj );
|
||||
// transfer results to the output
|
||||
Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
|
||||
Pdr_ManExtendOneEval( pAig, pObj );
|
||||
// check the results
|
||||
Aig_ManForEachNodeVec( pAig, vCoObjs, pObj, i )
|
||||
if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) )
|
||||
return 0;
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Tries to assign ternary value to one of the CIs.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec_Int_t * vVis )
|
||||
{
|
||||
Aig_Obj_t * pFanout;
|
||||
int i, k, iFanout, Value, Value2;
|
||||
assert( Saig_ObjIsLo(pAig, pObj) );
|
||||
assert( Aig_ObjIsTravIdCurrent(pAig, pObj) );
|
||||
// save original value
|
||||
Value = Pdr_ManSimInfoGet( pAig, pObj );
|
||||
assert( Value == PDR_ZER || Value == PDR_ONE );
|
||||
Vec_IntPush( vUndo, Aig_ObjId(pObj) );
|
||||
Vec_IntPush( vUndo, Value );
|
||||
// update original value
|
||||
Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
|
||||
// traverse
|
||||
Vec_IntClear( vVis );
|
||||
Vec_IntPush( vVis, Aig_ObjId(pObj) );
|
||||
Aig_ManForEachNodeVec( pAig, vVis, pObj, i )
|
||||
{
|
||||
Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k )
|
||||
{
|
||||
if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
|
||||
continue;
|
||||
assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
|
||||
Value = Pdr_ManSimInfoGet( pAig, pFanout );
|
||||
if ( Value == PDR_UND )
|
||||
continue;
|
||||
Value2 = Pdr_ManExtendOneEval( pAig, pFanout );
|
||||
if ( Value2 == Value )
|
||||
continue;
|
||||
assert( Value2 == PDR_UND );
|
||||
Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
|
||||
Vec_IntPush( vUndo, Value );
|
||||
if ( Aig_ObjIsPo(pFanout) )
|
||||
return 0;
|
||||
assert( Aig_ObjIsNode(pFanout) );
|
||||
Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
|
||||
}
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Undoes the partial results of ternary simulation.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i, Value;
|
||||
Aig_ManForEachNodeVec( pAig, vUndo, pObj, i )
|
||||
{
|
||||
Value = Vec_IntEntry(vUndo, ++i);
|
||||
assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND );
|
||||
Pdr_ManSimInfoSet( pAig, pObj, Value );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives the resulting cube.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem, Vec_Int_t * vRes, Vec_Int_t * vPiLits )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i, Lit;
|
||||
// mark removed flop outputs
|
||||
Aig_ManIncrementTravId( pAig );
|
||||
Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
|
||||
{
|
||||
assert( Saig_ObjIsLo( pAig, pObj ) );
|
||||
Aig_ObjSetTravIdCurrent(pAig, pObj);
|
||||
}
|
||||
// collect flop outputs that are not marked
|
||||
Vec_IntClear( vRes );
|
||||
Vec_IntClear( vPiLits );
|
||||
Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
|
||||
{
|
||||
if ( Saig_ObjIsPi(pAig, pObj) )
|
||||
{
|
||||
Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
|
||||
Vec_IntPush( vPiLits, Lit );
|
||||
continue;
|
||||
}
|
||||
assert( Saig_ObjIsLo(pAig, pObj) );
|
||||
if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
|
||||
continue;
|
||||
Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
|
||||
Vec_IntPush( vRes, Lit );
|
||||
}
|
||||
if ( Vec_IntSize(vRes) == 0 )
|
||||
Vec_IntPush(vRes, 0);
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Derives the resulting cube.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem )
|
||||
{
|
||||
Aig_Obj_t * pObj;
|
||||
int i;
|
||||
char * pBuff = ABC_ALLOC( char, Aig_ManPiNum(pAig)+1 );
|
||||
for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
|
||||
pBuff[i] = '-';
|
||||
pBuff[i] = 0;
|
||||
Aig_ManForEachNodeVec( pAig, vCiObjs, pObj, i )
|
||||
pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
|
||||
if ( vCi2Rem )
|
||||
Aig_ManForEachNodeVec( pAig, vCi2Rem, pObj, i )
|
||||
pBuff[Aig_ObjPioNum(pObj)] = 'x';
|
||||
printf( "%s\n", pBuff );
|
||||
ABC_FREE( pBuff );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Shrinks values using ternary simulation.]
|
||||
|
||||
Description [The cube contains the set of flop index literals which,
|
||||
when converted into a clause and applied to the combinational outputs,
|
||||
led to a satisfiable SAT run in frame k (values stored in the SAT solver).
|
||||
If the cube is NULL, it is assumed that the first property output was
|
||||
asserted and failed.
|
||||
The resulting array is a set of flop index literals that asserts the COs.
|
||||
Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
|
||||
{
|
||||
Vec_Int_t * vPrio = p->vPrio; // priority flops (flop indices)
|
||||
Vec_Int_t * vPiLits = p->vLits; // array of literals (0/1 PI values)
|
||||
Vec_Int_t * vCiObjs = p->vCiObjs; // cone leaves (CI obj IDs)
|
||||
Vec_Int_t * vCoObjs = p->vCoObjs; // cone roots (CO obj IDs)
|
||||
Vec_Int_t * vCiVals = p->vCiVals; // cone leaf values (0/1 CI values)
|
||||
Vec_Int_t * vCoVals = p->vCoVals; // cone root values (0/1 CO values)
|
||||
Vec_Int_t * vNodes = p->vNodes; // cone nodes (node obj IDs)
|
||||
Vec_Int_t * vUndo = p->vUndo; // cone undos (node obj IDs)
|
||||
Vec_Int_t * vVisits = p->vVisits; // intermediate (obj IDs)
|
||||
Vec_Int_t * vCi2Rem = p->vCi2Rem; // CIs to be removed (CI obj IDs)
|
||||
Vec_Int_t * vRes = p->vRes; // final result (flop literals)
|
||||
Aig_Obj_t * pObj;
|
||||
int i, Entry, RetValue;
|
||||
int clk = clock();
|
||||
|
||||
// collect CO objects
|
||||
Vec_IntClear( vCoObjs );
|
||||
if ( pCube == NULL ) // the target is the property output
|
||||
Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
|
||||
else // the target is the cube
|
||||
{
|
||||
for ( i = 0; i < pCube->nLits; i++ )
|
||||
{
|
||||
if ( pCube->Lits[i] == -1 )
|
||||
continue;
|
||||
pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1));
|
||||
Vec_IntPush( vCoObjs, Aig_ObjId(pObj) );
|
||||
}
|
||||
}
|
||||
if ( p->pPars->fVeryVerbose )
|
||||
{
|
||||
printf( "Trying to justify cube " );
|
||||
if ( pCube )
|
||||
Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
|
||||
else
|
||||
printf( "<prop=fail>" );
|
||||
printf( " in frame %d.\n", k );
|
||||
}
|
||||
|
||||
// collect CI objects
|
||||
Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes );
|
||||
// collect values
|
||||
Pdr_ManCollectValues( p, k, vCiObjs, vCiVals );
|
||||
Pdr_ManCollectValues( p, k, vCoObjs, vCoVals );
|
||||
// simulate for the first time
|
||||
if ( p->pPars->fVeryVerbose )
|
||||
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
|
||||
RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
|
||||
assert( RetValue );
|
||||
|
||||
// try removing high-priority flops
|
||||
Vec_IntClear( vCi2Rem );
|
||||
Aig_ManForEachNodeVec( p->pAig, vCiObjs, pObj, i )
|
||||
{
|
||||
if ( !Saig_ObjIsLo( p->pAig, pObj ) )
|
||||
continue;
|
||||
Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig);
|
||||
if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
|
||||
continue;
|
||||
Vec_IntClear( vUndo );
|
||||
if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
|
||||
Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
|
||||
else
|
||||
Pdr_ManExtendUndo( p->pAig, vUndo );
|
||||
}
|
||||
// try removing low-priority flops
|
||||
Aig_ManForEachNodeVec( p->pAig, vCiObjs, pObj, i )
|
||||
{
|
||||
if ( !Saig_ObjIsLo( p->pAig, pObj ) )
|
||||
continue;
|
||||
Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig);
|
||||
if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
|
||||
continue;
|
||||
Vec_IntClear( vUndo );
|
||||
if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
|
||||
Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
|
||||
else
|
||||
Pdr_ManExtendUndo( p->pAig, vUndo );
|
||||
}
|
||||
if ( p->pPars->fVeryVerbose )
|
||||
Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
|
||||
RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
|
||||
assert( RetValue );
|
||||
|
||||
// derive the set of resulting registers
|
||||
Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
|
||||
assert( Vec_IntSize(vRes) > 0 );
|
||||
p->tTsim += clock() - clk;
|
||||
return Pdr_SetCreate( vRes, vPiLits );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
@ -0,0 +1,547 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [pdrUtil.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Netlist representation.]
|
||||
|
||||
Synopsis [Various utilities.]
|
||||
|
||||
Author [Alan Mishchenko]
|
||||
|
||||
Affiliation [UC Berkeley]
|
||||
|
||||
Date [Ver. 1.0. Started - November 20, 2010.]
|
||||
|
||||
Revision [$Id: pdrUtil.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "pdrInt.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs fast mapping for one node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static inline void Vec_IntSelectSort( int * pArray, int nSize )
|
||||
{
|
||||
int temp, i, j, best_i;
|
||||
for ( i = 0; i < nSize-1; i++ )
|
||||
{
|
||||
best_i = i;
|
||||
for ( j = i+1; j < nSize; j++ )
|
||||
if ( pArray[j] < pArray[best_i] )
|
||||
best_i = j;
|
||||
temp = pArray[i];
|
||||
pArray[i] = pArray[best_i];
|
||||
pArray[best_i] = temp;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Set_t * Pdr_SetCreate( Vec_Int_t * vLits, Vec_Int_t * vPiLits )
|
||||
{
|
||||
Pdr_Set_t * p;
|
||||
int i;
|
||||
assert( Vec_IntSize(vLits) + Vec_IntSize(vPiLits) < (1<<15) );
|
||||
p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (Vec_IntSize(vLits) + Vec_IntSize(vPiLits)) * sizeof(int) );
|
||||
p->nLits = Vec_IntSize(vLits);
|
||||
p->nTotal = Vec_IntSize(vLits) + Vec_IntSize(vPiLits);
|
||||
p->nRefs = 1;
|
||||
p->Sign = 0;
|
||||
for ( i = 0; i < p->nLits; i++ )
|
||||
{
|
||||
p->Lits[i] = Vec_IntEntry(vLits, i);
|
||||
p->Sign |= ((word)1 << (p->Lits[i] % 63));
|
||||
}
|
||||
Vec_IntSelectSort( p->Lits, p->nLits );
|
||||
/*
|
||||
for ( i = 0; i < p->nLits; i++ )
|
||||
printf( "%d ", p->Lits[i] );
|
||||
printf( "\n" );
|
||||
*/
|
||||
// remember PI literals
|
||||
for ( i = p->nLits; i < p->nTotal; i++ )
|
||||
p->Lits[i] = Vec_IntEntry(vPiLits, i-p->nLits);
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Set_t * Pdr_SetCreateFrom( Pdr_Set_t * pSet, int iRemove )
|
||||
{
|
||||
Pdr_Set_t * p;
|
||||
int i, k = 0;
|
||||
assert( iRemove >= 0 && iRemove < pSet->nLits );
|
||||
p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (pSet->nTotal - 1) * sizeof(int) );
|
||||
p->nLits = pSet->nLits - 1;
|
||||
p->nTotal = pSet->nTotal - 1;
|
||||
p->nRefs = 1;
|
||||
p->Sign = 0;
|
||||
for ( i = 0; i < pSet->nTotal; i++ )
|
||||
{
|
||||
if ( i == iRemove )
|
||||
continue;
|
||||
p->Lits[k++] = pSet->Lits[i];
|
||||
if ( i >= pSet->nLits )
|
||||
continue;
|
||||
p->Sign |= ((word)1 << (pSet->Lits[i] % 63));
|
||||
}
|
||||
assert( k == p->nTotal );
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Set_t * Pdr_SetCreateSubset( Pdr_Set_t * pSet, int * pLits, int nLits )
|
||||
{
|
||||
Pdr_Set_t * p;
|
||||
int i, k = 0;
|
||||
assert( nLits >= 0 && nLits <= pSet->nLits );
|
||||
p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + (nLits + pSet->nTotal - pSet->nLits) * sizeof(int) );
|
||||
p->nLits = nLits;
|
||||
p->nTotal = nLits + pSet->nTotal - pSet->nLits;
|
||||
p->nRefs = 1;
|
||||
p->Sign = 0;
|
||||
for ( i = 0; i < nLits; i++ )
|
||||
{
|
||||
assert( pLits[i] >= 0 );
|
||||
p->Lits[k++] = pLits[i];
|
||||
p->Sign |= ((word)1 << (pLits[i] % 63));
|
||||
}
|
||||
Vec_IntSelectSort( p->Lits, p->nLits );
|
||||
for ( i = pSet->nLits; i < pSet->nTotal; i++ )
|
||||
p->Lits[k++] = pSet->Lits[i];
|
||||
assert( k == p->nTotal );
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Set_t * Pdr_SetDup( Pdr_Set_t * pSet )
|
||||
{
|
||||
Pdr_Set_t * p;
|
||||
int i;
|
||||
p = (Pdr_Set_t *)ABC_ALLOC( char, sizeof(Pdr_Set_t) + pSet->nTotal * sizeof(int) );
|
||||
p->nLits = pSet->nLits;
|
||||
p->nTotal = pSet->nTotal;
|
||||
p->nRefs = 1;
|
||||
p->Sign = pSet->Sign;
|
||||
for ( i = 0; i < pSet->nTotal; i++ )
|
||||
p->Lits[i] = pSet->Lits[i];
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Set_t * Pdr_SetRef( Pdr_Set_t * p )
|
||||
{
|
||||
p->nRefs++;
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_SetDeref( Pdr_Set_t * p )
|
||||
{
|
||||
if ( --p->nRefs == 0 )
|
||||
ABC_FREE( p );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_SetPrint( FILE * pFile, Pdr_Set_t * p, int nRegs, Vec_Int_t * vFlopCounts )
|
||||
{
|
||||
char * pBuff;
|
||||
int i, k, Entry;
|
||||
pBuff = ABC_ALLOC( char, nRegs + 1 );
|
||||
for ( i = 0; i < nRegs; i++ )
|
||||
pBuff[i] = '-';
|
||||
pBuff[i] = 0;
|
||||
for ( i = 0; i < p->nLits; i++ )
|
||||
{
|
||||
if ( p->Lits[i] == -1 )
|
||||
continue;
|
||||
pBuff[lit_var(p->Lits[i])] = (lit_sign(p->Lits[i])? '0':'1');
|
||||
}
|
||||
if ( vFlopCounts )
|
||||
{
|
||||
// skip some literals
|
||||
k = 0;
|
||||
Vec_IntForEachEntry( vFlopCounts, Entry, i )
|
||||
if ( Entry )
|
||||
pBuff[k++] = pBuff[i];
|
||||
pBuff[k] = 0;
|
||||
}
|
||||
fprintf( pFile, "%s", pBuff );
|
||||
ABC_FREE( pBuff );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Return 1 if pOld set-theoretically contains pNew.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_SetContains( Pdr_Set_t * pOld, Pdr_Set_t * pNew )
|
||||
{
|
||||
int * pOldInt, * pNewInt;
|
||||
assert( pOld->nLits > 0 );
|
||||
assert( pNew->nLits > 0 );
|
||||
if ( pOld->nLits < pNew->nLits )
|
||||
return 0;
|
||||
if ( (pOld->Sign & pNew->Sign) != pNew->Sign )
|
||||
return 0;
|
||||
pOldInt = pOld->Lits + pOld->nLits - 1;
|
||||
pNewInt = pNew->Lits + pNew->nLits - 1;
|
||||
while ( pNew->Lits <= pNewInt )
|
||||
{
|
||||
if ( pOld->Lits > pOldInt )
|
||||
return 0;
|
||||
assert( *pNewInt != -1 );
|
||||
assert( *pOldInt != -1 );
|
||||
if ( *pNewInt == *pOldInt )
|
||||
pNewInt--, pOldInt--;
|
||||
else if ( *pNewInt < *pOldInt )
|
||||
pOldInt--;
|
||||
else
|
||||
return 0;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Return 1 if the state cube contains init state (000...0).]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_SetIsInit( Pdr_Set_t * pCube, int iRemove )
|
||||
{
|
||||
int i;
|
||||
for ( i = 0; i < pCube->nLits; i++ )
|
||||
{
|
||||
assert( pCube->Lits[i] != -1 );
|
||||
if ( i == iRemove )
|
||||
continue;
|
||||
if ( lit_sign( pCube->Lits[i] ) == 0 )
|
||||
return 0;
|
||||
}
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_SetCompare( Pdr_Set_t ** pp1, Pdr_Set_t ** pp2 )
|
||||
{
|
||||
Pdr_Set_t * p1 = *pp1;
|
||||
Pdr_Set_t * p2 = *pp2;
|
||||
int i;
|
||||
for ( i = 0; i < p1->nLits && i < p2->nLits; i++ )
|
||||
{
|
||||
if ( p1->Lits[i] > p2->Lits[i] )
|
||||
return -1;
|
||||
if ( p1->Lits[i] < p2->Lits[i] )
|
||||
return 1;
|
||||
}
|
||||
if ( i == p1->nLits && i < p2->nLits )
|
||||
return -1;
|
||||
if ( i < p1->nLits && i == p2->nLits )
|
||||
return 1;
|
||||
return 0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Obl_t * Pdr_OblStart( int k, int prio, Pdr_Set_t * pState, Pdr_Obl_t * pNext )
|
||||
{
|
||||
Pdr_Obl_t * p;
|
||||
p = ABC_ALLOC( Pdr_Obl_t, 1 );
|
||||
p->iFrame = k;
|
||||
p->prio = prio;
|
||||
p->nRefs = 1;
|
||||
p->pState = pState;
|
||||
p->pNext = pNext;
|
||||
p->pLink = NULL;
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Obl_t * Pdr_OblRef( Pdr_Obl_t * p )
|
||||
{
|
||||
p->nRefs++;
|
||||
return p;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_OblDeref( Pdr_Obl_t * p )
|
||||
{
|
||||
if ( --p->nRefs == 0 )
|
||||
{
|
||||
if ( p->pNext )
|
||||
Pdr_OblDeref( p->pNext );
|
||||
Pdr_SetDeref( p->pState );
|
||||
ABC_FREE( p );
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Pdr_QueueIsEmpty( Pdr_Man_t * p )
|
||||
{
|
||||
return p->pQueue == NULL;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Obl_t * Pdr_QueueHead( Pdr_Man_t * p )
|
||||
{
|
||||
return p->pQueue;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
|
||||
{
|
||||
Pdr_Obl_t * pRes = p->pQueue;
|
||||
if ( p->pQueue == NULL )
|
||||
return NULL;
|
||||
p->pQueue = p->pQueue->pLink;
|
||||
Pdr_OblDeref( pRes );
|
||||
return pRes;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
|
||||
{
|
||||
Pdr_Obl_t * pTemp, ** ppPrev;
|
||||
p->nObligs++;
|
||||
Pdr_OblRef( pObl );
|
||||
if ( p->pQueue == NULL )
|
||||
{
|
||||
p->pQueue = pObl;
|
||||
return;
|
||||
}
|
||||
for ( ppPrev = &p->pQueue, pTemp = p->pQueue; pTemp; ppPrev = &pTemp->pLink, pTemp = pTemp->pLink )
|
||||
if ( pTemp->iFrame > pObl->iFrame || (pTemp->iFrame == pObl->iFrame && pTemp->prio > pObl->prio) )
|
||||
break;
|
||||
*ppPrev = pObl;
|
||||
pObl->pLink = pTemp;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_QueuePrint( Pdr_Man_t * p )
|
||||
{
|
||||
Pdr_Obl_t * pObl;
|
||||
for ( pObl = p->pQueue; pObl; pObl = pObl->pLink )
|
||||
printf( "Frame = %2d. Prio = %8d.\n", pObl->iFrame, pObl->prio );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Pdr_QueueStop( Pdr_Man_t * p )
|
||||
{
|
||||
Pdr_Obl_t * pObl;
|
||||
while ( !Pdr_QueueIsEmpty(p) )
|
||||
{
|
||||
pObl = Pdr_QueuePop(p);
|
||||
Pdr_OblDeref( pObl );
|
||||
}
|
||||
p->pQueue = NULL;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
Loading…
Reference in New Issue