Skip to content

A
abc
Commit 765a2124 by Alan Mishchenko
Options

Version abc71002

parent 4812c904
Showing with 521 additions and 28 deletions
abc.rc
......@@ -119,6 +119,6 @@ alias chnewrs "st; haig_start; resyn2rs; haig_use"
alias stdsd "r test/6in.blif; st; ps; u; bdd; dsd -g; st; ps"
alias trec "rec_start; r c.blif; st; rec_add; rec_use"
alias trec4 "rec_start -K 4; r i10.blif; st; rec_add; rec_use"
alias bmc "frames -i -F 10; orpos; iprove"
alias bmc2 "frames -i -F 10; orpos; iprove"
src/aig/aig/aig.h
......@@ -139,6 +139,7 @@ struct Aig_Man_t_
Aig_TMan_t * pManTime; // the timing manager
Vec_Ptr_t * vMapped;
Vec_Int_t * vFlopNums;
void * pSeqModel;
// timing statistics
int time1;
int time2;
......@@ -175,6 +176,14 @@ static inline int Aig_WordCountOnes( unsigned uWord )
uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
return (uWord & 0x0000FFFF) + (uWord>>16);
}
static inline int Aig_WordFindFirstBit( unsigned uWord )
{
int i;
for ( i = 0; i < 32; i++ )
if ( uWord & (1 << i) )
return i;
return -1;
}
static inline Aig_Obj_t * Aig_Regular( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) & ~01); }
static inline Aig_Obj_t * Aig_Not( Aig_Obj_t * p ) { return (Aig_Obj_t *)((unsigned long)(p) ^ 01); }
......
src/aig/aig/aigMan.c
......@@ -251,6 +251,7 @@ void Aig_ManStop( Aig_Man_t * p )
if ( p->vLevelR ) Vec_IntFree( p->vLevelR );
if ( p->vLevels ) Vec_VecFree( p->vLevels );
if ( p->vFlopNums) Vec_IntFree( p->vFlopNums );
FREE( p->pSeqModel );
FREE( p->pName );
FREE( p->pObjCopies );
FREE( p->pReprs );
......
src/aig/cnf/cnfWrite.c
......@@ -324,8 +324,8 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
Synopsis [Derives a simple CNF for the AIG.]
Description [The last argument shows the number of last outputs
of the manager, which will not be converted into clauses but the
new variables for which will be introduced.]
of the manager, which will not be converted into clauses.
New variables will be introduced for these outputs.]
SideEffects []
......
src/aig/fra/fra.h
......@@ -53,6 +53,7 @@ typedef struct Fra_Par_t_ Fra_Par_t;
typedef struct Fra_Man_t_ Fra_Man_t;
typedef struct Fra_Cla_t_ Fra_Cla_t;
typedef struct Fra_Sml_t_ Fra_Sml_t;
typedef struct Fra_Cex_t_ Fra_Cex_t;
typedef struct Fra_Bmc_t_ Fra_Bmc_t;
// FRAIG parameters
......@@ -118,6 +119,17 @@ struct Fra_Sml_t_
unsigned pData[0]; // simulation data for the nodes
};
// simulation manager
struct Fra_Cex_t_
{
int iPo; // the zero-based number of PO, for which verification failed
int iFrame; // the zero-based number of the time-frame, for which verificaiton failed
int nRegs; // the number of registers in the miter
int nPis; // the number of primary inputs in the miter
int nBits; // the number of words of bit data used
unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis)
};
// FRAIG manager
struct Fra_Man_t_
{
......@@ -227,6 +239,7 @@ extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
extern void Fra_BmcStop( Fra_Bmc_t * p );
extern void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
extern void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
/*=== fraClass.c ========================================================*/
extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
extern void Fra_ClassesStop( Fra_Cla_t * p );
......@@ -247,9 +260,10 @@ extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pO
/*=== fraCore.c ========================================================*/
extern void Fra_FraigSweep( Fra_Man_t * pManAig );
extern int Fra_FraigMiterStatus( Aig_Man_t * p );
extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
/*=== fraImp.c ========================================================*/
extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
......@@ -291,7 +305,11 @@ extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrame
extern void Fra_SmlStop( Fra_Sml_t * p );
extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
extern void Fra_SmlFreeCounterExample( Fra_Cex_t * p );
extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
extern Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
#ifdef __cplusplus
}
......
src/aig/fra/fraBmc.c
......@@ -213,6 +213,7 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
void Fra_BmcStop( Fra_Bmc_t * p )
{
Aig_ManStop( p->pAigFrames );
if ( p->pAigFraig )
Aig_ManStop( p->pAigFraig );
free( p->pObjToFrames );
free( p->pObjToFraig );
......@@ -230,7 +231,7 @@ void Fra_BmcStop( Fra_Bmc_t * p )
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p, int fKeepPos )
{
Aig_Man_t * pAigFrames;
Aig_Obj_t * pObj, * pObjNew;
......@@ -274,11 +275,20 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
assert( k == Aig_ManRegNum(p->pAig) );
}
free( pLatches );
if ( fKeepPos )
{
for ( f = 0; f < p->nFramesAll; f++ )
Aig_ManForEachPoSeq( p->pAig, pObj, i )
Aig_ObjCreatePo( pAigFrames, Bmc_ObjChild0Frames(pObj,f) );
Aig_ManCleanup( pAigFrames );
}
else
{
// add POs to all the dangling nodes
Aig_ManForEachObj( pAigFrames, pObjNew, i )
if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
Aig_ObjCreatePo( pAigFrames, pObjNew );
}
// return the new manager
return pAigFrames;
}
......@@ -301,7 +311,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
assert( p->pBmc == NULL );
// derive and fraig the frames
p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc, 0 );
// if implications are present, configure the AIG manager to check them
if ( p->pCla->vImps )
{
......@@ -310,7 +320,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
p->pBmc->vImps = p->pCla->vImps;
nImpsOld = Vec_IntSize(p->pCla->vImps);
}
p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 );
p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000, 0 );
p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
p->pBmc->pAigFrames->pObjCopies = NULL;
// annotate frames nodes with pointers to the manager
......@@ -354,6 +364,56 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
p->pBmc = NULL;
}
/**Function*************************************************************
Synopsis [Performs BMC for the given AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose )
{
extern Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig );
Fra_Man_t * pTemp;
Fra_Bmc_t * pBmc;
Aig_Man_t * pAigTemp;
int iOutput;
// derive and fraig the frames
pBmc = Fra_BmcStart( pAig, 0, nFrames );
pTemp = Fra_LcrAigPrepare( pAig );
pTemp->pBmc = pBmc;
pBmc->pAigFrames = Fra_BmcFrames( pBmc, 1 );
if ( fRewrite )
{
pBmc->pAigFrames = Dar_ManRwsat( pAigTemp = pBmc->pAigFrames, 1, 0 );
Aig_ManStop( pAigTemp );
}
iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames );
if ( iOutput >= 0 )
pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
else
{
pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 );
iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFraig );
if ( pBmc->pAigFraig->pData )
{
pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pBmc->pAigFrames, pBmc->pAigFraig->pData );
FREE( pBmc->pAigFraig->pData );
}
else if ( iOutput >= 0 )
pAig->pSeqModel = Fra_SmlTrivCounterExample( pAig, iOutput );
}
if ( fVerbose )
printf( "nFrames = %3d. Aig = %6d. Init frames = %6d. Fraiged init frames = %6d.\n",
nFrames, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pBmc->pAigFrames), pBmc->pAigFraig? Aig_ManNodeNum(pBmc->pAigFraig) : -1 );
Fra_BmcStop( pBmc );
free( pTemp );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/aig/fra/fraCore.c
......@@ -58,27 +58,27 @@
***********************************************************************/
int Fra_FraigMiterStatus( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pObjNew;
Aig_Obj_t * pObj, * pChild;
int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
if ( p->pData )
return 0;
Aig_ManForEachPoSeq( p, pObj, i )
{
pObjNew = Aig_ObjChild0(pObj);
pChild = Aig_ObjChild0(pObj);
// check if the output is constant 0
if ( pObjNew == Aig_ManConst0(p) )
if ( pChild == Aig_ManConst0(p) )
{
CountConst0++;
continue;
}
// check if the output is constant 1
if ( pObjNew == Aig_ManConst1(p) )
if ( pChild == Aig_ManConst1(p) )
{
CountNonConst0++;
continue;
}
// check if the output can be not constant 0
if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
{
CountNonConst0++;
continue;
......@@ -104,6 +104,37 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
/**Function*************************************************************
Synopsis [Reports the status of the miter.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_FraigMiterAssertedOutput( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pChild;
int i;
Aig_ManForEachPoSeq( p, pObj, i )
{
pChild = Aig_ObjChild0(pObj);
// check if the output is constant 0
if ( pChild == Aig_ManConst0(p) )
continue;
// check if the output is constant 1
if ( pChild == Aig_ManConst1(p) )
return i;
// check if the output can be not constant 0
if ( Aig_Regular(pChild)->fPhase != (unsigned)Aig_IsComplement(pChild) )
return i;
}
return -1;
}
/**Function*************************************************************
Synopsis [Write speculative miter for one node.]
Description []
......@@ -410,7 +441,7 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
SeeAlso []
***********************************************************************/
Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve )
{
Aig_Man_t * pFraig;
Fra_Par_t Pars, * pPars = &Pars;
......@@ -419,7 +450,7 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
pPars->fChoicing = 0;
pPars->fDoSparse = 1;
pPars->fSpeculate = 0;
pPars->fProve = 0;
pPars->fProve = fProve;
pPars->fVerbose = 0;
pPars->fDontShowBar = 1;
pFraig = Fra_FraigPerform( pManAig, pPars );
......
src/aig/fra/fraLcr.c
......@@ -159,7 +159,8 @@ Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
int i;
p = ALLOC( Fra_Man_t, 1 );
memset( p, 0, sizeof(Fra_Man_t) );
Aig_ManForEachPi( pAig, pObj, i )
// Aig_ManForEachPi( pAig, pObj, i )
Aig_ManForEachObj( pAig, pObj, i )
pObj->pData = p;
return p;
}
......@@ -532,6 +533,7 @@ timeSim = clock() - clk2;
// check if simulation discovered non-constant-0 POs
if ( fProve && pSml->fNonConstOut )
{
pAig->pSeqModel = Fra_SmlGetCounterExample( pSml );
Fra_SmlStop( pSml );
return NULL;
}
......@@ -587,7 +589,7 @@ clk2 = clock();
pAigPart = Fra_LcrCreatePart( p, vPart );
p->timeTrav += clock() - clk2;
clk2 = clock();
pAigNew = Fra_FraigEquivence( pAigPart, nConfMax );
pAigNew = Fra_FraigEquivence( pAigPart, nConfMax, 0 );
p->timeFraig += clock() - clk2;
Vec_PtrPush( p->vFraigs, pAigNew );
Aig_ManStop( pAigPart );
......
src/aig/fra/fraSec.c
......@@ -150,6 +150,7 @@ clk = clock();
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
Aig_ManStop( pTemp );
if ( pNew == NULL )
{
......@@ -169,7 +170,7 @@ PRT( "Time", clock() - clk );
// perform fraiging
clk = clock();
pNew = Fra_FraigEquivence( pTemp = pNew, 100 );
pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
......@@ -240,6 +241,7 @@ PRT( "Time", clock() - clk );
}
if ( pSml->fNonConstOut )
{
p->pSeqModel = Fra_SmlGetCounterExample( pSml );
Fra_SmlStop( pSml );
Aig_ManStop( pNew );
RetValue = 0;
......
src/aig/fra/fraSim.c
......@@ -252,12 +252,14 @@ void Fra_SmlSavePattern( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo )
{
Aig_Obj_t * pFanin, * pObjPi;
unsigned * pSims;
int i, k, BestPat, * pModel;
// find the word of the pattern
pSims = Fra_ObjSim(p->pSml, pObj->Id);
pFanin = Aig_ObjFanin0(pObjPo);
pSims = Fra_ObjSim(p->pSml, pFanin->Id);
for ( i = 0; i < p->pSml->nWordsTotal; i++ )
if ( pSims[i] )
break;
......@@ -270,12 +272,13 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
// determine the best pattern
BestPat = i * 32 + k;
// fill in the counter-example data
pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
Aig_ManForEachPi( p->pManAig, pObj, i )
pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 );
Aig_ManForEachPi( p->pManAig, pObjPi, i )
{
pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObj->Id), BestPat);
pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
// printf( "%d", pModel[i] );
}
pModel[Aig_ManPiNum(p->pManAig)] = pObjPo->Id;
// printf( "\n" );
// set the model
assert( p->pManFraig->pData == NULL );
......@@ -306,7 +309,7 @@ int Fra_SmlCheckOutput( Fra_Man_t * p )
if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
{
// create the counter-example from this pattern
Fra_SmlCheckOutputSavePattern( p, Aig_ObjFanin0(pObj) );
Fra_SmlCheckOutputSavePattern( p, pObj );
return 1;
}
}
......@@ -680,6 +683,8 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
// start the classes
Fra_SmlInitialize( p->pSml, fInit );
Fra_SmlSimulateOne( p->pSml );
if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
return;
Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
// Fra_ClassesPrint( p->pCla, 0 );
if ( fVerbose )
......@@ -816,6 +821,244 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
return p;
}
/**Function*************************************************************
Synopsis [Resimulates the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
{
Fra_Sml_t * pSml;
Aig_Obj_t * pObj;
int RetValue, i, k, iBit;
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
// start a new sequential simulator
pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
// assign simulation info for the registers
iBit = 0;
Aig_ManForEachLoSeq( pAig, pObj, i )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
// assign simulation info for the primary inputs
for ( i = 0; i <= p->iFrame; i++ )
Aig_ManForEachPiSeq( pAig, pObj, k )
Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
assert( iBit == p->nBits );
// run random simulation
Fra_SmlSimulateOne( pSml );
// check if the given output has failed
RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
Fra_SmlStop( pSml );
return RetValue;
}
/**Function*************************************************************
Synopsis [Allocates a counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Cex_t * Fra_SmlAllocCounterExample( int nRegs, int nRealPis, int nFrames )
{
Fra_Cex_t * pCex;
int nWords = Aig_BitWordNum( nRegs + nRealPis * nFrames );
pCex = (Fra_Cex_t *)malloc( sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
memset( pCex, 0, sizeof(Fra_Cex_t) + sizeof(unsigned) * nWords );
pCex->nRegs = nRegs;
pCex->nPis = nRealPis;
pCex->nBits = nRegs + nRealPis * nFrames;
return pCex;
}
/**Function*************************************************************
Synopsis [Frees the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_SmlFreeCounterExample( Fra_Cex_t * pCex )
{
free( pCex );
}
/**Function*************************************************************
Synopsis [Creates sequential counter-example from the simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
{
Fra_Cex_t * pCex;
Aig_Obj_t * pObj;
unsigned * pSims;
int iPo, iFrame, iBit, i, k;
// make sure the simulation manager has it
assert( p->fNonConstOut );
// find the first output that failed
iPo = -1;
iBit = -1;
iFrame = -1;
Aig_ManForEachPoSeq( p->pAig, pObj, iPo )
{
if ( Fra_SmlNodeIsZero(p, pObj) )
continue;
pSims = Fra_ObjSim( p, pObj->Id );
for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
if ( pSims[i] )
{
iFrame = i / p->nWordsFrame;
iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
break;
}
break;
}
assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
assert( iFrame < p->nFrames );
assert( iBit < 32 * p->nWordsFrame );
// allocate the counter example
pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
// copy the bit data
Aig_ManForEachLoSeq( p->pAig, pObj, k )
{
pSims = Fra_ObjSim( p, pObj->Id );
if ( Aig_InfoHasBit( pSims, iBit ) )
Aig_InfoSetBit( pCex->pData, k );
}
for ( i = 0; i <= iFrame; i++ )
{
Aig_ManForEachPiSeq( p->pAig, pObj, k )
{
pSims = Fra_ObjSim( p, pObj->Id );
if ( Aig_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
}
}
// verify the counter example
if ( !Fra_SmlRunCounterExample( p->pAig, pCex ) )
{
printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
Fra_SmlFreeCounterExample( pCex );
pCex = NULL;
}
return pCex;
}
/**Function*************************************************************
Synopsis [Generates seq counter-example from the combinational one.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel )
{
Fra_Cex_t * pCex;
Aig_Obj_t * pObj;
int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
// get the number of frames
assert( Aig_ManRegNum(pAig) > 0 );
assert( Aig_ManRegNum(pFrames) == 0 );
nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
nFrames = Aig_ManPiNum(pFrames) / nTruePis;
assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) );
assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) );
// find the PO that failed
iPo = -1;
iFrame = -1;
Aig_ManForEachPo( pFrames, pObj, i )
if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] )
{
iPo = i % nTruePos;
iFrame = i / nTruePos;
break;
}
assert( iPo >= 0 );
// allocate the counter example
pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
// copy the bit data
for ( i = 0; i < Aig_ManPiNum(pFrames); i++ )
{
if ( pModel[i] )
Aig_InfoSetBit( pCex->pData, pCex->nRegs + i );
if ( pCex->nRegs + i == pCex->nBits - 1 )
break;
}
// verify the counter example
if ( !Fra_SmlRunCounterExample( pAig, pCex ) )
{
printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
Fra_SmlFreeCounterExample( pCex );
pCex = NULL;
}
return pCex;
}
/**Function*************************************************************
Synopsis [Make the trivial counter-example for the trivially asserted output.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
{
Fra_Cex_t * pCex;
int nTruePis, nTruePos, iPo, iFrame;
assert( Aig_ManRegNum(pAig) > 0 );
nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig);
nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig);
iPo = iFrameOut % nTruePos;
iFrame = iFrameOut / nTruePos;
// allocate the counter example
pCex = Fra_SmlAllocCounterExample( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
pCex->iPo = iPo;
pCex->iFrame = iFrame;
return pCex;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/abc/abc.h
......@@ -197,6 +197,7 @@ struct Abc_Ntk_t_
Vec_Int_t * vLevelsR; // level in the reverse topological order (for AIGs)
Vec_Ptr_t * vSupps; // CO support information
int * pModel; // counter-example (for miters)
void * pSeqModel; // counter-example (for sequential miters)
Abc_Ntk_t * pExdc; // the EXDC network (if given)
void * pData; // misc
Abc_Ntk_t * pCopy;
......
src/base/abc/abcNtk.c
......@@ -979,7 +979,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
Vec_PtrFree( pNtk->vObjs );
Vec_PtrFree( pNtk->vBoxes );
if ( pNtk->vLevelsR ) Vec_IntFree( pNtk->vLevelsR );
if ( pNtk->pModel ) free( pNtk->pModel );
FREE( pNtk->pModel );
FREE( pNtk->pSeqModel );
TotalMemory = 0;
TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj) : 0;
TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
......
src/base/abci/abcDar.c
......@@ -1070,6 +1070,44 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
SeeAlso []
***********************************************************************/
int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fVerbose )
{
Aig_Man_t * pMan;
int clk = clock();
// derive the AIG manager
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
{
printf( "Converting miter into AIG has failed.\n" );
return -1;
}
assert( pMan->nRegs > 0 );
// perform verification
Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
}
else
printf( "No output was asserted after BMC with %d frames. ", nFrames );
PRT( "Time", clock() - clk );
Aig_ManStop( pMan );
return 1;
}
/**Function*************************************************************
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pMan;
......@@ -1084,6 +1122,12 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbo
assert( pMan->nRegs > 0 );
// perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace).\n", pCex->iPo, pCex->iFrame );
}
Aig_ManStop( pMan );
return RetValue;
}
......@@ -1238,6 +1282,46 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
return pNtkAig;
}
/**Function*************************************************************
Synopsis [Performs random simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
{
Aig_Man_t * pMan;
Fra_Sml_t * pSml;
Fra_Cex_t * pCex;
int RetValue, clk = clock();
pMan = Abc_NtkToDar( pNtk, 1 );
pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
if ( pSml->fNonConstOut )
{
pCex = Fra_SmlGetCounterExample( pSml );
if ( pCex )
printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
nFrames, nWords, pCex->iPo, pCex->iFrame );
pNtk->pSeqModel = pCex;
RetValue = 1;
}
else
{
RetValue = 0;
printf( "Simulation of %d frames with %d words did not assert the outputs. ",
nFrames, nWords );
}
PRT( "Time", clock() - clk );
Fra_SmlStop( pSml );
Aig_ManStop( pMan );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/base/io/io.c
......@@ -1569,6 +1569,8 @@ usage:
return 1;
}
#include "fra.h"
/**Function*************************************************************
Synopsis []
......@@ -1617,13 +1619,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
// get the input file name
pFileName = argv[globalUtilOptind];
if ( pNtk->pModel == NULL )
if ( pNtk->pModel == NULL && pNtk->pSeqModel == NULL )
{
fprintf( pAbc->Out, "Counter-example is not available.\n" );
return 0;
}
// write the counter-example into the file
if ( pNtk->pModel )
{
Abc_Obj_t * pObj;
FILE * pFile = fopen( pFileName, "w" );
......@@ -1646,12 +1649,50 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
fprintf( pFile, "\n" );
fclose( pFile );
}
else
{
Fra_Cex_t * pCex = pNtk->pSeqModel;
Abc_Obj_t * pObj;
FILE * pFile;
int i, f;
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( !Abc_LatchIsInit0(pObj) )
{
fprintf( stdout, "IoCommandWriteCounter(): The init-state should be all-0 for counter-example to work.\n" );
fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
return 1;
}
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
return 1;
}
if ( fNames )
{
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "%s@0=%c ", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
for ( f = 0; f <= pCex->iFrame; f++ )
Abc_NtkForEachPi( pNtk, pObj, i )
fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
}
else
{
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
for ( i = pCex->nRegs; i < pCex->nBits; i++ )
fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) );
}
fprintf( pFile, "\n" );
fclose( pFile );
}
return 0;
usage:
fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" );
fprintf( pAbc->Err, "\t writes the counter-example derived by \"prove\" or \"sat\"\n" );
fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" );
fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment