src/opt/ret/retInt.h File Reference

#include "abc.h"
Include dependency graph for retInt.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

int Abc_NtkRetimeMinArea (Abc_Ntk_t *pNtk, int fForwardOnly, int fBackwardOnly, int fVerbose)
int Abc_NtkRetime (Abc_Ntk_t *pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fOneStep, int fVerbose)
int Abc_NtkRetimeMinDelay (Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkCopy, int nIterLimit, int fForward, int fVerbose)
int Abc_NtkRetimeIncremental (Abc_Ntk_t *pNtk, int fForward, int fMinDelay, int fOneStep, int fVerbose)
void Abc_NtkRetimeShareLatches (Abc_Ntk_t *pNtk, int fInitial)
int Abc_NtkRetimeNodeIsEnabled (Abc_Obj_t *pObj, int fForward)
void Abc_NtkRetimeNode (Abc_Obj_t *pObj, int fForward, int fInitial)
st_table * Abc_NtkRetimePrepareLatches (Abc_Ntk_t *pNtk)
int Abc_NtkRetimeFinalizeLatches (Abc_Ntk_t *pNtk, st_table *tLatches, int nIdMaxStart)
void Abc_NtkMaxFlowTest (Abc_Ntk_t *pNtk)
Vec_Ptr_t * Abc_NtkMaxFlow (Abc_Ntk_t *pNtk, int fForward, int fVerbose)
Vec_Int_t * Abc_NtkRetimeInitialValues (Abc_Ntk_t *pNtkSat, Vec_Int_t *vValues, int fVerbose)
int Abc_ObjSopSimulate (Abc_Obj_t *pObj)
void Abc_NtkRetimeTranferToCopy (Abc_Ntk_t *pNtk)
void Abc_NtkRetimeTranferFromCopy (Abc_Ntk_t *pNtk)
Vec_Int_t * Abc_NtkRetimeCollectLatchValues (Abc_Ntk_t *pNtk)
void Abc_NtkRetimeInsertLatchValues (Abc_Ntk_t *pNtk, Vec_Int_t *vValues)
Abc_Ntk_t * Abc_NtkRetimeBackwardInitialStart (Abc_Ntk_t *pNtk)
void Abc_NtkRetimeBackwardInitialFinish (Abc_Ntk_t *pNtk, Abc_Ntk_t *pNtkNew, Vec_Int_t *vValuesOld, int fVerbose)
int Abc_NtkRetimeLValue (Abc_Ntk_t *pNtk, int nIterLimit, int fVerbose)

Function Documentation

Vec_Ptr_t* Abc_NtkMaxFlow ( Abc_Ntk_t *  pNtk,
int  fForward,
int  fVerbose 
)

Function*************************************************************

