diff options
Diffstat (limited to 'src/base/abcs/abcRetImpl.c')
| -rw-r--r-- | src/base/abcs/abcRetImpl.c | 368 |
1 files changed, 225 insertions, 143 deletions
diff --git a/src/base/abcs/abcRetImpl.c b/src/base/abcs/abcRetImpl.c index ea849c1c..0082ff22 100644 --- a/src/base/abcs/abcRetImpl.c +++ b/src/base/abcs/abcRetImpl.c @@ -26,6 +26,8 @@ static void Abc_ObjRetimeForward( Abc_Obj_t * pObj ); static int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtk, stmm_table * tTable, Vec_Int_t * vValues ); +static void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable ); +static void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -51,7 +53,9 @@ int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags ) // forward retiming vSteps = Abc_NtkUtilRetimingSplit( vLags, 1 ); // translate each set of steps into moves + printf( "The number of forward steps = %6d.\n", Vec_IntSize(vSteps) ); vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 1 ); + printf( "The number of forward moves = %6d.\n", Vec_PtrSize(vMoves) ); // implement this retiming Abc_NtkImplementRetimingForward( pNtk, vMoves ); Vec_IntFree( vSteps ); @@ -60,7 +64,9 @@ int Abc_NtkImplementRetiming( Abc_Ntk_t * pNtk, Vec_Str_t * vLags ) // backward retiming vSteps = Abc_NtkUtilRetimingSplit( vLags, 0 ); // translate each set of steps into moves + printf( "The number of backward steps = %6d.\n", Vec_IntSize(vSteps) ); vMoves = Abc_NtkUtilRetimingGetMoves( pNtk, vSteps, 0 ); + printf( "The number of backward moves = %6d.\n", Vec_PtrSize(vMoves) ); // implement this retiming RetValue = Abc_NtkImplementRetimingBackward( pNtk, vMoves ); Vec_IntFree( vSteps ); @@ -89,6 +95,58 @@ void Abc_NtkImplementRetimingForward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ) /**Function************************************************************* + Synopsis [Retimes node forward by one latch.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjRetimeForward( Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanout; + int Init0, Init1, Init, i; + assert( Abc_ObjFaninNum(pObj) == 2 ); + assert( Abc_ObjFaninL0(pObj) >= 1 ); + assert( Abc_ObjFaninL1(pObj) >= 1 ); + // remove the init values from the fanins + Init0 = Abc_ObjFaninLDeleteFirst( pObj, 0 ); + Init1 = Abc_ObjFaninLDeleteFirst( pObj, 1 ); + assert( Init0 != ABC_INIT_NONE ); + assert( Init1 != ABC_INIT_NONE ); + // take into account the complements in the node + if ( Abc_ObjFaninC0(pObj) ) + { + if ( Init0 == ABC_INIT_ZERO ) + Init0 = ABC_INIT_ONE; + else if ( Init0 == ABC_INIT_ONE ) + Init0 = ABC_INIT_ZERO; + } + if ( Abc_ObjFaninC1(pObj) ) + { + if ( Init1 == ABC_INIT_ZERO ) + Init1 = ABC_INIT_ONE; + else if ( Init1 == ABC_INIT_ONE ) + Init1 = ABC_INIT_ZERO; + } + // compute the value at the output of the node + if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO ) + Init = ABC_INIT_ZERO; + else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE ) + Init = ABC_INIT_ONE; + else + Init = ABC_INIT_DC; + // add the init values to the fanouts + Abc_ObjForEachFanout( pObj, pFanout, i ) + Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout), Init ); +} + + + +/**Function************************************************************* + Synopsis [Implements the given retiming on the sequential AIG.] Description [Returns 0 of initial state computation fails.] @@ -106,39 +164,50 @@ int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ) Vec_Int_t * vValues; Abc_Ntk_t * pNtkProb, * pNtkMiter, * pNtkCnf; Abc_Obj_t * pNode, * pNodeNew; - int * pModel, Init, nDigits, RetValue, i; + int * pModel, RetValue, i, clk; // return if the retiming is trivial if ( Vec_PtrSize(vMoves) == 0 ) return 1; - // start the table and the array of PO values - tTable = stmm_init_table( stmm_numcmp, stmm_numhash ); - vValues = Vec_IntAlloc( 100 ); - // create the network for the initial state computation + // start the table and the array of PO values pNtkProb = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP ); + tTable = stmm_init_table( stmm_numcmp, stmm_numhash ); + vValues = Vec_IntAlloc( 100 ); - // perform the backward moves and build the network + // perform the backward moves and build the network for initial state computation + RetValue = 0; Vec_PtrForEachEntry( vMoves, pNode, i ) - Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues ); + RetValue |= Abc_ObjRetimeBackward( pNode, pNtkProb, tTable, vValues ); // add the PIs corresponding to the white spots stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew ) Abc_ObjAddFanin( pNodeNew, Abc_NtkCreatePi(pNtkProb) ); // add the PI/PO names - nDigits = Extra_Base10Log( Abc_NtkPiNum(pNtkProb) ); - Abc_NtkForEachPi( pNtkProb, pNodeNew, i ) - Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("pi", i, nDigits) ); - nDigits = Extra_Base10Log( Abc_NtkPoNum(pNtkProb) ); - Abc_NtkForEachPo( pNtkProb, pNodeNew, i ) - Abc_NtkLogicStoreName( pNodeNew, Abc_ObjNameDummy("po", i, nDigits) ); + Abc_NtkAddDummyPiNames( pNtkProb ); + Abc_NtkAddDummyPoNames( pNtkProb ); // make sure everything is okay with the network structure if ( !Abc_NtkDoCheck( pNtkProb ) ) { printf( "Abc_NtkImplementRetimingBackward: The internal network check has failed.\n" ); + Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); + Abc_NtkDelete( pNtkProb ); + stmm_free_table( tTable ); + Vec_IntFree( vValues ); + return 0; + } + + // check if conflict is found + if ( RetValue ) + { + printf( "Abc_NtkImplementRetimingBackward: A top level conflict is detected. DC latch values are used.\n" ); + Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); + Abc_NtkDelete( pNtkProb ); + stmm_free_table( tTable ); + Vec_IntFree( vValues ); return 0; } @@ -147,31 +216,36 @@ int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ) Abc_NtkDelete( pNtkProb ); Vec_IntFree( vValues ); + printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) ); + // transform the miter into a logic network for efficient CNF construction pNtkCnf = Abc_NtkRenode( pNtkMiter, 0, 100, 1, 0, 0 ); Abc_NtkDelete( pNtkMiter ); // solve the miter +clk = clock(); RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 ); +if ( clock() - clk > 500 ) +{ +PRT( "SAT solving time", clock() - clk ); +} pModel = pNtkCnf->pModel; pNtkCnf->pModel = NULL; Abc_NtkDelete( pNtkCnf ); // analyze the result if ( RetValue == -1 || RetValue == 1 ) { + Abc_NtkRetimeSetInitialValues( pNtk, tTable, NULL ); + if ( RetValue == 1 ) + printf( "Abc_NtkImplementRetimingBackward: The problem is unsatisfiable. DC latch values are used.\n" ); + else + printf( "Abc_NtkImplementRetimingBackward: The SAT problem timed out. DC latch values are used.\n" ); stmm_free_table( tTable ); return 0; } // set the values of the latches - i = 0; - stmm_foreach_item( tTable, gen, (char **)&RetEdge, (char **)&pNodeNew ) - { - pNode = Abc_NtkObj( pNtk, RetEdge.iNode ); - Init = pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO; - Abc_ObjFaninLSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init ); - i++; - } + Abc_NtkRetimeSetInitialValues( pNtk, tTable, pModel ); stmm_free_table( tTable ); free( pModel ); return 1; @@ -179,59 +253,10 @@ int Abc_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves ) /**Function************************************************************* - Synopsis [Retimes node forward by one latch.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_ObjRetimeForward( Abc_Obj_t * pObj ) -{ - Abc_Obj_t * pFanout; - int Init0, Init1, Init, i; - assert( Abc_ObjFaninNum(pObj) == 2 ); - assert( Abc_ObjFaninL0(pObj) >= 1 ); - assert( Abc_ObjFaninL1(pObj) >= 1 ); - // remove the init values from the fanins - Init0 = Abc_ObjFaninLDeleteFirst( pObj, 0 ); - Init1 = Abc_ObjFaninLDeleteFirst( pObj, 1 ); - assert( Init0 != ABC_INIT_NONE ); - assert( Init1 != ABC_INIT_NONE ); - // take into account the complements in the node - if ( Abc_ObjFaninC0(pObj) ) - { - if ( Init0 == ABC_INIT_ZERO ) - Init0 = ABC_INIT_ONE; - else if ( Init0 == ABC_INIT_ONE ) - Init0 = ABC_INIT_ZERO; - } - if ( Abc_ObjFaninC1(pObj) ) - { - if ( Init1 == ABC_INIT_ZERO ) - Init1 = ABC_INIT_ONE; - else if ( Init1 == ABC_INIT_ONE ) - Init1 = ABC_INIT_ZERO; - } - // compute the value at the output of the node - if ( Init0 == ABC_INIT_ZERO || Init1 == ABC_INIT_ZERO ) - Init = ABC_INIT_ZERO; - else if ( Init0 == ABC_INIT_ONE && Init1 == ABC_INIT_ONE ) - Init = ABC_INIT_ONE; - else - Init = ABC_INIT_DC; - // add the init values to the fanouts - Abc_ObjForEachFanout( pObj, pFanout, i ) - Abc_ObjFaninLInsertLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout), Init ); -} - -/**Function************************************************************* - Synopsis [Retimes node backward by one latch.] - Description [Constructs the problem for initial state computation.] + Description [Constructs the problem for initial state computation. + Returns 1 if the conflict is found.] SideEffects [] @@ -242,15 +267,14 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t { Abc_Obj_t * pFanout; Abc_InitType_t Init, Value; - Abc_RetEdge_t Edge; - Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuf; - unsigned Entry; - int i, fMet0, fMet1, fMetX; + Abc_RetEdge_t RetEdge; + Abc_Obj_t * pNodeNew, * pFanoutNew, * pBuffer; + int i, Edge, fMet0, fMet1, fMetN; // make sure the node can be retimed assert( Abc_ObjFanoutLMin(pObj) > 0 ); // get the fanout values - fMet0 = fMet1 = fMetX = 0; + fMet0 = fMet1 = fMetN = 0; Abc_ObjForEachFanout( pObj, pFanout, i ) { Init = Abc_ObjFaninLGetInitLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) ); @@ -259,101 +283,159 @@ int Abc_ObjRetimeBackward( Abc_Obj_t * pObj, Abc_Ntk_t * pNtkNew, stmm_table * t else if ( Init == ABC_INIT_ONE ) fMet1 = 1; else if ( Init == ABC_INIT_NONE ) - fMetX = 1; + fMetN = 1; } - // quit if conflict is found - if ( fMet0 && fMet1 ) + + // consider the case when all fanout latchs have don't-care values + // the new values on the fanin edges will be don't-cares + if ( !fMet0 && !fMet1 && !fMetN ) + { + // update the fanout edges + Abc_ObjForEachFanout( pObj, pFanout, i ) + Abc_ObjFaninLDeleteLast( pFanout, Abc_ObjEdgeNum(pObj, pFanout) ); + // update the fanin edges + Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable ); + Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable ); + Abc_ObjFaninLInsertFirst( pObj, 0, ABC_INIT_DC ); + Abc_ObjFaninLInsertFirst( pObj, 1, ABC_INIT_DC ); return 0; + } + // the initial values on the fanout edges contain 0, 1, or unknown + // the new values on the fanin edges will be unknown - // get the new initial value - if ( !fMet0 && !fMet1 && !fMetX ) + // add new AND-gate to the network + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + + // add PO fanouts if any + if ( fMet0 ) { - Init = ABC_INIT_DC; - // do not add the node - pNodeNew = NULL; + Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew ); + Vec_IntPush( vValues, 0 ); } - else + if ( fMet1 ) { - Init = ABC_INIT_NONE; - // add the node to the network - pNodeNew = Abc_NtkCreateNode( pNtkNew ); - pNodeNew->pData = Abc_SopCreateAnd2( pNtkNew->pManFunc, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); + Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew ); + Vec_IntPush( vValues, 1 ); } // perform the changes Abc_ObjForEachFanout( pObj, pFanout, i ) { - Edge.iNode = pFanout->Id; - Edge.iEdge = Abc_ObjEdgeNum(pObj, pFanout); - Edge.iLatch = Abc_ObjFaninL( pFanout, Edge.iEdge ) - 1; - // try to delete this edge - stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ); - // delete the entry - Value = Abc_ObjFaninLDeleteLast( pFanout, Edge.iEdge ); - if ( Value == ABC_INIT_NONE ) - Abc_ObjAddFanin( pFanoutNew, pNodeNew ); - } - - // update the table for each of the edges - Abc_ObjFaninLForEachValue( pObj, 0, Entry, i, Value ) - { + Edge = Abc_ObjEdgeNum( pObj, pFanout ); + Value = Abc_ObjFaninLDeleteLast( pFanout, Edge ); if ( Value != ABC_INIT_NONE ) continue; - if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) ) - assert( 0 ); - Edge.iLatch++; - if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) ) + // value is unknown, remove it from the table + RetEdge.iNode = pFanout->Id; + RetEdge.iEdge = Edge; + RetEdge.iLatch = Abc_ObjFaninL( pFanout, Edge ); // after edge is removed + if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) ) assert( 0 ); + // create the fanout of the AND gate + Abc_ObjAddFanin( pFanoutNew, pNodeNew ); } - Abc_ObjFaninLForEachValue( pObj, 1, Entry, i, Value ) - { - if ( Value != ABC_INIT_NONE ) - continue; - if ( !stmm_delete( tTable, (char **)&Edge, (char **)&pFanoutNew ) ) - assert( 0 ); - Edge.iLatch++; - if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pFanoutNew ) ) - assert( 0 ); - } - Abc_ObjFaninLInsertFirst( pObj, 0, Init ); - Abc_ObjFaninLInsertFirst( pObj, 1, Init ); - // do not insert the don't-care node into the network - if ( Init == ABC_INIT_DC ) - return 1; + // update the fanin edges + Abc_ObjRetimeBackwardUpdateEdge( pObj, 0, tTable ); + Abc_ObjRetimeBackwardUpdateEdge( pObj, 1, tTable ); + Abc_ObjFaninLInsertFirst( pObj, 0, ABC_INIT_NONE ); + Abc_ObjFaninLInsertFirst( pObj, 1, ABC_INIT_NONE ); // add the buffer - pBuf = Abc_NtkCreateNode( pNtkNew ); - pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc ); - Abc_ObjAddFanin( pNodeNew, pBuf ); + pBuffer = Abc_NtkCreateNode( pNtkNew ); + pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc ); + Abc_ObjAddFanin( pNodeNew, pBuffer ); // point to it from the table - Edge.iNode = pObj->Id; - Edge.iEdge = 0; - Edge.iLatch = 0; - if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) ) + RetEdge.iNode = pObj->Id; + RetEdge.iEdge = 0; + RetEdge.iLatch = 0; + if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pBuffer ) ) assert( 0 ); // add the buffer - pBuf = Abc_NtkCreateNode( pNtkNew ); - pBuf->pData = Abc_SopCreateBuf( pNtkNew->pManFunc ); - Abc_ObjAddFanin( pNodeNew, pBuf ); + pBuffer = Abc_NtkCreateNode( pNtkNew ); + pBuffer->pData = Abc_SopCreateBuf( pNtkNew->pManFunc ); + Abc_ObjAddFanin( pNodeNew, pBuffer ); // point to it from the table - Edge.iNode = pObj->Id; - Edge.iEdge = 1; - Edge.iLatch = 0; - if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(Edge), (char *)pBuf ) ) + RetEdge.iNode = pObj->Id; + RetEdge.iEdge = 1; + RetEdge.iLatch = 0; + if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pBuffer ) ) assert( 0 ); - // check if the output value is required - if ( fMet0 || fMet1 ) + // report conflict is found + return fMet0 && fMet1; +} + +/**Function************************************************************* + + Synopsis [Generates the printable edge label with the initial state.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_ObjRetimeBackwardUpdateEdge( Abc_Obj_t * pObj, int Edge, stmm_table * tTable ) +{ + Abc_Obj_t * pFanoutNew; + Abc_RetEdge_t RetEdge; + Abc_InitType_t Init; + int nLatches, i; + + // get the number of latches on the edge + nLatches = Abc_ObjFaninL( pObj, Edge ); + assert( nLatches <= ABC_MAX_EDGE_LATCH ); + for ( i = nLatches - 1; i >= 0; i-- ) { - // add the PO and the value - Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew ); - Vec_IntPush( vValues, fMet1 ); + // get the value of this latch + Init = Abc_ObjFaninLGetInitOne( pObj, Edge, i ); + if ( Init != ABC_INIT_NONE ) + continue; + // get the retiming edge + RetEdge.iNode = pObj->Id; + RetEdge.iEdge = Edge; + RetEdge.iLatch = i; + // remove entry from table and add it with a different key + if ( !stmm_delete( tTable, (char **)&RetEdge, (char **)&pFanoutNew ) ) + assert( 0 ); + RetEdge.iLatch++; + if ( stmm_insert( tTable, (char *)Abc_RetEdge2Int(RetEdge), (char *)pFanoutNew ) ) + assert( 0 ); } - return 1; } +/**Function************************************************************* + + Synopsis [Sets the initial values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeSetInitialValues( Abc_Ntk_t * pNtk, stmm_table * tTable, int * pModel ) +{ + Abc_Obj_t * pNode; + stmm_generator * gen; + Abc_RetEdge_t RetEdge; + Abc_InitType_t Init; + int i; + + i = 0; + stmm_foreach_item( tTable, gen, (char **)&RetEdge, NULL ) + { + pNode = Abc_NtkObj( pNtk, RetEdge.iNode ); + Init = pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC; + Abc_ObjFaninLSetInitOne( pNode, RetEdge.iEdge, RetEdge.iLatch, Init ); + i++; + } +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// |