From 0f77840520775cd9ac4bdf4cae2813dadc67ae4e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 25 Oct 2011 18:32:06 +0800 Subject: New proof-based abstraction code. --- src/base/abci/abc.c | 133 ++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 128 insertions(+), 5 deletions(-) (limited to 'src/base/abci/abc.c') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fec9d78b..06da9698 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -379,6 +379,7 @@ static int Abc_CommandAbc9AbsCba ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9AbsPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaDerive ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GlaCba ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GlaPba ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Reparam ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Posplit ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ReachM ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -832,6 +833,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&abs_pba", Abc_CommandAbc9AbsPba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_derive", Abc_CommandAbc9GlaDerive, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gla_cba", Abc_CommandAbc9GlaCba, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&gla_pba", Abc_CommandAbc9GlaPba, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reparam", Abc_CommandAbc9Reparam, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&posplit", Abc_CommandAbc9Posplit, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reachm", Abc_CommandAbc9ReachM, 0 ); @@ -28714,12 +28716,12 @@ int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &abs_cba [-SFCMT num] [-vh]\n" ); + Abc_Print( -2, "usage: &abs_cba [-SFCT num] [-vh]\n" ); Abc_Print( -2, "\t refines abstracted flop map with CEX-based abstraction\n" ); Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit ); - Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax ); +// Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax ); Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -29020,6 +29022,11 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" ); return 0; } + if ( pPars->nFramesMax < 1 ) + { + Abc_Print( 1, "The number of frames should be a positive integer.\n" ); + return 0; + } pAbc->Status = Gia_ManGlaCbaPerform( pAbc->pGia, pPars, fNaiveCnf ); if ( pPars->nStart == 0 ) pAbc->nFrames = pPars->iFrame; @@ -29028,12 +29035,12 @@ int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &gla_cba [-SFCMT num] [-cvh]\n" ); + Abc_Print( -2, "usage: &gla_cba [-FCT num] [-cvh]\n" ); Abc_Print( -2, "\t refines abstracted object map with CEX-based abstraction\n" ); - Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); +// Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit ); - Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax ); +// Abc_Print( -2, "\t-M num : the max number of flops to add (0 = not used) [default = %d]\n", pPars->nFfToAddMax ); Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); Abc_Print( -2, "\t-c : toggle using naive CNF computation [default = %s]\n", fNaiveCnf? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); @@ -29041,6 +29048,122 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Saig_ParBmc_t Pars, * pPars = &Pars; + int c; + Saig_ParBmcSetDefaultParams( pPars ); + pPars->nStart = 0; //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0; + pPars->nFramesMax = 10; //pPars->nStart + 10; + pPars->nConfLimit = 1000000; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTcvh" ) ) != EOF ) + { + switch ( c ) + { + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nStart = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nStart < 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->nFramesMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nFramesMax < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nConfLimit < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nTimeOut < 0 ) + goto usage; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "The network is combinational.\n" ); + return 0; + } + if ( Gia_ManPoNum(pAbc->pGia) > 1 ) + { + Abc_Print( 1, "The network is more than one PO (run \"orpos\").\n" ); + return 0; + } + if ( pPars->nFramesMax < 1 ) + { + Abc_Print( 1, "The number of frames should be a positive integer.\n" ); + return 0; + } + pAbc->Status = Gia_ManGlaPbaPerform( pAbc->pGia, pPars ); + if ( pPars->nStart == 0 ) + pAbc->nFrames = pPars->iFrame; + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); +// printf( "This command is currently not enabled.\n" ); + return 0; + +usage: + Abc_Print( -2, "usage: &gla_pba [-FCT num] [-vh]\n" ); + Abc_Print( -2, "\t refines abstracted object map with proof-based abstraction\n" ); +// Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart ); + Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); + Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit ); + Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] -- cgit v1.2.3