luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Version abc80422

This commit is contained in:
Alan Mishchenko 2008-04-22 08:01:00 -07:00
parent 7ec48bc20d
commit e2e9aed11d
12 changed files with 1347 additions and 191 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/aig/aig/aig.h
View File

@ -273,6 +273,7 @@ static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_
static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; } static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; }
static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; } static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; }
static inline int Aig_ObjId( Aig_Obj_t * pObj ) { return pObj->Id; }
static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; } static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; }
static inline int Aig_ObjIsConst1( Aig_Obj_t * pObj ) { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; } static inline int Aig_ObjIsConst1( Aig_Obj_t * pObj ) { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; }
static inline int Aig_ObjIsPi( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI; } static inline int Aig_ObjIsPi( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI; }
@ -493,6 +494,7 @@ extern void Aig_ManStop( Aig_Man_t * p );
extern int Aig_ManCleanup( Aig_Man_t * p ); extern int Aig_ManCleanup( Aig_Man_t * p );
extern int Aig_ManPiCleanup( Aig_Man_t * p ); extern int Aig_ManPiCleanup( Aig_Man_t * p );
extern void Aig_ManPrintStats( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p );
extern void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
/*=== aigMem.c ==========================================================*/ /*=== aigMem.c ==========================================================*/
extern void Aig_ManStartMemory( Aig_Man_t * p ); extern void Aig_ManStartMemory( Aig_Man_t * p );
extern void Aig_ManStopMemory( Aig_Man_t * p ); extern void Aig_ManStopMemory( Aig_Man_t * p );
@ -513,6 +515,7 @@ extern void Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
extern void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop ); extern void Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop );
extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew ); extern void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel ); extern void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel );
extern void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
/*=== aigOper.c =========================================================*/ /*=== aigOper.c =========================================================*/
extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i ); extern Aig_Obj_t * Aig_IthVar( Aig_Man_t * p, int i );
extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type ); extern Aig_Obj_t * Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );

22
src/aig/aig/aigMan.c
View File

@ -337,6 +337,28 @@ void Aig_ManPrintStats( Aig_Man_t * p )
fflush( stdout ); fflush( stdout );
} }
/**Function*************************************************************
Synopsis [Reports the reduction of the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew )
{
printf( "REGs: Beg = %d. End = %d. (R = %6.2f %%). ",
Aig_ManRegNum(p), Aig_ManRegNum(pNew),
Aig_ManRegNum(p)? 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pNew))/Aig_ManRegNum(p) : 0.0 );
printf( "ANDs: Beg = %d. End = %d. (R = %6.2f %%).",
Aig_ManNodeNum(p), Aig_ManNodeNum(pNew),
Aig_ManNodeNum(p)? 100.0*(Aig_ManNodeNum(p)-Aig_ManNodeNum(pNew))/Aig_ManNodeNum(p) : 0.0 );
printf( "\n" );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

75
src/aig/aig/aigObj.c
View File

@ -416,6 +416,81 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
pObjOld->pHaig = pHaig; pObjOld->pHaig = pHaig;
} }
/**Function*************************************************************
Synopsis [Verbose printing of the AIG node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
{
int fHaig = 0;
int fShowFanouts = 0;
Aig_Obj_t * pTemp;
assert( !Aig_IsComplement(pObj) );
printf( "Node %4d : ", Aig_ObjId(pObj) );
if ( Aig_ObjIsConst1(pObj) )
printf( "constant 1" );
else if ( Aig_ObjIsPi(pObj) )
printf( "PI" );
else if ( Aig_ObjIsPo(pObj) )
printf( "PO( %4d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
else if ( Aig_ObjIsBuf(pObj) )
printf( "BUF( %d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
else
printf( "AND( %4d%s, %4d%s )",
Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "),
Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") );
printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
if ( fShowFanouts && p->pFanData )
{
Aig_Obj_t * pFanout;
int i, iFan;
printf( "\nFanouts:\n" );
Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i )
{
printf( " " );
printf( "Node %4d : ", Aig_ObjId(pFanout) );
if ( Aig_ObjIsPo(pFanout) )
printf( "PO( %4d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") );
else if ( Aig_ObjIsBuf(pFanout) )
printf( "BUF( %d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") );
else
printf( "AND( %4d%s, %4d%s )",
Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " "),
Aig_ObjFanin1(pFanout)->Id, (Aig_ObjFaninC1(pFanout)? "\'" : " ") );
printf( "\n" );
}
return;
}
if ( fHaig )
{
if ( pObj->pHaig == NULL )
printf( " HAIG node not given" );
else
printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") );
return;
}
// there are choices
if ( p->pEquivs && p->pEquivs[pObj->Id] )
{
// print equivalence class
printf( " { %4d ", pObj->Id );
for ( pTemp = p->pEquivs[pObj->Id]; pTemp; pTemp = p->pEquivs[pTemp->Id] )
printf( " %4d%s", pTemp->Id, (pTemp->fPhase != pObj->fPhase)? "\'" : " " );
printf( " }" );
return;
}
// this is a secondary node
if ( p->pReprs && p->pReprs[pObj->Id] )
printf( " class of %d", pObj->Id );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

42
src/aig/aig/aigUtil.c
View File

@ -947,6 +947,48 @@ int Aig_ManCountChoices( Aig_Man_t * p )
return Counter; return Counter;
} }
/**Function*************************************************************
Synopsis [Prints the fanouts of the control register.]
Description [Useful only for Intel MC benchmarks.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManPrintControlFanouts( Aig_Man_t * p )
{
Aig_Obj_t * pObj, * pFanin0, * pFanin1, * pCtrl;
int i, Counter = 0;
pCtrl = Aig_ManPi( p, Aig_ManPiNum(p) - 1 );
printf( "Control signal:\n" );
Aig_ObjPrint( p, pCtrl ); printf( "\n\n" );
Aig_ManForEachObj( p, pObj, i )
{
if ( !Aig_ObjIsNode(pObj) )
continue;
assert( pObj != pCtrl );
pFanin0 = Aig_ObjFanin0(pObj);
pFanin1 = Aig_ObjFanin1(pObj);
if ( pFanin0 == pCtrl && Aig_ObjIsPi(pFanin1) )
{
Aig_ObjPrint( p, pObj ); printf( "\n" );
Aig_ObjPrint( p, pFanin1 ); printf( "\n" );
printf( "\n" );
}
if ( pFanin1 == pCtrl && Aig_ObjIsPi(pFanin0) )
{
Aig_ObjPrint( p, pObj ); printf( "\n" );
Aig_ObjPrint( p, pFanin0 ); printf( "\n" );
printf( "\n" );
}
}
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

1
src/aig/cnf/cnf.h
View File

@ -152,6 +152,7 @@ extern Vec_Ptr_t * Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPre
extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover ); extern void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ); extern Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ); extern Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );
extern Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p );
#ifdef __cplusplus #ifdef __cplusplus
} }

102
src/aig/cnf/cnfWrite.c
View File

@ -440,6 +440,108 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
return pCnf; return pCnf;
} }
/**Function*************************************************************
Synopsis [Derives a simple CNF for backward retiming computation.]
Description [The last argument shows the number of last outputs
of the manager, which will not be converted into clauses.
New variables will be introduced for these outputs.]
SideEffects []
SeeAlso []
***********************************************************************/
Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p )
{
Aig_Obj_t * pObj;
Cnf_Dat_t * pCnf;
int OutVar, PoVar, pVars[32], * pLits, ** pClas;
int i, nLiterals, nClauses, Number;
// count the number of literals and clauses
nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManPoNum(p);
nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManPoNum(p);
// allocate CNF
pCnf = ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf->pMan = p;
pCnf->nLiterals = nLiterals;
pCnf->nClauses = nClauses;
pCnf->pClauses = ALLOC( int *, nClauses + 1 );
pCnf->pClauses[0] = ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
// create room for variable numbers
pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) );
memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
// assign variables to the last (nOutputs) POs
Number = 1;
Aig_ManForEachPo( p, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
// assign variables to the internal nodes
Aig_ManForEachNode( p, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
// assign variables to the PIs and constant node
Aig_ManForEachPi( p, pObj, i )
pCnf->pVarNums[pObj->Id] = Number++;
pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
pCnf->nVars = Number;
// assign the clauses
pLits = pCnf->pClauses[0];
pClas = pCnf->pClauses;
Aig_ManForEachNode( p, pObj, i )
{
OutVar = pCnf->pVarNums[ pObj->Id ];
pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];
// positive phase
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
*pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj);
*pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj);
// negative phase
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
*pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj);
*pClas++ = pLits;
*pLits++ = 2 * OutVar + 1;
*pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj);
}
// write the constant literal
OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
assert( OutVar <= Aig_ManObjNumMax(p) );
*pClas++ = pLits;
*pLits++ = 2 * OutVar;
// write the output literals
Aig_ManForEachPo( p, pObj, i )
{
OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
PoVar = pCnf->pVarNums[ pObj->Id ];
// first clause
*pClas++ = pLits;
*pLits++ = 2 * PoVar;
*pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj);
// second clause
*pClas++ = pLits;
*pLits++ = 2 * PoVar + 1;
*pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj);
// final clause (init-state is always 0 -> set the output to 0)
*pClas++ = pLits;
*pLits++ = 2 * PoVar + 1;
}
// verify that the correct number of literals and clauses was written
assert( pLits - pCnf->pClauses[0] == nLiterals );
assert( pClas - pCnf->pClauses == nClauses );
return pCnf;
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// END OF FILE /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