Synopsis [Implementation of max-flow/min-cut computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file retFlow.c.

00141 {
00142     Vec_Ptr_t * vMinCut;
00143     Abc_Obj_t * pLatch;
00144     int Flow, FlowCur, RetValue, i;
00145     int clk = clock();
00146     int fUseDirectedFlow = 1;
00147 
00148     // find the max-flow
00149     Abc_NtkCleanCopy( pNtk );
00150     Flow = 0;
00151     Abc_NtkIncrementTravId(pNtk);
00152     Abc_NtkForEachLatch( pNtk, pLatch, i )
00153     {
00154         if ( fForward )
00155         {
00156 //            assert( !Abc_ObjFanout0(pLatch)->fMarkA );
00157             FlowCur  = Abc_NtkMaxFlowFwdPath2_rec( Abc_ObjFanout0(pLatch) );
00158 //            FlowCur  = Abc_NtkMaxFlowFwdPath3_rec( Abc_ObjFanout0(pLatch), pLatch, 1 );
00159             Flow    += FlowCur;
00160         }
00161         else
00162         {
00163             assert( !Abc_ObjFanin0(pLatch)->fMarkA );
00164             FlowCur  = Abc_NtkMaxFlowBwdPath2_rec( Abc_ObjFanin0(pLatch) );
00165             Flow    += FlowCur;
00166         }
00167         if ( FlowCur )
00168             Abc_NtkIncrementTravId(pNtk);
00169     }
00170 
00171     if ( !fUseDirectedFlow )
00172     {
00173         Abc_NtkIncrementTravId(pNtk);
00174         Abc_NtkForEachLatch( pNtk, pLatch, i )
00175         {
00176             if ( fForward )
00177             {
00178     //            assert( !Abc_ObjFanout0(pLatch)->fMarkA );
00179                 FlowCur  = Abc_NtkMaxFlowFwdPath_rec( Abc_ObjFanout0(pLatch) );
00180                 Flow    += FlowCur;
00181             }
00182             else
00183             {
00184                 assert( !Abc_ObjFanin0(pLatch)->fMarkA );
00185                 FlowCur  = Abc_NtkMaxFlowBwdPath_rec( Abc_ObjFanin0(pLatch) );
00186                 Flow    += FlowCur;
00187             }
00188             if ( FlowCur )
00189                 Abc_NtkIncrementTravId(pNtk);
00190         }
00191     }
00192 //    Abc_NtkMaxFlowPrintFlow( pNtk, fForward );
00193 
00194     // mark the nodes reachable from the latches
00195     Abc_NtkIncrementTravId(pNtk);
00196     Abc_NtkForEachLatch( pNtk, pLatch, i )
00197     {
00198         if ( fForward )
00199         {
00200 //            assert( !Abc_ObjFanout0(pLatch)->fMarkA );
00201             if ( fUseDirectedFlow )
00202                 RetValue = Abc_NtkMaxFlowFwdPath2_rec( Abc_ObjFanout0(pLatch) );
00203 //                RetValue = Abc_NtkMaxFlowFwdPath3_rec( Abc_ObjFanout0(pLatch), pLatch, 1 );
00204             else
00205                 RetValue = Abc_NtkMaxFlowFwdPath_rec( Abc_ObjFanout0(pLatch) );
00206         }
00207         else
00208         {
00209             assert( !Abc_ObjFanin0(pLatch)->fMarkA );
00210             if ( fUseDirectedFlow )
00211                 RetValue = Abc_NtkMaxFlowBwdPath2_rec( Abc_ObjFanin0(pLatch) );
00212             else
00213                 RetValue = Abc_NtkMaxFlowBwdPath_rec( Abc_ObjFanin0(pLatch) );
00214         }
00215         assert( RetValue == 0 );
00216     }
00217 
00218     // find the min-cut with the smallest volume
00219     vMinCut = Abc_NtkMaxFlowMinCut( pNtk, fForward );
00220     // verify the cut
00221     if ( !Abc_NtkMaxFlowVerifyCut(pNtk, vMinCut, fForward) )
00222         printf( "Abc_NtkMaxFlow() error! The computed min-cut is not a cut!\n" );
00223     // make the cut retimable
00224     Abc_NtkMaxFlowMinCutUpdate( pNtk, vMinCut, fForward );
00225 
00226     // report the results
00227     if ( fVerbose )
00228     {
00229     printf( "L = %6d. %s max-flow = %6d.  Min-cut = %6d.  ", 
00230         Abc_NtkLatchNum(pNtk), fForward? "Forward " : "Backward", Flow, Vec_PtrSize(vMinCut) );
00231 PRT( "Time", clock() - clk );
00232     }
00233 
00234 //    Abc_NtkMaxFlowPrintCut( pNtk, vMinCut );
00235     return vMinCut;
00236 }

void Abc_NtkMaxFlowTest ( Abc_Ntk_t *  pNtk  ) 

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Test-bench for the max-flow computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 101 of file retFlow.c.

00102 {
00103     Vec_Ptr_t * vMinCut;
00104     Abc_Obj_t * pObj;
00105     int i;
00106 
00107     // forward flow
00108     Abc_NtkForEachPo( pNtk, pObj, i )
00109         pObj->fMarkA = 1;
00110     Abc_NtkForEachLatch( pNtk, pObj, i )
00111         pObj->fMarkA = Abc_ObjFanin0(pObj)->fMarkA = 1;
00112 //        Abc_ObjFanin0(pObj)->fMarkA = 1;
00113     vMinCut = Abc_NtkMaxFlow( pNtk, 1, 1 );
00114     Vec_PtrFree( vMinCut );
00115     Abc_NtkCleanMarkA( pNtk );
00116 
00117     // backward flow
00118     Abc_NtkForEachPi( pNtk, pObj, i )
00119         pObj->fMarkA = 1;
00120     Abc_NtkForEachLatch( pNtk, pObj, i )
00121         pObj->fMarkA = Abc_ObjFanout0(pObj)->fMarkA = 1;
00122 //        Abc_ObjFanout0(pObj)->fMarkA = 1;
00123     vMinCut = Abc_NtkMaxFlow( pNtk, 0, 1 );
00124     Vec_PtrFree( vMinCut );
00125     Abc_NtkCleanMarkA( pNtk );
00126 
00127 }

int Abc_NtkRetime ( Abc_Ntk_t *  pNtk,
int  Mode,
int  fForwardOnly,
int  fBackwardOnly,
int  fOneStep,
int  fVerbose 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Implementation of retiming.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file retCore.c.

00045 {
00046     int nLatches = Abc_NtkLatchNum(pNtk);
00047     int nLevels  = Abc_NtkLevel(pNtk);
00048     int RetValue = 0, clkTotal = clock();
00049     int nNodesOld, nLatchesOld;
00050     assert( Mode > 0 && Mode < 7 );
00051     assert( !fForwardOnly || !fBackwardOnly );
00052 
00053     // cleanup the network
00054     nNodesOld   = Abc_NtkNodeNum(pNtk);
00055     nLatchesOld = Abc_NtkLatchNum(pNtk);
00056     Abc_NtkCleanupSeq(pNtk, 0, 0, 0);
00057     if ( nNodesOld > Abc_NtkNodeNum(pNtk) || nLatchesOld > Abc_NtkLatchNum(pNtk) )
00058         printf( "Cleanup before retiming removed %d dangling nodes and %d dangling latches.\n",
00059             nNodesOld - Abc_NtkNodeNum(pNtk), nLatchesOld - Abc_NtkLatchNum(pNtk) );
00060 
00061     // perform retiming
00062     switch ( Mode )
00063     {
00064     case 1: // forward 
00065         RetValue = Abc_NtkRetimeIncremental( pNtk, 1, 0, 0, fVerbose );
00066         break;
00067     case 2: // backward 
00068         RetValue = Abc_NtkRetimeIncremental( pNtk, 0, 0, 0, fVerbose );
00069         break;
00070     case 3: // min-area 
00071         RetValue = Abc_NtkRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose );
00072         break;
00073     case 4: // min-delay
00074         if ( !fBackwardOnly )
00075             RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fOneStep, fVerbose );
00076         if ( !fForwardOnly )
00077             RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fOneStep, fVerbose );
00078         break;
00079     case 5: // min-area + min-delay
00080         RetValue  = Abc_NtkRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose );
00081         if ( !fBackwardOnly )
00082             RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, 0, fVerbose );
00083         if ( !fForwardOnly )
00084             RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, 0, fVerbose );
00085         break;
00086     case 6: // Pan's algorithm
00087         RetValue = Abc_NtkRetimeLValue( pNtk, 500, fVerbose );
00088         break;
00089     default:
00090         printf( "Unknown retiming option.\n" );
00091         break;
00092     }
00093     if ( fVerbose )
00094     {
00095         printf( "Reduction in area = %3d. Reduction in delay = %3d. ", 
00096             nLatches - Abc_NtkLatchNum(pNtk), nLevels - Abc_NtkLevel(pNtk) );
00097         PRT( "Total runtime", clock() - clkTotal );
00098     }
00099     timeRetime = clock() - clkTotal;
00100     return RetValue;
00101 }

