summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/bar/bar.c8
-rw-r--r--src/aig/bbr/bbrCex.c177
-rw-r--r--src/aig/fra/fra.h1
-rw-r--r--src/aig/fra/fraLcr.c5
-rw-r--r--src/aig/ssw/ssw.h1
-rw-r--r--src/aig/ssw/sswPairs.c33
-rw-r--r--src/base/abci/abc.c34
-rw-r--r--src/base/abci/abcDar.c19
-rw-r--r--src/base/main/main.h1
-rw-r--r--src/base/main/mainFrame.c15
10 files changed, 275 insertions, 19 deletions
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 <num>] [-plsvh]\n" );
+ fprintf( stdout, "usage: *scorr [-PQFCLNSD <num>] [-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 ///
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-19 22:58:31 +0000