summaryrefslogtreecommitdiffstats
path: root/src/aig/saig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/saig')
-rw-r--r--src/aig/saig/module.make1
-rw-r--r--src/aig/saig/saig.h3
-rw-r--r--src/aig/saig/saigBmc2.c9
-rw-r--r--src/aig/saig/saigDup.c52
-rw-r--r--src/aig/saig/saigPhase.c68
5 files changed, 118 insertions, 15 deletions
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 88935121..a1f0e976 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -24,5 +24,6 @@ SRC += src/aig/saig/saigAbs.c \
src/aig/saig/saigStrSim.c \
src/aig/saig/saigSwitch.c \
src/aig/saig/saigSynch.c \
+ src/aig/saig/saigTempor.c \
src/aig/saig/saigTrans.c \
src/aig/saig/saigWnd.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index fc85d52a..b1017bdb 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -146,7 +146,8 @@ extern void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrame
extern Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
extern Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
/*=== saigDup.c ==========================================================*/
-extern Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * p );
+extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p );
+extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
extern Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
/*=== saigHaig.c ==========================================================*/
extern Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index c7129c67..3d57ae6e 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -820,7 +820,12 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{
printf( "No output was asserted in %d frames. ", p->iFramePrev-1 );
if ( piFrames )
- *piFrames = p->iFramePrev-1;
+ {
+ if ( p->iOutputLast > 0 )
+ *piFrames = p->iFramePrev - 1;
+ else
+ *piFrames = p->iFramePrev;
+ }
}
if ( fVerbOverwrite )
{
@@ -834,7 +839,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
{
if ( p->iFrameLast >= p->nFramesMax )
printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
- else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
+ else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
else
printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 268540da..4d34224e 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
+Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * pAig )
{
Aig_Man_t * pAigNew;
Aig_Obj_t * pObj, * pMiter;
@@ -79,6 +79,56 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig )
/**Function*************************************************************
+ Synopsis [Duplicates while ORing the POs of sequential circuit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs )
+{
+ Aig_Man_t * pAigNew;
+ Aig_Obj_t * pObj, * pObj2, * pMiter;
+ int i;
+ if ( pAig->nConstrs > 0 )
+ {
+ printf( "The AIG manager should have no constraints.\n" );
+ return NULL;
+ }
+ // start the new manager
+ pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
+ pAigNew->pName = Aig_UtilStrsav( pAig->pName );
+ pAigNew->nConstrs = pAig->nConstrs;
+ // map the constant node
+ Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
+ // create variables for PIs
+ Aig_ManForEachPi( pAig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pAigNew );
+ // add internal nodes of this frame
+ Aig_ManForEachNode( pAig, pObj, i )
+ pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ // create POs
+ assert( Vec_IntSize(vPairs) % 2 == 0 );
+ Aig_ManForEachNodeVec( pAig, vPairs, pObj, i )
+ {
+ pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
+ pMiter = Aig_Exor( pAigNew, pObj->pData, pObj2->pData );
+ pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
+ Aig_ObjCreatePo( pAigNew, pMiter );
+ }
+ // transfer to register outputs
+ Saig_ManForEachLi( pAig, pObj, i )
+ Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+ Aig_ManCleanup( pAigNew );
+ Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
+ return pAigNew;
+}
+
+/**Function*************************************************************
+
Synopsis [Duplicates the AIG manager recursively.]
Description []
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index 340910d0..4a23ecf3 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -255,15 +255,22 @@ int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref )
SeeAlso []
***********************************************************************/
-void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
+void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix, int nLoop )
{
unsigned * pState;
int nRegs = p->pAig->nRegs;
int Value, i, k, Counter = 0;
- if ( Vec_PtrSize(p->vStates) > 80 )
- return;
+ printf( "Ternary traces for each flop:\n" );
+ printf( " : " );
+ for ( i = 0; i < Vec_PtrSize(p->vStates) - nLoop - 1; i++ )
+ printf( "%d", i%10 );
+ printf( " " );
+ for ( i = 0; i < nLoop; i++ )
+ printf( "%d", i%10 );
+ printf( "\n" );
for ( i = 0; i < nRegs; i++ )
{
+/*
Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
@@ -274,8 +281,11 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
Counter++;
else
continue;
+*/
+
// print trace
- printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
+// printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
+ printf( "%5d : ", Counter++ );
Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
{
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
@@ -488,7 +498,7 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int f
Saig_ManForEachLo( p, pObj, i )
Saig_ObjSetXsim( pObj, Saig_XsimConvertValue(Vec_IntEntry(vInits, i)) );
}
- else
+ else
{
Saig_ManForEachLo( p, pObj, i )
Saig_ObjSetXsim( pObj, SAIG_XVS0 );
@@ -811,6 +821,42 @@ int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits )
SeeAlso []
***********************************************************************/
+int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
+{
+ Saig_Tsim_t * pTsi;
+ int nFrames, nPrefix, nNonXRegs;
+ assert( Saig_ManRegNum(p) );
+ assert( Saig_ManPiNum(p) );
+ assert( Saig_ManPoNum(p) );
+ // perform terminary simulation
+ pTsi = Saig_ManReachableTernary( p, NULL, 0 );
+ if ( pTsi == NULL )
+ return 0;
+ // derive information
+ nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
+ nFrames = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
+ nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, pTsi->nWords, nPrefix );
+ // print statistics
+ if ( fVerbose )
+ printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs );
+ if ( fVeryVerbose )
+ Saig_TsiPrintTraces( pTsi, pTsi->nWords, nPrefix, nFrames );
+ Saig_TsiStop( pTsi );
+ // potentially, may need to reduce nFrames if nPrefix is less than nFrames
+ return nPrefix;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs automated phase abstraction.]
+
+ Description [Takes the AIG manager and the array of initial states.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose )
{
Aig_Man_t * pNew = NULL;
@@ -829,10 +875,10 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
// print statistics
if ( fVerbose )
{
- printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n",
+ printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
- if ( pTsi->nNonXRegs < 100 )
- Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix );
+ if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
+ Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
}
if ( fPrint )
printf( "Print-out finished. Phase assignment is not performed.\n" );
@@ -885,10 +931,10 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
// print statistics
if ( fVerbose )
{
- printf( "Prefix = %5d. Cycle = %5d. Total = %5d. Non-ternary = %5d.\n",
+ printf( "Lead = %5d. Loop = %5d. Total flops = %5d. Binary flops = %5d.\n",
pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
- if ( pTsi->nNonXRegs < 100 )
- Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix );
+ if ( pTsi->nNonXRegs < 100 && Vec_PtrSize(pTsi->vStates) < 80 )
+ Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix, pTsi->nCycle );
}
nFrames = pTsi->nCycle;
if ( fPrint )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 12:38:02 +0000