void Abc_NtkRetimeBackwardInitialFinish ( Abc_Ntk_t *  pNtk,
Abc_Ntk_t *  pNtkNew,
Vec_Int_t *  vValuesOld,
int  fVerbose 
)

Function*************************************************************

Synopsis [Transfer latch initial values to pCopy.]

Description []

SideEffects []

SeeAlso []

Definition at line 275 of file retInit.c.

00276 {
00277     Vec_Int_t * vValuesNew;
00278     Abc_Obj_t * pObj;
00279     int i;
00280     // create PIs corresponding to the initial values
00281     Abc_NtkForEachObj( pNtk, pObj, i )
00282         if ( Abc_ObjIsLatch(pObj) )
00283             Abc_ObjAddFanin( pObj->pCopy, Abc_NtkCreatePi(pNtkNew) );
00284     // assign dummy node names
00285     Abc_NtkAddDummyPiNames( pNtkNew );
00286     Abc_NtkAddDummyPoNames( pNtkNew );
00287     // check the network
00288     if ( !Abc_NtkCheck( pNtkNew ) )
00289         fprintf( stdout, "Abc_NtkRetimeBackwardInitialFinish(): Network check has failed.\n" );
00290     // derive new initial values
00291     vValuesNew = Abc_NtkRetimeInitialValues( pNtkNew, vValuesOld, fVerbose );
00292     // insert new initial values
00293     Abc_NtkRetimeInsertLatchValues( pNtk, vValuesNew );
00294     if ( vValuesNew ) Vec_IntFree( vValuesNew );
00295 }

Abc_Ntk_t* Abc_NtkRetimeBackwardInitialStart ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Transfer latch initial values to pCopy.]

Description []

SideEffects []

SeeAlso []

Definition at line 250 of file retInit.c.

00251 {
00252     Abc_Ntk_t * pNtkNew;
00253     Abc_Obj_t * pObj;
00254     int i;
00255     // create the network used for the initial state computation
00256     pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
00257     // create POs corresponding to the initial values
00258     Abc_NtkForEachObj( pNtk, pObj, i )
00259         if ( Abc_ObjIsLatch(pObj) )
00260             pObj->pCopy = Abc_NtkCreatePo(pNtkNew);
00261     return pNtkNew;
00262 }

Vec_Int_t* Abc_NtkRetimeCollectLatchValues ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Transfer latch initial values to pCopy.]

Description []

SideEffects []

SeeAlso []

Definition at line 204 of file retInit.c.

00205 {
00206     Vec_Int_t * vValues;
00207     Abc_Obj_t * pObj;
00208     int i;
00209     vValues = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
00210     Abc_NtkForEachObj( pNtk, pObj, i )
00211         if ( Abc_ObjIsLatch(pObj) )
00212             Vec_IntPush( vValues, Abc_LatchIsInit1(pObj) );
00213     return vValues;
00214 }

int Abc_NtkRetimeFinalizeLatches ( Abc_Ntk_t *  pNtk,
st_table *  tLatches,
int  nIdMaxStart 
)

Function*************************************************************

Synopsis [Finalizes the latches after retiming.]

Description [Reuses the LIs/LOs for old latches.]

SideEffects []

SeeAlso []

Definition at line 142 of file retIncrem.c.