28
src/aig/nwk/nwkFlow.c
View File

@ -20,6 +20,14 @@
#include "nwk.h" #include "nwk.h"
/*
This code is based on the papers:
A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming
via binary maximum-flow", Proc. FMCAD '07, pp. 181-187.
A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming
under simultaneous delay and initial state constraints". Proc. DAC'08.
*/
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -368,7 +376,7 @@ int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj )
return 0; return 0;
return 1; return 1;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Verifies the forward cut.] Synopsis [Verifies the forward cut.]
@ -453,7 +461,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
Counter++; Counter++;
} }
if ( fVerbose ) if ( fVerbose )
printf( "Forward: Max-flow1 = %5d. ", Counter ); printf( "Forward: Max-flow = %4d -> ", Counter );
// continue flow computation from each LO // continue flow computation from each LO
Nwk_ManIncrementTravIdFlow( pMan ); Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLoSeq( pMan, pObj, i ) Nwk_ManForEachLoSeq( pMan, pObj, i )
@ -464,7 +472,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
Counter2++; Counter2++;
} }
if ( fVerbose ) if ( fVerbose )
printf( "Max-flow2 = %5d. ", Counter+Counter2 ); printf( "%4d. ", Counter+Counter2 );
// repeat flow computation from each LO // repeat flow computation from each LO
if ( Counter2 > 0 ) if ( Counter2 > 0 )
{ {
@ -489,10 +497,10 @@ Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbos
} }
} }
Nwk_ManCleanMarks( pMan ); Nwk_ManCleanMarks( pMan );
assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) ); // assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Min-cut = %5d. Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter ); printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
PRT( "Time", clock() - clk ); PRT( "Time", clock() - clk );
} }
return vNodes; return vNodes;
@ -536,8 +544,8 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
Nwk_ManIncrementTravIdFlow( pMan ); Nwk_ManIncrementTravIdFlow( pMan );
Counter++; Counter++;
} }
if ( fVerbose ) if ( fVerbose )
printf( "Backward: Max-flow1 = %5d. ", Counter ); printf( "Backward: Max-flow = %4d -> ", Counter );
// continue flow computation from each LI driver // continue flow computation from each LI driver
Nwk_ManIncrementTravIdFlow( pMan ); Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLiSeq( pMan, pObj, i ) Nwk_ManForEachLiSeq( pMan, pObj, i )
@ -548,7 +556,7 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
Counter2++; Counter2++;
} }
if ( fVerbose ) if ( fVerbose )
printf( "Max-flow2 = %5d. ", Counter+Counter2 ); printf( "%4d. ", Counter+Counter2 );
// repeat flow computation from each LI driver // repeat flow computation from each LI driver
if ( Counter2 > 0 ) if ( Counter2 > 0 )
{ {
@ -576,10 +584,10 @@ Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbo
if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) ) if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
Counter++; Counter++;
Nwk_ManCleanMarks( pMan ); Nwk_ManCleanMarks( pMan );
assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) ); // assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Min-cut = %5d. Unmoved regs = %5d. ", Vec_PtrSize(vNodes), Counter ); printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
PRT( "Time", clock() - clk ); PRT( "Time", clock() - clk );
} }
return vNodes; return vNodes;

626
src/aig/nwk/nwkFlow_depth.c Normal file
View File

