From 655a50101e18176f1163ccfc67cf69d86623d1f2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 18 Sep 2008 08:01:00 -0700 Subject: Version abc80918 --- abc.dsp | 4 ++ src/aig/bar/bar.c | 8 ++- src/aig/bbr/bbrCex.c | 177 ++++++++++++++++++++++++++++++++++++++++++++++ src/aig/fra/fra.h | 1 + src/aig/fra/fraLcr.c | 5 +- src/aig/ssw/ssw.h | 1 + src/aig/ssw/sswPairs.c | 33 +++++++++ src/base/abci/abc.c | 34 ++++++--- src/base/abci/abcDar.c | 19 +++-- src/base/main/main.h | 1 + src/base/main/mainFrame.c | 15 ++++ 11 files changed, 279 insertions(+), 19 deletions(-) create mode 100644 src/aig/bbr/bbrCex.c diff --git a/abc.dsp b/abc.dsp index e2b33479..3a89ced6 100644 --- a/abc.dsp +++ b/abc.dsp @@ -3246,6 +3246,10 @@ SOURCE=.\src\aig\bbr\bbr.h # End Source File # Begin Source File +SOURCE=.\src\aig\bbr\bbrCex.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\bbr\bbrImage.c # End Source File # Begin Source File diff --git a/src/aig/bar/bar.c b/src/aig/bar/bar.c index 13bd9fe7..f802d60c 100644 --- a/src/aig/bar/bar.c +++ b/src/aig/bar/bar.c @@ -60,9 +60,13 @@ static void Bar_ProgressClean( Bar_Progress_t * p ); Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal ) { Bar_Progress_t * p; + void * pFrame; extern int Abc_FrameShowProgress( void * p ); - extern void * Abc_FrameGetGlobalFrame(); - if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL; + extern void * Abc_FrameReadGlobalFrame(); + pFrame = Abc_FrameReadGlobalFrame(); + if ( pFrame == NULL ) + return NULL; + if ( !Abc_FrameShowProgress(pFrame) ) return NULL; p = (Bar_Progress_t *) malloc(sizeof(Bar_Progress_t)); memset( p, 0, sizeof(Bar_Progress_t) ); p->pFile = pFile; diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c new file mode 100644 index 00000000..f5981439 --- /dev/null +++ b/src/aig/bbr/bbrCex.c @@ -0,0 +1,177 @@ +/**CFile**************************************************************** + + FileName [bbrCex.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [BDD-based reachability analysis.] + + Synopsis [Procedures to derive a satisfiable counter-example.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bbrCex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bbr.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the initial state and sets up the variable map.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose ) +{ + DdNode ** pbVarsX, ** pbVarsY; + Aig_Obj_t * pLatch; + int i; + + // set the variable mapping for Cudd_bddVarMap() + pbVarsX = ALLOC( DdNode *, dd->size ); + pbVarsY = ALLOC( DdNode *, dd->size ); + Saig_ManForEachLo( p, pLatch, i ) + { + pbVarsY[i] = dd->vars[ Saig_ManPiNum(p) + i ]; + pbVarsX[i] = dd->vars[ Saig_ManCiNum(p) + i ]; + } + Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) ); + FREE( pbVarsX ); + FREE( pbVarsY ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManComputeCountExample( Aig_Man_t * p, DdManager * dd, DdNode ** pbParts, Vec_Ptr_t * vCareSets, int nBddMax, int fVerbose, int fSilent ) +{ +/* + Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized" + DdNode * bCubeCs; + DdNode * bCurrent; + DdNode * bNext = NULL; // Suppress "might be used uninitialized" + DdNode * bTemp; + DdNode ** pbVarsY; + Aig_Obj_t * pObj; + int i, nIters, nBddSize; + int nThreshold = 10000; + int * pCex; + char * pValues; + + // allocate room for the counter-example + pCex = ALLOC( int, Vec_PtrSize(vCareSets) ); + + // allocate room for the cube + pValues = ALLOC( char, dd->size ); + + // collect the NS variables + // set the variable mapping for Cudd_bddVarMap() + pbVarsY = ALLOC( DdNode *, dd->size ); + Aig_ManForEachPi( p, pObj, i ) + pbVarsY[i] = dd->vars[ i ]; + + // create the initial state and the variable map + Aig_ManStateVarMap( dd, p, fVerbose ); + + // start the image computation + bCubeCs = Bbr_bddComputeRangeCube( dd, Aig_ManPiNum(p), 2*Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs ); + pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose ); + Cudd_RecursiveDeref( dd, bCubeCs ); + free( pbVarsY ); + if ( pTree == NULL ) + { + if ( !fSilent ) + printf( "BDDs blew up during qualitification scheduling. " ); + return -1; + } + + // create counter-example in terms of next state variables + // pNext = ... + + // perform reachability analisys + Vec_PtrForEachEntryReverse( vCareSets, pCurrent, i ) + { + // compute the next states + bImage = Bbr_bddImageCompute( pTree, bCurrent ); + if ( bImage == NULL ) + { + if ( !fSilent ) + printf( "BDDs blew up during image computation. " ); + Bbr_bddImageTreeDelete( pTree ); + return -1; + } + Cudd_Ref( bImage ); + + // intersect with the previous set + bImage = Cudd_bddAnd( dd, pTemp = bImage, pCurrent ); + Cudd_RecursiveDeref( dd, pTemp ); + + // find any assignment of the BDD + RetValue = Cudd_bddPickOneCube( dd, bImage, pValues ); + + // transform the assignment into the cube in terms of the next state vars + + + + // pCurrent = ... + + // save values of the PI variables + + + // check if there are any new states + if ( Cudd_bddLeq( dd, bNext, bReached ) ) + break; + // check the BDD size + nBddSize = Cudd_DagSize(bNext); + if ( nBddSize > nBddMax ) + break; + // check the result + for ( i = 0; i < Saig_ManPoNum(p); i++ ) + { + if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) ) + { + if ( !fSilent ) + printf( "Output %d was asserted in frame %d. ", i, nIters ); + Cudd_RecursiveDeref( dd, bReached ); + bReached = NULL; + break; + } + } + if ( i < Saig_ManPoNum(p) ) + break; + // get the new states + bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent ); +*/ +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 91689196..eceda480 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -123,6 +123,7 @@ struct Fra_Sec_t_ int fInterpolation; // enables interpolation int fReachability; // enables BDD based reachability int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove + int fUseNewProver; // the new prover int fSilent; // disables all output int fVerbose; // enables verbose reporting of statistics int fVeryVerbose; // enables very verbose reporting diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index f597e090..d3be9842 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -629,16 +629,17 @@ clk2 = clock(); pAigTemp = Fra_FraigEquivence( pAigPart, nConfMax, 0 ); p->timeFraig += clock() - clk2; Vec_PtrPush( p->vFraigs, pAigTemp ); +/* { char Name[1000]; sprintf( Name, "part%04d.blif", i ); Aig_ManDumpBlif( pAigPart, Name, NULL, NULL ); } - Aig_ManStop( pAigPart ); - printf( "Finished part %4d (out of %4d). ", i, Vec_PtrSize(p->vParts) ); PRT( "Time", clock() - clk3 ); +*/ + Aig_ManStop( pAigPart ); } Fra_ClassNodesUnmark( p ); // report the intermediate results diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h index 14c10f6a..91c2165a 100644 --- a/src/aig/ssw/ssw.h +++ b/src/aig/ssw/ssw.h @@ -85,6 +85,7 @@ extern Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t /*=== sswPairs.c ===================================================*/ extern int Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars ); extern int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ); +extern int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ); #ifdef __cplusplus } diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c index 92d3d91d..a11bdf98 100644 --- a/src/aig/ssw/sswPairs.c +++ b/src/aig/ssw/sswPairs.c @@ -430,6 +430,39 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars ) return RetValue; } +/**Function************************************************************* + + Synopsis [Runs inductive SEC for the miter of two AIGs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars ) +{ + Aig_Man_t * pAigRes; + int RetValue, clk = clock(); + // try the new AIGs +// printf( "Performing general verification without node pairs.\n" ); + pAigRes = Ssw_SignalCorrespondence( pMiter, pPars ); + // report the results + RetValue = Ssw_MiterStatus( pAigRes, 1 ); + if ( RetValue == 1 ) + printf( "Verification successful. " ); + else if ( RetValue == 0 ) + printf( "Verification failed with a counter-example. " ); + else + printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ", + Aig_ManRegNum(pAigRes), Aig_ManRegNum(pMiter) ); + PRT( "Time", clock() - clk ); + // cleanup + Aig_ManStop( pAigRes ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a0d26e3b..26d72934 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -15145,7 +15145,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Fra_SecSetDefaultParams( pSecPar ); pSecPar->TimeLimit = 300; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cbTFarmfwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cbTFarmfnwvh" ) ) != EOF ) { switch ( c ) { @@ -15189,6 +15189,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': pSecPar->fFraiging ^= 1; break; + case 'n': + pSecPar->fUseNewProver ^= 1; + break; case 'w': pSecPar->fVeryVerbose ^= 1; break; @@ -15214,7 +15217,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dprove [-F num] [-T num] [-cbarmfwvh]\n" ); + fprintf( pErr, "usage: dprove [-F num] [-T num] [-cbarmfnwvh]\n" ); fprintf( pErr, "\t performs SEC on the sequential miter\n" ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); fprintf( pErr, "\t-T num : the approximate runtime limit (in seconds) [default = %d]\n", pSecPar->TimeLimit ); @@ -15224,6 +15227,7 @@ usage: fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", pSecPar->fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-m : toggles min-register retiming [default = %s]\n", pSecPar->fRetimeRegs? "yes": "no" ); fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" ); + fprintf( pErr, "\t-n : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -18717,7 +18721,7 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fVerbose = 0; pPars->TimeLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILCirfletvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQNFILDirfletvh" ) ) != EOF ) { switch ( c ) { @@ -18787,10 +18791,10 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nMaxLevs <= 0 ) goto usage; break; - case 'C': + case 'D': if ( globalUtilOptind >= argc ) { - fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" ); + fprintf( stdout, "Command line switch \"-D\" should be followed by an integer.\n" ); goto usage; } pPars->nMinDomSize = atoi(argv[globalUtilOptind]); @@ -18874,14 +18878,14 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: *ssw [-PQNFLC num] [-lrfetvh]\n" ); + fprintf( stdout, "usage: *ssw [-PQNFLD num] [-lrfetvh]\n" ); fprintf( stdout, "\t performs sequential sweep using K-step induction on the netlist \n" ); fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); fprintf( stdout, "\t-N num : number of time frames to use as the prefix [default = %d]\n", pPars->nFramesP ); fprintf( stdout, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK ); fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs ); - fprintf( stdout, "\t-C num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize ); + fprintf( stdout, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize ); // fprintf( stdout, "\t-I num : max number of implications to consider [default = %d]\n", pPars->nMaxImps ); // fprintf( stdout, "\t-i : toggle using implications [default = %s]\n", pPars->fUseImps? "yes": "no" ); fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); @@ -18917,7 +18921,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Ssw_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSDplsvh" ) ) != EOF ) { switch ( c ) { @@ -18998,6 +19002,17 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nFramesAddSim < 0 ) goto usage; break; + case 'D': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-D\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nMinDomSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nMinDomSize < 0 ) + goto usage; + break; case 'p': pPars->fPolarFlip ^= 1; break; @@ -19053,7 +19068,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: *scorr [-PQFCLNS ] [-plsvh]\n" ); + fprintf( stdout, "usage: *scorr [-PQFCLNSD ] [-plsvh]\n" ); fprintf( stdout, "\t performs sequential sweep using K-step induction\n" ); fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); @@ -19062,6 +19077,7 @@ usage: fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs ); fprintf( stdout, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs ); fprintf( stdout, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim ); + fprintf( stdout, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize ); fprintf( stdout, "\t-p : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" ); fprintf( stdout, "\t-l : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" ); fprintf( stdout, "\t-s : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 388fc5df..b84c5191 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1468,7 +1468,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) } return RetValue; } - } + } // derive the AIG manager pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) @@ -1478,12 +1478,19 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar ) } assert( pMan->nRegs > 0 ); // perform verification - RetValue = Fra_FraigSec( pMan, pSecPar ); - pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - if ( pNtk->pSeqModel ) + if ( pSecPar->fUseNewProver ) + { + RetValue = Ssw_SecGeneralMiter( pMan, NULL ); + } + else { - 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 ); + RetValue = Fra_FraigSec( pMan, pSecPar ); + 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; diff --git a/src/base/main/main.h b/src/base/main/main.h index 62dc394a..af0ed24d 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -97,6 +97,7 @@ extern ABC_DLL void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p ); extern ABC_DLL void Abc_FrameSetGlobalFrame( Abc_Frame_t * p ); extern ABC_DLL Abc_Frame_t * Abc_FrameGetGlobalFrame(); +extern ABC_DLL Abc_Frame_t * Abc_FrameReadGlobalFrame(); extern ABC_DLL Vec_Ptr_t * Abc_FrameReadStore(); extern ABC_DLL int Abc_FrameReadStoreSize(); diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 462b5a02..f02ade1c 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -495,6 +495,21 @@ Abc_Frame_t * Abc_FrameGetGlobalFrame() return s_GlobalFrame; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Frame_t * Abc_FrameReadGlobalFrame() +{ + return s_GlobalFrame; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3