From 47afd0f4f4f258ddc9231b791e6149430240ba52 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 23 Oct 2013 16:26:13 -0700 Subject: Multi-output property solver. --- src/base/abci/abc.c | 62 +++++++++++++++++++++++++++++++++++--- src/base/abci/abcDar.c | 82 +++++++++++++++++++++++++++----------------------- 2 files changed, 101 insertions(+), 43 deletions(-) (limited to 'src/base') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 21ace6d8..5c66958f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -398,6 +398,7 @@ static int Abc_CommandAbc9Cycle ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Slice ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -961,6 +962,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&cone", Abc_CommandAbc9Cone, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&slice", Abc_CommandAbc9Slice, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&popart", Abc_CommandAbc9PoPart, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 ); @@ -32259,9 +32261,9 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandAbc9GroupProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Vec_Int_t * Gia_ManMultiProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose ); + extern Vec_Int_t * Gia_ManGroupProve( Gia_Man_t * p, char * pCommLine, int nGroupSize, int fVerbose ); Vec_Int_t * vStatus; char * pCommLine = NULL; int c, nGroupSize = 1, fVerbose = 0; @@ -32300,15 +32302,15 @@ int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pAbc->pGia == NULL ) { - Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" ); + Abc_Print( -1, "Abc_CommandAbc9GroupProve(): There is no AIG.\n" ); return 1; } - vStatus = Gia_ManMultiProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose ); + vStatus = Gia_ManGroupProve( pAbc->pGia, pCommLine, nGroupSize, fVerbose ); Vec_IntFree( vStatus ); return 0; usage: - Abc_Print( -2, "usage: &mprove [-GS num] [-vh]\n" ); + Abc_Print( -2, "usage: &gprove [-GS num] [-vh]\n" ); Abc_Print( -2, "\t proves multi-output testcase by splitting outputs into groups\n" ); Abc_Print( -2, "\t (currently, group size more than one works only for \"bmc3\" and \"pdr\")\n" ); Abc_Print( -2, "\t-G num : the size of one group [default = %d]\n", nGroupSize ); @@ -32318,6 +32320,56 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9MultiProve( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose ); + Vec_Int_t * vStatuses; + char * pCommLine = NULL; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9PoPart(): There is no AIG.\n" ); + return 1; + } + pAbc->Status = Gia_ManMultiProve( pAbc->pGia, fVerbose ); + vStatuses = Abc_FrameDeriveStatusArray( pAbc->pGia->vSeqModelVec ); + Abc_FrameReplacePoStatuses( pAbc, &vStatuses ); + Abc_FrameReplaceCexVec( pAbc, &pAbc->pGia->vSeqModelVec ); + return 0; + +usage: + Abc_Print( -2, "usage: &mprove [-vh]\n" ); + Abc_Print( -2, "\t proves multi-output testcase by applying several engines\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 4fbf7c70..d662f376 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -2138,56 +2138,62 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp ) ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - if ( RetValue == 1 ) - { - Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<fSilent ) { - if ( pPars->nFailOuts == 0 ) + if ( RetValue == 1 ) { - Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) ); - if ( nTimeOut && Abc_Clock() > nTimeOut ) - Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut ); - else - Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit ); + Abc_Print( 1, "Explored all reachable states after completing %d frames. ", 1<nFailOuts, pPars->iFrame ); - if ( Abc_Clock() > nTimeOut ) - Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut ); + if ( pPars->nFailOuts == 0 ) + { + Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) ); + if ( nTimeOut && Abc_Clock() > nTimeOut ) + Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut ); + else + Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit ); + } else - Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit ); - } - } - else // if ( RetValue == 0 ) - { - if ( !pPars->fSolveAll ) - { - Abc_Cex_t * pCex = pNtk->pSeqModel; - Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame ); + { + Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame ); + if ( Abc_Clock() > nTimeOut ) + Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut ); + else + Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit ); + } } - else + else // if ( RetValue == 0 ) { - int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan); - if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs ) - Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs ); - else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 ) - Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs ); + if ( !pPars->fSolveAll ) + { + Abc_Cex_t * pCex = pNtk->pSeqModel; + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame ); + } else { - Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs ); - if ( pPars->nDropOuts ) - Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs ); - Abc_Print( 1, ". " ); + int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan); + if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs ) + Abc_Print( 1, "None of the %d outputs is found to be SAT. ", nOutputs ); + else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 ) + Abc_Print( 1, "All %d outputs are found to be SAT. ", nOutputs ); + else + { + Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs ); + if ( pPars->nDropOuts ) + Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs ); + Abc_Print( 1, ". " ); + } } - if ( pNtk->vSeqModelVec ) - Vec_PtrFreeFree( pNtk->vSeqModelVec ); - pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; } + ABC_PRT( "Time", Abc_Clock() - clk ); + } + if ( RetValue == 0 && pPars->fSolveAll ) + { + if ( pNtk->vSeqModelVec ) + Vec_PtrFreeFree( pNtk->vSeqModelVec ); + pNtk->vSeqModelVec = pMan->vSeqModelVec; pMan->vSeqModelVec = NULL; } - ABC_PRT( "Time", Abc_Clock() - clk ); if ( pNtk->pSeqModel ) { status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel ); -- cgit v1.2.3