summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/giaAbsIter.c149
-rw-r--r--src/aig/gia/giaEquiv.c2
-rw-r--r--src/aig/gia/module.make1
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigAbsStart.c4
-rw-r--r--src/aig/saig/saigBmc2.c48
-rw-r--r--src/aig/saig/saigTempor.c2
7 files changed, 182 insertions, 26 deletions
diff --git a/src/aig/gia/giaAbsIter.c b/src/aig/gia/giaAbsIter.c
new file mode 100644
index 00000000..4600530b
--- /dev/null
+++ b/src/aig/gia/giaAbsIter.c
@@ -0,0 +1,149 @@
+/**CFile****************************************************************
+
+ FileName [giaIter.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Scalable AIG package.]
+
+ Synopsis [Iterative improvement of abstraction.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: giaIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Gia_ObjIsInGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj)); }
+static inline void Gia_ObjAddToGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { Vec_IntWriteEntry(p->vGateClasses, Gia_ObjId(p, pObj), 1); }
+static inline void Gia_ObjRemFromGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { Vec_IntWriteEntry(p->vGateClasses, Gia_ObjId(p, pObj), 0); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 )
+{
+ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
+ Gia_Man_t * pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
+ Aig_Man_t * pAig = Gia_ManToAigSimple( pAbs );
+ int nStart = 0;
+ int nFrames = iFrame0 ? iFrame0 + 1 : 10000000;
+ int nNodeDelta = 2000;
+ int nBTLimit = 0;
+ int nBTLimitAll = 0;
+ int fVerbose = 0;
+ int RetValue, iFrame;
+ RetValue = Saig_BmcPerform( pAig, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, &iFrame, 1 );
+ assert( RetValue == 0 || RetValue == -1 );
+ Aig_ManStop( pAig );
+ Gia_ManStop( pAbs );
+ return iFrame;
+}
+Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose )
+{
+ Gia_Obj_t * pObj;
+ int i, iFrame0, iFrame;
+ int nTotal = 0, nRemoved = 0;
+ Vec_Int_t * vGScopy;
+ clock_t clk, clkTotal = clock();
+ assert( Gia_ManPoNum(p) == 1 );
+ assert( p->vGateClasses != NULL );
+ vGScopy = Vec_IntDup( p->vGateClasses );
+ if ( nFrameMax == 0 )
+ iFrame0 = Gia_IterTryImprove( p, 0, 0 );
+ else
+ iFrame0 = nFrameMax - 1;
+ while ( 1 )
+ {
+ int fChanges = 0;
+ Gia_ManForEachObj1( p, pObj, i )
+ {
+ if ( pObj->fMark0 )
+ continue;
+ if ( !Gia_ObjIsInGla(p, pObj) )
+ continue;
+ if ( pObj == Gia_ObjFanin0( Gia_ManPo(p, 0) ) )
+ continue;
+ if ( Gia_ObjIsAnd(pObj) )
+ {
+ if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsInGla(p, Gia_ObjFanin1(pObj)) )
+ continue;
+ }
+ if ( Gia_ObjIsRo(p, pObj) )
+ {
+ if ( Gia_ObjIsInGla(p, Gia_ObjRoToRi(p, pObj)) )
+ continue;
+ }
+ clk = clock();
+ printf( "%5d : ", nTotal );
+ printf( "Obj =%7d ", i );
+ Gia_ObjRemFromGla( p, pObj );
+ iFrame = Gia_IterTryImprove( p, nTimeOut, iFrame0 );
+ if ( nFrameMax )
+ assert( iFrame <= nFrameMax );
+ else
+ assert( iFrame <= iFrame0 );
+ printf( "Frame =%6d ", iFrame );
+ if ( iFrame < iFrame0 )
+ {
+ pObj->fMark0 = 1;
+ Gia_ObjAddToGla( p, pObj );
+ printf( " " );
+ }
+ else
+ {
+ fChanges = 1;
+ nRemoved++;
+ printf( "Removing " );
+ Vec_IntWriteEntry( vGScopy, Gia_ObjId(p, pObj), 0 );
+ }
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ nTotal++;
+ // update the classes
+ Vec_IntFreeP( &p->vGateClasses );
+ p->vGateClasses = Vec_IntDup(vGScopy);
+ }
+ if ( !fChanges )
+ break;
+ }
+ Gia_ManCleanMark0(p);
+ Vec_IntFree( vGScopy );
+ printf( "Tried = %d. ", nTotal );
+ printf( "Removed = %d. (%.2f %%) ", nRemoved, 100.0 * nRemoved / Vec_IntCountPositive(p->vGateClasses) );
+ Abc_PrintTime( 1, "Time", clock() - clkTotal );
+ return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index bf1e4c06..62afe26c 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1723,7 +1723,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
pTemp = Gia_ManToAig( pSrm, 0 );
// Aig_ManPrintStats( pTemp );
Gia_ManStop( pSrm );
- Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL );
+ Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0 );
pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
Aig_ManStop( pTemp );
if ( pCex == NULL )
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 83399eb8..cac2986e 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -2,6 +2,7 @@ SRC += src/aig/gia/gia.c \
src/aig/gia/giaAbs.c \
src/aig/gia/giaAbsGla.c \
src/aig/gia/giaAbsGla2.c \
+ src/aig/gia/giaAbsIter.c \
src/aig/gia/giaAbsRef.c \
src/aig/gia/giaAbsRef2.c \
src/aig/gia/giaAbsVta.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index ec33b3eb..e7cdea90 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -147,7 +147,7 @@ extern int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlop
extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
/*=== saigBmc.c ==========================================================*/
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
-extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
+extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
/*=== saigBmc3.c ==========================================================*/
extern void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
extern int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index 51033dee..90efef26 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -72,7 +72,7 @@ int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
***********************************************************************/
Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames )
{
- extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
+ extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
Vec_Int_t * vFlopsNew;
int i, Entry, RetValue;
*piRetValue = -1;
@@ -119,7 +119,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
}
else
{
- Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames );
+ Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0 );
}
if ( pAbs->pSeqModel == NULL )
return NULL;
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index a1dee6e4..f70a0015 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -754,7 +754,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
SeeAlso []
***********************************************************************/
-int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames )
+int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent )
{
Saig_Bmc_t * p;
Aig_Man_t * pNew;
@@ -817,7 +817,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
// check the timeout
if ( nTimeOut && clock() > nTimeToStop )
{
- printf( "Reached timeout (%d seconds).\n", nTimeOut );
+ if ( !fSilent )
+ printf( "Reached timeout (%d seconds).\n", nTimeOut );
if ( piFrames )
*piFrames = p->iFrameLast-1;
Saig_BmcManStop( p );
@@ -827,15 +828,17 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
if ( RetValue == l_True )
{
assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
- printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ",
- p->iOutputFail, p->iFrameFail );
+ if ( !fSilent )
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ",
+ p->iOutputFail, p->iFrameFail );
Status = 0;
if ( piFrames )
*piFrames = p->iFrameFail;
}
else // if ( RetValue == l_False || RetValue == l_Undef )
{
- printf( "No output was asserted in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) );
+ if ( !fSilent )
+ printf( "No output was asserted in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) );
if ( piFrames )
{
if ( p->iOutputLast > 0 )
@@ -844,24 +847,27 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
*piFrames = p->iFramePrev;
}
}
- if ( fVerbOverwrite )
+ if ( !fSilent )
{
- ABC_PRTr( "Time", clock() - clk );
- }
- else
- {
- ABC_PRT( "Time", clock() - clk );
- }
- if ( RetValue != l_True )
- {
- if ( p->iFrameLast >= p->nFramesMax )
- printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
- else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
- printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
- else if ( nTimeOut && clock() > nTimeToStop )
- printf( "Reached timeout (%d seconds).\n", nTimeOut );
+ if ( fVerbOverwrite )
+ {
+ ABC_PRTr( "Time", clock() - clk );
+ }
else
- printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+ {
+ ABC_PRT( "Time", clock() - clk );
+ }
+ if ( RetValue != l_True )
+ {
+ if ( p->iFrameLast >= p->nFramesMax )
+ printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
+ else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
+ printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
+ else if ( nTimeOut && clock() > nTimeToStop )
+ printf( "Reached timeout (%d seconds).\n", nTimeOut );
+ else
+ printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+ }
}
Saig_BmcManStop( p );
fflush( stdout );
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index c8c33680..040df1f9 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -222,7 +222,7 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon
// run BMC2
if ( fUseBmc )
{
- RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
+ RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0 );
if ( RetValue == 0 )
{
Vec_IntFreeP( &vTransSigs );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 19:29:58 +0000