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

Merged in ysho/abc (pull request #59) 

added a new abstraction
This commit is contained in:
Alan Mishchenko 2017-02-22 04:31:10 +00:00
parent 9d46d84b27 fb2fbd70bd
commit 0e9f8093c3
7 changed files with 1043 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
.hgignore
View File

@ -52,9 +52,14 @@ build/
*.rej
*.orig
tags
syntax: regexp
^libabc.a$
^abc$
^arch_flags$
^cmake
^cscope

3
src/base/wlc/wlc.h
View File

@ -170,6 +170,8 @@ struct Wlc_Par_t_
int nBitsFlop; // flop bit-width
int nIterMax; // the max number of iterations
int fXorOutput; // XOR outputs of word-level miter
int fCheckClauses; // Check clauses in the reloaded trace
int fPushClauses; // Push clauses in the reloaded trace
int fVerbose; // verbose output
int fPdrVerbose; // verbose output
};
@ -277,6 +279,7 @@ static inline Wlc_Obj_t * Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId )
/*=== wlcAbs.c ========================================================*/
extern int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcAbs2.c ========================================================*/
extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
/*=== wlcBlast.c ========================================================*/

158
src/base/wlc/wlcAbs.c
View File

@ -20,6 +20,7 @@
#include "wlc.h"
#include "proof/pdr/pdr.h"
#include "proof/pdr/pdrInt.h"
#include "aig/gia/giaAig.h"
#include "sat/bmc/bmc.h"
@ -29,6 +30,10 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
extern int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses );
extern int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -128,6 +133,17 @@ static void Wlc_NtkAbsMarkNodes( Wlc_Ntk_t * p, Vec_Bit_t * vLeaves, Vec_Int_t *
Wlc_NtkCleanMarks( p );
Wlc_NtkForEachCo( p, pObj, i )
Wlc_NtkAbsMarkNodes_rec( p, pObj, vLeaves, vPisOld, vPisNew, vFlops );
Vec_IntClear(vFlops);
Wlc_NtkForEachCi( p, pObj, i ) {
if ( !Wlc_ObjIsPi(pObj) ) {
Vec_IntPush( vFlops, Wlc_ObjId(p, pObj) );
pObj->Mark = 1;
}
}
Wlc_NtkForEachObjVec( vFlops, p, pObj, i )
Wlc_NtkAbsMarkNodes_rec( p, Wlc_ObjFo2Fi(p, pObj), vLeaves, vPisOld, vPisNew, vFlops );
Wlc_NtkForEachObj( p, pObj, i )
@ -283,6 +299,141 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
return nNodes;
}
/**Function*************************************************************
Synopsis [Performs PDR with word-level abstraction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
abctime clk = Abc_Clock();
abctime pdrClk;
Pdr_Man_t * pPdr;
Vec_Vec_t * vClauses = NULL;
int nIters, nNodes, nDcFlops, RetValue = -1;
// start the bitmap to mark objects that cannot be abstracted because of refinement
// currently, this bitmap is empty because abstraction begins without refinement
Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
// set up parameters to run PDR
Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
Pdr_ManSetDefaultParams( pPdrPars );
pPdrPars->fVerbose = pPars->fPdrVerbose;
pPdrPars->fVeryVerbose = 0;
// perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{
Aig_Man_t * pAig;
Abc_Cex_t * pCex;
Vec_Int_t * vPisNew, * vRefine;
Gia_Man_t * pGia, * pTemp;
Wlc_Ntk_t * pAbs;
if ( pPars->fVerbose )
printf( "\nIteration %d:\n", nIters );
// get abstracted GIA and the set of pseudo-PIs (vPisNew)
pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
// if the abstraction has flops with DC-init state,
// new PIs were introduced by bit-blasting at the end of the PI list
// here we move these variables to be *before* PPIs, because
// PPIs are supposed to be at the end of the PI list for refinement
nDcFlops = Wlc_NtkDcFlopNum(pAbs);
if ( nDcFlops > 0 ) // DC-init flops are present
{
pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
Gia_ManStop( pTemp );
}
// if the word-level outputs have to be XORs, this is a place to do it
if ( pPars->fXorOutput )
{
pGia = Gia_ManTransformMiter2( pTemp = pGia );
Gia_ManStop( pTemp );
}
if ( pPars->fVerbose )
{
printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) );
Gia_ManPrintStats( pGia, NULL );
}
Wlc_NtkFree( pAbs );
// try to prove abstracted GIA by converting it to AIG and calling PDR
pAig = Gia_ManToAigSimple( pGia );
pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
pdrClk = Abc_Clock();
if ( vClauses ) {
assert( Vec_VecSize( vClauses) >= 2 );
IPdr_ManRestore( pPdr, vClauses );
}
RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
pPdr->tTotal += Abc_Clock() - pdrClk;
pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
// consider outcomes
if ( pCex == NULL )
{
assert( RetValue ); // proved or undecided
Gia_ManStop( pGia );
Vec_IntFree( vPisNew );
Pdr_ManStop( pPdr );
Aig_ManStop( pAig );
break;
}
// perform refinement
vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
Gia_ManStop( pGia );
Vec_IntFree( vPisNew );
if ( vRefine == NULL ) // real CEX
{
Abc_CexFree( pCex ); // return CEX in the future
Pdr_ManStop( pPdr );
Aig_ManStop( pAig );
break;
}
// spurious CEX, continue solving
vClauses = IPdr_ManSaveClauses( pPdr, 0 );
Pdr_ManStop( pPdr );
// update the set of objects to be un-abstracted
nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
if ( pPars->fVerbose )
printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
Vec_IntFree( vRefine );
Abc_CexFree( pCex );
Aig_ManStop( pAig );
}
Vec_BitFree( vUnmark );
// report the result
if ( pPars->fVerbose )
printf( "\n" );
printf( "Abstraction " );
if ( RetValue == 0 )
printf( "resulted in a real CEX" );
else if ( RetValue == 1 )
printf( "is successfully proved" );
else
printf( "timed out" );
printf( " after %d iterations. ", nIters );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return RetValue;
}
/**Function*************************************************************
Synopsis [Performs abstraction.]
@ -309,11 +460,12 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
// set up parameters to run PDR
Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
Pdr_ManSetDefaultParams( pPdrPars );
pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
//pPdrPars->fUseAbs = 1; // use 'pdr -t' (on-the-fly abstraction)
//pPdrPars->fCtgs = 1; // use 'pdr -nc' (improved generalization)
//pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization)
//pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this
pPdrPars->fVerbose = pPars->fPdrVerbose;
pPdrPars->fVeryVerbose = 0;
// perform refinement iterations
for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
{

125
src/base/wlc/wlcCom.c
View File

@ -33,6 +33,7 @@ static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv )
static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPdrAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -75,6 +76,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%pdra", Abc_CommandPdrAbs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%abs2", Abc_CommandAbs2, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
@ -442,6 +444,129 @@ usage:
return 1;
}
/**Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
Wlc_Par_t Pars, * pPars = &Pars;
int c;
Wlc_ManSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF )
{
switch ( c )
{
case 'A':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBitsAdd < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBitsMul = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBitsMul < 0 )
goto usage;
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBitsMux = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBitsMux < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nBitsFlop < 0 )
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
pPars->nIterMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nIterMax < 0 )
goto usage;
break;
case 'x':
pPars->fXorOutput ^= 1;
break;
case 'c':
pPars->fCheckClauses ^= 1;
break;
case 'p':
pPars->fPushClauses ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'w':
pPars->fPdrVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
return 0;
}
Wlc_NtkPdrAbs( pNtk, pPars );
return 0;
usage:
Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" );
Abc_Print( -2, "\t abstraction for word-level networks\n" );
Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" );
Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function********************************************************************
Synopsis []

2
src/base/wlc/wlcNtk.c
View File

@ -114,6 +114,8 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->nBitsFlop = ABC_INFINITY; // flop bit-width
pPars->nIterMax = 1000; // the max number of iterations
pPars->fXorOutput = 1; // XOR outputs of word-level miter
pPars->fCheckClauses = 1; // Check clauses in the reloaded trace
pPars->fPushClauses = 0; // Push clauses in the reloaded trace
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}

3
src/proof/pdr/module.make
View File

@ -5,4 +5,5 @@ SRC += src/proof/pdr/pdrCnf.c \
src/proof/pdr/pdrSat.c \
src/proof/pdr/pdrTsim.c \
src/proof/pdr/pdrTsim2.c \
src/proof/pdr/pdrUtil.c
src/proof/pdr/pdrUtil.c \
src/proof/pdr/pdrIncr.c

751
src/proof/pdr/pdrIncr.c Normal file
View File

@ -0,0 +1,751 @@
/**CFile****************************************************************
FileName [pdrIncr.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Property driven reachability.]
Synopsis [PDR with incremental solving.]
Author [Yen-Sheng Ho, Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - Feb. 17, 2017.]
Revision [$Id: pdrIncr.c$]
***********************************************************************/
#include "pdrInt.h"
#include "base/main/main.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
extern int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube );
extern int Pdr_ManPushClauses( Pdr_Man_t * p );
extern int Gia_ManToBridgeAbort( FILE * pFile, int Size, unsigned char * pBuffer );
extern int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex, int iPoProved );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs )
{
Vec_Ptr_t * vArrayK;
Pdr_Set_t * pCube;
int i, k, Counter = 0;
Vec_VecForEachLevelStart( vClauses, vArrayK, k, kStart )
{
Vec_PtrSort( vArrayK, (int (*)(void))Pdr_SetCompare );
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCube, i )
{
Abc_Print( 1, "C=%4d. F=%4d ", Counter++, k );
Pdr_SetPrint( stdout, pCube, nRegs, NULL );
Abc_Print( 1, "\n" );
}
}
}
/**Function*************************************************************
Synopsis [ Check if each cube c_k in frame k satisfies the query
R_{k-1} && T && !c_k && c_k' (must be UNSAT).
Return True if all cubes pass the check. ]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IPdr_ManCheckClauses( Pdr_Man_t * p )
{
Pdr_Set_t * pCubeK;
Vec_Ptr_t * vArrayK;
int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers);
int iStartFrame = 1;
int counter = 0;
Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
{
Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
{
++counter;
RetValue = Pdr_ManCheckCube( p, k - 1, pCubeK, NULL, 0, 0, 1 );
if ( !RetValue ) {
printf( "Cube[%d][%d] not inductive!\n", k, j );
}
assert( RetValue == 1 );
}
}
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast )
{
int i, k;
Vec_Vec_t * vClausesSaved;
Pdr_Set_t * pCla;
if ( Vec_VecSize( p->vClauses ) == 1 )
return NULL;
if ( Vec_VecSize( p->vClauses ) == 2 && fDropLast )
return NULL;
if ( fDropLast )
vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 );
else
vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses) );
Vec_VecForEachEntryStartStop( Pdr_Set_t *, p->vClauses, pCla, i, k, 0, Vec_VecSize(vClausesSaved) )
Vec_VecPush(vClausesSaved, i, Pdr_SetDup(pCla));
return vClausesSaved;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * IPdr_ManSetSolver( Pdr_Man_t * p, int k, int nTotal )
{
sat_solver * pSat;
Vec_Ptr_t * vArrayK;
Pdr_Set_t * pCube;
int i, j;
assert( Vec_PtrSize(p->vSolvers) == k );
assert( Vec_IntSize(p->vActVars) == k );
pSat = zsat_solver_new_seed(p->pPars->nRandomSeed);
pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
Vec_PtrPush( p->vSolvers, pSat );
Vec_IntPush( p->vActVars, 0 );
// set the property output
if ( k < nTotal - 1 )
Pdr_ManSetPropertyOutput( p, k );
if (k == 0)
return pSat;
// 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 []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses )
{
int i;
assert(vClauses);
Vec_VecFree(p->vClauses);
p->vClauses = vClauses;
for ( i = 0; i < Vec_VecSize(p->vClauses); ++i )
IPdr_ManSetSolver( p, i, Vec_VecSize( p->vClauses ) );
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
{
int fPrintClauses = 0;
Pdr_Set_t * pCube = NULL;
Aig_Obj_t * pObj;
Abc_Cex_t * pCexNew;
int iFrame, RetValue = -1;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
abctime clkStart = Abc_Clock(), clkOne = 0;
p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
// assert( Vec_PtrSize(p->vSolvers) == 0 );
// in the multi-output mode, mark trivial POs (those fed by const0) as solved
if ( p->pPars->fSolveAll )
Saig_ManForEachPo( p->pAig, pObj, iFrame )
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
{
Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
p->pPars->nProveOuts++;
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
}
// create the first timeframe
p->pPars->timeLastSolved = Abc_Clock();
if ( Vec_VecSize(p->vClauses) == 0 )
Pdr_ManCreateSolver( p, (iFrame = 0) );
else {
iFrame = Vec_VecSize(p->vClauses) - 1;
if ( fCheckClauses )
{
if ( p->pPars->fVerbose )
Abc_Print( 1, "IPDR: Checking the reloaded length-%d trace...", iFrame + 1 ) ;
IPdr_ManCheckClauses( p );
if ( p->pPars->fVerbose )
Abc_Print( 1, " Passed!\n" ) ;
}
if ( fPushClauses )
{
p->iUseFrame = Abc_MaxInt(iFrame, 1);
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "IPDR: Pushing the reloaded clauses. Before:\n" );
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
}
RetValue = Pdr_ManPushClauses( p );
if ( p->pPars->fVerbose )
{
Abc_Print( 1, "IPDR: Finished pushing. After:\n" );
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
}
if ( RetValue )
{
Pdr_ManReportInvariant( p );
Pdr_ManVerifyInvariant( p );
return 1;
}
}
}
while ( 1 )
{
int fRefined = 0;
if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 1 )
{
// int i, Prio;
assert( p->vAbsFlops == NULL );
p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) );
p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
p->vMapPpi2Ff = Vec_IntAlloc( 100 );
// Vec_IntForEachEntry( p->vPrio, Prio, i )
// if ( Prio >> p->nPrioShift )
// Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
}
//if ( p->pPars->fUseAbs && p->vAbsFlops )
// printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
p->nFrames = iFrame;
assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
p->iUseFrame = Abc_MaxInt(iFrame, 1);
Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
{
// skip disproved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
continue;
// skip output whose time has run out
if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
continue;
// check if the output is trivially solved
if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
continue;
// check if the output is trivially solved
if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) )
{
if ( !p->pPars->fSolveAll )
{
pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur );
p->pAig->pSeqModel = pCexNew;
return 0; // SAT
}
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
p->pPars->nFailOuts++;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
if ( !p->pPars->fNotVerbose )
Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
p->pPars->iFrame = iFrame;
return -1;
}
if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
p->pPars->timeLastSolved = Abc_Clock();
continue;
}
// try to solve this output
if ( p->pTime4Outs )
{
assert( p->pTime4Outs[p->iOutCur] > 0 );
clkOne = Abc_Clock();
p->timeToStopOne = p->pTime4Outs[p->iOutCur] + Abc_Clock();
}
while ( 1 )
{
if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
p->pPars->iFrame = iFrame;
return -1;
}
RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0, 1 );
if ( RetValue == 1 )
break;
if ( RetValue == -1 )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
{
Pdr_QueueClean( p );
pCube = NULL;
break; // keep solving
}
else if ( p->pPars->nConfLimit )
Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
else if ( p->pPars->fVerbose )
Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
p->pPars->iFrame = iFrame;
return -1;
}
if ( RetValue == 0 )
{
RetValue = Pdr_ManBlockCube( p, pCube );
if ( RetValue == -1 )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
{
Pdr_QueueClean( p );
pCube = NULL;
break; // keep solving
}
else if ( p->pPars->nConfLimit )
Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
else if ( p->pPars->fVerbose )
Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
p->pPars->iFrame = iFrame;
return -1;
}
if ( RetValue == 0 )
{
if ( fPrintClauses )
{
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose && !p->pPars->fUseAbs )
Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
p->pPars->iFrame = iFrame;
if ( !p->pPars->fSolveAll )
{
abctime clk = Abc_Clock();
Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p);
p->tAbs += Abc_Clock() - clk;
if ( pCex == NULL )
{
assert( p->pPars->fUseAbs );
Pdr_QueueClean( p );
pCube = NULL;
fRefined = 1;
break; // keep solving
}
p->pAig->pSeqModel = pCex;
return 0; // SAT
}
p->pPars->nFailOuts++;
pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Pdr_ManDeriveCex(p) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCexNew );
if ( p->pPars->pFuncOnFail && p->pPars->pFuncOnFail(p->iOutCur, p->pPars->fStoreCex ? (Abc_Cex_t *)Vec_PtrEntry(p->vCexes, p->iOutCur) : NULL) )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
p->pPars->iFrame = iFrame;
return -1;
}
if ( !p->pPars->fNotVerbose )
Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT
Pdr_QueueClean( p );
pCube = NULL;
break; // keep solving
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
}
}
if ( fRefined )
break;
if ( p->pTime4Outs )
{
abctime timeSince = Abc_Clock() - clkOne;
assert( p->pTime4Outs[p->iOutCur] > 0 );
p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
if ( p->pTime4Outs[p->iOutCur] == 0 && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) // undecided
{
p->pPars->nDropOuts++;
if ( p->pPars->vOutMap )
Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
if ( !p->pPars->fNotVerbose )
Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
}
p->timeToStopOne = 0;
}
}
if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
{
int i, Used;
Vec_IntForEachEntry( p->vAbsFlops, Used, i )
if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 )
Vec_IntWriteEntry( p->vAbsFlops, i, 0 );
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
if ( fRefined )
continue;
//if ( p->pPars->fUseAbs && p->vAbsFlops )
// printf( "Finished frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
// open a new timeframe
p->nQueLim = p->pPars->nRestLimit;
assert( pCube == NULL );
Pdr_ManSetPropertyOutput( p, iFrame );
Pdr_ManCreateSolver( p, ++iFrame );
if ( fPrintClauses )
{
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
Pdr_ManPrintClauses( p, 0 );
}
// push clauses into this timeframe
RetValue = Pdr_ManPushClauses( p );
if ( RetValue == -1 )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
{
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
else
Abc_Print( 1, "Reached conflict limit (%d) in frame.\n", p->pPars->nConfLimit, iFrame );
}
p->pPars->iFrame = iFrame;
return -1;
}
if ( RetValue )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Pdr_ManReportInvariant( p );
if ( !p->pPars->fSilent )
Pdr_ManVerifyInvariant( p );
p->pPars->iFrame = iFrame;
// count the number of UNSAT outputs
p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
// convert previously 'unknown' into 'unsat'
if ( p->pPars->vOutMap )
for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
{
Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
}
if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
return 1; // UNSAT
if ( p->pPars->nFailOuts > 0 )
return 0; // SAT
return -1;
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 0, Abc_Clock() - clkStart );
// check termination
if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
{
p->pPars->iFrame = iFrame;
return -1;
}
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
{
if ( fPrintClauses )
{
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
p->pPars->iFrame = iFrame;
return -1;
}
if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
{
if ( fPrintClauses )
{
Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
Pdr_ManPrintClauses( p, 0 );
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOutGap, iFrame );
p->pPars->iFrame = iFrame;
return -1;
}
if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax )
{
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
if ( !p->pPars->fSilent )
Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
p->pPars->iFrame = iFrame;
return -1;
}
}
assert( 0 );
return -1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
{
Pdr_Man_t * p;
int k, RetValue;
Vec_Vec_t * vClausesSaved;
abctime clk = Abc_Clock();
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
pPars->nTimeOutOne = 0;
if ( pPars->nTimeOutOne && pPars->nTimeOut == 0 )
pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + (int)((pPars->nTimeOutOne * Saig_ManPoNum(pAig) % 1000) > 0);
if ( pPars->fVerbose )
{
// Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ",
pPars->nRecycle,
pPars->nFrameMax,
pPars->nRestLimit,
pPars->nTimeOut );
Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n",
pPars->fMonoCnf ? "yes" : "no",
pPars->fSkipGeneral ? "yes" : "no",
pPars->fSolveAll ? "yes" : "no" );
}
ABC_FREE( pAig->pSeqModel );
p = Pdr_ManStart( pAig, pPars, NULL );
while ( 1 ) {
RetValue = IPdr_ManSolveInt( p, 1, 0 );
if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) {
vClausesSaved = IPdr_ManSaveClauses( p, 1 );
Pdr_ManStop( p );
p = Pdr_ManStart( pAig, pPars, NULL );
IPdr_ManRestore( p, vClausesSaved );
pPars->nFrameMax = pPars->nFrameMax << 1;
continue;
}
if ( RetValue == 0 )
assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
if ( p->vCexes )
{
assert( p->pAig->vSeqModelVec == NULL );
p->pAig->vSeqModelVec = p->vCexes;
p->vCexes = NULL;
}
if ( p->pPars->fDumpInv )
{
char * pFileName = Extra_FileNameGenericAppend(p->pAig->pName, "_inv.pla");
Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
Pdr_ManDumpClauses( p, pFileName, RetValue==1 );
}
else if ( RetValue == 1 )
Abc_FrameSetInv( Pdr_ManDeriveInfinityClauses( p, RetValue!=1 ) );
p->tTotal += Abc_Clock() - clk;
Pdr_ManStop( p );
break;
}
pPars->iFrame--;
// convert all -2 (unknown) entries into -1 (undec)
if ( pPars->vOutMap )
for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
if ( pPars->fUseBridge )
Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkDarIPdr ( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
{
int RetValue = -1;
abctime clk = Abc_Clock();
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
RetValue = IPdr_ManSolve( pMan, pPars );
if ( RetValue == 1 )
Abc_Print( 1, "Property proved. " );
else
{
if ( RetValue == 0 )
{
if ( pMan->pSeqModel == NULL )
Abc_Print( 1, "Counter-example is not available.\n" );
else
{
Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
Abc_Print( 1, "Counter-example verification has FAILED.\n" );
}
}
else if ( RetValue == -1 )
Abc_Print( 1, "Property UNDECIDED. " );
else
assert( 0 );
}
ABC_PRT( "Time", Abc_Clock() - clk );
ABC_FREE( pNtk->pSeqModel );
pNtk->pSeqModel = pMan->pSeqModel;
pMan->pSeqModel = NULL;
if ( pNtk->vSeqModelVec )
Vec_PtrFreeFree( pNtk->vSeqModelVec );
pNtk->vSeqModelVec = pMan->vSeqModelVec;
pMan->vSeqModelVec = NULL;
Aig_ManStop( pMan );
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END