Skip to content

A
abc
Commit 655a5010 by Alan Mishchenko
Options

Version abc80918

parent ce690b29
Showing with 273 additions and 13 deletions
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
......
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;
......
src/aig/bbr/bbrCex.c 0 → 100644
/**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 ///
////////////////////////////////////////////////////////////////////////
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
......
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
......
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
}
......
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 ///
////////////////////////////////////////////////////////////////////////
......
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" );
......
src/base/abci/abcDar.c
......@@ -1478,6 +1478,12 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
}
assert( pMan->nRegs > 0 );
// perform verification
if ( pSecPar->fUseNewProver )
{
RetValue = Ssw_SecGeneralMiter( pMan, NULL );
}
else
{
RetValue = Fra_FraigSec( pMan, pSecPar );
pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
if ( pNtk->pSeqModel )
......@@ -1485,6 +1491,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
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;
}
......
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();
......
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 ///
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment