summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/aig/aig.h15
-rw-r--r--src/aig/aig/aigMan.c5
-rw-r--r--src/aig/aig/aigScl.c9
-rw-r--r--src/aig/aig/aigTime.c299
-rw-r--r--src/aig/fra/fra.h3
-rw-r--r--src/aig/fra/fraBmc.c25
-rw-r--r--src/aig/fra/fraImp.c33
-rw-r--r--src/aig/fra/fraInd.c7
-rw-r--r--src/aig/fra/fraLcr.c33
-rw-r--r--src/aig/fra/fraSat.c9
-rw-r--r--src/aig/fra/fraSec.c33
-rw-r--r--src/aig/fra/fraSim.c50
-rw-r--r--src/aig/ivy/ivyFraig.c6
-rw-r--r--src/aig/kit/kitDsd.c2
-rw-r--r--src/base/abci/abc.c2
-rw-r--r--src/base/abci/abcDar.c23
-rw-r--r--src/base/abci/abcStrash.c4
-rw-r--r--src/base/seq/seqCreate.c2
-rw-r--r--src/base/seq/seqRetCore.c2
19 files changed, 515 insertions, 47 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index d5c2a4db..fe237142 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -50,6 +50,7 @@ typedef struct Aig_Obj_t_ Aig_Obj_t;
typedef struct Aig_MmFixed_t_ Aig_MmFixed_t;
typedef struct Aig_MmFlex_t_ Aig_MmFlex_t;
typedef struct Aig_MmStep_t_ Aig_MmStep_t;
+typedef struct Aig_TMan_t_ Aig_TMan_t;
// object types
typedef enum {
@@ -131,6 +132,7 @@ struct Aig_Man_t_
Aig_Obj_t ** pObjCopies; // mapping of AIG nodes into FRAIG nodes
void (*pImpFunc) (void*, void*); // implication checking precedure
void * pImpData; // implication checking data
+ Aig_TMan_t * pManTime; // the timing manager
// timing statistics
int time1;
int time2;
@@ -520,6 +522,19 @@ extern char * Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes );
extern void Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes );
extern int Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
+/*=== aigTime.c ===========================================================*/
+extern Aig_TMan_t * Aig_TManStart( int nPis, int nPos );
+extern void Aig_TManStop( Aig_TMan_t * p );
+extern void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes );
+extern void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay );
+extern void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay );
+extern void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay );
+extern void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay );
+extern void Aig_TManIncrementTravId( Aig_TMan_t * p );
+extern float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi );
+extern float Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo );
+
+
#ifdef __cplusplus
}
#endif
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 30a7991a..1e0ee278 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -229,6 +229,9 @@ void Aig_ManStop( Aig_Man_t * p )
// print time
if ( p->time1 ) { PRT( "time1", p->time1 ); }
if ( p->time2 ) { PRT( "time2", p->time2 ); }
+ // delete timing
+ if ( p->pManTime )
+ Aig_TManStop( p->pManTime );
// delete fanout
if ( p->pFanData )
Aig_ManFanoutStop( p );
@@ -304,6 +307,8 @@ void Aig_ManPrintStats( Aig_Man_t * p )
// printf( "Lev = %3d. ", Aig_ManCountLevels(p) );
printf( "Max = %7d. ", Aig_ManObjNumMax(p) );
printf( "Lev = %3d. ", Aig_ManLevels(p) );
+ if ( Aig_ManRegNum(p) )
+ printf( "Lat = %5d. ", Aig_ManRegNum(p) );
printf( "\n" );
}
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 166377bf..2f00a7eb 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -157,12 +157,21 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
Aig_ManForEachPi( p, pObj, i )
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
Vec_PtrPush( vCis, pObj );
+ else
+ {
+ Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+// Aig_ManRecycleMemory( p, pObj );
+ }
vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
Aig_ManForEachPo( p, pObj, i )
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
Vec_PtrPush( vCos, pObj );
else
+ {
Aig_ObjDisconnect( p, pObj );
+ Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+// Aig_ManRecycleMemory( p, pObj );
+ }
// remember the number of true PIs/POs
nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
diff --git a/src/aig/aig/aigTime.c b/src/aig/aig/aigTime.c
new file mode 100644
index 00000000..42f5f575
--- /dev/null
+++ b/src/aig/aig/aigTime.c
@@ -0,0 +1,299 @@
+/**CFile****************************************************************
+
+ FileName [aigTime.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [AIG package.]
+
+ Synopsis [Representation of timing information.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: aigTime.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Aig_TBox_t_ Aig_TBox_t;
+typedef struct Aig_TObj_t_ Aig_TObj_t;
+
+// timing manager
+struct Aig_TMan_t_
+{
+ Vec_Ptr_t * vBoxes; // the timing boxes
+ Aig_MmFlex_t * pMemObj; // memory manager for boxes
+ int nTravIds; // traversal ID of the manager
+ int nPis; // the number of PIs
+ int nPos; // the number of POs
+ Aig_TObj_t * pPis; // timing info for the PIs
+ Aig_TObj_t * pPos; // timing info for the POs
+};
+
+// timing box
+struct Aig_TBox_t_
+{
+ int iBox; // the unique ID of this box
+ int TravId; // traversal ID of this box
+ int nInputs; // the number of box inputs
+ int nOutputs; // the number of box outputs
+ int Inouts[0]; // the int numbers of PIs and POs
+};
+
+// timing object
+struct Aig_TObj_t_
+{
+ int iObj2Box; // mapping of the object into its box
+ float timeOffset; // the static timing of the node
+ float timeActual; // the actual timing of the node
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Starts the network manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
+{
+ Aig_TMan_t * p;
+ int i;
+ p = ALLOC( Aig_TMan_t, 1 );
+ memset( p, 0, sizeof(Aig_TMan_t) );
+ p->pMemObj = Aig_MmFlexStart();
+ p->vBoxes = Vec_PtrAlloc( 100 );
+ Vec_PtrPush( p->vBoxes, NULL );
+ p->nPis = nPis;
+ p->nPos = nPos;
+ p->pPis = ALLOC( Aig_TObj_t, nPis );
+ memset( p->pPis, 0, sizeof(Aig_TObj_t) * nPis );
+ p->pPos = ALLOC( Aig_TObj_t, nPos );
+ memset( p->pPos, 0, sizeof(Aig_TObj_t) * nPos );
+ for ( i = 0; i < nPis; i++ )
+ p->pPis[i].iObj2Box = -1;
+ for ( i = 0; i < nPos; i++ )
+ p->pPos[i].iObj2Box = -1;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Stops the network manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TManStop( Aig_TMan_t * p )
+{
+ Vec_PtrFree( p->vBoxes );
+ Aig_MmFlexStop( p->pMemObj, 0 );
+ free( p->pPis );
+ free( p->pPos );
+ free( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the new timing box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes )
+{
+ Aig_TBox_t * pBox;
+ int i;
+ pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nPis+nPos) );
+ memset( pBox, 0, sizeof(Aig_TBox_t) );
+ pBox->iBox = Vec_PtrSize( p->vBoxes );
+ Vec_PtrPush( p->vBoxes, pBox );
+ pBox->nInputs = nPis;
+ pBox->nOutputs = nPos;
+ for ( i = 0; i < nPis; i++ )
+ {
+ assert( pPis[i] < p->nPis );
+ pBox->Inouts[i] = pPis[i];
+ Aig_TManSetPiArrival( p, pPis[i], pPiTimes[i] );
+ p->pPis[pPis[i]].iObj2Box = pBox->iBox;
+ }
+ for ( i = 0; i < nPos; i++ )
+ {
+ assert( pPos[i] < p->nPos );
+ pBox->Inouts[nPis+i] = pPos[i];
+ Aig_TManSetPoRequired( p, pPos[i], pPoTimes[i] );
+ p->pPos[pPos[i]].iObj2Box = pBox->iBox;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the new timing box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay )
+{
+ assert( iPi < p->nPis );
+ p->pPis[iPi].timeActual = Delay;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the new timing box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay )
+{
+ assert( iPo < p->nPos );
+ p->pPos[iPo].timeActual = Delay;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the new timing box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay )
+{
+ assert( iPi < p->nPis );
+ p->pPis[iPi].timeOffset = Delay;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the new timing box.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay )
+{
+ assert( iPo < p->nPos );
+ p->pPos[iPo].timeOffset = Delay;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Increments the trav ID of the manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_TManIncrementTravId( Aig_TMan_t * p )
+{
+ p->nTravIds++;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns PI arrival time.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi )
+{
+ Aig_TBox_t * pBox;
+ Aig_TObj_t * pObj;
+ float DelayMax;
+ int i;
+ assert( iPi < p->nPis );
+ if ( p->pPis[iPi].iObj2Box < 0 )
+ return p->pPis[iPi].timeOffset;
+ pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box );
+ // check if box timing is updated
+ if ( pBox->TravId == p->nTravIds )
+ return p->pPis[iPi].timeOffset;
+ pBox->TravId = p->nTravIds;
+ // update box timing
+ DelayMax = -1.0e+20F;
+ for ( i = 0; i < pBox->nOutputs; i++ )
+ {
+ pObj = p->pPos + pBox->Inouts[pBox->nInputs+i];
+ DelayMax = AIG_MAX( DelayMax, pObj->timeActual + pObj->timeOffset );
+ }
+ for ( i = 0; i < pBox->nInputs; i++ )
+ {
+ pObj = p->pPis + pBox->Inouts[i];
+ pObj->timeActual = DelayMax + pObj->timeOffset;
+ }
+ return p->pPis[iPi].timeActual;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns PO required time.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+float Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo )
+{
+ return 0.0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index cd6bdfd4..210af244 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -111,6 +111,7 @@ struct Fra_Sml_t_
int nWordsFrame; // the number of words in each time frame
int nWordsTotal; // the total number of words at a node
int nWordsPref; // the number of word in the prefix
+ int fNonConstOut; // have seen a non-const-0 output during simulation
int nSimRounds; // statistics
int timeSim; // statistics
unsigned pData[0]; // simulation data for the nodes
@@ -256,7 +257,7 @@ extern void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pN
/*=== fraInd.c ========================================================*/
extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
/*=== fraLcr.c ========================================================*/
-extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter );
+extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
/*=== fraMan.c ========================================================*/
extern void Fra_ParamsDefault( Fra_Par_t * pParams );
extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 1df25c0a..1140f3a4 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -128,7 +128,7 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
{
if ( Imp == 0 )
continue;
- Left = Fra_ImpLeft(Imp);
+ Left = Fra_ImpLeft(Imp);
Right = Fra_ImpRight(Imp);
// get the corresponding nodes
pLeft = Aig_ManObj( pBmc->pAig, Left );
@@ -136,7 +136,7 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
// iterate through the timeframes
for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
{
- // get timeframes nodes
+ // get timeframe nodes
pLeftT = Bmc_ObjFrames( pLeft, f );
pRightT = Bmc_ObjFrames( pRight, f );
// get the corresponding FRAIG nodes
@@ -148,14 +148,21 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
// check equality
if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
{
- if ( fComplL != fComplR )
- Vec_IntWriteEntry( pBmc->vImps, i, 0 );
+ if ( fComplL == fComplR ) // x => x - always true
+ continue;
+ assert( fComplL != fComplR );
+ // consider 4 possibilities:
+ // NOT(1) => 1 or 0 => 1 - always true
+ // 1 => NOT(1) or 1 => 0 - never true
+ // NOT(x) => x or x - not always true
+ // x => NOT(x) or NOT(x) - not always true
+ if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
+ continue;
+ // disproved implication
+ Vec_IntWriteEntry( pBmc->vImps, i, 0 );
break;
}
// check the implication
- // - if true, a clause is added
- // - if false, a cex is simulated
- // make sure the implication is refined
if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
{
Vec_IntWriteEntry( pBmc->vImps, i, 0 );
@@ -320,7 +327,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
// Fra_ClassesPrint( p->pCla, 0 );
printf( "Const = %5d. Class = %5d. Lit = %5d. ",
Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
- if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
+ if ( p->pCla->vImps )
printf( "Imp = %5d. ", nImpsOld );
printf( "\n" );
}
@@ -338,7 +345,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
// Fra_ClassesPrint( p->pCla, 0 );
printf( "Const = %5d. Class = %5d. Lit = %5d. ",
Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
- if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
+ if ( p->pCla->vImps )
printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
printf( "\n" );
}
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index d8bf4e48..a5fc7d58 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -96,7 +96,7 @@ static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
/**Function*************************************************************
- Synopsis [Counts the number of 1s in the reverse implication.]
+ Synopsis [Counts the number of 1s in the complement of the implication.]
Description []
@@ -118,7 +118,7 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
/**Function*************************************************************
- Synopsis [Counts the number of 1s in the reverse implication.]
+ Synopsis [Computes the complement of the implication.]
Description []
@@ -495,7 +495,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
{
Aig_Obj_t * pLeft, * pRight;
Aig_Obj_t * pLeftF, * pRightF;
- int i, Imp, Left, Right, Max;
+ int i, Imp, Left, Right, Max, RetValue;
int fComplL, fComplR;
Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
{
@@ -519,18 +519,31 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
// check equality
if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
{
- if ( fComplL != fComplR )
- Vec_IntWriteEntry( vImps, i, 0 );
+ if ( fComplL == fComplR ) // x => x - always true
+ continue;
+ assert( fComplL != fComplR );
+ // consider 4 possibilities:
+ // NOT(1) => 1 or 0 => 1 - always true
+ // 1 => NOT(1) or 1 => 0 - never true
+ // NOT(x) => x or x - not always true
+ // x => NOT(x) or NOT(x) - not always true
+ if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
+ continue;
+ // disproved implication
+ p->pCla->fRefinement = 1;
+ Vec_IntWriteEntry( vImps, i, 0 );
continue;
}
// check the implication
// - if true, a clause is added
// - if false, a cex is simulated
// make sure the implication is refined
- if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 )
+ RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
+ if ( RetValue != 1 )
{
p->pCla->fRefinement = 1;
- Fra_SmlResimulate( p );
+ if ( RetValue == 0 )
+ Fra_SmlResimulate( p );
if ( Vec_IntEntry(vImps, i) != 0 )
printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
assert( Vec_IntEntry(vImps, i) == 0 );
@@ -642,14 +655,15 @@ double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
***********************************************************************/
int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
{
- int nSimWords = 2000;
+ int nFrames = 2000;
+ int nSimWords = 8;
Fra_Sml_t * pSeq;
char * pfFails;
int Left, Right, Imp, i, Counter;
if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
return 0;
// simulate the AIG manager with combinational patterns
- pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 4 );
+ pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
// go through the implications and check how many of them do not hold
pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
@@ -664,6 +678,7 @@ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
Counter += pfFails[i];
free( pfFails );
+ Fra_SmlStop( pSeq );
return Counter;
}
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 14fba9ba..98025280 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -257,7 +257,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
Aig_Man_t * pManAigNew;
- int nNodesBeg, nRegsBeg, Temp;
+ int nNodesBeg, nRegsBeg;
int nIter, i, clk = clock(), clk2;
if ( Aig_ManNodeNum(pManAig) == 0 )
@@ -424,17 +424,18 @@ PRT( "Time", clock() - clk );
break;
}
}
+/*
// check implications using simulation
if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
{
- int clk = clock();
+ int Temp, clk = clock();
if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
else
printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
PRT( "Time", clock() - clk );
}
-
+*/
// move the classes into representatives and reduce AIG
clk2 = clock();
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index e73d610f..50fd6687 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -500,17 +500,18 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
SeeAlso []
***********************************************************************/
-Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter )
{
int nPartSize = 200;
int fReprSelect = 0;
Fra_Lcr_t * p;
+ Fra_Sml_t * pSml;
Fra_Man_t * pTemp;
Aig_Man_t * pAigPart, * pAigNew = NULL;
Vec_Int_t * vPart;
// Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
- int i, nIter, clk = clock(), clk2, clk3;
+ int i, nIter, timeSim, clk = clock(), clk2, clk3;
if ( Aig_ManNodeNum(pAig) == 0 )
{
if ( pnIter ) *pnIter = 0;
@@ -519,23 +520,33 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
assert( Aig_ManLatchNum(pAig) == 0 );
assert( Aig_ManRegNum(pAig) > 0 );
- // start the manager
- p = Lcr_ManAlloc( pAig );
- p->nFramesP = nFramesP;
- p->fVerbose = fVerbose;
-
// simulate the AIG
clk2 = clock();
if ( fVerbose )
printf( "Simulating AIG with %d nodes for %d cycles ... ", Aig_ManNodeNum(pAig), nFramesP + 32 );
- pTemp = Fra_LcrAigPrepare( p->pAig );
- pTemp->pBmc = (Fra_Bmc_t *)p;
- pTemp->pSml = Fra_SmlSimulateSeq( p->pAig, p->nFramesP, 32, 1 );
+ pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 );
if ( fVerbose )
{
PRT( "Time", clock() - clk2 );
-p->timeSim += clock() - clk2;
+timeSim = clock() - clk2;
}
+ // check if simulation discovered non-constant-0 POs
+ if ( fProve && pSml->fNonConstOut )
+ {
+ Fra_SmlStop( pSml );
+ return NULL;
+ }
+
+ // start the manager
+ p = Lcr_ManAlloc( pAig );
+ p->nFramesP = nFramesP;
+ p->fVerbose = fVerbose;
+ p->timeSim += timeSim;
+
+ pTemp = Fra_LcrAigPrepare( pAig );
+ pTemp->pBmc = (Fra_Bmc_t *)p;
+ pTemp->pSml = pSml;
+
// get preliminary info about equivalence classes
pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
Fra_ClassesPrepare( p->pCla, 1 );
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index e1cc4c32..11029b69 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -75,6 +75,9 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
+ // var 0 is reserved for const1 node - add the clause
+ pLits[0] = toLit( 0 );
+ sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
@@ -232,6 +235,9 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
+ // var 0 is reserved for const1 node - add the clause
+ pLits[0] = toLit( 0 );
+ sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
@@ -318,6 +324,9 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
+ // var 0 is reserved for const1 node - add the clause
+ pLits[0] = toLit( 0 );
+ sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 0146ac5a..0919e035 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -103,6 +103,7 @@ PRT( "Time", clock() - clkTotal );
***********************************************************************/
int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
+ Fra_Sml_t * pSml;
Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
@@ -148,8 +149,16 @@ clk = clock();
{
pNew = Aig_ManDup( pTemp = pNew, 1 );
Aig_ManStop( pTemp );
- pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
+ pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
Aig_ManStop( pTemp );
+ if ( pNew == NULL )
+ {
+ RetValue = 0;
+ printf( "Networks are NOT EQUIVALENT after simulation. " );
+PRT( "Time", clock() - clkTotal );
+ return RetValue;
+ }
+
if ( fVerbose )
{
printf( "Latch-corr (I=%3d): Latches = %5d. Nodes = %6d. ",
@@ -196,7 +205,7 @@ clk = clock();
printf( "Rewriting: Latches = %5d. Nodes = %6d. ",
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
- }
+ }
// perform retiming
clk = clock();
pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@@ -211,6 +220,26 @@ PRT( "Time", clock() - clk );
}
if ( pNew->nRegs )
pNew = Aig_ManConstReduce( pNew, 0 );
+
+ // perform sequential simulation
+clk = clock();
+ pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) );
+ if ( fVerbose )
+ {
+ printf( "Seq simulation : Latches = %5d. Nodes = %6d. ",
+ Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+ }
+ if ( pSml->fNonConstOut )
+ {
+ Fra_SmlStop( pSml );
+ Aig_ManStop( pNew );
+ RetValue = 0;
+ printf( "Networks are NOT EQUIVALENT after simulation. " );
+PRT( "Time", clock() - clkTotal );
+ return RetValue;
+ }
+ Fra_SmlStop( pSml );
}
// get the miter status
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index d6f6d74a..d379cf53 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -137,6 +137,28 @@ int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
return Counter;
}
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if simulation info is composed of all zeros.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj )
+{
+ unsigned * pSims;
+ int i;
+ pSims = Fra_ObjSim(p, pObj->Id);
+ for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
+ if ( pSims[i] )
+ return 0;
+ return 1;
+}
+
/**Function*************************************************************
@@ -550,6 +572,27 @@ void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
/**Function*************************************************************
+ Synopsis [Check if any of the POs becomes non-constant.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p )
+{
+ Aig_Obj_t * pObj;
+ int i;
+ Aig_ManForEachPoSeq( p->pAig, pObj, i )
+ if ( !Fra_SmlNodeIsZero(p, pObj) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
Synopsis [Simulates AIG manager.]
Description [Assumes that the PI simulation info is attached.]
@@ -569,14 +612,16 @@ clk = clock();
// simulate the nodes
Aig_ManForEachNode( p->pAig, pObj, i )
Fra_SmlNodeSimulate( p, pObj, f );
+ // copy simulation info into outputs
+ Aig_ManForEachPoSeq( p->pAig, pObj, i )
+ Fra_SmlNodeCopyFanin( p, pObj, f );
+ // quit if this is the last timeframe
if ( f == p->nFrames - 1 )
break;
// copy simulation info into outputs
Aig_ManForEachLiSeq( p->pAig, pObj, i )
Fra_SmlNodeCopyFanin( p, pObj, f );
// copy simulation info into the inputs
-// for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
-// Fra_SmlNodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f );
Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
}
@@ -768,6 +813,7 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
Fra_SmlInitialize( p, 1 );
Fra_SmlSimulateOne( p );
+ p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
return p;
}
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index a922674d..81ed895e 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2100,6 +2100,9 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
+ // var 0 is reserved for const1 node - add the clause
+ pLits[0] = toLit( 0 );
+ sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
@@ -2231,6 +2234,9 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
p->pSat = sat_solver_new();
p->nSatVars = 1;
sat_solver_setnvars( p->pSat, 1000 );
+ // var 0 is reserved for const1 node - add the clause
+ pLits[0] = toLit( 0 );
+ sat_solver_addclause( p->pSat, pLits, pLits + 1 );
}
// if the nodes do not have SAT variables, allocate them
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index ada4ef09..abd07e68 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -48,7 +48,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
p->nWords = Kit_TruthWordNum( p->nVars );
p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
- p->dd = Cloud_Init( 16, 13 );
+ p->dd = Cloud_Init( 16, 14 );
p->vTtBdds = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
p->vNodes = Vec_IntAlloc( 512 );
return p;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a8888d81..bbaa80a4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3095,7 +3095,7 @@ usage:
fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
- fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
+ fprintf( pErr, "\t-L <num> : max level increase after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
fprintf( pErr, "\t-s : toggle iteration till saturation [default = %s]\n", pPars->fSatur? "yes": "no" );
fprintf( pErr, "\t-z : toggle zero-cost replacements [default = %s]\n", pPars->fZeroCost? "yes": "no" );
fprintf( pErr, "\t-f : toggle using only first node and first cut [default = %s]\n", pPars->fFirst? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 356a5565..06e425d5 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -49,10 +49,10 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
Aig_Man_t * pMan;
Aig_Obj_t * pObjNew;
Abc_Obj_t * pObj;
- int i, nNodes;
+ int i, nNodes, nDontCares;
// make sure the latches follow PIs/POs
- if ( fRegisters )
- {
+ if ( fRegisters )
+ {
assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
Abc_NtkForEachCi( pNtk, pObj, i )
if ( i < Abc_NtkPiNum(pNtk) )
@@ -64,6 +64,21 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
assert( Abc_ObjIsPo(pObj) );
else
assert( Abc_ObjIsBi(pObj) );
+ // print warning about initial values
+ nDontCares = 0;
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ if ( Abc_LatchIsInitDc(pObj) )
+ {
+ Abc_LatchSetInit0(pObj);
+ nDontCares++;
+ }
+ if ( nDontCares )
+ {
+ printf( "Warning: %d registers in this network have don't-care init values.\n", nDontCares );
+ printf( "The don't-care are assumed to be 0. The result may not verify.\n" );
+ printf( "Use command \"print_latch\" to see the init values of registers.\n" );
+ printf( "Use command \"init\" to change the values.\n" );
+ }
}
// create the manager
pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
@@ -985,7 +1000,7 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
pMan = Abc_NtkToDar( pNtk, 1 );
if ( pMan == NULL )
return NULL;
- pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, fVerbose, NULL );
+ pMan = Fra_FraigLatchCorrespondence( pTemp = pMan, nFramesP, nConfMax, 0, fVerbose, NULL );
Aig_ManStop( pTemp );
if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 69373597..c77f8dea 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -80,7 +80,7 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
}
//timeRetime = clock() - timeRetime;
// if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
-// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+// printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
return pNtkAig;
}
@@ -145,7 +145,7 @@ Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
}
//timeRetime = clock() - timeRetime;
// if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
-// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+// printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
return pNtkAig;
}
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index a4bcaefc..16c7cc92 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -82,7 +82,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
assert( Abc_NtkIsDfsOrdered(pNtk) );
if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
- printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+ printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
// start the network
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index ba2c154c..27638644 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -99,7 +99,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
// make sure it is an AIG without self-feeding latches
assert( !Abc_NtkHasAig(pNtk) );
if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtk) )
- printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+ printf( "Modified %d self-feeding latches. The result may not verify.\n", RetValue );
assert( Abc_NtkCountSelfFeedLatches(pNtk) == 0 );
// remove the dangling nodes
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-10 07:25:40 +0000