summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-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
6 files changed, 221 insertions, 4 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 ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-19 23:32:12 +0000