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

Changes to support sequential verification with reduction without speculation.

This commit is contained in:
Alan Mishchenko 2011-02-19 16:47:05 -08:00
parent 2619edf8c0
commit e3f88c81c6
5 changed files with 243 additions and 421 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/cec/cecSeq.c
View File

@ -393,7 +393,7 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
// write equivalence classes
Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
// reduce the model
pReduce = Gia_ManSpecReduce( pAig, 0, 0, 0 );
pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0 );
if ( pReduce )
{
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );

2
src/aig/gia/gia.h
View File

@ -659,7 +659,7 @@ extern void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose
extern Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
extern Gia_Man_t * Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq, int fMiterPairs );
extern int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fReduce, int fVerbose );
extern Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames, int fDualOut );
extern Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs );
extern void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );

79
src/aig/gia/giaEquiv.c
View File

@ -748,7 +748,7 @@ int Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose )
SeeAlso []
***********************************************************************/
static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut )
static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate )
{
Gia_Obj_t * pRepr;
unsigned iLitNew;
@ -761,7 +761,8 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) )
Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, pObj->Value, iLitNew) );
pObj->Value = iLitNew;
if ( fSpeculate )
pObj->Value = iLitNew;
}
/**Function*************************************************************
@ -798,15 +799,15 @@ int Gia_ManHasNoEquivs( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut )
void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXorLits, int fDualOut, int fSpeculate )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), vXorLits, fDualOut, fSpeculate );
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate );
}
/**Function*************************************************************
@ -820,7 +821,7 @@ void Gia_ManSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, V
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fVerbose )
Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int fSpeculate, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
@ -862,9 +863,9 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut );
Gia_ManSpecBuild( pNew, p, pObj, vXorLits, fDualOut, fSpeculate );
Gia_ManForEachCo( p, pObj, i )
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut );
Gia_ManSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), vXorLits, fDualOut, fSpeculate );
if ( !fSynthesis )
{
Gia_ManForEachPo( p, pObj, i )
@ -1125,6 +1126,62 @@ void Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose )
nRemovedClas, nTotalClas, nRemovedLits, nTotalLits );
}
/**Function*************************************************************
Synopsis [Marks proved equivalences.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fVerbose )
{
Gia_Man_t * pMiter;
Gia_Obj_t * pObj;
int i, nLits = 0;
int nLitsAll, Counter = 0;
nLitsAll = Gia_ManEquivCountLitsAll( p );
if ( nLitsAll == 0 )
{
printf( "Gia_ManEquivMark(): Current AIG does not have equivalences.\n" );
return;
}
// read AIGER file
pMiter = Gia_ReadAiger( pFileName, 0 );
if ( pMiter == NULL )
{
printf( "Gia_ManEquivMark(): Input file %s could not be read.\n", pFileName );
return;
}
if ( Gia_ManPoNum(pMiter) != Gia_ManPoNum(p) + nLitsAll )
{
printf( "Gia_ManEquivMark(): The number of POs is not correct: MiterPONum(%d) != AIGPONum(%d) + AIGEquivNum(%d).\n",
Gia_ManPoNum(pMiter), Gia_ManPoNum(p), nLitsAll );
Gia_ManStop( pMiter );
return;
}
// mark corresponding POs as solved
nLits = 0;
for ( i = 0; i < Gia_ManObjNum(p); i++ )
{
if ( Gia_ObjRepr(p, i) == GIA_VOID )
continue;
pObj = Gia_ManPo( pMiter, Gia_ManPoNum(p) + nLits++ );
if ( Gia_ObjFaninLit0p(pMiter, pObj) == 0 ) // const 0 - proven
{
Gia_ObjSetProved(p, i);
Counter++;
}
}
if ( fVerbose )
printf( "Set %d equivalences as proved.\n", Counter );
assert( nLits == nLitsAll );
Gia_ManStop( pMiter );
}
/**Function*************************************************************
Synopsis [Transforms equiv classes by setting a good representative.]
@ -1534,7 +1591,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
break;
}
pSrm = Gia_ManSpecReduce( pGia, 0, 0, 0 );
pSrm = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 );
// bmc2 -F 100 -C 25000
{
Abc_Cex_t * pCex;
@ -1571,7 +1628,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
// write equivalence classes
Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
// reduce the model
pReduce = Gia_ManSpecReduce( pGia, 0, 0, 0 );
pReduce = Gia_ManSpecReduce( pGia, 0, 0, 1, 0 );
if ( pReduce )
{
pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );

176
src/aig/ivy/ivyFraig.c
View File

@ -200,6 +200,7 @@ static void Ivy_FraigMiterPrint( Ivy_Man_t * pNtk, char * pString, int
static int * Ivy_FraigCreateModel( Ivy_FraigMan_t * p );
static int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 );
static int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit );
static ABC_INT64_T s_nBTLimitGlobal = 0;
static ABC_INT64_T s_nInsLimitGlobal = 0;
@ -593,10 +594,10 @@ Ivy_FraigMan_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParam
}
assert( k == Ivy_ManObjNum(pManAig) );
// allocate storage for sim pattern
p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords );
p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords );
p->pPatScores = ABC_ALLOC( int, 32 * p->nSimWords );
p->vPiVars = Vec_PtrAlloc( 100 );
p->vPiVars = Vec_PtrAlloc( 100 );
// set random number generator
srand( 0xABCABC );
return p;
@ -1992,6 +1993,7 @@ p->nClassesEnd = p->lClasses.nItems;
if ( Ivy_ObjFaninVec(pObj) )
Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
pObj->pNextFan0 = pObj->pNextFan1 = NULL;
pObj->pEquiv = NULL;
}
// remove dangling nodes
Ivy_ManCleanup( p->pManFraig );
@ -2154,6 +2156,14 @@ p->timeSatSat += clock() - clk;
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
/*
if ( nBTLimit > 1000 )
{
RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit );
if ( RetValue != -1 )
return RetValue;
}
*/
// mark the node as the failed node
if ( pOld != p->pManFraig->pConst1 )
pOld->fFailTfo = 1;
@ -2197,6 +2207,14 @@ p->timeSatSat += clock() - clk;
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
/*
if ( nBTLimit > 1000 )
{
RetValue = Ivy_FraigCheckCone( p, p->pManFraig, pOld, pNew, nBTLimit );
if ( RetValue != -1 )
return RetValue;
}
*/
// mark the node as the failed node
pOld->fFailTfo = 1;
pNew->fFailTfo = 1;
@ -2286,6 +2304,14 @@ p->timeSatSat += clock() - clk;
else // if ( RetValue1 == l_Undef )
{
p->timeSatFail += clock() - clk;
/*
if ( p->pParams->nBTLimitMiter > 1000 )
{
RetValue = Ivy_FraigCheckCone( p, p->pManFraig, p->pManFraig->pConst1, pNew, p->pParams->nBTLimitMiter );
if ( RetValue != -1 )
return RetValue;
}
*/
// mark the node as the failed node
pNew->fFailTfo = 1;
p->nSatFailsReal++;
@ -2773,6 +2799,150 @@ int Ivy_FraigNodesAreEquivBdd( Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2 )
return RetValue;
}
ABC_NAMESPACE_IMPL_END
#include "aig.h"
ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis [Computes truth table of the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ivy_FraigExtractCone_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
{
if ( pNode->fMarkB )
return;
pNode->fMarkB = 1;
if ( Ivy_ObjIsPi(pNode) )
{
Vec_IntPush( vLeaves, pNode->Id );
return;
}
assert( Ivy_ObjIsAnd(pNode) );
Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin0(pNode), vLeaves, vNodes );
Ivy_FraigExtractCone_rec( p, Ivy_ObjFanin1(pNode), vLeaves, vNodes );
Vec_IntPush( vNodes, pNode->Id );
}
/**Function*************************************************************
Synopsis [Checks equivalence using BDDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ivy_FraigExtractCone( Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, Vec_Int_t * vLeaves )
{
Aig_Man_t * pMan;
Aig_Obj_t * pMiter;
Vec_Int_t * vNodes;
Ivy_Obj_t * pObjIvy;
int i;
// collect nodes
vNodes = Vec_IntAlloc( 100 );
Ivy_ManConst1(p)->fMarkB = 1;
Ivy_FraigExtractCone_rec( p, pObj1, vLeaves, vNodes );
Ivy_FraigExtractCone_rec( p, pObj2, vLeaves, vNodes );
Ivy_ManConst1(p)->fMarkB = 0;
// create new manager
pMan = Aig_ManStart( 1000 );
Ivy_ManConst1(p)->pEquiv = (Ivy_Obj_t *)Aig_ManConst1(pMan);
Ivy_ManForEachNodeVec( p, vLeaves, pObjIvy, i )
{
pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_ObjCreatePi( pMan );
pObjIvy->fMarkB = 0;
}
// duplicate internal nodes
Ivy_ManForEachNodeVec( p, vNodes, pObjIvy, i )
{
pObjIvy->pEquiv = (Ivy_Obj_t *)Aig_And( pMan, (Aig_Obj_t *)Ivy_ObjChild0Equiv(pObjIvy), (Aig_Obj_t *)Ivy_ObjChild1Equiv(pObjIvy) );
pObjIvy->fMarkB = 0;
pMiter = (Aig_Obj_t *)pObjIvy->pEquiv;
assert( pMiter->fPhase == pObjIvy->fPhase );
}
// create the PO
pMiter = Aig_Exor( pMan, (Aig_Obj_t *)pObj1->pEquiv, (Aig_Obj_t *)pObj2->pEquiv );
pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
/*
printf( "Polarity = %d\n", pMiter->fPhase );
if ( Ivy_ObjIsConst1(pObj1) || Ivy_ObjIsConst1(pObj2) )
{
pMiter = Aig_NotCond( pMiter, 1 );
printf( "***************\n" );
}
*/
pMiter = Aig_ObjCreatePo( pMan, pMiter );
//printf( "Polarity = %d\n", pMiter->fPhase );
Aig_ManCleanup( pMan );
Vec_IntFree( vNodes );
return pMan;
}
/**Function*************************************************************
Synopsis [Checks equivalence using BDDs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
{
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
Vec_Int_t * vLeaves;
Aig_Man_t * pMan;
Aig_Obj_t * pObj;
int i, RetValue;
vLeaves = Vec_IntAlloc( 100 );
pMan = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves );
RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 1 );
if ( RetValue == 0 )
{
int Counter = 0;
memset( pGlo->pPatWords, 0, sizeof(unsigned) * pGlo->nPatWords );
Aig_ManForEachPi( pMan, pObj, i )
if ( ((int *)pMan->pData)[i] )
{
int iObjIvy = Vec_IntEntry( vLeaves, i );
assert( iObjIvy > 0 && iObjIvy <= Ivy_ManPiNum(p) );
Ivy_InfoSetBit( pGlo->pPatWords, iObjIvy-1 );
//printf( "%d ", iObjIvy );
Counter++;
}
assert( Counter > 0 );
}
Vec_IntFree( vLeaves );
if ( RetValue == 1 )
printf( "UNSAT\n" );
else if ( RetValue == 0 )
printf( "SAT\n" );
else if ( RetValue == -1 )
printf( "UNDEC\n" );
// p->pModel = (int *)pMan->pData, pMan2->pData = NULL;
Aig_ManStop( pMan );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

405
src/base/abci/abcDprove2.c
View File

@ -1,405 +0,0 @@
/**CFile****************************************************************
FileName [abcDprove2.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Implementation of "dprove2".]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcDprove2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "aig.h"
#include "saig.h"
#include "fra.h"
#include "ssw.h"
#include "gia.h"
#include "giaAig.h"
#include "cec.h"
#include "int.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars );
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar );
extern void * Abc_FrameReadSave1();
extern void * Abc_FrameReadSave2();
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Implements model checking based on abstraction and speculation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkDProve2( Abc_Ntk_t * pNtk, int nConfLast, int fSeparate, int fVeryVerbose, int fVerbose )
{
Abc_Ntk_t * pNtk2;
Aig_Man_t * pMan, * pTemp;
Aig_Man_t * pSave1 = NULL;
Gia_Man_t * pGia, * pSrm;
int spectried = 0;
int absquit = 0;
int absfail = 0;
int RetValue = -1;
int clkTotal = clock();
// derive the AIG manager
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
{
printf( "Converting miter into AIG has failed.\n" );
return RetValue;
}
assert( pMan->nRegs > 0 );
if ( fVerbose )
{
printf( "Starting BMC...\n" );
Aig_ManPrintStats( pMan );
}
// bmc2 -C 10000
{
int nFrames = 2000;
int nNodeDelta = 2000;
int nBTLimit = 10000; // different from default
int nBTLimitAll = 2000000;
Saig_BmcPerform( pMan, 0, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVeryVerbose, 0, NULL );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
goto finish;
}
if ( fVerbose )
{
printf( "Starting \"dprove\"...\n" );
Aig_ManPrintStats( pMan );
}
// dprove -r -F 8
{
Fra_Sec_t SecPar, * pSecPar = &SecPar;
Fra_SecSetDefaultParams( pSecPar );
pSecPar->fTryBmc ^= 1;
pSecPar->fRetimeFirst ^= 1;
pSecPar->nFramesMax = 8;
pSecPar->fInterSeparate = 0; //fSeparate;
pSecPar->fVerbose = fVeryVerbose;
RetValue = Abc_NtkDarProve( pNtk, pSecPar );
// analize the result
if ( RetValue != -1 )
goto finish;
}
Aig_ManStop( pMan );
pSave1 = (Aig_Man_t *)Abc_FrameReadSave1();
pMan = Aig_ManDupSimple( pSave1 );
// abstraction
if ( fVerbose )
{
printf( "Abstraction...\n" );
Aig_ManPrintStats( pMan );
}
abstraction:
{
Gia_ParAbs_t Pars, * pPars = &Pars;
Gia_ManAbsSetDefaultParams( pPars );
pPars->nConfMaxBmc = 25000;
pPars->nRatio = 2;
pPars->fVerbose = fVeryVerbose;
/*
int nFramesMax = 10;
int nConfMax = 10000;
int fDynamic = 1;
int fExtend = 0;
int fSkipProof = 0;
int nFramesBmc = 2000;
int nConfMaxBmc = 25000; // default 5000;
int nRatio = 2; // default 10;
int fUseBdds = 0;
int fUseDprove = 0;
int fVerbose = fVeryVerbose;
fExtend ^= 1;
fSkipProof ^= 1;
*/
pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
// if abstractin has solved the problem
if ( pTemp->pSeqModel )
{
pNtk->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
Aig_ManStop( pTemp );
goto finish;
}
Aig_ManStop( pTemp );
if ( pMan == NULL ) // abstraction quits
{
absquit = 1;
pMan = Aig_ManDupSimple( pSave1 );
goto speculation;
}
}
if ( fVerbose )
{
printf( "Problem before trimming...\n" );
Aig_ManPrintStats( pMan );
}
// trim off useless primary inputs
pMan = Aig_ManDupTrim( pTemp = pMan );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "\"dprove\" after abstraction...\n" );
Aig_ManPrintStats( pMan );
}
// dprove -r -F 8
{
Fra_Sec_t SecPar, * pSecPar = &SecPar;
Fra_SecSetDefaultParams( pSecPar );
pSecPar->fTryBmc ^= 1;
pSecPar->fRetimeFirst ^= 1;
pSecPar->nFramesMax = 8;
pSecPar->fInterSeparate = 0; //fSeparate;
pSecPar->fVerbose = fVeryVerbose;
// convert pMan into pNtk
pNtk2 = Abc_NtkFromAigPhase( pMan );
RetValue = Abc_NtkDarProve( pNtk2, pSecPar );
Abc_NtkDelete( pNtk2 );
// analize the result
if ( RetValue == 1 )
goto finish;
if ( RetValue == 0 )
{
// transfer the counter-example!!!
goto finish;
}
assert( RetValue == -1 );
Aig_ManStop( pMan );
pMan = (Aig_Man_t *)Abc_FrameReadSave1(); // save2
}
speculation:
if ( spectried )
goto finalbmc;
spectried = 1;
if ( fVerbose )
{
printf( "Speculation...\n" );
Aig_ManPrintStats( pMan );
}
// convert AIG into GIA
// pGia = Gia_ManFromAigSimple( pMan ); // DID NOT WORK!
pGia = Gia_ManFromAig( pMan );
Aig_ManStop( pMan );
// &get, eclass,
{
Cec_ParSim_t Pars, * pPars = &Pars;
Cec_ManSimSetDefaultParams( pPars );
pPars->fSeqSimulate ^= 1;
pPars->nWords = 255;
pPars->nFrames = 1000;
Cec_ManSimulation( pGia, pPars );
}
// (spech)* where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
while ( 1 )
{
// perform speculative reduction
pSrm = Gia_ManSpecReduce( pGia, 0, 0, fVeryVerbose ); // save3
// Gia_ManPrintStats( pGia, 0 );
// Gia_ManPrintStats( pSrm, 0 );
// bmc2 -F 100 -C 25000
{
Abc_Cex_t * pCex;
int nFrames = 100; // different from default
int nNodeDelta = 2000;
int nBTLimit = 25000; // different from default
int nBTLimitAll = 2000000;
pTemp = Gia_ManToAig( pSrm, 0 );
// Aig_ManPrintStats( pTemp );
Gia_ManStop( pSrm );
Saig_BmcPerform( pTemp, 0, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVeryVerbose, 0, NULL );
pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
Aig_ManStop( pTemp );
if ( pCex == NULL )
break;
// perform simulation
{
Cec_ParSim_t Pars, * pPars = &Pars;
Cec_ManSimSetDefaultParams( pPars );
Cec_ManSeqResimulateCounter( pGia, pPars, pCex );
ABC_FREE( pCex );
}
}
}
Gia_ManStop( pGia );
// speculatively reduced model is available in pTemp
// trim off useless primary inputs
if ( fVerbose )
{
printf( "Problem before trimming...\n" );
Aig_ManPrintStats( pTemp );
}
pMan = Aig_ManDupTrim( pTemp );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "After speculation...\n" );
Aig_ManPrintStats( pMan );
}
/*
// solve the speculatively reduced model
// dprove -r -F 8
{
Fra_Sec_t SecPar, * pSecPar = &SecPar;
Fra_SecSetDefaultParams( pSecPar );
pSecPar->fTryBmc ^= 1;
pSecPar->fRetimeFirst ^= 1;
pSecPar->nFramesMax = 8;
pSecPar->fVerbose = fVeryVerbose;
pSecPar->fInterSeparate = 0; //fSeparate;
// convert pMan into pNtk
pNtk2 = Abc_NtkFromAigPhase( pMan );
RetValue = Abc_NtkDarProve( pNtk2, pSecPar );
Abc_NtkDelete( pNtk2 );
// analize the result
if ( RetValue == 1 )
goto finish;
if ( RetValue == 0 )
goto finalbmc;
// could not solve
Aig_ManStop( pMan );
pMan = Abc_FrameReadSave1(); // save4
if ( absquit || absfail )
goto abstraction;
}
*/
// scorr; dc2; orpos; int -r -C 25000
{
Ssw_Pars_t Pars, * pPars = &Pars;
Ssw_ManSetDefaultParams( pPars );
pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "After \"scorr\"...\n" );
Aig_ManPrintStats( pMan );
}
pMan = Dar_ManCompress2( pTemp = pMan, 1, 0, 1, 0, 0 );
Aig_ManStop( pTemp );
if ( fVerbose )
{
printf( "After \"dc2\"...\n" );
Aig_ManPrintStats( pMan );
}
}
{
Inter_ManParams_t Pars, * pPars = &Pars;
Inter_ManSetDefaultParams( pPars );
pPars->fUseSeparate = fSeparate;
pPars->fRewrite = 1;
pPars->nBTLimit = 25000;
if ( Saig_ManPoNum(pMan) > 1 && !fSeparate )
{
Aig_Man_t * pAux = Aig_ManDupSimple(pMan);
pTemp = Aig_ManDupOrpos( pAux, 1 );
RetValue = Abc_NtkDarBmcInter_int( pTemp, pPars );
Aig_ManStop( pTemp );
Aig_ManStop( pAux );
}
else
RetValue = Abc_NtkDarBmcInter_int( pMan, pPars );
// analize the result
if ( RetValue == 1 )
goto finish;
if ( RetValue == 0 )
goto finalbmc;
// could not solve
// Aig_ManStop( pMan );
// pMan = Abc_FrameReadSave1(); // save4
if ( absquit || absfail )
goto abstraction;
}
finalbmc:
Aig_ManStop( pMan );
pMan = pSave1; pSave1 = NULL;
if ( fVerbose )
{
printf( "Final BMC...\n" );
Aig_ManPrintStats( pMan );
}
// bmc2 unlimited
{
int nFrames = 2000;
int nNodeDelta = 2000;
int nBTLimit = nConfLast; // different from default
int nBTLimitAll = 2000000;
Saig_BmcPerform( pMan, 0, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVeryVerbose, 0, NULL );
ABC_FREE( pNtk->pModel );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
goto finish;
}
finish:
if ( RetValue == 1 )
printf( "Networks are equivalent. " );
if ( RetValue == 0 )
printf( "Networks are not equivalent. " );
if ( RetValue == -1 )
printf( "Networks are UNDECIDED. " );
ABC_PRT( "Time", clock() - clkTotal );
if ( pNtk->pSeqModel )
printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).\n", pNtk->pSeqModel->iPo, pNtk->pSeqModel->iFrame );
// verify counter-example
if ( pNtk->pSeqModel )
{
int status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
if ( status == 0 )
printf( "Abc_NtkDarBmc(): Counter-example verification has FAILED.\n" );
}
if ( pSave1 )
Aig_ManStop( pSave1 );
Aig_ManStop( pMan );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END