summaryrefslogtreecommitdiffstats
path: root/src/opt/fret/fretInit.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/fret/fretInit.c')
-rw-r--r--src/opt/fret/fretInit.c1334
1 files changed, 0 insertions, 1334 deletions
diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c
deleted file mode 100644
index ce9adefa..00000000
--- a/src/opt/fret/fretInit.c
+++ /dev/null
@@ -1,1334 +0,0 @@
-/**CFile****************************************************************
-
- FileName [fretInit.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Flow-based retiming package.]
-
- Synopsis [Initialization for retiming package.]
-
- Author [Aaron Hurst]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - January 1, 2008.]
-
- Revision [$Id: fretInit.c,v 1.00 2008/01/01 00:00:00 ahurst Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "vec.h"
-#include "ioAbc.h"
-#include "fretime.h"
-#include "mio.h"
-#include "hop.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-#undef DEBUG_PRINT_INIT_NTK
-
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION PROTOTYPES ///
-////////////////////////////////////////////////////////////////////////
-
-static void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj );
-static void Abc_FlowRetime_VerifyBackwardInit( Abc_Ntk_t * pNtk );
-static void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj );
-static Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj );
-
-static void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj );
-static void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop );
-
-static void Abc_FlowRetime_SetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t *pOrig );
-static void Abc_FlowRetime_GetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t **pOrig, int *lag );
-static void Abc_FlowRetime_ClearInitToOrig( Abc_Obj_t *pInit );
-
-extern void * Abc_FrameReadLibGen();
-
-extern void Abc_NtkMarkCone_rec( Abc_Obj_t * pObj, int fForward );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-
-/**Function*************************************************************
-
- Synopsis [Updates initial state information.]
-
- Description [Assumes latch boxes in original position, latches in
- new positions.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void
-Abc_FlowRetime_InitState( Abc_Ntk_t * pNtk ) {
-
- if (!pManMR->fComputeInitState) return;
-
- if (pManMR->fIsForward)
- Abc_FlowRetime_UpdateForwardInit( pNtk );
- else {
- Abc_FlowRetime_UpdateBackwardInit( pNtk );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Prints initial state information.]
-
- Description [Prints distribution of 0,1,and X initial states.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-inline int
-Abc_FlowRetime_ObjFirstNonLatchBox( Abc_Obj_t * pOrigObj, Abc_Obj_t ** pResult ) {
- int lag = 0;
- Abc_Ntk_t *pNtk;
- *pResult = pOrigObj;
- pNtk = Abc_ObjNtk( pOrigObj );
-
- Abc_NtkIncrementTravId( pNtk );
-
- while( Abc_ObjIsBo(*pResult) || Abc_ObjIsLatch(*pResult) || Abc_ObjIsBi(*pResult) ) {
- assert(Abc_ObjFaninNum(*pResult));
- *pResult = Abc_ObjFanin0(*pResult);
-
- if (Abc_NodeIsTravIdCurrent(*pResult))
- return -1;
- Abc_NodeSetTravIdCurrent(*pResult);
-
- if (Abc_ObjIsLatch(*pResult)) ++lag;
- }
-
- return lag;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Prints initial state information.]
-
- Description [Prints distribution of 0,1,and X initial states.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void
-Abc_FlowRetime_PrintInitStateInfo( Abc_Ntk_t * pNtk ) {
- int i, n0=0, n1=0, nDC=0, nOther=0;
- Abc_Obj_t *pLatch;
-
- Abc_NtkForEachLatch( pNtk, pLatch, i ) {
- if (Abc_LatchIsInit0(pLatch)) n0++;
- else if (Abc_LatchIsInit1(pLatch)) n1++;
- else if (Abc_LatchIsInitDc(pLatch)) nDC++;
- else nOther++;
- }
-
- printf("\tinitial states {0,1,x} = {%d, %d, %d}", n0, n1, nDC);
- if (nOther)
- printf(" + %d UNKNOWN", nOther);
- printf("\n");
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Computes initial state after forward retiming.]
-
- Description [Assumes box outputs in old positions stored w/ init values.
- Uses three-value simulation to preserve don't cares.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_UpdateForwardInit( Abc_Ntk_t * pNtk ) {
- Abc_Obj_t *pObj, *pFanin;
- int i;
-
- vprintf("\t\tupdating init state\n");
-
- Abc_NtkIncrementTravId( pNtk );
-
- Abc_NtkForEachLatch( pNtk, pObj, i ) {
- pFanin = Abc_ObjFanin0(pObj);
- Abc_FlowRetime_UpdateForwardInit_rec( pFanin );
-
- if (FTEST(pFanin, INIT_0))
- Abc_LatchSetInit0( pObj );
- else if (FTEST(pFanin, INIT_1))
- Abc_LatchSetInit1( pObj );
- else
- Abc_LatchSetInitDc( pObj );
- }
-}
-
-void Abc_FlowRetime_UpdateForwardInit_rec( Abc_Obj_t * pObj ) {
- Abc_Obj_t *pNext;
- int i;
-
- assert(!Abc_ObjIsPi(pObj)); // should never reach the inputs
-
- if (Abc_ObjIsBo(pObj)) return;
-
- // visited?
- if (Abc_NodeIsTravIdCurrent(pObj)) return;
- Abc_NodeSetTravIdCurrent(pObj);
-
- Abc_ObjForEachFanin( pObj, pNext, i ) {
- Abc_FlowRetime_UpdateForwardInit_rec( pNext );
- }
-
- Abc_FlowRetime_SimulateNode( pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Recursively evaluates HOP netlist.]
-
- Description [Exponential. There aren't enough flags on a HOP node.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static void Abc_FlowRetime_EvalHop_rec( Hop_Man_t *pHop, Hop_Obj_t *pObj, int *f, int *dc ) {
- int f1, dc1, f2, dc2;
- Hop_Obj_t *pReg = Hop_Regular(pObj);
-
- // const 0
- if (Hop_ObjIsConst1(pReg)) {
- *f = 1;
- *f ^= (pReg == pObj ? 1 : 0);
- *dc = 0;
- return;
- }
-
- // PI
- if (Hop_ObjIsPi(pReg)) {
- *f = pReg->fMarkA;
- *f ^= (pReg == pObj ? 1 : 0);
- *dc = pReg->fMarkB;
- return;
- }
-
- // PO
- if (Hop_ObjIsPo(pReg)) {
- assert( pReg == pObj );
- Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild0(pReg), f, dc);
- return;
- }
-
- // AND
- if (Hop_ObjIsAnd(pReg)) {
- Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild0(pReg), &f1, &dc1);
- Abc_FlowRetime_EvalHop_rec(pHop, Hop_ObjChild1(pReg), &f2, &dc2);
-
- *dc = (dc1 & f2) | (dc2 & f1) | (dc1 & dc2);
- *f = f1 & f2;
- *f ^= (pReg == pObj ? 1 : 0);
- return;
- }
-
- assert(0);
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Sets initial value flags.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline void Abc_FlowRetime_SetInitValue( Abc_Obj_t * pObj,
- int val, int dc ) {
-
- // store init value
- FUNSET(pObj, INIT_CARE);
- if (!dc){
- if (val) {
- FSET(pObj, INIT_1);
- } else {
- FSET(pObj, INIT_0);
- }
- }
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Propogates initial state through a logic node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_SimulateNode( Abc_Obj_t * pObj ) {
- Abc_Ntk_t *pNtk = Abc_ObjNtk(pObj);
- Abc_Obj_t * pFanin;
- int i, rAnd, rVar, dcAnd, dcVar;
- DdManager * dd = pNtk->pManFunc;
- DdNode *pBdd = pObj->pData, *pVar;
- Hop_Man_t *pHop = pNtk->pManFunc;
-
- assert(!Abc_ObjIsLatch(pObj));
- assert(Abc_ObjRegular(pObj));
-
- // (i) constant nodes
- if (Abc_NtkIsStrash(pNtk) && Abc_AigNodeIsConst(pObj)) {
- Abc_FlowRetime_SetInitValue(pObj, 1, 0);
- return;
- }
- if (!Abc_NtkIsStrash( pNtk ) && Abc_ObjIsNode(pObj)) {
- if (Abc_NodeIsConst0(pObj)) {
- Abc_FlowRetime_SetInitValue(pObj, 0, 0);
- return;
- } else if (Abc_NodeIsConst1(pObj)) {
- Abc_FlowRetime_SetInitValue(pObj, 1, 0);
- return;
- }
- }
-
- // (ii) terminal nodes
- if (!Abc_ObjIsNode(pObj)) {
- pFanin = Abc_ObjFanin0(pObj);
-
- Abc_FlowRetime_SetInitValue(pObj,
- (FTEST(pFanin, INIT_1) ? 1 : 0) ^ pObj->fCompl0,
- !FTEST(pFanin, INIT_CARE));
- return;
- }
-
- // (iii) logic nodes
-
- // ------ SOP network
- if ( Abc_NtkHasSop( pNtk )) {
- Abc_FlowRetime_SimulateSop( pObj, (char *)Abc_ObjData(pObj) );
- return;
- }
-
- // ------ BDD network
- else if ( Abc_NtkHasBdd( pNtk )) {
- assert(dd);
- assert(pBdd);
-
- // cofactor for 0,1 inputs
- // do nothing for X values
- Abc_ObjForEachFanin(pObj, pFanin, i) {
- pVar = Cudd_bddIthVar( dd, i );
- if (FTEST(pFanin, INIT_CARE)) {
- if (FTEST(pFanin, INIT_0))
- pBdd = Cudd_Cofactor( dd, pBdd, Cudd_Not(pVar) );
- else
- pBdd = Cudd_Cofactor( dd, pBdd, pVar );
- }
- }
-
- // if function has not been reduced to
- // a constant, propagate an X
- rVar = (pBdd == Cudd_ReadOne(dd));
- dcVar = !Cudd_IsConstant(pBdd);
-
- Abc_FlowRetime_SetInitValue(pObj, rVar, dcVar);
- return;
- }
-
-
- // ------ AIG logic network
- else if ( Abc_NtkHasAig( pNtk ) && !Abc_NtkIsStrash( pNtk )) {
-
- assert(Abc_ObjIsNode(pObj));
- assert(pObj->pData);
- assert(Abc_ObjFaninNum(pObj) <= Hop_ManPiNum(pHop) );
-
- // set vals at inputs
- Abc_ObjForEachFanin(pObj, pFanin, i) {
- Hop_ManPi(pHop, i)->fMarkA = FTEST(pFanin, INIT_1)?1:0;
- Hop_ManPi(pHop, i)->fMarkB = FTEST(pFanin, INIT_CARE)?1:0;
- }
-
- Abc_FlowRetime_EvalHop_rec( pHop, pObj->pData, &rVar, &dcVar );
-
- Abc_FlowRetime_SetInitValue(pObj, rVar, dcVar);
-
- // clear flags
- Abc_ObjForEachFanin(pObj, pFanin, i) {
- Hop_ManPi(pHop, i)->fMarkA = 0;
- Hop_ManPi(pHop, i)->fMarkB = 0;
- }
-
- return;
- }
-
- // ------ strashed network
- else if ( Abc_NtkIsStrash( pNtk )) {
-
- assert(Abc_ObjType(pObj) == ABC_OBJ_NODE);
- dcAnd = 0, rAnd = 1;
-
- pFanin = Abc_ObjFanin0(pObj);
- dcAnd |= FTEST(pFanin, INIT_CARE) ? 0 : 1;
- rVar = FTEST(pFanin, INIT_0) ? 0 : 1;
- if (pObj->fCompl0) rVar ^= 1; // complimented?
- rAnd &= rVar;
-
- pFanin = Abc_ObjFanin1(pObj);
- dcAnd |= FTEST(pFanin, INIT_CARE) ? 0 : 1;
- rVar = FTEST(pFanin, INIT_0) ? 0 : 1;
- if (pObj->fCompl1) rVar ^= 1; // complimented?
- rAnd &= rVar;
-
- if (!rAnd) dcAnd = 0; /* controlling value */
-
- Abc_FlowRetime_SetInitValue(pObj, rAnd, dcAnd);
- return;
- }
-
- // ------ MAPPED network
- else if ( Abc_NtkHasMapping( pNtk )) {
- Abc_FlowRetime_SimulateSop( pObj, (char *)Mio_GateReadSop(pObj->pData) );
- return;
- }
-
- assert(0);
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Propogates initial state through a SOP node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_SimulateSop( Abc_Obj_t * pObj, char *pSop ) {
- Abc_Obj_t * pFanin;
- char *pCube;
- int i, j, rAnd, rOr, rVar, dcAnd, dcOr, v;
-
- assert( pSop && !Abc_SopIsExorType(pSop) );
-
- rOr = 0, dcOr = 0;
-
- i = Abc_SopGetVarNum(pSop);
- Abc_SopForEachCube( pSop, i, pCube ) {
- rAnd = 1, dcAnd = 0;
- Abc_CubeForEachVar( pCube, v, j ) {
- pFanin = Abc_ObjFanin(pObj, j);
- if ( v == '0' )
- rVar = FTEST(pFanin, INIT_0) ? 1 : 0;
- else if ( v == '1' )
- rVar = FTEST(pFanin, INIT_1) ? 1 : 0;
- else
- continue;
-
- if (FTEST(pFanin, INIT_CARE))
- rAnd &= rVar;
- else
- dcAnd = 1;
- }
- if (!rAnd) dcAnd = 0; /* controlling value */
- if (dcAnd)
- dcOr = 1;
- else
- rOr |= rAnd;
- }
- if (rOr) dcOr = 0; /* controlling value */
-
- // complement the result if necessary
- if ( !Abc_SopGetPhase(pSop) )
- rOr ^= 1;
-
- Abc_FlowRetime_SetInitValue(pObj, rOr, dcOr);
-}
-
-/**Function*************************************************************
-
- Synopsis [Sets up backward initial state computation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_SetupBackwardInit( Abc_Ntk_t * pNtk ) {
- Abc_Obj_t *pLatch, *pObj, *pPi;
- int i;
- Vec_Ptr_t *vObj = Vec_PtrAlloc(100);
-
- // create the network used for the initial state computation
- if (Abc_NtkIsStrash(pNtk)) {
- pManMR->pInitNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
- } else if (Abc_NtkHasMapping(pNtk))
- pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, ABC_FUNC_SOP, 1 );
- else
- pManMR->pInitNtk = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 );
-
- // mitre inputs
- Abc_NtkForEachLatch( pNtk, pLatch, i ) {
- // map latch to initial state network
- pPi = Abc_NtkCreatePi( pManMR->pInitNtk );
-
- // DEBUG
- // printf("setup : mapping latch %d to PI %d\n", pLatch->Id, pPi->Id);
-
- // has initial state requirement?
- if (Abc_LatchIsInit0(pLatch)) {
- pObj = Abc_NtkCreateNodeInv( pManMR->pInitNtk, pPi );
- Vec_PtrPush(vObj, pObj);
- }
- else if (Abc_LatchIsInit1(pLatch)) {
- Vec_PtrPush(vObj, pPi);
- }
-
- Abc_ObjSetData( pLatch, pPi ); // if not verifying init state
- // FDATA(pLatch)->pInitObj = pPi; // if verifying init state
- }
-
- // are there any nodes not DC?
- if (!Vec_PtrSize(vObj)) {
- pManMR->fSolutionIsDc = 1;
- return;
- } else
- pManMR->fSolutionIsDc = 0;
-
- // mitre output
-
- // create n-input AND gate
- pObj = Abc_NtkCreateNodeAnd( pManMR->pInitNtk, vObj );
-
- Abc_ObjAddFanin( Abc_NtkCreatePo( pManMR->pInitNtk ), pObj );
-
- Vec_PtrFree( vObj );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Solves backward initial state computation.]
-
- Description []
-
- SideEffects [Sets object copies in init ntk.]
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_FlowRetime_SolveBackwardInit( Abc_Ntk_t * pNtk ) {
- int i;
- Abc_Obj_t *pObj, *pInitObj;
- Vec_Ptr_t *vDelete = Vec_PtrAlloc(0);
- Abc_Ntk_t *pSatNtk;
- int result;
-
- assert(pManMR->pInitNtk);
-
- // is the solution entirely DC's?
- if (pManMR->fSolutionIsDc) {
- Vec_PtrFree(vDelete);
- Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_LatchSetInitDc( pObj );
- vprintf("\tno init state computation: all-don't-care solution\n");
- return 1;
- }
-
- // check that network is combinational
- Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i ) {
- assert(!Abc_ObjIsLatch(pObj));
- assert(!Abc_ObjIsBo(pObj));
- assert(!Abc_ObjIsBi(pObj));
- }
-
- // delete superfluous nodes
- while(Vec_PtrSize( vDelete )) {
- pObj = (Abc_Obj_t *)Vec_PtrPop( vDelete );
- Abc_NtkDeleteObj( pObj );
- }
- Vec_PtrFree(vDelete);
-
- // do some final cleanup on the network
- Abc_NtkAddDummyPoNames(pManMR->pInitNtk);
- Abc_NtkAddDummyPiNames(pManMR->pInitNtk);
- if (Abc_NtkIsLogic(pManMR->pInitNtk))
- Abc_NtkCleanup(pManMR->pInitNtk, 0);
-
-#if defined(DEBUG_PRINT_INIT_NTK)
- Abc_NtkLevelReverse( pManMR->pInitNtk );
- Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i )
- if (Abc_ObjLevel( pObj ) < 2)
- Abc_ObjPrint(stdout, pObj);
-#endif
-
- vprintf("\tsolving for init state (%d nodes)... ", Abc_NtkObjNum(pManMR->pInitNtk));
- fflush(stdout);
-
- // convert SOPs to BDD
- if (Abc_NtkHasSop(pManMR->pInitNtk))
- Abc_NtkSopToBdd( pManMR->pInitNtk );
- // convert AIGs to BDD
- if (Abc_NtkHasAig(pManMR->pInitNtk))
- Abc_NtkAigToBdd( pManMR->pInitNtk );
-
- pSatNtk = pManMR->pInitNtk;
-
- // solve
- result = Abc_NtkMiterSat( pSatNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
-
- if (!result) {
- vprintf("SUCCESS\n");
- } else {
- vprintf("FAILURE\n");
- return 0;
- }
-
- // clear initial values, associate PIs to latches
- Abc_NtkForEachPi( pManMR->pInitNtk, pInitObj, i ) Abc_ObjSetCopy( pInitObj, NULL );
- Abc_NtkForEachLatch( pNtk, pObj, i ) {
- pInitObj = Abc_ObjData( pObj );
- assert( Abc_ObjIsPi( pInitObj ));
- Abc_ObjSetCopy( pInitObj, pObj );
- Abc_LatchSetInitNone( pObj );
-
- // DEBUG
- // printf("solve : getting latch %d from PI %d\n", pObj->Id, pInitObj->Id);
- }
-
- // copy solution from PIs to latches
- assert(pManMR->pInitNtk->pModel);
- Abc_NtkForEachPi( pManMR->pInitNtk, pInitObj, i ) {
- if ((pObj = Abc_ObjCopy( pInitObj ))) {
- if ( pManMR->pInitNtk->pModel[i] )
- Abc_LatchSetInit1( pObj );
- else
- Abc_LatchSetInit0( pObj );
- }
- }
-
-#if defined(DEBUG_CHECK)
- // check that all latches have initial state
- Abc_NtkForEachLatch( pNtk, pObj, i ) assert( !Abc_LatchIsInitNone( pObj ) );
-#endif
-
- return 1;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Updates backward initial state computation problem.]
-
- Description [Assumes box outputs in old positions stored w/ init values.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_UpdateBackwardInit( Abc_Ntk_t * pNtk ) {
- Abc_Obj_t *pOrigObj, *pInitObj;
- Vec_Ptr_t *vBo = Vec_PtrAlloc(100);
- Vec_Ptr_t *vPi = Vec_PtrAlloc(100);
- Abc_Ntk_t *pInitNtk = pManMR-> pInitNtk;
- Abc_Obj_t *pBuf;
- int i;
-
- // remove PIs from network (from BOs)
- Abc_NtkForEachObj( pNtk, pOrigObj, i )
- if (Abc_ObjIsBo(pOrigObj)) {
- pInitObj = FDATA(pOrigObj)->pInitObj;
- assert(Abc_ObjIsPi(pInitObj));
-
- // DEBUG
- // printf("update : freeing PI %d\n", pInitObj->Id);
-
- // create a buffer instead
- pBuf = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
- Abc_FlowRetime_ClearInitToOrig( pBuf );
-
- Abc_ObjBetterTransferFanout( pInitObj, pBuf, 0 );
- FDATA(pOrigObj)->pInitObj = pBuf;
- pOrigObj->fMarkA = 1;
-
- Vec_PtrPush(vBo, pOrigObj);
- Vec_PtrPush(vPi, pInitObj);
- }
-
- // check that PIs are all free
- Abc_NtkForEachPi( pInitNtk, pInitObj, i) {
- assert( Abc_ObjFanoutNum( pInitObj ) == 0);
- }
-
- // add PIs to to latches
- Abc_NtkForEachLatch( pNtk, pOrigObj, i ) {
- assert(Vec_PtrSize(vPi) > 0);
- pInitObj = Vec_PtrPop(vPi);
-
- // DEBUG
- // printf("update : mapping latch %d to PI %d\n", pOrigObj->Id, pInitObj->Id);
-
- pOrigObj->fMarkA = pOrigObj->fMarkB = 1;
- FDATA(pOrigObj)->pInitObj = pInitObj;
- Abc_ObjSetData(pOrigObj, pInitObj);
- }
-
- // recursively build init network
- Vec_PtrForEachEntry( Abc_Obj_t *, vBo, pOrigObj, i )
- Abc_FlowRetime_UpdateBackwardInit_rec( pOrigObj );
-
- // clear flags
- Abc_NtkForEachObj( pNtk, pOrigObj, i )
- pOrigObj->fMarkA = pOrigObj->fMarkB = 0;
-
- // deallocate
- Vec_PtrFree( vBo );
- Vec_PtrFree( vPi );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Creates a corresponding node in the init state network]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t *Abc_FlowRetime_CopyNodeToInitNtk( Abc_Obj_t *pOrigObj ) {
- Abc_Ntk_t *pNtk = pManMR->pNtk;
- Abc_Ntk_t *pInitNtk = pManMR->pInitNtk;
- Abc_Obj_t *pInitObj;
- void *pData;
- int fCompl[2];
-
- assert(pOrigObj);
-
- // what we do depends on the ntk types of original / init networks...
-
- // (0) convert BI/BO nodes to buffers
- if (Abc_ObjIsBi( pOrigObj ) || Abc_ObjIsBo( pOrigObj ) ) {
- pInitObj = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
- Abc_FlowRetime_ClearInitToOrig( pInitObj );
- return pInitObj;
- }
-
- // (i) strash node -> SOP node
- if (Abc_NtkIsStrash( pNtk )) {
-
- if (Abc_AigNodeIsConst( pOrigObj )) {
- return Abc_NtkCreateNodeConst1( pInitNtk );
- }
- if (!Abc_ObjIsNode( pOrigObj )) {
- assert(Abc_ObjFaninNum(pOrigObj) == 1);
- pInitObj = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
- Abc_FlowRetime_ClearInitToOrig( pInitObj );
- return pInitObj;
- }
-
- assert( Abc_ObjIsNode(pOrigObj) );
- pInitObj = Abc_NtkCreateObj( pInitNtk, ABC_OBJ_NODE );
-
- fCompl[0] = pOrigObj->fCompl0 ? 1 : 0;
- fCompl[1] = pOrigObj->fCompl1 ? 1 : 0;
-
- pData = Abc_SopCreateAnd( (Extra_MmFlex_t *)pInitNtk->pManFunc, 2, fCompl );
- assert(pData);
- pInitObj->pData = Abc_SopRegister( (Extra_MmFlex_t *)pInitNtk->pManFunc, pData );
- }
-
- // (ii) mapped node -> SOP node
- else if (Abc_NtkHasMapping( pNtk )) {
- if (!pOrigObj->pData) {
- // assume terminal...
- assert(Abc_ObjFaninNum(pOrigObj) == 1);
-
- pInitObj = Abc_NtkCreateNodeBuf( pInitNtk, NULL );
- Abc_FlowRetime_ClearInitToOrig( pInitObj );
- return pInitObj;
- }
-
- pInitObj = Abc_NtkCreateObj( pInitNtk, Abc_ObjType(pOrigObj) );
- pData = Mio_GateReadSop(pOrigObj->pData);
- assert( Abc_SopGetVarNum(pData) == Abc_ObjFaninNum(pOrigObj) );
-
- pInitObj->pData = Abc_SopRegister( (Extra_MmFlex_t *)pInitNtk->pManFunc, pData );
- }
-
- // (iii) otherwise, duplicate obj
- else {
- pInitObj = Abc_NtkDupObj( pInitNtk, pOrigObj, 0 );
-
- // copy phase
- pInitObj->fPhase = pOrigObj->fPhase;
- }
-
- assert(pInitObj);
- return pInitObj;
-}
-
-/**Function*************************************************************
-
- Synopsis [Updates backward initial state computation problem.]
-
- Description [Creates a duplicate node in the initial state network
- corresponding to a node in the original circuit. If
- fRecurse is set, the procedure recurses on and connects
- the new node to its fan-ins. A latch in the original
- circuit corresponds to a PI in the initial state network.
- An existing PI may be supplied by pUseThisPi, and if the
- node is a latch, it will be used; otherwise the PI is
- saved in the list vOtherPis and subsequently used for
- another latch.]
-
- SideEffects [Nodes that have a corresponding initial state node
- are marked with fMarkA. Nodes that have been fully
- connected in the initial state network are marked with
- fMarkB.]
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Obj_t* Abc_FlowRetime_UpdateBackwardInit_rec( Abc_Obj_t *pOrigObj) {
- Abc_Obj_t *pOrigFanin, *pInitFanin, *pInitObj;
- int i;
-
- assert(pOrigObj);
-
- // should never reach primary IOs
- assert(!Abc_ObjIsPi(pOrigObj));
- assert(!Abc_ObjIsPo(pOrigObj));
-
- // skip bias nodes
- if (FTEST(pOrigObj, BIAS_NODE))
- return NULL;
-
- // does an init node already exist?
- if(!pOrigObj->fMarkA) {
-
- pInitObj = Abc_FlowRetime_CopyNodeToInitNtk( pOrigObj );
-
- Abc_FlowRetime_SetInitToOrig( pInitObj, pOrigObj );
- FDATA(pOrigObj)->pInitObj = pInitObj;
-
- pOrigObj->fMarkA = 1;
- } else {
- pInitObj = FDATA(pOrigObj)->pInitObj;
- }
- assert(pInitObj);
-
- // have we already connected this object?
- if (!pOrigObj->fMarkB) {
-
- // create and/or connect fanins
- Abc_ObjForEachFanin( pOrigObj, pOrigFanin, i ) {
- // should not reach BOs (i.e. the start of the next frame)
- // the new latch bounday should lie before it
- assert(!Abc_ObjIsBo( pOrigFanin ));
- pInitFanin = Abc_FlowRetime_UpdateBackwardInit_rec( pOrigFanin );
- Abc_ObjAddFanin( pInitObj, pInitFanin );
- }
-
- pOrigObj->fMarkB = 1;
- }
-
- return pInitObj;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Verifies backward init state computation.]
-
- Description [This procedure requires the BOs to store the original
- latch values and the latches to store the new values:
- both in the INIT_0 and INIT_1 flags in the Flow_Data
- structure. (This is not currently the case in the rest
- of the code.) Also, can not verify backward state
- computations that span multiple combinational frames.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_VerifyBackwardInit( Abc_Ntk_t * pNtk ) {
- Abc_Obj_t *pObj, *pFanin;
- int i;
-
- vprintf("\t\tupdating init state\n");
-
- Abc_NtkIncrementTravId( pNtk );
-
- Abc_NtkForEachObj( pNtk, pObj, i )
- if (Abc_ObjIsBo( pObj )) {
- pFanin = Abc_ObjFanin0(pObj);
- Abc_FlowRetime_VerifyBackwardInit_rec( pFanin );
-
- if (FTEST(pObj, INIT_CARE)) {
- if(FTEST(pObj, INIT_CARE) != FTEST(pFanin, INIT_CARE)) {
- printf("ERROR: expected val=%d care=%d and got val=%d care=%d\n",
- FTEST(pObj, INIT_1)?1:0, FTEST(pObj, INIT_CARE)?1:0,
- FTEST(pFanin, INIT_1)?1:0, FTEST(pFanin, INIT_CARE)?1:0 );
-
- }
- }
- }
-}
-
-void Abc_FlowRetime_VerifyBackwardInit_rec( Abc_Obj_t * pObj ) {
- Abc_Obj_t *pNext;
- int i;
-
- assert(!Abc_ObjIsBo(pObj)); // should never reach the inputs
- assert(!Abc_ObjIsPi(pObj)); // should never reach the inputs
-
- // visited?
- if (Abc_NodeIsTravIdCurrent(pObj)) return;
- Abc_NodeSetTravIdCurrent(pObj);
-
- if (Abc_ObjIsLatch(pObj)) {
- FUNSET(pObj, INIT_CARE);
- if (Abc_LatchIsInit0(pObj))
- FSET(pObj, INIT_0);
- else if (Abc_LatchIsInit1(pObj))
- FSET(pObj, INIT_1);
- return;
- }
-
- Abc_ObjForEachFanin( pObj, pNext, i ) {
- Abc_FlowRetime_VerifyBackwardInit_rec( pNext );
- }
-
- Abc_FlowRetime_SimulateNode( pObj );
-}
-
-/**Function*************************************************************
-
- Synopsis [Constrains backward retiming for initializability.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_FlowRetime_PartialSat(Vec_Ptr_t *vNodes, int cut) {
- Abc_Ntk_t *pPartNtk, *pInitNtk = pManMR->pInitNtk;
- Abc_Obj_t *pObj, *pNext, *pPartObj, *pPartNext, *pPo;
- int i, j, result;
-
- assert( Abc_NtkPoNum( pInitNtk ) == 1 );
-
- pPartNtk = Abc_NtkAlloc( pInitNtk->ntkType, pInitNtk->ntkFunc, 0 );
-
- // copy network
- Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i ) {
- pObj->Level = i;
- assert(!Abc_ObjIsPo( pObj ));
-
- if (i < cut && !pObj->fMarkA) {
- pPartObj = Abc_NtkCreatePi( pPartNtk );
- Abc_ObjSetCopy( pObj, pPartObj );
- } else {
- // copy node
- pPartObj = Abc_NtkDupObj( pPartNtk, pObj, 0 );
- // copy complementation
- pPartObj->fPhase = pObj->fPhase;
-
- // connect fanins
- Abc_ObjForEachFanin( pObj, pNext, j ) {
- pPartNext = Abc_ObjCopy( pNext );
- assert(pPartNext);
- Abc_ObjAddFanin( pPartObj, pPartNext );
- }
- }
-
- assert(pObj->pCopy == pPartObj);
- }
-
- // create PO
- pPo = Abc_NtkCreatePo( pPartNtk );
- pNext = Abc_ObjFanin0( Abc_NtkPo( pInitNtk, 0 ) );
- pPartNext = Abc_ObjCopy( pNext );
- assert( pPartNext );
- Abc_ObjAddFanin( pPo, pPartNext );
-
- // check network
-#if defined(DEBUG_CHECK)
- Abc_NtkAddDummyPoNames(pPartNtk);
- Abc_NtkAddDummyPiNames(pPartNtk);
- Abc_NtkCheck( pPartNtk );
-#endif
-
- result = Abc_NtkMiterSat( pPartNtk, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
-
- Abc_NtkDelete( pPartNtk );
-
- return !result;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Constrains backward retiming for initializability.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_ConstrainInit( ) {
- Vec_Ptr_t *vNodes;
- int low, high, mid;
- int i, n, lag;
- Abc_Obj_t *pObj = NULL, *pOrigObj;
- InitConstraint_t *pConstraint = ALLOC( InitConstraint_t, 1 );
-
- memset( pConstraint, 0, sizeof(InitConstraint_t) );
-
- assert(pManMR->pInitNtk);
-
- vprintf("\tsearch for initial state conflict...\n");
-
- vNodes = Abc_NtkDfs(pManMR->pInitNtk, 0);
- n = Vec_PtrSize(vNodes);
- // also add PIs to vNodes
- Abc_NtkForEachPi(pManMR->pInitNtk, pObj, i)
- Vec_PtrPush(vNodes, pObj);
- Vec_PtrReorder(vNodes, n);
-
-#if defined(DEBUG_CHECK)
- assert(!Abc_FlowRetime_PartialSat( vNodes, 0 ));
-#endif
-
- // grow initialization constraint
- do {
- vprintf("\t\t");
-
- // find element to add to set...
- low = 0, high = Vec_PtrSize(vNodes);
- while (low != high-1) {
- mid = (low + high) >> 1;
-
- if (!Abc_FlowRetime_PartialSat( vNodes, mid )) {
- low = mid;
- vprintf("-");
- } else {
- high = mid;
- vprintf("*");
- }
- fflush(stdout);
- }
-
-#if defined(DEBUG_CHECK)
- assert(Abc_FlowRetime_PartialSat( vNodes, high ));
- assert(!Abc_FlowRetime_PartialSat( vNodes, low ));
-#endif
-
- // mark its TFO
- pObj = Vec_PtrEntry( vNodes, low );
- Abc_NtkMarkCone_rec( pObj, 1 );
- vprintf(" conflict term = %d ", low);
-
-#if 0
- printf("init ------\n");
- Abc_ObjPrint(stdout, pObj);
- printf("\n");
- Abc_ObjPrintNeighborhood( pObj, 1 );
- printf("------\n");
-#endif
-
- // add node to constraint
- Abc_FlowRetime_GetInitToOrig( pObj, &pOrigObj, &lag );
- assert(pOrigObj);
- vprintf(" <=> %d/%d\n", Abc_ObjId(pOrigObj), lag);
-
-#if 0
- printf("orig ------\n");
- Abc_ObjPrint(stdout, pOrigObj);
- printf("\n");
- Abc_ObjPrintNeighborhood( pOrigObj, 1 );
- printf("------\n");
-#endif
- Vec_IntPush( &pConstraint->vNodes, Abc_ObjId(pOrigObj) );
- Vec_IntPush( &pConstraint->vLags, lag );
-
- } while (Abc_FlowRetime_PartialSat( vNodes, Vec_PtrSize(vNodes) ));
-
- pConstraint->pBiasNode = NULL;
-
- // add constraint
- Vec_PtrPush( pManMR->vInitConstraints, pConstraint );
-
- // clear marks
- Abc_NtkForEachObj( pManMR->pInitNtk, pObj, i)
- pObj->fMarkA = 0;
-
- // free
- Vec_PtrFree( vNodes );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Removes nodes to bias against uninitializable cuts.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_RemoveInitBias( ) {
- // Abc_Ntk_t *pNtk = pManMR->pNtk;
- Abc_Obj_t *pBiasNode;
- InitConstraint_t *pConstraint;
- int i;
-
- Vec_PtrForEachEntry( Abc_Obj_t *, pManMR->vInitConstraints, pConstraint, i ) {
- pBiasNode = pConstraint->pBiasNode;
- pConstraint->pBiasNode = NULL;
-
- if (pBiasNode)
- Abc_NtkDeleteObj(pBiasNode);
- }
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Connects the bias node to one of the constraint vertices.]
-
- Description [ACK!
- Currently this is dumb dumb hack.
- What should we do with biases that belong on BOs? These
- move through the circuit.
- Currently, the bias gets marked on the fan-in of BO
- and the bias gets implemented on every BO fan-out of a
- node.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static void Abc_FlowRetime_ConnectBiasNode(Abc_Obj_t *pBiasNode, Abc_Obj_t *pObj, int biasLag) {
- Abc_Obj_t *pCur, *pNext;
- int i;
- int lag;
- Vec_Ptr_t *vNodes = Vec_PtrAlloc(1);
- Vec_Int_t *vLags = Vec_IntAlloc(1);
- Abc_Ntk_t *pNtk = Abc_ObjNtk( pObj );
-
- Vec_PtrPush( vNodes, pObj );
- Vec_IntPush( vLags, 0 );
-
- Abc_NtkIncrementTravId( pNtk );
-
- while (Vec_PtrSize( vNodes )) {
- pCur = Vec_PtrPop( vNodes );
- lag = Vec_IntPop( vLags );
-
- if (Abc_NodeIsTravIdCurrent( pCur )) continue;
- Abc_NodeSetTravIdCurrent( pCur );
-
- if (!Abc_ObjIsLatch(pCur) &&
- !Abc_ObjIsBo(pCur) &&
- Abc_FlowRetime_GetLag(pObj)+lag == biasLag ) {
-
- // printf("biasing : ");
- // Abc_ObjPrint(stdout, pCur );
-#if 1
- FSET( pCur, BLOCK );
-#else
- Abc_ObjAddFanin( pCur, pBiasNode );
-#endif
- }
-
- Abc_ObjForEachFanout( pCur, pNext, i ) {
- if (Abc_ObjIsBi(pNext) ||
- Abc_ObjIsLatch(pNext) ||
- Abc_ObjIsBo(pNext) ||
- Abc_ObjIsBo(pCur)) {
- Vec_PtrPush( vNodes, pNext );
- Vec_IntPush( vLags, lag - Abc_ObjIsLatch(pNext) ? 1 : 0 );
- }
- }
- }
-
- Vec_PtrFree( vNodes );
- Vec_IntFree( vLags );
-}
-
-/**Function*************************************************************
-
- Synopsis [Adds nodes to bias against uninitializable cuts.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_AddInitBias( ) {
- Abc_Ntk_t *pNtk = pManMR->pNtk;
- Abc_Obj_t *pBiasNode, *pObj;
- InitConstraint_t *pConstraint;
- int i, j, id;
- const int nConstraints = Vec_PtrSize( pManMR->vInitConstraints );
-
- pManMR->pDataArray = REALLOC( Flow_Data_t, pManMR->pDataArray, pManMR->nNodes + (nConstraints*(pManMR->iteration+1)) );
- memset(pManMR->pDataArray + pManMR->nNodes, 0, sizeof(Flow_Data_t)*(nConstraints*(pManMR->iteration+1)));
-
- vprintf("\t\tcreating %d bias structures\n", nConstraints);
-
- Vec_PtrForEachEntry( Abc_Obj_t *, pManMR->vInitConstraints, pConstraint, i ) {
- if (pConstraint->pBiasNode) continue;
-
- // printf("\t\t\tbias %d...\n", i);
- pBiasNode = Abc_NtkCreateBlackbox( pNtk );
-
- Vec_IntForEachEntry( &pConstraint->vNodes, id, j ) {
- pObj = Abc_NtkObj(pNtk, id);
- Abc_FlowRetime_ConnectBiasNode(pBiasNode, pObj, Vec_IntEntry(&pConstraint->vLags, j));
- }
-
- // pConstraint->pBiasNode = pBiasNode;
- }
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Clears mapping from init node to original node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_ClearInitToOrig( Abc_Obj_t *pInit )
-{
- int id = Abc_ObjId( pInit );
-
- // grow data structure if necessary
- if (id >= pManMR->sizeInitToOrig) {
- int oldSize = pManMR->sizeInitToOrig;
- pManMR->sizeInitToOrig = 1.5*id + 10;
- pManMR->pInitToOrig = realloc(pManMR->pInitToOrig, sizeof(NodeLag_t)*pManMR->sizeInitToOrig);
- memset( &(pManMR->pInitToOrig[oldSize]), 0, sizeof(NodeLag_t)*(pManMR->sizeInitToOrig-oldSize) );
- }
- assert( pManMR->pInitToOrig );
-
- pManMR->pInitToOrig[id].id = -1;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Sets mapping from init node to original node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_SetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t *pOrig)
-{
- int lag;
- int id = Abc_ObjId( pInit );
-
- // grow data structure if necessary
- if (id >= pManMR->sizeInitToOrig) {
- int oldSize = pManMR->sizeInitToOrig;
- pManMR->sizeInitToOrig = 1.5*id + 10;
- pManMR->pInitToOrig = realloc(pManMR->pInitToOrig, sizeof(NodeLag_t)*pManMR->sizeInitToOrig);
- memset( &(pManMR->pInitToOrig[oldSize]), 0, sizeof(NodeLag_t)*(pManMR->sizeInitToOrig-oldSize) );
- }
- assert( pManMR->pInitToOrig );
-
- // ignore BI, BO, and latch nodes
- if (Abc_ObjIsBo(pOrig) || Abc_ObjIsBi(pOrig) || Abc_ObjIsLatch(pOrig)) {
- Abc_FlowRetime_ClearInitToOrig(pInit);
- return;
- }
-
- // move out of latch boxes
- lag = Abc_FlowRetime_ObjFirstNonLatchBox(pOrig, &pOrig);
-
- pManMR->pInitToOrig[id].id = Abc_ObjId(pOrig);
- pManMR->pInitToOrig[id].lag = Abc_FlowRetime_GetLag(pOrig) + lag;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Gets mapping from init node to original node.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_FlowRetime_GetInitToOrig( Abc_Obj_t *pInit, Abc_Obj_t **pOrig, int *lag ) {
-
- int id = Abc_ObjId( pInit );
- int origId;
-
- assert(id < pManMR->sizeInitToOrig);
-
- origId = pManMR->pInitToOrig[id].id;
-
- if (origId < 0) {
- assert(Abc_ObjFaninNum(pInit));
- Abc_FlowRetime_GetInitToOrig( Abc_ObjFanin0(pInit), pOrig, lag);
- return;
- }
-
- *pOrig = Abc_NtkObj(pManMR->pNtk, origId);
- *lag = pManMR->pInitToOrig[id].lag;
-}
-ABC_NAMESPACE_IMPL_END
-