summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/ssw')
-rw-r--r--src/aig/ssw/ssw.h1
-rw-r--r--src/aig/ssw/sswConstr.c4
-rw-r--r--src/aig/ssw/sswCore.c2
-rw-r--r--src/aig/ssw/sswDyn.c4
-rw-r--r--src/aig/ssw/sswInt.h2
-rw-r--r--src/aig/ssw/sswSemi.c2
-rw-r--r--src/aig/ssw/sswSim.c96
-rw-r--r--src/aig/ssw/sswSweep.c52
8 files changed, 76 insertions, 87 deletions
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 207ebea9..bf8c918e 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -68,6 +68,7 @@ struct Ssw_Pars_t_
int fUseCSat; // new SAT solver using when fScorrGia is selected
int fVerbose; // verbose stats
int fFlopVerbose; // verbose printout of redundant flops
+ int fEquivDump; // enables dumping equivalences
// optimized latch correspondence
int fLatchCorrOpt; // perform register correspondence (optimized)
int nSatVarMax; // max number of SAT vars before recycling SAT solver (optimized latch corr only)
diff --git a/src/aig/ssw/sswConstr.c b/src/aig/ssw/sswConstr.c
index e233f133..6afdd270 100644
--- a/src/aig/ssw/sswConstr.c
+++ b/src/aig/ssw/sswConstr.c
@@ -83,8 +83,8 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames )
}
// remove dangling nodes
Aig_ManCleanup( pFrames );
- return pFrames;
-}
+ return pFrames;
+}
/**Function*************************************************************
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index c277d76e..1419b889 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -64,6 +64,8 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
p->fDynamic = 0; // dynamic partitioning
p->fLocalSim = 0; // local simulation
p->fVerbose = 0; // verbose stats
+ p->fEquivDump = 0; // enables dumping equivalences
+
// latch correspondence
p->fLatchCorrOpt = 0; // performs optimized register correspondence
p->nSatVarMax = 1000; // the max number of SAT variables
diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c
index 7e8edc66..7bdb2652 100644
--- a/src/aig/ssw/sswDyn.c
+++ b/src/aig/ssw/sswDyn.c
@@ -409,12 +409,12 @@ p->timeReduce += clock() - clk;
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
}
// check if it is time to recycle the solver
if ( p->pMSat->pSat == NULL ||
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index e3a9a341..ad868c6e 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -277,7 +277,7 @@ extern void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Ai
/*=== sswSweep.c ===================================================*/
extern int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
extern void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f );
-extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc );
+extern int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs );
extern int Ssw_ManSweepBmc( Ssw_Man_t * p );
extern int Ssw_ManSweep( Ssw_Man_t * p );
/*=== sswUnique.c ===================================================*/
diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c
index dfb2fb0f..2a28a29b 100644
--- a/src/aig/ssw/sswSemi.c
+++ b/src/aig/ssw/sswSemi.c
@@ -204,7 +204,7 @@ clk = clock();
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- if ( Ssw_ManSweepNode( p, pObj, f, 1 ) )
+ if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) )
{
Ssw_ManFilterBmcSavePattern( pBmc );
if ( fFirst == 0 )
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index 37bf5717..404302f2 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -304,6 +304,23 @@ int Ssw_SmlNodeIsZero( Ssw_Sml_t * p, Aig_Obj_t * pObj )
/**Function*************************************************************
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Ssw_SmlNodeIsZeroFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int f )
+{
+ unsigned * pSims = Ssw_ObjSim(p, pObj->Id);
+ return pSims[f] == 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Counts the number of one's in the patten the object.]
Description []
@@ -1308,7 +1325,7 @@ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
// run random simulation
Ssw_SmlSimulateOne( pSml );
// check if the given output has failed
- RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
+ RetValue = !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, p->iPo), p->iFrame );
Ssw_SmlStop( pSml );
return RetValue;
}
@@ -1347,7 +1364,7 @@ int Ssw_SmlFindOutputCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p )
// check if the given output has failed
iOut = -1;
Saig_ManForEachPo( pAig, pObj, k )
- if ( !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, k) ) )
+ if ( !Ssw_SmlNodeIsZeroFrame( pSml, Aig_ManPo(pAig, k), p->iFrame ) )
{
iOut = k;
break;
@@ -1541,81 +1558,6 @@ Abc_Cex_t * Ssw_SmlDupCounterExample( Abc_Cex_t * p, int nRegsNew )
return pCex;
}
-/**Function*************************************************************
-
- Synopsis [Resimulates the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Abc_Cex_t * p )
-{
- Ssw_Sml_t * pSml;
- Aig_Obj_t * pObj;
- int RetValue, i, k, iBit;
- unsigned * pSims;
- assert( Aig_ManRegNum(pAig) > 0 );
- assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
- // start a new sequential simulator
- pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
- // assign simulation info for the registers
- iBit = 0;
- Saig_ManForEachLo( pAig, pObj, i )
-// Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
- Ssw_SmlObjAssignConst( pSml, pObj, 0, 0 );
- // assign simulation info for the primary inputs
- iBit = p->nRegs;
- for ( i = 0; i <= p->iFrame; i++ )
- Saig_ManForEachPi( pAig, pObj, k )
- Ssw_SmlObjAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
- assert( iBit == p->nBits );
- // run random simulation
- Ssw_SmlSimulateOne( pSml );
- // check if the given output has failed
- RetValue = !Ssw_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
-
- // write the output file
- for ( i = 0; i <= p->iFrame; i++ )
- {
-/*
- Saig_ManForEachLo( pAig, pObj, k )
- {
- pSims = Ssw_ObjSim(pSml, pObj->Id);
- fprintf( pFile, "%d", (int)(pSims[i] != 0) );
- }
- fprintf( pFile, " " );
-*/
- Saig_ManForEachPi( pAig, pObj, k )
- {
- pSims = Ssw_ObjSim(pSml, pObj->Id);
- fprintf( pFile, "%d", (int)(pSims[i] != 0) );
- }
-/*
- fprintf( pFile, " " );
- Saig_ManForEachPo( pAig, pObj, k )
- {
- pSims = Ssw_ObjSim(pSml, pObj->Id);
- fprintf( pFile, "%d", (int)(pSims[i] != 0) );
- }
- fprintf( pFile, " " );
- Saig_ManForEachLi( pAig, pObj, k )
- {
- pSims = Ssw_ObjSim(pSml, pObj->Id);
- fprintf( pFile, "%d", (int)(pSims[i] != 0) );
- }
-*/
- fprintf( pFile, "\n" );
- }
-
- Ssw_SmlStop( pSml );
- return RetValue;
-}
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 39fcd48e..40121e42 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -184,7 +184,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
SeeAlso []
***********************************************************************/
-int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
+int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc, Vec_Int_t * vPairs )
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue, clk;
@@ -221,6 +221,11 @@ p->timeMarkCones += clock() - clk;
Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
return 0;
}
+ if ( vPairs )
+ {
+ Vec_IntPush( vPairs, pObjRepr->Id );
+ Vec_IntPush( vPairs, pObj->Id );
+ }
if ( RetValue == -1 ) // timed out
{
Ssw_ClassesRemoveNode( p->ppClasses, pObj );
@@ -287,7 +292,7 @@ clk = clock();
Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
}
// quit if this is the last timeframe
if ( f == p->pPars->nFramesK - 1 )
@@ -312,6 +317,39 @@ p->timeBmc += clock() - clk;
return p->fRefined;
}
+
+/**Function*************************************************************
+
+ Synopsis [Generates AIG with the following nodes put into seq miters.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num )
+{
+ extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+ FILE * pFile;
+ char pBuffer[16];
+ Aig_Man_t * pNew;
+ sprintf( pBuffer, "equiv%03d.aig", Num );
+ pFile = fopen( pBuffer, "w" );
+ if ( pFile == NULL )
+ {
+ printf( "Cannot open file %s for writing.\n", pBuffer );
+ return;
+ }
+ fclose( pFile );
+ pNew = Saig_ManCreateEquivMiter( p, vPairs );
+ Ioa_WriteAiger( pNew, pBuffer, 0, 0 );
+ Aig_ManStop( pNew );
+ printf( "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer );
+}
+
+
/**Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.]
@@ -325,9 +363,11 @@ p->timeBmc += clock() - clk;
***********************************************************************/
int Ssw_ManSweep( Ssw_Man_t * p )
{
+ static int Counter;
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObj2, * pObjNew;
int nConstrPairs, clk, i, f;
+ Vec_Int_t * vDisproved;
// perform speculative reduction
clk = clock();
@@ -362,17 +402,18 @@ p->timeReduce += clock() - clk;
Ssw_ClassesClearRefined( p->ppClasses );
if ( p->pPars->fVerbose )
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+ vDisproved = p->pPars->fEquivDump? Vec_IntAlloc(1000) : NULL;
Aig_ManForEachObj( p->pAig, pObj, i )
{
if ( p->pPars->fVerbose )
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Saig_ObjIsLo(p->pAig, pObj) )
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
else if ( Aig_ObjIsNode(pObj) )
{
pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+ p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved );
}
}
if ( p->pPars->fVerbose )
@@ -380,6 +421,9 @@ p->timeReduce += clock() - clk;
// cleanup
// Ssw_ClassesCheck( p->ppClasses );
+ if ( p->pPars->fEquivDump )
+ Ssw_ManDumpEquivMiter( p->pAig, vDisproved, Counter++ );
+ Vec_IntFreeP( &vDisproved );
return p->fRefined;
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-13 22:52:53 +0000