@ -0,0 +1,626 @@
/**CFile****************************************************************
FileName [nwkFlow.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Netlist representation.]
Synopsis [Max-flow/min-cut computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: nwkFlow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "nwk.h"
/*
This code is based on the papers:
A. Hurst, A. Mishchenko, and R. Brayton, "Fast minimum-register retiming
via binary maximum-flow", Proc. FMCAD '07, pp. 181-187.
A. Hurst, A. Mishchenko, and R. Brayton, "Scalable min-area retiming
under simultaneous delay and initial state constraints". Proc. DAC'08.
*/
int DepthFwd, DepthBwd, DepthFwdMax, DepthBwdMax;
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
// predecessors
static inline Nwk_Obj_t * Nwk_ObjPred( Nwk_Obj_t * pObj ) { return pObj->pCopy; }
static inline int Nwk_ObjSetPred( Nwk_Obj_t * pObj, Nwk_Obj_t * p ) { pObj->pCopy = p; return 1; }
// sink
static inline int Nwk_ObjIsSink( Nwk_Obj_t * pObj ) { return pObj->MarkA; }
static inline void Nwk_ObjSetSink( Nwk_Obj_t * pObj ) { pObj->MarkA = 1; }
// flow
static inline int Nwk_ObjHasFlow( Nwk_Obj_t * pObj ) { return pObj->MarkB; }
static inline void Nwk_ObjSetFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 1; }
static inline void Nwk_ObjClearFlow( Nwk_Obj_t * pObj ) { pObj->MarkB = 0; }
// representation of visited nodes
// pObj->TravId < pNtk->nTravIds-2 --- not visited
// pObj->TravId == pNtk->nTravIds-2 --- visited bot only
// pObj->TravId == pNtk->nTravIds-1 --- visited top only
// pObj->TravId == pNtk->nTravIds --- visited bot and top
static inline int Nwk_ObjVisitedBotOnly( Nwk_Obj_t * pObj )
{
return pObj->TravId == pObj->pMan->nTravIds - 2;
}
static inline int Nwk_ObjVisitedBot( Nwk_Obj_t * pObj )
{
return pObj->TravId == pObj->pMan->nTravIds - 2 || pObj->TravId == pObj->pMan->nTravIds;
}
static inline int Nwk_ObjVisitedTop( Nwk_Obj_t * pObj )
{
return pObj->TravId == pObj->pMan->nTravIds - 1 || pObj->TravId == pObj->pMan->nTravIds;
}
static inline void Nwk_ObjSetVisitedBot( Nwk_Obj_t * pObj )
{
if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
pObj->TravId = pObj->pMan->nTravIds - 2;
else if ( pObj->TravId == pObj->pMan->nTravIds - 1 )
pObj->TravId = pObj->pMan->nTravIds;
else
assert( 0 );
}
static inline void Nwk_ObjSetVisitedTop( Nwk_Obj_t * pObj )
{
if ( pObj->TravId < pObj->pMan->nTravIds - 2 )
pObj->TravId = pObj->pMan->nTravIds - 1;
else if ( pObj->TravId == pObj->pMan->nTravIds - 2 )
pObj->TravId = pObj->pMan->nTravIds;
else
assert( 0 );
}
static inline Nwk_ManIncrementTravIdFlow( Nwk_Man_t * pMan )
{
Nwk_ManIncrementTravId( pMan );
Nwk_ManIncrementTravId( pMan );
Nwk_ManIncrementTravId( pMan );
}
static int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
static int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
static int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
static int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Marks TFI of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Nwk_ManMarkTfiCone_rec( Nwk_Obj_t * pObj )
{
Nwk_Obj_t * pNext;
int i;
if ( pObj->MarkA )
return;
pObj->MarkA = 1;
Nwk_ObjForEachFanin( pObj, pNext, i )
Nwk_ManMarkTfiCone_rec( pNext );
}
/**Function*************************************************************
Synopsis [Marks TFO of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Nwk_ManMarkTfoCone_rec( Nwk_Obj_t * pObj )
{
Nwk_Obj_t * pNext;
int i;
if ( pObj->MarkA )
return;
pObj->MarkA = 1;
Nwk_ObjForEachFanout( pObj, pNext, i )
Nwk_ManMarkTfoCone_rec( pNext );
}
/**Function*************************************************************
Synopsis [Fast forward flow pushing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManPushForwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
{
Nwk_Obj_t * pNext;
int i;
if ( Nwk_ObjIsTravIdCurrent( pObj ) )
return 0;
Nwk_ObjSetTravIdCurrent( pObj );
if ( Nwk_ObjHasFlow(pObj) )
return 0;
if ( Nwk_ObjIsSink(pObj) )
{
Nwk_ObjSetFlow(pObj);
return Nwk_ObjSetPred( pObj, pPred );
}
Nwk_ObjForEachFanout( pObj, pNext, i )
if ( Nwk_ManPushForwardFast_rec( pNext, pObj ) )
{
Nwk_ObjSetFlow(pObj);
return Nwk_ObjSetPred( pObj, pPred );
}
return 0;
}
/**Function*************************************************************
Synopsis [Fast backward flow pushing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManPushBackwardFast_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
{
Nwk_Obj_t * pNext;
int i;
if ( Nwk_ObjIsTravIdCurrent( pObj ) )
return 0;
Nwk_ObjSetTravIdCurrent( pObj );
if ( Nwk_ObjHasFlow(pObj) )
return 0;
if ( Nwk_ObjIsSink(pObj) )
{
Nwk_ObjSetFlow(pObj);
return Nwk_ObjSetPred( pObj, pPred );
}
Nwk_ObjForEachFanin( pObj, pNext, i )
if ( Nwk_ManPushBackwardFast_rec( pNext, pObj ) )
{
Nwk_ObjSetFlow(pObj);
return Nwk_ObjSetPred( pObj, pPred );
}
return 0;
}
/**Function*************************************************************
Synopsis [Pushing the flow through the bottom part of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManPushForwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
{
Nwk_Obj_t * pNext;
int i;
if ( Nwk_ObjVisitedBot(pObj) )
return 0;
Nwk_ObjSetVisitedBot(pObj);
DepthFwd++;
if ( DepthFwdMax < DepthFwd )
DepthFwdMax = DepthFwd;
// propagate through the internal edge
if ( Nwk_ObjHasFlow(pObj) )
{
if ( Nwk_ObjPred(pObj) )
if ( Nwk_ManPushForwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
{
DepthFwd--;
return Nwk_ObjSetPred( pObj, pPred );
}
}
else if ( Nwk_ManPushForwardTop_rec(pObj, pObj) )
{
DepthFwd--;
Nwk_ObjSetFlow( pObj );
return Nwk_ObjSetPred( pObj, pPred );
}
// try to push through the fanins
Nwk_ObjForEachFanin( pObj, pNext, i )
if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
{
DepthFwd--;
return 1;
}
DepthFwd--;
return 0;
}
/**Function*************************************************************
Synopsis [Pushing the flow through the top part of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManPushForwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
{
Nwk_Obj_t * pNext;
int i;
if ( Nwk_ObjVisitedTop(pObj) )
return 0;
Nwk_ObjSetVisitedTop(pObj);
// check if this is the sink
if ( Nwk_ObjIsSink(pObj) )
return 1;
DepthFwd++;
if ( DepthFwdMax < DepthFwd )
DepthFwdMax = DepthFwd;
// try to push through the fanouts
Nwk_ObjForEachFanout( pObj, pNext, i )
if ( Nwk_ManPushForwardBot_rec( pNext, pPred ) )
{
DepthFwd--;
return 1;
}
// redirect the flow
if ( Nwk_ObjHasFlow(pObj) && !Nwk_ObjIsCi(pObj) )
if ( Nwk_ManPushForwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
{
DepthFwd--;
Nwk_ObjClearFlow( pObj );
return Nwk_ObjSetPred( pObj, NULL );
}
DepthFwd--;
return 0;
}
/**Function*************************************************************
Synopsis [Pushing the flow through the bottom part of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManPushBackwardBot_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
{
if ( Nwk_ObjVisitedBot(pObj) )
return 0;
Nwk_ObjSetVisitedBot(pObj);
// propagate through the internal edge
if ( Nwk_ObjHasFlow(pObj) )
{
if ( Nwk_ObjPred(pObj) )
if ( Nwk_ManPushBackwardTop_rec( Nwk_ObjPred(pObj), Nwk_ObjPred(pObj) ) )
return Nwk_ObjSetPred( pObj, pPred );
}
else if ( Nwk_ManPushBackwardTop_rec(pObj, pObj) )
{
Nwk_ObjSetFlow( pObj );
return Nwk_ObjSetPred( pObj, pPred );
}
return 0;
}
/**Function*************************************************************
Synopsis [Pushing the flow through the top part of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManPushBackwardTop_rec( Nwk_Obj_t * pObj, Nwk_Obj_t * pPred )
{
Nwk_Obj_t * pNext;
int i;
if ( Nwk_ObjVisitedTop(pObj) )
return 0;
Nwk_ObjSetVisitedTop(pObj);
// check if this is the sink
if ( Nwk_ObjIsSink(pObj) )
return 1;
// try to push through the fanins
Nwk_ObjForEachFanin( pObj, pNext, i )
if ( Nwk_ManPushBackwardBot_rec( pNext, pPred ) )
return 1;
// try to push through the fanouts
Nwk_ObjForEachFanout( pObj, pNext, i )
if ( !Nwk_ObjIsCo(pObj) && Nwk_ManPushBackwardTop_rec( pNext, pPred ) )
return 1;
// redirect the flow
if ( Nwk_ObjHasFlow(pObj) )
if ( Nwk_ObjPred(pObj) && Nwk_ManPushBackwardBot_rec( pObj, Nwk_ObjPred(pObj) ) )
{
Nwk_ObjClearFlow( pObj );
return Nwk_ObjSetPred( pObj, NULL );
}
return 0;
}
/**Function*************************************************************
Synopsis [Returns 0 if there is an unmarked path to a CI.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManVerifyCut_rec( Nwk_Obj_t * pObj )
{
Nwk_Obj_t * pNext;
int i;
if ( pObj->MarkA )
return 1;
if ( Nwk_ObjIsLo(pObj) )
return 0;
if ( Nwk_ObjIsTravIdCurrent( pObj ) )
return 1;
Nwk_ObjSetTravIdCurrent( pObj );
Nwk_ObjForEachFanin( pObj, pNext, i )
if ( !Nwk_ManVerifyCut_rec( pNext ) )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Verifies the forward cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManRetimeVerifyCutForward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
{
Nwk_Obj_t * pObj;
int i;
// mark the nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
{
assert( pObj->MarkA == 0 );
pObj->MarkA = 1;
}
// traverse from the COs
Nwk_ManIncrementTravId( pMan );
Nwk_ManForEachCo( pMan, pObj, i )
if ( !Nwk_ManVerifyCut_rec( pObj ) )
printf( "Nwk_ManRetimeVerifyCutForward(): Internal cut verification failed.\n" );
// unmark the nodes
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->MarkA = 0;
return 1;
}
/**Function*************************************************************
Synopsis [Verifies the forward cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Nwk_ManRetimeVerifyCutBackward( Nwk_Man_t * pMan, Vec_Ptr_t * vNodes )
{
return 1;
}
/**Function*************************************************************
Synopsis [Computes minimum cut for forward retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Nwk_ManRetimeCutForward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
{
Vec_Ptr_t * vNodes;
Nwk_Obj_t * pObj;
int i, RetValue, Counter = 0, Counter2 = 0;
int clk = clock();
// set the sequential parameters
pMan->nLatches = nLatches;
pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
// mark the COs and the TFO of PIs
Nwk_ManForEachCo( pMan, pObj, i )
pObj->MarkA = 1;
Nwk_ManForEachPiSeq( pMan, pObj, i )
Nwk_ManMarkTfoCone_rec( pObj );
// start flow computation from each LO
Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLoSeq( pMan, pObj, i )
{
if ( !Nwk_ManPushForwardFast_rec( pObj, NULL ) )
continue;
Nwk_ManIncrementTravIdFlow( pMan );
Counter++;
}
if ( fVerbose )
printf( "Forward: Max-flow = %4d -> ", Counter );
// continue flow computation from each LO
DepthFwdMax = DepthFwd = 0;
Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLoSeq( pMan, pObj, i )
{
printf( "%d ", DepthFwdMax );
if ( !Nwk_ManPushForwardBot_rec( pObj, NULL ) )
continue;
assert( DepthFwd == 0 );
Nwk_ManIncrementTravIdFlow( pMan );
Counter2++;
}
printf( "DepthMax = %d.\n", DepthFwdMax );
if ( fVerbose )
printf( "%4d. ", Counter+Counter2 );
// repeat flow computation from each LO
if ( Counter2 > 0 )
{
Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLoSeq( pMan, pObj, i )
{
RetValue = Nwk_ManPushForwardBot_rec( pObj, NULL );
assert( !RetValue );
}
}
// cut is a set of nodes whose bottom is visited but top is not visited
vNodes = Vec_PtrAlloc( Counter+Counter2 );
Counter = 0;
Nwk_ManForEachObj( pMan, pObj, i )
{
if ( Nwk_ObjVisitedBotOnly(pObj) )
{
assert( Nwk_ObjHasFlow(pObj) );
assert( !Nwk_ObjIsCo(pObj) );
Vec_PtrPush( vNodes, pObj );
Counter += Nwk_ObjIsCi(pObj);
}
}
Nwk_ManCleanMarks( pMan );
assert( Nwk_ManRetimeVerifyCutForward(pMan, vNodes) );
if ( fVerbose )
{
printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
PRT( "Time", clock() - clk );
}
return vNodes;
}
/**Function*************************************************************
Synopsis [Computes minimum cut for backward retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Nwk_ManRetimeCutBackward( Nwk_Man_t * pMan, int nLatches, int fVerbose )
{
Vec_Ptr_t * vNodes;
Nwk_Obj_t * pObj;
int i, RetValue, Counter = 0, Counter2 = 0;
int clk = clock();
// set the sequential parameters
pMan->nLatches = nLatches;
pMan->nTruePis = Nwk_ManCiNum(pMan) - nLatches;
pMan->nTruePos = Nwk_ManCoNum(pMan) - nLatches;
// mark the CIs, the TFI of POs, and the constant nodes
Nwk_ManForEachCi( pMan, pObj, i )
pObj->MarkA = 1;
Nwk_ManForEachPoSeq( pMan, pObj, i )
Nwk_ManMarkTfiCone_rec( pObj );
Nwk_ManForEachNode( pMan, pObj, i )
if ( Nwk_ObjFaninNum(pObj) == 0 )
pObj->MarkA = 1;
// start flow computation from each LI driver
Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLiSeq( pMan, pObj, i )
{
if ( !Nwk_ManPushBackwardFast_rec( Nwk_ObjFanin0(pObj), NULL ) )
continue;
Nwk_ManIncrementTravIdFlow( pMan );
Counter++;
}
if ( fVerbose )
printf( "Backward: Max-flow = %4d -> ", Counter );
// continue flow computation from each LI driver
Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLiSeq( pMan, pObj, i )
{
if ( !Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL ) )
continue;
Nwk_ManIncrementTravIdFlow( pMan );
Counter2++;
}
if ( fVerbose )
printf( "%4d. ", Counter+Counter2 );
// repeat flow computation from each LI driver
if ( Counter2 > 0 )
{
Nwk_ManIncrementTravIdFlow( pMan );
Nwk_ManForEachLiSeq( pMan, pObj, i )
{
RetValue = Nwk_ManPushBackwardBot_rec( Nwk_ObjFanin0(pObj), NULL );
assert( !RetValue );
}
}
// cut is a set of nodes whose bottom is visited but top is not visited
vNodes = Vec_PtrAlloc( Counter+Counter2 );
Nwk_ManForEachObj( pMan, pObj, i )
{
if ( Nwk_ObjVisitedBotOnly(pObj) )
{
assert( Nwk_ObjHasFlow(pObj) );
assert( !Nwk_ObjIsCo(pObj) );
Vec_PtrPush( vNodes, pObj );
}
}
// count CO drivers
Counter = 0;
Nwk_ManForEachLiSeq( pMan, pObj, i )
if ( Nwk_ObjVisitedBotOnly( Nwk_ObjFanin0(pObj) ) )
Counter++;
Nwk_ManCleanMarks( pMan );
assert( Nwk_ManRetimeVerifyCutBackward(pMan, vNodes) );
if ( fVerbose )
{
printf( "Min-cut = %4d. Unmoved = %4d. ", Vec_PtrSize(vNodes), Counter );
PRT( "Time", clock() - clk );
}
return vNodes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

62
src/aig/saig/saigPhase.c
View File

@ -272,7 +272,7 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix )
else else
continue; continue;
// print trace // print trace
printf( "%5d : %5d ", Counter, i ); printf( "%5d : %5d %5d ", Counter, i, Saig_ManLo(p->pAig, i)->Id );
Vec_PtrForEachEntryStop( p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 ) Vec_PtrForEachEntryStop( p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 )
{ {
Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
@ -534,6 +534,60 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits )
return NULL; return NULL;
} }
/**Function*************************************************************
Synopsis [Analize initial value of the selected register.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg )
{
Aig_Obj_t * pObj, * pReg, * pCtrl, * pAnd;
int i;
pReg = Saig_ManLo( p, Reg );
pCtrl = Saig_ManLo( p, Saig_ManRegNum(p)-1 );
assert( pReg->Id < pCtrl->Id );
// find a node pointing to both
pAnd = NULL;
Aig_ManForEachNode( p, pObj, i )
{
if ( Aig_ObjFanin0(pObj) == pReg && Aig_ObjFanin1(pObj) == pCtrl )
{
pAnd = pObj;
break;
}
}
if ( pAnd == NULL )
{
printf( "Register is not found.\n" );
return;
}
printf( "Clock-like register: \n" );
Aig_ObjPrint( p, pReg );
printf( "\n" );
printf( "Control register: \n" );
Aig_ObjPrint( p, pCtrl );
printf( "\n" );
printf( "Their fanout: \n" );
Aig_ObjPrint( p, pAnd );
printf( "\n" );
// find the fanouts of pAnd
printf( "Fanouts of the fanout: \n" );
Aig_ManForEachObj( p, pObj, i )
if ( Aig_ObjFanin0(pObj) == pAnd || Aig_ObjFanin1(pObj) == pAnd )
{
Aig_ObjPrint( p, pObj );
printf( "\n" );
}
printf( "\n" );
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Finds the registers to phase-abstract.] Synopsis [Finds the registers to phase-abstract.]
@ -587,6 +641,9 @@ int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVe
for ( k = 0; k < nFrames; k++ ) for ( k = 0; k < nFrames; k++ )
Saig_XsimPrint( stdout, Values[k] ); Saig_XsimPrint( stdout, Values[k] );
printf( "]\n" ); printf( "]\n" );
if ( fVerbose )
Saig_ManAnalizeControl( pTsi->pAig, Reg );
} }
} }
Vec_IntShrink( pTsi->vNonXRegs, r ); Vec_IntShrink( pTsi->vNonXRegs, r );
@ -595,6 +652,7 @@ int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVe
return Vec_IntSize(pTsi->vNonXRegs); return Vec_IntSize(pTsi->vNonXRegs);
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Mapping of AIG nodes into frames nodes.] Synopsis [Mapping of AIG nodes into frames nodes.]
@ -662,7 +720,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe
pState = Vec_PtrEntry( pTsi->vStates, f ); pState = Vec_PtrEntry( pTsi->vStates, f );
Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg ); Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg );
assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 ); assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 );
pObjNew = Value? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames); pObjNew = (Value == SAIG_XVS1)? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames);
Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
} }
// add internal nodes of this frame // add internal nodes of this frame

549
src/aig/saig/saigRetMin.c
View File

@ -19,8 +19,10 @@
***********************************************************************/ ***********************************************************************/
#include "saig.h" #include "saig.h"
#include "satSolver.h"
#include "cnf.h" #include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
@ -32,6 +34,147 @@ extern Vec_Ptr_t * Nwk_ManDeriveRetimingCut( Aig_Man_t * p, int fForward, int fV
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Derives the initial state after backward retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManRetimeInitState( Aig_Man_t * p )
{
int nConfLimit = 1000000;
Vec_Int_t * vCiIds, * vInit = NULL;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj;
int i, RetValue, * pModel;
// solve the SAT problem
pCnf = Cnf_DeriveSimpleForRetiming( p );
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
if ( pSat == NULL )
{
Cnf_DataFree( pCnf );
return NULL;
}
RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
assert( RetValue != l_Undef );
// create counter-example
if ( RetValue == l_True )
{
// accumulate SAT variables of the CIs
vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
Aig_ManForEachPi( p, pObj, i )
Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
// create the model
pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) );
Vec_IntFree( vCiIds );
}
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
return vInit;
}
/**Function*************************************************************
Synopsis [Uses UNSAT core to find the part of AIG to be excluded.]
Description [Returns the number of the PO that appears in the UNSAT core.]
SideEffects []
SeeAlso []
***********************************************************************/
int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose )
{
int fVeryVerbose = 0;
int nConfLimit = 1000000;
void * pSatCnf = NULL;
Intp_Man_t * pManProof;
Vec_Int_t * vCore = NULL;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj;
int * pClause1, * pClause2, * pLit, * pVars;
int i, RetValue, iBadPo, iClause, nVars, nPos;
// create the SAT solver
pCnf = Cnf_DeriveSimpleForRetiming( p );
pSat = sat_solver_new();
sat_solver_store_alloc( pSat );
sat_solver_setnvars( pSat, pCnf->nVars );
for ( i = 0; i < pCnf->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
{
Cnf_DataFree( pCnf );
sat_solver_delete( pSat );
return -1;
}
}
sat_solver_store_mark_roots( pSat );
// solve the problem
RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
assert( RetValue != l_Undef );
assert( RetValue == l_False );
pSatCnf = sat_solver_store_release( pSat );
sat_solver_delete( pSat );
// derive the UNSAT core
pManProof = Intp_ManAlloc();
vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVeryVerbose );
Intp_ManFree( pManProof );
Sto_ManFree( pSatCnf );
// derive the set of variables on which the core depends
// collect the variable numbers
nVars = 0;
pVars = ALLOC( int, pCnf->nVars );
memset( pVars, 0, sizeof(int) * pCnf->nVars );
Vec_IntForEachEntry( vCore, iClause, i )
{
pClause1 = pCnf->pClauses[iClause];
pClause2 = pCnf->pClauses[iClause+1];
for ( pLit = pClause1; pLit < pClause2; pLit++ )
{
if ( pVars[ (*pLit) >> 1 ] == 0 )
nVars++;
pVars[ (*pLit) >> 1 ] = 1;
if ( fVeryVerbose )
printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
}
if ( fVeryVerbose )
printf( "\n" );
}
// collect the nodes
if ( fVeryVerbose )
Aig_ManForEachObj( p, pObj, i )
if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
{
Aig_ObjPrint( p, pObj );
printf( "\n" );
}
// pick the first PO in the list
nPos = 0;
iBadPo = -1;
Aig_ManForEachPo( p, pObj, i )
if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
{
if ( iBadPo == -1 )
iBadPo = i;
nPos++;
}
if ( fVerbose )
printf( "UNSAT core: %d clauses, %d variables, %d POs. ", Vec_IntSize(vCore), nVars, nPos );
free( pVars );
Vec_IntFree( vCore );
Cnf_DataFree( pCnf );
return iBadPo;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Marks the TFI cone with the current traversal ID.] Synopsis [Marks the TFI cone with the current traversal ID.]
@ -100,52 +243,6 @@ int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )
return RetValue; return RetValue;
} }
/**Function*************************************************************
Synopsis [Computes the new cut after excluding the nodes in the set.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Saig_ManRetimeExtendCut( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Ptr_t * vToExclude )
{
Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj, * pFanin;
int i;
// mark the cones
Aig_ManIncrementTravId( p );
Vec_PtrForEachEntry( vCut, pObj, i )
Saig_ManMarkCone_rec( p, pObj );
Vec_PtrForEachEntry( vToExclude, pObj, i )
Saig_ManMarkCone_rec( p, pObj );
// collect the new cut
vNodes = Vec_PtrAlloc( 1000 );
Aig_ManForEachObj( p, pObj, i )
{
if ( Aig_ObjIsTravIdCurrent(p, pObj) )
continue;
pFanin = Aig_ObjFanin0( pObj );
if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
{
Vec_PtrPush( vNodes, pFanin );
pFanin->fMarkA = 1;
}
pFanin = Aig_ObjFanin1( pObj );
if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )
{
Vec_PtrPush( vNodes, pFanin );
pFanin->fMarkA = 1;
}
}
Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->fMarkA = 0;
return vNodes;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Duplicates the AIG recursively.] Synopsis [Duplicates the AIG recursively.]
@ -222,6 +319,73 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut )
Saig_ManRetimeDup_rec( pNew, pObj ); Saig_ManRetimeDup_rec( pNew, pObj );
Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, pObj->fPhase) ); Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, pObj->fPhase) );
} }
Aig_ManCleanup( pNew );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG while retiming the registers to the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Int_t * vInit )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj, * pObjLi, * pObjLo;
int i;
// mark the cones under the cut
// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = Vec_PtrSize(vCut);
pNew->nTruePis = p->nTruePis;
pNew->nTruePos = p->nTruePos;
// create the true PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Saig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
// create the registers
Vec_PtrForEachEntry( vCut, pObj, i )
pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), vInit?Vec_IntEntry(vInit,i):0 );
// duplicate logic above the cut and remember values
Saig_ManForEachLi( p, pObj, i )
{
Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
pObj->pData = Aig_ObjChild0Copy(pObj);
}
// transfer values from the LIs to the LOs
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData;
// erase the data values on the internal nodes of the cut
Vec_PtrForEachEntry( vCut, pObj, i )
if ( Aig_ObjIsNode(pObj) )
pObj->pData = NULL;
// replicate the data on the constant node and the PIs
pObj = Aig_ManConst1(p);
pObj->pData = Aig_ManConst1(pNew);
Saig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ManPi( pNew, i );
// duplicate logic below the cut
Saig_ManForEachPo( p, pObj, i )
{
Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
}
Vec_PtrForEachEntry( vCut, pObj, i )
{
Saig_ManRetimeDup_rec( pNew, pObj );
Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) );
}
Aig_ManCleanup( pNew );
return pNew; return pNew;
} }
@ -260,49 +424,6 @@ Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut )
return pNew; return pNew;
} }
/**Function*************************************************************
Synopsis [Derives the initial state after backward retiming.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p )
{
int nConfLimit = 1000000;
Vec_Int_t * vCiIds, * vInit = NULL;
Cnf_Dat_t * pCnf;
sat_solver * pSat;
Aig_Obj_t * pObj;
int i, RetValue, * pAssumps, * pModel;
// solve the SAT problem
pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
pAssumps = ALLOC( int, Aig_ManPoNum(p) );
Aig_ManForEachPo( p, pObj, i )
pAssumps[i] = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
RetValue = sat_solver_solve( pSat, pAssumps, pAssumps+Aig_ManPoNum(p), (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
free( pAssumps );
if ( RetValue == l_True )
{
// accumulate SAT variables of the CIs
vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );
Aig_ManForEachPi( p, pObj, i )
Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
// create the model
pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) );
Vec_IntFree( vCiIds );
}
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
return vInit;
}
/**Function************************************************************* /**Function*************************************************************
Synopsis [Returns the array of bad registers.] Synopsis [Returns the array of bad registers.]
@ -316,7 +437,7 @@ Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p )
***********************************************************************/ ***********************************************************************/
Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p ) Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
{ {
Vec_Ptr_t * vNodes = NULL; Vec_Ptr_t * vNodes;
Aig_Obj_t * pObj, * pFanin; Aig_Obj_t * pObj, * pFanin;
int i, Diffs; int i, Diffs;
assert( Saig_ManRegNum(p) > 0 ); assert( Saig_ManRegNum(p) > 0 );
@ -334,13 +455,20 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
pFanin = Aig_ObjFanin0(pObj); pFanin = Aig_ObjFanin0(pObj);
Diffs += pFanin->fMarkA && pFanin->fMarkB; Diffs += pFanin->fMarkA && pFanin->fMarkB;
} }
vNodes = Vec_PtrAlloc( 100 );
if ( Diffs > 0 ) if ( Diffs > 0 )
vNodes = Vec_PtrAlloc( Diffs ); {
Saig_ManForEachLi( p, pObj, i )
{
pFanin = Aig_ObjFanin0(pObj);
if ( pFanin->fMarkA && pFanin->fMarkB )
Vec_PtrPush( vNodes, pObj );
}
assert( Vec_PtrSize(vNodes) == Diffs );
}
Saig_ManForEachLi( p, pObj, i ) Saig_ManForEachLi( p, pObj, i )
{ {
pFanin = Aig_ObjFanin0(pObj); pFanin = Aig_ObjFanin0(pObj);
if ( vNodes && pFanin->fMarkA && pFanin->fMarkB )
Vec_PtrPush( vNodes, pFanin );
pFanin->fMarkA = pFanin->fMarkB = 0; pFanin->fMarkA = pFanin->fMarkB = 0;
} }
return vNodes; return vNodes;
@ -348,7 +476,7 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Duplicates the AIG while retiming the registers to the cut.] Synopsis [Hides the registers that cannot be backward retimed.]
Description [] Description []
@ -357,79 +485,125 @@ Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCutInit ) int Saig_ManHideBadRegs( Aig_Man_t * p, Vec_Ptr_t * vBadRegs )
{ {
Vec_Ptr_t * vToExclude, * vCut; Vec_Ptr_t * vPisNew, * vPosNew;
Vec_Int_t * vInit = NULL; Aig_Obj_t * pObjLi, * pObjLo;
Aig_Man_t * pNew, * pInit; int nTruePi, nTruePo, nBadRegs, i;
Aig_Obj_t * pObj, * pObjLi, * pObjLo; if ( Vec_PtrSize(vBadRegs) == 0 )
int i; return 0;
// check if there are bad registers // attached LOs to LIs
vToExclude = Saig_ManGetRegistersToExclude( p );
if ( vToExclude )
{
vCut = Saig_ManRetimeExtendCut( p, vCutInit, vToExclude );
printf( "Bad registers = %d. Extended cut from %d to %d nodes.\n",
Vec_PtrSize(vToExclude), Vec_PtrSize(vCutInit), Vec_PtrSize(vCut) );
Vec_PtrFree( vToExclude );
}
else
vCut = Vec_PtrDup( vCutInit );
// mark the cones under the cut
// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );
// count if there are registers to disable
// derive the initial state
pInit = Saig_ManRetimeDupInitState( p, vCut );
vInit = Saig_ManRetimeFindInitState( pInit );
if ( vInit == NULL )
printf( "Initial state computation has failed.\n" );
Aig_ManStop( pInit );
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = Vec_PtrSize(vCut);
pNew->nTruePis = p->nTruePis;
pNew->nTruePos = p->nTruePos;
// create the true PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Saig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
// create the registers
Vec_PtrForEachEntry( vCut, pObj, i )
pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), vInit?Vec_IntEntry(vInit,i):0 );
// duplicate logic above the cut and remember values
Saig_ManForEachLi( p, pObj, i )
{
Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
pObj->pData = Aig_ObjChild0Copy(pObj);
}
// transfer values from the LIs to the LOs
Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
pObjLo->pData = pObjLi->pData; pObjLi->pData = pObjLo;
// erase the data values on the internal nodes of the cut // reorder them by putting bad registers first
Vec_PtrForEachEntry( vCut, pObj, i ) vPisNew = Vec_PtrDup( p->vPis );
if ( Aig_ObjIsNode(pObj) ) vPosNew = Vec_PtrDup( p->vPos );
pObj->pData = NULL; nTruePi = Aig_ManPiNum(p) - Aig_ManRegNum(p);
// replicate the data on the primary inputs nTruePo = Aig_ManPoNum(p) - Aig_ManRegNum(p);
Saig_ManForEachPi( p, pObj, i ) assert( nTruePi == p->nTruePis );
pObj->pData = Aig_ManPi( pNew, i ); assert( nTruePo == p->nTruePos );
// duplicate logic below the cut Vec_PtrForEachEntry( vBadRegs, pObjLi, i )
Saig_ManForEachPo( p, pObj, i )
{ {
Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) ); Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLi->pData );
Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi );
pObjLi->fMarkA = 1;
} }
Vec_PtrForEachEntry( vCut, pObj, i ) Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
{ {
Saig_ManRetimeDup_rec( pNew, pObj ); if ( pObjLi->fMarkA )
Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) ); {
pObjLi->fMarkA = 0;
continue;
}
Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLo );
Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi );
} }
if ( vInit ) // check the sizes
Vec_IntFree( vInit ); assert( nTruePi == Aig_ManPiNum(p) );
Vec_PtrFree( vCut ); assert( nTruePo == Aig_ManPoNum(p) );
return pNew; // transfer the arrays
Vec_PtrFree( p->vPis ); p->vPis = vPisNew;
Vec_PtrFree( p->vPos ); p->vPos = vPosNew;
// update the PIs
nBadRegs = Vec_PtrSize(vBadRegs);
p->nRegs -= nBadRegs;
p->nTruePis += nBadRegs;
p->nTruePos += nBadRegs;
return nBadRegs;
}
/**Function*************************************************************
Synopsis [Exposes bad registers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Saig_ManExposeBadRegs( Aig_Man_t * p, int nBadRegs )
{
p->nRegs += nBadRegs;
p->nTruePis -= nBadRegs;
p->nTruePos -= nBadRegs;
}
/**Function*************************************************************
Synopsis [Performs min-area retiming backward with initial state.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Saig_ManRetimeMinAreaBackward( Aig_Man_t * pNew, int fVerbose )
{
Aig_Man_t * pInit, * pFinal;
Vec_Ptr_t * vBadRegs, * vCut;
Vec_Int_t * vInit;
int iBadReg;
// transform the AIG to have no bad registers
vBadRegs = Saig_ManGetRegistersToExclude( pNew );
if ( fVerbose && Vec_PtrSize(vBadRegs) )
printf( "Excluding %d registers that cannot be backward retimed.\n", Vec_PtrSize(vBadRegs) );
while ( 1 )
{
Saig_ManHideBadRegs( pNew, vBadRegs );
Vec_PtrFree( vBadRegs );
// compute cut
vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
{
Vec_PtrFree( vCut );
return NULL;
}
// derive the initial state
pInit = Saig_ManRetimeDupInitState( pNew, vCut );
vInit = Saig_ManRetimeInitState( pInit );
if ( vInit != NULL )
{
pFinal = Saig_ManRetimeDupBackward( pNew, vCut, vInit );
Vec_IntFree( vInit );
Vec_PtrFree( vCut );
Aig_ManStop( pInit );
return pFinal;
}
Vec_PtrFree( vCut );
// there is no initial state - find the offending output
iBadReg = Saig_ManRetimeUnsatCore( pInit, fVerbose );
Aig_ManStop( pInit );
if ( fVerbose )
printf( "Excluding register %d.\n", iBadReg );
// prepare to remove this output
vBadRegs = Vec_PtrAlloc( 1 );
Vec_PtrPush( vBadRegs, Aig_ManPo( pNew, Saig_ManPoNum(pNew) + iBadReg ) );
}
return NULL;
} }
/**Function************************************************************* /**Function*************************************************************
@ -443,36 +617,73 @@ Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCutInit )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fVerbose ) Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
{ {
Vec_Ptr_t * vCut; Vec_Ptr_t * vCut;
Aig_Man_t * pNew, * pTemp; Aig_Man_t * pNew, * pTemp, * pCopy;
int fChanges;
pNew = Aig_ManDup( p ); pNew = Aig_ManDup( p );
// perform several iterations of forward retiming // perform several iterations of forward retiming
fChanges = 0;
if ( !fBackwardOnly ) if ( !fBackwardOnly )
while ( 1 ) while ( 1 )
{ {
vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose ); vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) ) if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
{ {
if ( fVerbose && !fChanges )
printf( "Forward retiming cannot reduce registers.\n" );
Vec_PtrFree( vCut ); Vec_PtrFree( vCut );
break; break;
} }
pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut ); pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
Vec_PtrFree( vCut ); Vec_PtrFree( vCut );
if ( fVerbose )
Aig_ManReportImprovement( p, pNew );
fChanges = 1;
} }
// perform one iteration of backward retiming // perform several iterations of backward retiming
if ( !fForwardOnly ) fChanges = 0;
if ( !fForwardOnly && !fInitial )
while ( 1 )
{ {
vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose ); vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
if ( Vec_PtrSize(vCut) < Aig_ManRegNum(pNew) ) if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
{ {
pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut ); if ( fVerbose && !fChanges )
Aig_ManStop( pTemp ); printf( "Backward retiming cannot reduce registers.\n" );
Vec_PtrFree( vCut );
break;
} }
pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut, NULL );
Aig_ManStop( pTemp );
Vec_PtrFree( vCut ); Vec_PtrFree( vCut );
if ( fVerbose )
Aig_ManReportImprovement( p, pNew );
fChanges = 1;
} }
else if ( !fForwardOnly && fInitial )
while ( 1 )
{
pCopy = Aig_ManDup( pNew );
pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
Aig_ManStop( pCopy );
if ( pTemp == NULL )
{
if ( fVerbose && !fChanges )
printf( "Backward retiming cannot reduce registers.\n" );
break;
}
Saig_ManExposeBadRegs( pTemp, Saig_ManPoNum(pTemp) - Saig_ManPoNum(pNew) );
Aig_ManStop( pNew );
pNew = pTemp;
if ( fVerbose )
Aig_ManReportImprovement( p, pNew );
fChanges = 1;
}
if ( !fForwardOnly && !fInitial && fChanges )
printf( "Assuming const-0 init-state after backward retiming. Result will not verify.\n" );
return pNew; return pNew;
} }

20
src/base/abci/abc.c
View File

@ -11921,13 +11921,14 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
int fMinArea; int fMinArea;
int fForwardOnly; int fForwardOnly;
int fBackwardOnly; int fBackwardOnly;
int fInitial;
int nStepsMax; int nStepsMax;
int fFastAlgo; int fFastAlgo;
int fVerbose; int fVerbose;
int c; int c;
extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fVerbose ); extern Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
@ -11936,12 +11937,13 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults // set defaults
fMinArea = 1; fMinArea = 1;
fForwardOnly = 0; fForwardOnly = 0;
fBackwardOnly = 1; fBackwardOnly = 0;
fInitial = 1;
nStepsMax = 100000; nStepsMax = 100000;
fFastAlgo = 1; fFastAlgo = 1;
fVerbose = 0; fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Smfbavh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Smfbiavh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -11965,6 +11967,9 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'b': case 'b':
fBackwardOnly ^= 1; fBackwardOnly ^= 1;
break; break;
case 'i':
fInitial ^= 1;
break;
case 'a': case 'a':
fFastAlgo ^= 1; fFastAlgo ^= 1;
break; break;
@ -11998,7 +12003,7 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform the retiming // perform the retiming
if ( fMinArea ) if ( fMinArea )
pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose ); pNtkRes = Abc_NtkDarRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
else if ( fFastAlgo ) else if ( fFastAlgo )
pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose ); pNtkRes = Abc_NtkDarRetime( pNtk, nStepsMax, fVerbose );
else else
@ -12013,11 +12018,12 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: dretime [-S num] [-mfbavh]\n" ); fprintf( pErr, "usage: dretime [-S num] [-mfbiavh]\n" );
fprintf( pErr, "\t retimes the current network forward\n" ); fprintf( pErr, "\t new implementation of min-area retiming\n" );
fprintf( pErr, "\t-m : toggle min-area and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" ); fprintf( pErr, "\t-m : toggle min-area and most-forward retiming [default = %s]\n", fMinArea? "min-area": "most-fwd" );
fprintf( pErr, "\t-f : enables forward-only retiming [default = %s]\n", fForwardOnly? "yes": "no" ); fprintf( pErr, "\t-f : enables forward-only retiming [default = %s]\n", fForwardOnly? "yes": "no" );
fprintf( pErr, "\t-b : enables backward-only retiming [default = %s]\n", fBackwardOnly? "yes": "no" ); fprintf( pErr, "\t-b : enables backward-only retiming [default = %s]\n", fBackwardOnly? "yes": "no" );
fprintf( pErr, "\t-i : enables init state computation [default = %s]\n", fInitial? "yes": "no" );
fprintf( pErr, "\t-S num : the max number of forward retiming steps to perform [default = %d]\n", nStepsMax ); fprintf( pErr, "\t-S num : the max number of forward retiming steps to perform [default = %d]\n", nStepsMax );
fprintf( pErr, "\t-a : enables a fast most-forward algorithm [default = %s]\n", fFastAlgo? "yes": "no" ); fprintf( pErr, "\t-a : enables a fast most-forward algorithm [default = %s]\n", fFastAlgo? "yes": "no" );
fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" );
@ -13127,7 +13133,7 @@ int Abc_CommandDarPhase( Abc_Frame_t * pAbc, int argc, char ** argv )
nFrames = 0; nFrames = 0;
fIgnore = 0; fIgnore = 0;
fPrint = 0; fPrint = 0;
fVerbose = 1; fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fipvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "Fipvh" ) ) != EOF )
{ {

8
src/base/abci/abcDar.c
View File

@ -1364,6 +1364,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose ) Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchEqual, int fVerbose )
{ {
extern void Aig_ManPrintControlFanouts( Aig_Man_t * p );
Abc_Ntk_t * pNtkAig; Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp; Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 ); pMan = Abc_NtkToDar( pNtk, 0, 1 );
@ -1380,6 +1381,7 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchConst, int fLatchE
pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose ); pMan = Aig_ManScl( pTemp = pMan, fLatchConst, fLatchEqual, fVerbose );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
//Aig_ManPrintControlFanouts( pMan );
Aig_ManStop( pMan ); Aig_ManStop( pMan );
return pNtkAig; return pNtkAig;
} }
@ -1429,9 +1431,9 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fVerbose ) Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose )
{ {
extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fVerbose ); extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
Abc_Ntk_t * pNtkAig; Abc_Ntk_t * pNtkAig;
Aig_Man_t * pMan, * pTemp; Aig_Man_t * pMan, * pTemp;
pMan = Abc_NtkToDar( pNtk, 0, 1 ); pMan = Abc_NtkToDar( pNtk, 0, 1 );
@ -1444,7 +1446,7 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBa
pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
pMan = Saig_ManRetimeMinArea( pTemp = pMan, fForwardOnly, fBackwardOnly, fVerbose ); pMan = Saig_ManRetimeMinArea( pTemp = pMan, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
Aig_ManStop( pTemp ); Aig_ManStop( pTemp );
pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );