summaryrefslogtreecommitdiffstats
path: root/src/aig/fra
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra')
-rw-r--r--src/aig/fra/fra.h10
-rw-r--r--src/aig/fra/fraCec.c48
-rw-r--r--src/aig/fra/fraClass.c42
-rw-r--r--src/aig/fra/fraCore.c63
-rw-r--r--src/aig/fra/fraImp.c826
-rw-r--r--src/aig/fra/fraInd.c34
-rw-r--r--src/aig/fra/fraMan.c1
-rw-r--r--src/aig/fra/fraPart.c177
-rw-r--r--src/aig/fra/fraSec.c95
-rw-r--r--src/aig/fra/fraSim.c11
-rw-r--r--src/aig/fra/module.make5
11 files changed, 1286 insertions, 26 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 5d357290..1051aa30 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -71,6 +71,7 @@ struct Fra_Par_t_
int nBTLimitMiter; // conflict limit at an output
int nFramesK; // the number of timeframes to unroll
int fRewrite; // use rewriting for constraint reduction
+ int fLatchCorr; // computes latch correspondence only
};
// FRAIG equivalence classes
@@ -101,6 +102,7 @@ struct Fra_Man_t_
int nFramesAll; // the number of timeframes used
Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes
// simulation info
+ void * pSim; // the simulation manager
unsigned * pSimWords; // memory for simulation information
int nSimWords; // the number of simulation words
// counter example storage
@@ -187,21 +189,23 @@ extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig );
extern void Fra_ClassesStop( Fra_Cla_t * p );
extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
-extern void Fra_ClassesPrepare( Fra_Cla_t * p );
+extern void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
extern int Fra_ClassesRefine( Fra_Cla_t * p );
extern int Fra_ClassesRefine1( Fra_Cla_t * p );
extern int Fra_ClassesCountLits( Fra_Cla_t * p );
extern int Fra_ClassesCountPairs( Fra_Cla_t * p );
extern void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
+extern void Fra_ClassesLatchCorr( Fra_Man_t * p );
/*=== fraCnf.c ========================================================*/
extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
/*=== fraCore.c ========================================================*/
extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig );
extern void Fra_FraigSweep( Fra_Man_t * pManAig );
+extern int Fra_FraigMiterStatus( Aig_Man_t * p );
/*=== fraDfs.c ========================================================*/
/*=== fraInd.c ========================================================*/
-extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fVerbose );
+extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -214,6 +218,8 @@ extern void Fra_ManPrint( Fra_Man_t * p );
/*=== fraSat.c ========================================================*/
extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
+/*=== fraSec.c ========================================================*/
+extern int Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose );
/*=== fraSim.c ========================================================*/
extern int Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
extern int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
new file mode 100644
index 00000000..e705f4fc
--- /dev/null
+++ b/src/aig/fra/fraCec.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+ FileName [fraCec.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis [CEC engined based on fraiging.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 31d6270a..8923c7b0 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -250,7 +250,7 @@ void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
SeeAlso []
***********************************************************************/
-void Fra_ClassesPrepare( Fra_Cla_t * p )
+void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
{
Aig_Obj_t ** ppTable, ** ppNexts;
Aig_Obj_t * pObj, * pTemp;
@@ -266,8 +266,16 @@ void Fra_ClassesPrepare( Fra_Cla_t * p )
Vec_PtrClear( p->vClasses1 );
Aig_ManForEachObj( p->pAig, pObj, i )
{
- if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
- continue;
+ if ( fLatchCorr )
+ {
+ if ( !Aig_ObjIsPi(pObj) )
+ continue;
+ }
+ else
+ {
+ if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+ continue;
+ }
//printf( "%3d : ", pObj->Id );
//Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
//printf( "\n" );
@@ -312,7 +320,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p )
// allocate room for classes
p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
p->pMemClassesFree = p->pMemClasses + 2*nEntries;
-
+
// copy the entries into storage in the topological order
Vec_PtrClear( p->vClasses );
nEntries = 0;
@@ -563,6 +571,32 @@ void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
Vec_PtrPush( p->vClasses, pClass );
}
+/**Function*************************************************************
+
+ Synopsis [Creates latch correspondence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ClassesLatchCorr( Fra_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i, nEntries = 0;
+ Vec_PtrClear( p->pCla->vClasses1 );
+ Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+ {
+ Vec_PtrPush( p->pCla->vClasses1, pObj );
+ Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
+ }
+ // allocate room for classes
+ p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
+ p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 71e12a75..41d264bb 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -30,6 +30,63 @@
/**Function*************************************************************
+ Synopsis [Reports the status of the miter.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_FraigMiterStatus( Aig_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pObjNew;
+ int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
+ if ( p->pData )
+ return 0;
+ Aig_ManForEachPoSeq( p, pObj, i )
+ {
+ pObjNew = Aig_ObjChild0(pObj);
+ // check if the output is constant 0
+ if ( pObjNew == Aig_ManConst0(p) )
+ {
+ CountConst0++;
+ continue;
+ }
+ // check if the output is constant 1
+ if ( pObjNew == Aig_ManConst1(p) )
+ {
+ CountNonConst0++;
+ continue;
+ }
+ // check if the output can be constant 0
+ if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
+ {
+ CountNonConst0++;
+ continue;
+ }
+ CountUndecided++;
+ }
+/*
+ if ( p->pParams->fVerbose )
+ {
+ printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) );
+ printf( "Const0 = %d. ", CountConst0 );
+ printf( "NonConst0 = %d. ", CountNonConst0 );
+ printf( "Undecided = %d. ", CountUndecided );
+ printf( "\n" );
+ }
+*/
+ if ( CountNonConst0 )
+ return 0;
+ if ( CountUndecided )
+ return -1;
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Write speculative miter for one node.]
Description []
@@ -121,9 +178,9 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
Vec_PtrPush( p->vTimeouts, pObj );
// simulate the counter-example and return the Fraig node
Fra_Resimulate( p );
- assert( Fra_ClassObjRepr(pObj) != pObjRepr );
if ( Fra_ClassObjRepr(pObj) == pObjRepr )
printf( "Fra_FraigNode(): Error in class refinement!\n" );
+ assert( Fra_ClassObjRepr(pObj) != pObjRepr );
}
/**Function*************************************************************
@@ -196,7 +253,7 @@ clk = clock();
Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
// collect initial states
p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
- p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
+ p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
p->nNodesBeg = Aig_ManNodeNum(pManAig);
p->nRegsBeg = Aig_ManRegNum(pManAig);
// perform fraig sweep
@@ -228,7 +285,7 @@ p->timeTrav += clock() - clk2;
}
p->timeTotal = clock() - clk;
// collect final stats
- p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
+ p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
p->nRegsEnd = Aig_ManRegNum(pManAigNew);
Fra_ManStop( p );
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
new file mode 100644
index 00000000..9643b887
--- /dev/null
+++ b/src/aig/fra/fraImp.c
@@ -0,0 +1,826 @@
+/**CFile****************************************************************
+
+ FileName [fraImp.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis [Detecting and proving implications.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+// simulation manager
+typedef struct Sml_Man_t_ Sml_Man_t;
+struct Sml_Man_t_
+{
+ Aig_Man_t * pAig;
+ int nFrames;
+ int nWordsFrame;
+ int nWordsTotal;
+ unsigned pData[0];
+};
+
+static inline unsigned * Sml_ObjSim( Sml_Man_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; }
+static inline int Sml_ImpLeft( int Imp ) { return Imp & 0xFFFF; }
+static inline int Sml_ImpRight( int Imp ) { return Imp >> 16; }
+static inline int Sml_ImpCreate( int Left, int Right ) { return (Right << 16) | Left; }
+
+static int * s_ImpCost = NULL;
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Allocates simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sml_Man_t * Sml_ManStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame )
+{
+ Sml_Man_t * p;
+ assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) );
+ p = (Sml_Man_t *)malloc( sizeof(Sml_Man_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * nFrames * nWordsFrame );
+ memset( p, 0, sizeof(Sml_Man_t) + sizeof(unsigned) * nFrames * nWordsFrame );
+ p->nFrames = nFrames;
+ p->nWordsFrame = nWordsFrame;
+ p->nWordsTotal = nFrames * nWordsFrame;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates simulation manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_ManStop( Sml_Man_t * p )
+{
+ free( p );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Assigns random patterns to the PI node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_ManAssignRandom( Sml_Man_t * p, Aig_Obj_t * pObj )
+{
+ unsigned * pSims;
+ int i;
+ assert( Aig_ObjIsPi(pObj) );
+ pSims = Sml_ObjSim( p, pObj->Id );
+ for ( i = 0; i < p->nWordsTotal; i++ )
+ pSims[i] = Fra_ObjRandomSim();
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assigns constant patterns to the PI node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_ManAssignConst( Sml_Man_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
+{
+ unsigned * pSims;
+ int i;
+ assert( Aig_ObjIsPi(pObj) );
+ pSims = Sml_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
+ for ( i = 0; i < p->nWordsFrame; i++ )
+ pSims[i] = fConst1? ~(unsigned)0 : 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assings random simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_ManInitialize( Sml_Man_t * p, int fInit )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ if ( fInit )
+ {
+ assert( Aig_ManRegNum(p->pAig) > 0 );
+ assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+ // assign random info for primary inputs
+ Aig_ManForEachPiSeq( p->pAig, pObj, i )
+ Sml_ManAssignRandom( p, pObj );
+ // assign the initial state for the latches
+ Aig_ManForEachLoSeq( p->pAig, pObj, i )
+ Sml_ManAssignConst( p, pObj, 0, 0 );
+ }
+ else
+ {
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ Sml_ManAssignRandom( p, pObj );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Assings distance-1 simulation info for the PIs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_ManAssignDist1( Sml_Man_t * p, unsigned * pPat )
+{
+ Aig_Obj_t * pObj;
+ int f, i, k, Limit, nTruePis;
+ assert( p->nFrames > 0 );
+ if ( p->nFrames == 1 )
+ {
+ // copy the PI info
+ Aig_ManForEachPi( p->pAig, pObj, i )
+ Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
+ // flip one bit
+ Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
+ for ( i = 0; i < Limit; i++ )
+ Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
+ }
+ else
+ {
+ // copy the PI info for each frame
+ nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
+ for ( f = 0; f < p->nFrames; f++ )
+ Aig_ManForEachPiSeq( p->pAig, pObj, i )
+ Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
+ // copy the latch info
+ k = 0;
+ Aig_ManForEachLoSeq( p->pAig, pObj, i )
+ Sml_ManAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
+// assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
+
+ // flip one bit of the last frame
+ if ( p->nFrames == 2 )
+ {
+ Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
+ for ( i = 0; i < Limit; i++ )
+ Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
+// Aig_InfoXorBit( Sml_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 );
+ }
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_NodeSimulate( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+{
+ unsigned * pSims, * pSims0, * pSims1;
+ int fCompl, fCompl0, fCompl1, i;
+ int nSimWords = p->nWordsFrame;
+ assert( !Aig_IsComplement(pObj) );
+ assert( Aig_ObjIsNode(pObj) );
+ assert( iFrame == 0 || nSimWords < p->nWordsTotal );
+ // get hold of the simulation information
+ pSims = Fra_ObjSim(pObj) + nSimWords * iFrame;
+ pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
+ pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame;
+ // get complemented attributes of the children using their random info
+ fCompl = pObj->fPhase;
+ fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
+ fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
+ // simulate
+ if ( fCompl0 && fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = (pSims0[i] | pSims1[i]);
+ else
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = ~(pSims0[i] | pSims1[i]);
+ }
+ else if ( fCompl0 && !fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = (pSims0[i] | ~pSims1[i]);
+ else
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = (~pSims0[i] & pSims1[i]);
+ }
+ else if ( !fCompl0 && fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = (~pSims0[i] | pSims1[i]);
+ else
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = (pSims0[i] & ~pSims1[i]);
+ }
+ else // if ( !fCompl0 && !fCompl1 )
+ {
+ if ( fCompl )
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = ~(pSims0[i] & pSims1[i]);
+ else
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = (pSims0[i] & pSims1[i]);
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_NodeCopyFanin( Sml_Man_t * p, Aig_Obj_t * pObj, int iFrame )
+{
+ unsigned * pSims, * pSims0;
+ int fCompl, fCompl0, i;
+ int nSimWords = p->nWordsFrame;
+ assert( !Aig_IsComplement(pObj) );
+ assert( Aig_ObjIsPo(pObj) );
+ assert( iFrame == 0 || nSimWords < p->nWordsTotal );
+ // get hold of the simulation information
+ pSims = Sml_ObjSim(p, pObj->Id) + nSimWords * iFrame;
+ pSims0 = Sml_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + nSimWords * iFrame;
+ // get complemented attributes of the children using their random info
+ fCompl = pObj->fPhase;
+ fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
+ // copy information as it is
+ if ( fCompl0 )
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = ~pSims0[i];
+ else
+ for ( i = 0; i < nSimWords; i++ )
+ pSims[i] = pSims0[i];
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates one node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_NodeTransferNext( Sml_Man_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
+{
+ unsigned * pSims0, * pSims1;
+ int i, nSimWords = p->nWordsFrame;
+ assert( !Aig_IsComplement(pOut) );
+ assert( !Aig_IsComplement(pIn) );
+ assert( Aig_ObjIsPo(pOut) );
+ assert( Aig_ObjIsPi(pIn) );
+ assert( iFrame == 0 || nSimWords < p->nWordsTotal );
+ // get hold of the simulation information
+ pSims0 = Sml_ObjSim(p, pOut->Id) + nSimWords * iFrame;
+ pSims1 = Sml_ObjSim(p, pIn->Id) + nSimWords * (iFrame+1);
+ // copy information as it is
+ for ( i = 0; i < nSimWords; i++ )
+ pSims1[i] = pSims0[i];
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Simulates AIG manager.]
+
+ Description [Assumes that the PI simulation info is attached.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sml_SimulateOne( Sml_Man_t * p )
+{
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int f, i, clk;
+clk = clock();
+ for ( f = 0; f < p->nFrames; f++ )
+ {
+ // simulate the nodes
+ Aig_ManForEachNode( p->pAig, pObj, i )
+ Sml_NodeSimulate( p, pObj, f );
+ if ( f == p->nFrames - 1 )
+ break;
+ // copy simulation info into outputs
+ Aig_ManForEachLiSeq( p->pAig, pObj, i )
+ Sml_NodeCopyFanin( p, pObj, f );
+ // copy simulation info into the inputs
+// for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+// Sml_NodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f );
+ Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
+ Sml_NodeTransferNext( p, pObjLi, pObjLo, f );
+ }
+//p->timeSim += clock() - clk;
+//p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs simulation of the uninitialized circuit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sml_Man_t * Sml_ManSimulateComb( Aig_Man_t * pAig, int nWords )
+{
+ Sml_Man_t * p;
+ p = Sml_ManStart( pAig, 1, nWords );
+ Sml_ManInitialize( p, 0 );
+ Sml_SimulateOne( p );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs simulation of the initialized circuit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sml_Man_t * Sml_ManSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords )
+{
+ Sml_Man_t * p;
+ p = Sml_ManStart( pAig, nFrames, nWords );
+ Sml_ManInitialize( p, 1 );
+ Sml_SimulateOne( p );
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of 1s in each siminfo of each node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int * Sml_ManCountOnes( Sml_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ unsigned * pSim;
+ int i, k, * pnBits;
+ pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
+ memset( pnBits, 0, sizeof(int) * Aig_ManObjIdMax(p->pAig) + 1 );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ pSim = Sml_ObjSim( p, i );
+ for ( k = 0; k < p->nWordsTotal; k++ )
+ pnBits[i] += Aig_WordCountOnes( pSim[k] );
+ }
+ return pnBits;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Counts the number of 1s in the reverse implication.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sml_NodeNotImpCost( Sml_Man_t * p, int Left, int Right )
+{
+ unsigned * pSimL, * pSimR;
+ int k, Counter = 0;
+ pSimL = Sml_ObjSim( p, Left );
+ pSimR = Sml_ObjSim( p, Right );
+ for ( k = 0; k < p->nWordsTotal; k++ )
+ Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if implications holds.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sml_NodeCheckImp( Sml_Man_t * p, int Left, int Right )
+{
+ unsigned * pSimL, * pSimR;
+ int k;
+ pSimL = Sml_ObjSim( p, Left );
+ pSimR = Sml_ObjSim( p, Right );
+ for ( k = 0; k < p->nWordsTotal; k++ )
+ if ( pSimL[k] & ~pSimR[k] )
+ return 0;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the array of nodes sorted by the number of 1s.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Sml_ManSortUsingOnes( Sml_Man_t * p )
+{
+ Aig_Obj_t * pObj;
+ Vec_Ptr_t * vNodes;
+ int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
+ // count 1s in each node's siminfo
+ pnBits = Sml_ManCountOnes( p );
+ // count number of nodes having that many 1s
+ nBits = p->nWordsTotal * 32;
+ assert( nBits >= 32 );
+ nNodes = 0;
+ pnNodes = ALLOC( int, nBits );
+ memset( pnNodes, 0, sizeof(int) * nBits );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ if ( i == 0 ) continue;
+ assert( pnBits[i] < nBits ); // "<" because of normalized info
+ pnNodes[pnBits[i]]++;
+ nNodes++;
+ }
+ // allocate memory for all the nodes
+ pMemory = ALLOC( int, nNodes + nBits );
+ // markup the memory for each node
+ vNodes = Vec_PtrAlloc( nBits );
+ Vec_PtrPush( vNodes, pMemory );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ if ( i == 0 ) continue;
+ pMemory += pnBits[i-1] + 1;
+ Vec_PtrPush( vNodes, pMemory );
+ }
+ // add the nodes
+ memset( pnNodes, 0, sizeof(int) * nBits );
+ Aig_ManForEachObj( p->pAig, pObj, i )
+ {
+ if ( i == 0 ) continue;
+ pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
+ pMemory[ pnNodes[pnBits[i]]++ ] = i;
+ }
+ // add 0s in the end
+ nTotal = 0;
+ Vec_PtrForEachEntry( vNodes, pMemory, i )
+ {
+ pMemory[ pnNodes[i]++ ] = 0;
+ nTotal += pnNodes[i];
+ }
+ assert( nTotal == nNodes + nBits );
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compares two implications using their cost.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sml_CompareCost( int * pNum1, int * pNum2 )
+{
+ int Cost1 = s_ImpCost[*pNum1];
+ int Cost2 = s_ImpCost[*pNum2];
+ if ( Cost1 > Cost2 )
+ return -1;
+ if ( Cost1 < Cost2 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Compares two implications using their largest ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
+{
+ int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
+ int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
+ if ( Max1 < Max2 )
+ return -1;
+ if ( Max1 > Max2 )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Derives implication candidates.]
+
+ Description [Implication candidates have the property that
+ (1) they hold using sequential simulation information
+ (2) they do not hold using combinational simulation information
+ (3) they have as high expressive power as possible (heuristically)
+ - this means they are relatively far in terms of Humming distance
+ meaning their complement covers a larger Boolean space
+ - they are easy to disprove combinationally
+ meaning they cover relatively a larger sequential subspace.]
+
+ SideEffects [The managers should have the first pattern (000...)]
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Sml_ManImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit )
+{
+ Sml_Man_t * pSeq, * pComb;
+ Vec_Int_t * vImps, * vTemp;
+ Vec_Ptr_t * vNodes;
+ int * pNodesI, * pNodesK, * pNumbers;
+ int i, k, Imp;
+ assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
+ // normalize both managers
+ pComb = Sml_ManSimulateComb( p->pManAig, 32 );
+ pSeq = Sml_ManSimulateSeq( p->pManAig, 32, 1 );
+ // get the nodes sorted by the number of 1s
+ vNodes = Sml_ManSortUsingOnes( pSeq );
+ // compute implications and their costs
+ s_ImpCost = ALLOC( int, nImpMaxLimit );
+ vImps = Vec_IntAlloc( nImpMaxLimit );
+ for ( k = pSeq->nWordsTotal * 32 - 1; k >= 0; k-- )
+ for ( i = k - 1; i >= 0; i-- )
+ {
+ for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
+ for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
+ {
+ if ( Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) &&
+ !Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
+ {
+ Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
+ s_ImpCost[ Vec_IntSize(vImps) ] = Sml_NodeNotImpCost(pComb, *pNodesI, *pNodesK);
+ Vec_IntPush( vImps, Imp );
+ }
+ if ( Vec_IntSize(vImps) == nImpMaxLimit )
+ goto finish;
+ }
+ }
+finish:
+ Sml_ManStop( pComb );
+ Sml_ManStop( pSeq );
+
+ // sort implications by their cost
+ pNumbers = ALLOC( int, Vec_IntSize(vImps) );
+ for ( i = 0; i < Vec_IntSize(vImps); i++ )
+ pNumbers[i] = i;
+ qsort( (void *)pNumbers, Vec_IntSize(vImps), sizeof(int),
+ (int (*)(const void *, const void *)) Sml_CompareCost );
+ // reorder implications
+ vTemp = Vec_IntAlloc( nImpUseLimit );
+ for ( i = 0; i < nImpUseLimit; i++ )
+ Vec_IntPush( vTemp, Vec_IntEntry( vImps, pNumbers[i] ) );
+ Vec_IntFree( vImps ); vImps = vTemp;
+ // dealloc
+ free( pNumbers );
+ free( s_ImpCost ); s_ImpCost = NULL;
+ free( Vec_PtrEntry(vNodes, 0) );
+ Vec_PtrFree( vNodes );
+ // order implications by the max ID involved
+ qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int),
+ (int (*)(const void *, const void *)) Sml_CompareMaxId );
+ return vImps;
+}
+
+// the following three procedures are called to
+// - add implications to the SAT solver
+// - check implications using the SAT solver
+// - refine implications using after a cex is generated
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps )
+{
+ sat_solver * pSat = p->pSat;
+ Aig_Obj_t * pLeft, * pRight;
+ Aig_Obj_t * pLeftF, * pRightF;
+ int pLits[2], Imp, Left, Right, i, f, status;
+ Vec_IntForEachEntry( vImps, Imp, i )
+ {
+ // get the corresponding nodes
+ pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
+ pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
+ // add constraints in each timeframe
+ for ( f = 0; f < p->pPars->nFramesK; f++ )
+ {
+ // map these info fraig
+ pLeftF = Fra_ObjFraig( pLeft, f );
+ pRightF = Fra_ObjFraig( pRight, f );
+ // get the corresponding SAT numbers
+ Left = Fra_ObjSatNum( Aig_Regular(pLeftF) );
+ Right = Fra_ObjSatNum( Aig_Regular(pRightF) );
+ assert( Left > 0 && Left < p->nSatVars );
+ assert( Right > 0 && Right < p->nSatVars );
+ // get the constaint
+ // L => R L' v R L & R'
+ pLits[0] = 2 * Left + !Aig_ObjPhaseReal(pLeftF);
+ pLits[1] = 2 * Right + Aig_ObjPhaseReal(pRightF);
+ // add contraint to solver
+ if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
+ {
+ sat_solver_delete( pSat );
+ p->pSat = NULL;
+ return;
+ }
+ }
+ }
+ status = sat_solver_simplify(pSat);
+ if ( status == 0 )
+ {
+ sat_solver_delete( pSat );
+ p->pSat = NULL;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check implications for the node (if they are present).]
+
+ Description [Returns the new position in the array.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
+{
+ Aig_Obj_t * pLeft, * pRight;
+ int i, Imp, Left, Right, Max;
+ Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
+ {
+ Left = Sml_ImpLeft(Imp);
+ Right = Sml_ImpRight(Imp);
+ Max = AIG_MAX( Left, Right );
+ assert( Max >= pNode->Id );
+ if ( Max > pNode->Id )
+ return i;
+ // get the corresponding nodes
+ pLeft = Aig_ManObj( p->pManAig, Left );
+ pRight = Aig_ManObj( p->pManAig, Right );
+ // check the implication
+ // - if true, a clause is added
+ // - if false, a cex is simulated
+// Fra_NodesAreImp( p, pLeft, pRight );
+ // make sure the implication is refined
+ assert( Vec_IntEntry(vImps, Pos) == 0 );
+ }
+ return i;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes those implications that no longer hold.]
+
+ Description [Returns 1 if refinement has happened.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
+{
+ Aig_Obj_t * pLeft, * pRight;
+ int Imp, i, RetValue = 0;
+ Vec_IntForEachEntry( vImps, Imp, i )
+ {
+ if ( Imp == 0 )
+ continue;
+ // get the corresponding nodes
+ pLeft = Aig_ManObj( p->pManAig, Sml_ImpLeft(Imp) );
+ pRight = Aig_ManObj( p->pManAig, Sml_ImpRight(Imp) );
+ // check if implication holds using this simulation info
+ if ( !Sml_NodeCheckImp(p->pSim, pLeft->Id, pRight->Id) )
+ {
+ Vec_IntWriteEntry( vImps, i, 0 );
+ RetValue = 1;
+ }
+ }
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Removes empty implications.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ImpCompactArray( Vec_Int_t * vImps )
+{
+ int i, k, Imp;
+ k = 0;
+ Vec_IntForEachEntry( vImps, Imp, i )
+ if ( Imp )
+ Vec_IntWriteEntry( vImps, k++, Imp );
+ Vec_IntShrink( vImps, k );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index bb4c4287..4a7d7b7e 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -198,7 +198,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fVerbose )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter )
{
Fra_Man_t * p;
Fra_Par_t Pars, * pPars = &Pars;
@@ -208,7 +208,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
int nIter, i, clk = clock(), clk2;
if ( Aig_ManNodeNum(pManAig) == 0 )
+ {
+ if ( pnIter ) *pnIter = 0;
return Aig_ManDup(pManAig, 1);
+ }
assert( Aig_ManLatchNum(pManAig) == 0 );
assert( Aig_ManRegNum(pManAig) > 0 );
assert( nFramesK > 0 );
@@ -216,14 +219,18 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
// get parameters
Fra_ParamsDefaultSeq( pPars );
- pPars->nFramesK = nFramesK;
- pPars->fVerbose = fVerbose;
- pPars->fRewrite = fRewrite;
+ pPars->nFramesK = nFramesK;
+ pPars->fVerbose = fVerbose;
+ pPars->fRewrite = fRewrite;
+ pPars->fLatchCorr = fLatchCorr;
// start the fraig manager for this run
p = Fra_ManStart( pManAig, pPars );
// derive and refine e-classes using K initialized frames
- Fra_Simulate( p, 1 );
+// if ( fLatchCorr )
+// Fra_ClassesLatchCorr( p );
+// else
+ Fra_Simulate( p, 1 );
// refine e-classes using sequential simulation?
p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
@@ -239,6 +246,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
p->pCla->fRefinement = 0;
// derive non-init K-timeframes while implementing e-classes
p->pManFraig = Fra_FramesWithClasses( p );
+//Aig_ManDumpBlif( p->pManFraig, "testaig.blif" );
+
// perform AIG rewriting
if ( p->pPars->fRewrite )
Fra_FraigInductionRewrite( p );
@@ -252,8 +261,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
}
// convert the manager to SAT solver (the last nLatches outputs are inputs)
- pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-// pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+// pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+ pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
p->pSat = Cnf_DataWriteIntoSolver( pCnf );
@@ -278,7 +287,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
Fra_ObjSetFaninVec( pObj, (void *)1 );
}
Cnf_DataFree( pCnf );
-/*
+/*
Aig_ManForEachObj( p->pManFraig, pObj, i )
{
Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
@@ -300,6 +309,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
clk2 = clock();
Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
pManAigNew = Aig_ManDupRepr( pManAig );
+ Aig_ManSeqCleanup( pManAigNew );
+// Aig_ManCountMergeRegs( pManAigNew );
p->timeTrav += clock() - clk2;
p->timeTotal = clock() - clk;
// get the final stats
@@ -309,9 +320,10 @@ p->timeTotal = clock() - clk;
// free the manager
Fra_ManStop( p );
// check the output
- if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
- if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
- printf( "Proved output constant 0.\n" );
+// if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
+// if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
+// printf( "Proved output constant 0.\n" );
+ if ( pnIter ) *pnIter = nIter;
return pManAigNew;
}
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 95cf28d8..4dcc4988 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -86,6 +86,7 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
pPars->nFramesK = 1; // the number of timeframes to unroll
pPars->fConeBias = 0;
pPars->fRewrite = 0;
+ pPars->fLatchCorr = 0;
}
/**Function*************************************************************
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
new file mode 100644
index 00000000..d3fdbcfd
--- /dev/null
+++ b/src/aig/fra/fraPart.c
@@ -0,0 +1,177 @@
+/**CFile****************************************************************
+
+ FileName [fraPart.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis [Partitioning for induction.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraPart.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
+{
+ ProgressBar * pProgress;
+ Vec_Vec_t * vSupps, * vSuppsIn;
+ Vec_Ptr_t * vSuppsNew;
+ Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
+ Vec_Int_t * vOverNew, * vQuantNew;
+ Aig_Obj_t * pObj;
+ int i, k, nCommon, CountOver, CountQuant;
+ int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
+ double Ratio, R;
+ int clk;
+
+ nTotalSupp = 0;
+ nTotalSupp2 = 0;
+ Ratio = 0.0;
+
+ // compute supports
+clk = clock();
+ vSupps = Aig_ManSupports( p );
+PRT( "Supports", clock() - clk );
+ // remove last entry
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ vSup = Vec_VecEntry( vSupps, i );
+ Vec_IntPop( vSup );
+ // remember support
+// pObj->pNext = (Aig_Obj_t *)vSup;
+ }
+
+ // create reverse supports
+clk = clock();
+ vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ vSup = Vec_VecEntry( vSupps, i );
+ Vec_IntForEachEntry( vSup, Entry, k )
+ Vec_VecPush( vSuppsIn, Entry, (void *)i );
+ }
+PRT( "Inverse ", clock() - clk );
+
+clk = clock();
+ // compute extended supports
+ Largest = 0;
+ vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
+ vOverNew = Vec_IntAlloc( Aig_ManPoNum(p) );
+ vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
+ pProgress = Extra_ProgressBarStart( stdout, Aig_ManPoNum(p) );
+ Aig_ManForEachPo( p, pObj, i )
+ {
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ // get old supports
+ vSup = Vec_VecEntry( vSupps, i );
+ if ( Vec_IntSize(vSup) < 2 )
+ continue;
+ // compute new supports
+ CountOver = CountQuant = 0;
+ vSupNew = Vec_IntDup( vSup );
+ // go through the nodes where the first var appears
+ Aig_ManForEachPo( p, pObj, k )
+// iVar = Vec_IntEntry( vSup, 0 );
+// vSupIn = Vec_VecEntry( vSuppsIn, iVar );
+// Vec_IntForEachEntry( vSupIn, Entry, k )
+ {
+// pObj = Aig_ManObj( p, Entry );
+ // get support of this output
+// vSup2 = (Vec_Int_t *)pObj->pNext;
+ vSup2 = Vec_VecEntry( vSupps, k );
+ // count the number of common vars
+ nCommon = Vec_IntTwoCountCommon(vSup, vSup2);
+ if ( nCommon < 2 )
+ continue;
+ if ( nCommon > nComLim )
+ {
+ vSupNew = Vec_IntTwoMerge( vTemp = vSupNew, vSup2 );
+ Vec_IntFree( vTemp );
+ CountOver++;
+ }
+ else
+ CountQuant++;
+ }
+ // save the results
+ Vec_PtrPush( vSuppsNew, vSupNew );
+ Vec_IntPush( vOverNew, CountOver );
+ Vec_IntPush( vQuantNew, CountQuant );
+
+ if ( Largest < Vec_IntSize(vSupNew) )
+ Largest = Vec_IntSize(vSupNew);
+
+ nTotalSupp += Vec_IntSize(vSup);
+ nTotalSupp2 += Vec_IntSize(vSupNew);
+ if ( Vec_IntSize(vSup) )
+ R = Vec_IntSize(vSupNew) / Vec_IntSize(vSup);
+ else
+ R = 0;
+ Ratio += R;
+
+ if ( R < 5.0 )
+ continue;
+
+ printf( "%6d : ", i );
+ printf( "S = %5d. ", Vec_IntSize(vSup) );
+ printf( "SNew = %5d. ", Vec_IntSize(vSupNew) );
+ printf( "R = %7.2f. ", R );
+ printf( "Over = %5d. ", CountOver );
+ printf( "Quant = %5d. ", CountQuant );
+ printf( "\n" );
+/*
+ Vec_IntForEachEntry( vSupNew, Entry, k )
+ printf( "%d ", Entry );
+ printf( "\n" );
+*/
+ }
+ Extra_ProgressBarStop( pProgress );
+PRT( "Scanning", clock() - clk );
+
+ // print cumulative statistics
+ printf( "PIs = %6d. POs = %6d. Lim = %3d. AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
+ Aig_ManPiNum(p), Aig_ManPoNum(p), nComLim,
+ nTotalSupp/Aig_ManPoNum(p), nTotalSupp2/Aig_ManPoNum(p),
+ Ratio/Aig_ManPoNum(p), Largest );
+
+ Vec_VecFree( vSupps );
+ Vec_VecFree( vSuppsIn );
+ Vec_VecFree( (Vec_Vec_t *)vSuppsNew );
+ Vec_IntFree( vOverNew );
+ Vec_IntFree( vQuantNew );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
new file mode 100644
index 00000000..6afa6f89
--- /dev/null
+++ b/src/aig/fra/fraSec.c
@@ -0,0 +1,95 @@
+/**CFile****************************************************************
+
+ FileName [fraSec.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [New FRAIG package.]
+
+ Synopsis [Performs SEC based on seq sweeping.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 30, 2007.]
+
+ Revision [$Id: fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
+{
+ Aig_Man_t * pNew;
+ int nFrames, RetValue, nIter, clk, clkTotal = clock();
+ if ( nFramesFix )
+ {
+ nFrames = nFramesFix;
+ // perform seq sweeping for one frame number
+ pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
+ }
+ else
+ {
+ // perform seq sweeping while increasing the number of frames
+ for ( nFrames = 1; ; nFrames++ )
+ {
+clk = clock();
+ pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
+ RetValue = Fra_FraigMiterStatus( pNew );
+ if ( fVerbose )
+ {
+ printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
+ if ( RetValue == 1 )
+ printf( "UNSAT " );
+ else
+ printf( "UNDECIDED " );
+PRT( "Time", clock() - clk );
+ }
+ if ( RetValue != -1 )
+ break;
+ Aig_ManStop( pNew );
+ }
+ }
+
+ // get the miter status
+ RetValue = Fra_FraigMiterStatus( pNew );
+ Aig_ManStop( pNew );
+
+ // report the miter
+ if ( RetValue == 1 )
+ printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
+ else if ( RetValue == 0 )
+ printf( "Networks are NOT EQUIVALENT. " );
+ else
+ printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
+PRT( "Time", clock() - clkTotal );
+ return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 4a6e0251..c17cea9f 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -537,7 +537,7 @@ int Fra_SelectBestPat( Fra_Man_t * p )
***********************************************************************/
void Fra_SimulateOne( Fra_Man_t * p )
{
- Aig_Obj_t * pObj;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int f, i, clk;
clk = clock();
for ( f = 0; f < p->nFramesAll; f++ )
@@ -551,9 +551,10 @@ clk = clock();
Aig_ManForEachLiSeq( p->pManAig, pObj, i )
Fra_NodeCopyFanin( p, pObj, f );
// copy simulation info into the inputs
- for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
- Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f );
-
+// for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
+// Fra_NodeTransferNext( p, Aig_ManLi(p->pManAig, i), Aig_ManLo(p->pManAig, i), f );
+ Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, i )
+ Fra_NodeTransferNext( p, pObjLi, pObjLo, f );
}
p->timeSim += clock() - clk;
p->nSimRounds++;
@@ -627,7 +628,7 @@ void Fra_Simulate( Fra_Man_t * p, int fInit )
// start the classes
Fra_AssignRandom( p, fInit );
Fra_SimulateOne( p );
- Fra_ClassesPrepare( p->pCla );
+ Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
// Fra_ClassesPrint( p->pCla, 0 );
//printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index 191427c9..f2a8b230 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -1,7 +1,10 @@
-SRC += src/aig/fra/fraClass.c \
+SRC += src/aig/fra/fraCec.c \
+ src/aig/fra/fraClass.c \
src/aig/fra/fraCnf.c \
src/aig/fra/fraCore.c \
+ src/aig/fra/fraImp.c \
src/aig/fra/fraInd.c \
src/aig/fra/fraMan.c \
src/aig/fra/fraSat.c \
+ src/aig/fra/fraSec.c \
src/aig/fra/fraSim.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 20:31:05 +0000