00143 {
00144     Vec_Ptr_t * vCisOld, * vCosOld, * vBoxesOld, * vCisNew, * vCosNew, * vBoxesNew;
00145     Abc_Obj_t * pObj, * pLatch, * pLatchIn, * pLatchOut;
00146     int i, Index;
00147     // create new arrays
00148     vCisOld   = pNtk->vCis;    pNtk->vCis   = NULL;  vCisNew   = Vec_PtrAlloc( 100 );
00149     vCosOld   = pNtk->vCos;    pNtk->vCos   = NULL;  vCosNew   = Vec_PtrAlloc( 100 );  
00150     vBoxesOld = pNtk->vBoxes;  pNtk->vBoxes = NULL;  vBoxesNew = Vec_PtrAlloc( 100 );
00151     // copy boxes and their CIs/COs
00152     Vec_PtrForEachEntryStop( vCisOld, pObj, i, Vec_PtrSize(vCisOld) - st_count(tLatches) )
00153         Vec_PtrPush( vCisNew, pObj );
00154     Vec_PtrForEachEntryStop( vCosOld, pObj, i, Vec_PtrSize(vCosOld) - st_count(tLatches) )
00155         Vec_PtrPush( vCosNew, pObj );
00156     Vec_PtrForEachEntryStop( vBoxesOld, pObj, i, Vec_PtrSize(vBoxesOld) - st_count(tLatches) )
00157         Vec_PtrPush( vBoxesNew, pObj );
00158     // go through the latches
00159     Abc_NtkForEachObj( pNtk, pLatch, i )
00160     {
00161         if ( !Abc_ObjIsLatch(pLatch) )
00162             continue;
00163         if ( Abc_ObjId(pLatch) >= (unsigned)nIdMaxStart )
00164         {
00165             // this is a new latch 
00166             pLatchIn  = Abc_NtkCreateBi(pNtk);
00167             pLatchOut = Abc_NtkCreateBo(pNtk);
00168             Abc_ObjAssignName( pLatchOut, Abc_ObjName(pLatch), "_out" );
00169             Abc_ObjAssignName( pLatchIn,  Abc_ObjName(pLatch), "_in" );
00170         }
00171         else
00172         {
00173             // this is an old latch 
00174             // get its number in the original order
00175             if ( !st_lookup( tLatches, (char *)pLatch, (char **)&Index ) )
00176             {
00177                 printf( "Abc_NtkRetimeFinalizeLatches(): Internal error.\n" );
00178                 return 0;
00179             }
00180             assert( pLatch == Vec_PtrEntry(vBoxesOld, Vec_PtrSize(vBoxesOld) - st_count(tLatches) + Index) );
00181             // reconnect with the old LIs/LOs
00182             pLatchIn  = Vec_PtrEntry( vCosOld, Vec_PtrSize(vCosOld) - st_count(tLatches) + Index );
00183             pLatchOut = Vec_PtrEntry( vCisOld, Vec_PtrSize(vCisOld) - st_count(tLatches) + Index );
00184         }
00185         // connect
00186         Abc_ObjAddFanin( pLatchIn, Abc_ObjFanin0(pLatch) );
00187         Abc_ObjPatchFanin( pLatch, Abc_ObjFanin0(pLatch), pLatchIn );
00188         if ( Abc_ObjFanoutNum(pLatch) > 0 )
00189             Abc_ObjTransferFanout( pLatch, pLatchOut );
00190         Abc_ObjAddFanin( pLatchOut, pLatch );
00191         // add to the arrays
00192         Vec_PtrPush( vCisNew, pLatchOut );
00193         Vec_PtrPush( vCosNew, pLatchIn );
00194         Vec_PtrPush( vBoxesNew, pLatch );
00195     }
00196     // free useless Cis/Cos
00197     Vec_PtrForEachEntry( vCisOld, pObj, i )
00198         if ( !Abc_ObjIsPi(pObj) && Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
00199             Abc_NtkDeleteObj(pObj);
00200     Vec_PtrForEachEntry( vCosOld, pObj, i )
00201         if ( !Abc_ObjIsPo(pObj) && Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 )
00202             Abc_NtkDeleteObj(pObj);
00203     // set the new arrays
00204     pNtk->vCis   = vCisNew;   Vec_PtrFree( vCisOld );
00205     pNtk->vCos   = vCosNew;   Vec_PtrFree( vCosOld );
00206     pNtk->vBoxes = vBoxesNew; Vec_PtrFree( vBoxesOld );
00207     return 1;
00208 }

int Abc_NtkRetimeIncremental ( Abc_Ntk_t *  pNtk,
int  fForward,
int  fMinDelay,
int  fOneStep,
int  fVerbose 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Performs retiming in one direction.]

Description [Currently does not retime over black boxes.]

SideEffects []

SeeAlso []

Definition at line 44 of file retIncrem.c.

00045 {
00046     Abc_Ntk_t * pNtkCopy = NULL;
00047     Vec_Ptr_t * vBoxes;
00048     st_table * tLatches;
00049     int nLatches = Abc_NtkLatchNum(pNtk);
00050     int nIdMaxStart = Abc_NtkObjNumMax(pNtk);
00051     int RetValue, nIterLimit;
00052     if ( Abc_NtkNodeNum(pNtk) == 0 )
00053         return 0;
00054     // reorder CI/CO/latch inputs
00055     Abc_NtkOrderCisCos( pNtk );
00056     if ( fMinDelay ) 
00057     {
00058         nIterLimit = fOneStep? 1 : 2 * Abc_NtkLevel(pNtk);
00059         pNtkCopy = Abc_NtkDup( pNtk );
00060         tLatches = Abc_NtkRetimePrepareLatches( pNtkCopy );
00061         st_free_table( tLatches );
00062     }
00063     // collect latches and remove CIs/COs
00064     tLatches = Abc_NtkRetimePrepareLatches( pNtk );
00065     // share the latches
00066     Abc_NtkRetimeShareLatches( pNtk, 0 );    
00067     // save boxes
00068     vBoxes = pNtk->vBoxes;  pNtk->vBoxes = NULL;
00069     // perform the retiming
00070     if ( fMinDelay )
00071         Abc_NtkRetimeMinDelay( pNtk, pNtkCopy, nIterLimit, fForward, fVerbose );
00072     else
00073         Abc_NtkRetimeOneWay( pNtk, fForward, fVerbose );
00074     if ( fMinDelay ) 
00075         Abc_NtkDelete( pNtkCopy );
00076     // share the latches
00077     Abc_NtkRetimeShareLatches( pNtk, 0 );    
00078     // restore boxes
00079     pNtk->vBoxes = vBoxes;
00080     // finalize the latches
00081     RetValue = Abc_NtkRetimeFinalizeLatches( pNtk, tLatches, nIdMaxStart );
00082     st_free_table( tLatches );
00083     if ( RetValue == 0 )
00084         return 0;
00085     // fix the COs
00086 //    Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
00087     // check for correctness
00088     if ( !Abc_NtkCheck( pNtk ) )
00089         fprintf( stdout, "Abc_NtkRetimeForward(): Network check has failed.\n" );
00090     // return the number of latches saved
00091     return nLatches - Abc_NtkLatchNum(pNtk);
00092 }

Vec_Int_t* Abc_NtkRetimeInitialValues ( Abc_Ntk_t *  pNtkCone,
Vec_Int_t *  vValues,
int  fVerbose 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Computes initial values of the new latches.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file retInit.c.

00045 {
00046     Vec_Int_t * vSolution;
00047     Abc_Ntk_t * pNtkMiter, * pNtkLogic;
00048     int RetValue, clk;
00049     if ( pNtkCone == NULL )
00050         return Vec_IntDup( vValues );
00051     // convert the target network to AIG
00052     pNtkLogic = Abc_NtkDup( pNtkCone );
00053     Abc_NtkToAig( pNtkLogic );
00054     // get the miter
00055     pNtkMiter = Abc_NtkCreateTarget( pNtkLogic, pNtkLogic->vCos, vValues );
00056     if ( fVerbose )
00057         printf( "The miter for initial state computation has %d AIG nodes. ", Abc_NtkNodeNum(pNtkMiter) );
00058     // solve the miter
00059     clk = clock();
00060     RetValue = Abc_NtkMiterSat( pNtkMiter, (sint64)500000, (sint64)50000000, 0, NULL, NULL );
00061     if ( fVerbose ) 
00062         { PRT( "SAT solving time", clock() - clk ); }
00063     // analyze the result
00064     if ( RetValue == 1 )
00065         printf( "Abc_NtkRetimeInitialValues(): The problem is unsatisfiable. DC latch values are used.\n" );
00066     else if ( RetValue == -1 )
00067         printf( "Abc_NtkRetimeInitialValues(): The SAT problem timed out. DC latch values are used.\n" );
00068     else if ( !Abc_NtkRetimeVerifyModel( pNtkCone, vValues, pNtkMiter->pModel ) )
00069         printf( "Abc_NtkRetimeInitialValues(): The computed counter-example is incorrect.\n" );
00070     // set the values of the latches
00071     vSolution = RetValue? NULL : Vec_IntAllocArray( pNtkMiter->pModel, Abc_NtkPiNum(pNtkLogic) );
00072     pNtkMiter->pModel = NULL;
00073     Abc_NtkDelete( pNtkMiter );
00074     Abc_NtkDelete( pNtkLogic );
00075     return vSolution;
00076 }

void Abc_NtkRetimeInsertLatchValues ( Abc_Ntk_t *  pNtk,
Vec_Int_t *  vValues 
)

Function*************************************************************

Synopsis [Transfer latch initial values from pCopy.]

Description []

SideEffects []

SeeAlso []

Definition at line 227 of file retInit.c.

00228 {
00229     Abc_Obj_t * pObj;
00230     int i, Counter = 0;
00231     Abc_NtkForEachObj( pNtk, pObj, i )
00232         if ( Abc_ObjIsLatch(pObj) )
00233             pObj->pCopy = (void *)Counter++;
00234     Abc_NtkForEachObj( pNtk, pObj, i )
00235         if ( Abc_ObjIsLatch(pObj) )
00236             pObj->pData = (void *)(vValues? (Vec_IntEntry(vValues,(int)pObj->pCopy)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
00237 }

int Abc_NtkRetimeLValue ( Abc_Ntk_t *  pNtk,
int  nIterLimit,
int  fVerbose 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Implements Pan's retiming algorithm.]

Description []

SideEffects []

SeeAlso []

Definition at line 58 of file retLvalue.c.

00059 {
00060     Vec_Int_t * vLags;
00061     int nLatches = Abc_NtkLatchNum(pNtk);
00062     assert( Abc_NtkIsLogic( pNtk ) );
00063     // get the lags
00064     vLags = Abc_NtkRetimeGetLags( pNtk, nIterLimit, fVerbose );
00065     // compute the retiming
00066 //    Abc_NtkRetimeUsingLags( pNtk, vLags, fVerbose );
00067     Vec_IntFree( vLags );
00068     // fix the COs
00069 //    Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
00070     // check for correctness
00071     if ( !Abc_NtkCheck( pNtk ) )
00072         fprintf( stdout, "Abc_NtkRetimeLValue(): Network check has failed.\n" );
00073     // return the number of latches saved
00074     return nLatches - Abc_NtkLatchNum(pNtk);
00075 }

int Abc_NtkRetimeMinArea ( Abc_Ntk_t *  pNtk,
int  fForwardOnly,
int  fBackwardOnly,
int  fVerbose 
)

CFile****************************************************************

FileName [retInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Retiming package.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Oct 31, 2006.]

Revision [

Id
retInt.h,v 1.00 2006/10/31 00:00:00 alanmi Exp

] INCLUDES /// PARAMETERS /// STRUCTURE DEFINITIONS /// MACRO DEFINITIONS /// FUNCTION DECLARATIONS ///

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Performs min-area retiming.]

Description [Returns the number of latches reduced.]

SideEffects []

SeeAlso []

Definition at line 50 of file retArea.c.

00051 {
00052     Abc_Ntk_t * pNtkTotal = NULL, * pNtkBottom;
00053     Vec_Int_t * vValuesNew = NULL, * vValues;
00054     int nLatches = Abc_NtkLatchNum(pNtk);
00055     int fOneFrame = 0;
00056     assert( !fForwardOnly || !fBackwardOnly );
00057     // there should not be black boxes
00058     assert( Abc_NtkIsSopLogic(pNtk) );
00059     assert( Abc_NtkLatchNum(pNtk) == Vec_PtrSize(pNtk->vBoxes) );
00060     // reorder CI/CO/latch inputs
00061     Abc_NtkOrderCisCos( pNtk );
00062     // perform forward retiming
00063     if ( !fBackwardOnly )
00064     {
00065         if ( fOneFrame )
00066             Abc_NtkRetimeMinAreaOne( pNtk, 1, fVerbose );
00067         else
00068             while ( Abc_NtkRetimeMinAreaOne( pNtk, 1, fVerbose ) );
00069     }
00070     // remember initial values
00071     vValues = Abc_NtkCollectLatchValues( pNtk );
00072     // perform backward retiming
00073     if ( !fForwardOnly )
00074     {
00075         if ( fOneFrame )
00076             pNtkTotal = Abc_NtkRetimeMinAreaOne( pNtk, 0, fVerbose );
00077         else
00078             while ( pNtkBottom = Abc_NtkRetimeMinAreaOne( pNtk, 0, fVerbose ) )
00079                 pNtkTotal = Abc_NtkAttachBottom( pNtkTotal, pNtkBottom );  
00080     }
00081     // compute initial values
00082     vValuesNew = Abc_NtkRetimeInitialValues( pNtkTotal, vValues, fVerbose );
00083     if ( pNtkTotal ) Abc_NtkDelete( pNtkTotal );
00084     // insert new initial values
00085     Abc_NtkInsertLatchValues( pNtk, vValuesNew );
00086     if ( vValuesNew ) Vec_IntFree( vValuesNew );
00087     if ( vValues )    Vec_IntFree( vValues );
00088     // fix the COs (this changes the circuit structure)
00089 //    Abc_NtkLogicMakeSimpleCos( pNtk, 0 );
00090     // check for correctness
00091     if ( !Abc_NtkCheck( pNtk ) )
00092         fprintf( stdout, "Abc_NtkRetimeMinArea(): Network check has failed.\n" );
00093     // return the number of latches saved
00094     return nLatches - Abc_NtkLatchNum(pNtk);
00095 }

int Abc_NtkRetimeMinDelay ( Abc_Ntk_t *  pNtk,
Abc_Ntk_t *  pNtkCopy,
int  nIterLimit,
int  fForward,
int  fVerbose 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Retimes incrementally for minimum delay.]

Description [This procedure cannot be called in the application code because it assumes that the network is preprocessed by removing LIs/LOs.]

SideEffects []

SeeAlso []

Definition at line 47 of file retDelay.c.

00048 {
00049     int IterBest, DelayBest;
00050     int IterBest2, DelayBest2;
00051     // try to find the best delay iteration on a copy
00052     DelayBest = Abc_NtkRetimeMinDelayTry( pNtkCopy, fForward, 0, nIterLimit, &IterBest, fVerbose );
00053     if ( IterBest == 0 )
00054         return 1;
00055     // perform the given number of iterations on the original network
00056     DelayBest2 = Abc_NtkRetimeMinDelayTry( pNtk, fForward, 1, IterBest, &IterBest2, fVerbose );
00057     assert( DelayBest == DelayBest2 );
00058     assert( IterBest == IterBest2 );
00059     return 1;
00060 }

void Abc_NtkRetimeNode ( Abc_Obj_t *  pObj,
int  fForward,
int  fInitial 
)

Function*************************************************************

Synopsis [Retimes the node backward or forward.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file retIncrem.c.

00312 {
00313     Abc_Ntk_t * pNtkNew = NULL;
00314     Vec_Ptr_t * vNodes;
00315     Abc_Obj_t * pNext, * pLatch;
00316     int i;
00317     vNodes = Vec_PtrAlloc( 10 );
00318     if ( fForward )
00319     {
00320         // compute the initial value
00321         if ( fInitial )
00322             pObj->pCopy = (void *)Abc_ObjSopSimulate( pObj );
00323         // collect fanins
00324         Abc_NodeCollectFanins( pObj, vNodes );
00325         // make the node point to the fanins fanins
00326         Vec_PtrForEachEntry( vNodes, pNext, i )
00327         {
00328             assert( Abc_ObjIsLatch(pNext) );
00329             Abc_ObjPatchFanin( pObj, pNext, Abc_ObjFanin0(pNext) );
00330             if ( Abc_ObjFanoutNum(pNext) == 0 )
00331                 Abc_NtkDeleteObj(pNext);            
00332         }
00333         // add a new latch on top
00334         pNext = Abc_NtkCreateLatch(pObj->pNtk);
00335         if ( Abc_ObjFanoutNum(pObj) > 0 )
00336             Abc_ObjTransferFanout( pObj, pNext );
00337         Abc_ObjAddFanin( pNext, pObj );
00338         // set the initial value
00339         if ( fInitial )
00340             pNext->pCopy = pObj->pCopy;
00341     }
00342     else
00343     {
00344         // compute the initial value
00345         if ( fInitial )
00346         {
00347             pNtkNew = Abc_ObjFanout0(pObj)->pCopy->pNtk;
00348             Abc_NtkDupObj( pNtkNew, pObj, 0 );
00349             Abc_ObjForEachFanout( pObj, pNext, i )
00350             {
00351                 assert( Abc_ObjFaninNum(pNext->pCopy) == 0 );
00352                 Abc_ObjAddFanin( pNext->pCopy, pObj->pCopy );
00353             }
00354         }
00355         // collect fanouts
00356         Abc_NodeCollectFanouts( pObj, vNodes );
00357         // make the fanouts fanouts point to the node
00358         Vec_PtrForEachEntry( vNodes, pNext, i )
00359         {
00360             assert( Abc_ObjIsLatch(pNext) );
00361             Abc_ObjTransferFanout( pNext, pObj );
00362             Abc_NtkDeleteObj( pNext );  
00363         }
00364         // add new latches to the fanins
00365         Abc_ObjForEachFanin( pObj, pNext, i )
00366         {
00367             pLatch = Abc_NtkCreateLatch(pObj->pNtk);
00368             Abc_ObjPatchFanin( pObj, pNext, pLatch );
00369             Abc_ObjAddFanin( pLatch, pNext );
00370             // create buffer isomorphic to this latch
00371             if ( fInitial )
00372             {
00373                 pLatch->pCopy = Abc_NtkCreateNodeBuf( pNtkNew, NULL );
00374                 Abc_ObjAddFanin( pObj->pCopy, pLatch->pCopy );
00375             }
00376         }
00377     }
00378     Vec_PtrFree( vNodes );
00379 }

int Abc_NtkRetimeNodeIsEnabled ( Abc_Obj_t *  pObj,
int  fForward 
)

Function*************************************************************

Synopsis [Returns 1 if retiming forward/backward is possible.]

Description []

SideEffects []

SeeAlso []

Definition at line 280 of file retIncrem.c.

00281 {
00282     Abc_Obj_t * pNext;
00283     int i;
00284     assert( Abc_ObjIsNode(pObj) );
00285     if ( fForward )
00286     {
00287         Abc_ObjForEachFanin( pObj, pNext, i )
00288             if ( !Abc_ObjIsLatch(pNext) )
00289                 return 0;
00290     }
00291     else
00292     {
00293         Abc_ObjForEachFanout( pObj, pNext, i )
00294             if ( !Abc_ObjIsLatch(pNext) )
00295                 return 0;
00296     }
00297     return 1;
00298 }

st_table* Abc_NtkRetimePrepareLatches ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Prepares the network for retiming.]

Description [Hash latches into their number in the original network.]

SideEffects []

SeeAlso []

Definition at line 105 of file retIncrem.c.

00106 {
00107     st_table * tLatches;
00108     Abc_Obj_t * pLatch, * pLatchIn, * pLatchOut, * pFanin;
00109     int i, nOffSet = Abc_NtkBoxNum(pNtk) - Abc_NtkLatchNum(pNtk);
00110     // collect latches and remove CIs/COs
00111     tLatches = st_init_table( st_ptrcmp, st_ptrhash );
00112     Abc_NtkForEachLatch( pNtk, pLatch, i )
00113     {
00114         // map latch into its true number
00115         st_insert( tLatches, (void *)pLatch, (void *)(i-nOffSet) );
00116         // disconnect LI     
00117         pLatchIn = Abc_ObjFanin0(pLatch);
00118         pFanin = Abc_ObjFanin0(pLatchIn);
00119         Abc_ObjTransferFanout( pLatchIn, pFanin );
00120         Abc_ObjDeleteFanin( pLatchIn, pFanin );
00121         // disconnect LO     
00122         pLatchOut = Abc_ObjFanout0(pLatch);
00123         pFanin = Abc_ObjFanin0(pLatchOut);
00124         if ( Abc_ObjFanoutNum(pLatchOut) > 0 )
00125             Abc_ObjTransferFanout( pLatchOut, pFanin );
00126         Abc_ObjDeleteFanin( pLatchOut, pFanin );
00127     }
00128     return tLatches;
00129 }

void Abc_NtkRetimeShareLatches ( Abc_Ntk_t *  pNtk,
int  fInitial 
)

Function*************************************************************

Synopsis [Retimes the node backward or forward.]

Description []

SideEffects []

SeeAlso []

Definition at line 422 of file retIncrem.c.

00423 {
00424     Vec_Ptr_t * vNodes;
00425     Abc_Obj_t * pFanin, * pLatchTop, * pLatchCur;
00426     int i, k;
00427     vNodes = Vec_PtrAlloc( 10 );
00428     // consider latch fanins
00429     Abc_NtkForEachObj( pNtk, pFanin, i )
00430     {
00431         if ( Abc_NtkRetimeCheckCompatibleLatchFanouts(pFanin) <= 1 )
00432             continue;
00433         // get the first latch
00434         pLatchTop = NULL;
00435         Abc_ObjForEachFanout( pFanin, pLatchTop, k )
00436             if ( Abc_ObjIsLatch(pLatchTop) )
00437                 break;
00438         assert( pLatchTop && Abc_ObjIsLatch(pLatchTop) );
00439         // redirect compatible fanout latches to the first latch
00440         Abc_NodeCollectFanouts( pFanin, vNodes );
00441         Vec_PtrForEachEntry( vNodes, pLatchCur, k )
00442         {
00443             if ( !Abc_ObjIsLatch(pLatchCur) )
00444                 continue;
00445             if ( pLatchCur == pLatchTop )
00446                 continue;
00447             if ( pLatchCur->pData != pLatchTop->pData )
00448                 continue;
00449             // connect the initial state
00450             if ( fInitial )
00451                 Abc_ObjAddFanin( pLatchCur->pCopy, pLatchTop->pCopy );
00452             // redirect the fanouts
00453             Abc_ObjTransferFanout( pLatchCur, pLatchTop );
00454             Abc_NtkDeleteObj(pLatchCur);
00455         }
00456     }
00457     Vec_PtrFree( vNodes );
00458 }

void Abc_NtkRetimeTranferFromCopy ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Transfer latch initial values from pCopy.]

Description []

SideEffects []

SeeAlso []

Definition at line 184 of file retInit.c.

00185 {
00186     Abc_Obj_t * pObj;
00187     int i;
00188     Abc_NtkForEachObj( pNtk, pObj, i )
00189         if ( Abc_ObjIsLatch(pObj) )
00190             pObj->pData = (void *)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO);
00191 }

void Abc_NtkRetimeTranferToCopy ( Abc_Ntk_t *  pNtk  ) 

Function*************************************************************

Synopsis [Transfer latch initial values to pCopy.]

Description []

SideEffects []

SeeAlso []

Definition at line 164 of file retInit.c.

00165 {
00166     Abc_Obj_t * pObj;
00167     int i;
00168     Abc_NtkForEachObj( pNtk, pObj, i )
00169         if ( Abc_ObjIsLatch(pObj) )
00170             pObj->pCopy = (void *)Abc_LatchIsInit1(pObj);
00171 }

int Abc_ObjSopSimulate ( Abc_Obj_t *  pObj  ) 

Function*************************************************************

Synopsis [Computes the results of simulating one node.]

Description [Assumes that fanins have pCopy set to the input values.]

SideEffects []

SeeAlso []

Definition at line 89 of file retInit.c.

00090 {
00091     char * pCube, * pSop = pObj->pData;
00092     int nVars, Value, v, ResOr, ResAnd, ResVar;
00093     assert( pSop && !Abc_SopIsExorType(pSop) );
00094     // simulate the SOP of the node
00095     ResOr = 0;
00096     nVars = Abc_SopGetVarNum(pSop);
00097     Abc_SopForEachCube( pSop, nVars, pCube )
00098     {
00099         ResAnd = 1;
00100         Abc_CubeForEachVar( pCube, Value, v )
00101         {
00102             if ( Value == '0' )
00103                 ResVar = 1 ^ ((int)Abc_ObjFanin(pObj, v)->pCopy);
00104             else if ( Value == '1' )
00105                 ResVar = (int)Abc_ObjFanin(pObj, v)->pCopy;
00106             else
00107                 continue;
00108             ResAnd &= ResVar;
00109         }
00110         ResOr |= ResAnd;
00111     }
00112     // complement the result if necessary
00113     if ( !Abc_SopGetPhase(pSop) )
00114         ResOr ^= 1;
00115     return ResOr;
00116 }

Generated on Tue Jan 5 12:19:33 2010 for abc70930 by  doxygen 1.6.1