src/opt/ret/retInit.c File Reference

#include "retInt.h"
Include dependency graph for retInit.c:

Go to the source code of this file.

Functions

static int Abc_NtkRetimeVerifyModel (Abc_Ntk_t *pNtkCone, Vec_Int_t *vValues, int *pModel)
Vec_Int_t * Abc_NtkRetimeInitialValues (Abc_Ntk_t *pNtkCone, 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)
void Abc_NtkCycleInitStateSop (Abc_Ntk_t *pNtk, int nFrames, int fVerbose)

Function Documentation

void Abc_NtkCycleInitStateSop ( Abc_Ntk_t *  pNtk,
int  nFrames,
int  fVerbose 
)

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

Synopsis [Cycles the circuit to create a new initial state.]

Description [Simulates the circuit with random input for the given number of timeframes to get a better initial state.]

SideEffects []

SeeAlso []

Definition at line 310 of file retInit.c.

00311 {
00312     Vec_Ptr_t * vNodes;
00313     Abc_Obj_t * pObj;
00314     int i, f;
00315     assert( Abc_NtkIsSopLogic(pNtk) );
00316     srand( 0x12341234 );
00317     // initialize the values
00318     Abc_NtkForEachPi( pNtk, pObj, i )
00319         pObj->pCopy = (void *)(rand() & 1);
00320     Abc_NtkForEachLatch( pNtk, pObj, i )
00321         pObj->pCopy = (void *)Abc_LatchIsInit1(pObj);
00322     // simulate for the given number of timeframes
00323     vNodes = Abc_NtkDfs( pNtk, 0 );
00324     for ( f = 0; f < nFrames; f++ )
00325     {
00326         // simulate internal nodes
00327         Vec_PtrForEachEntry( vNodes, pObj, i )
00328             pObj->pCopy = (void *)Abc_ObjSopSimulate( pObj );
00329         // bring the results to the COs
00330         Abc_NtkForEachCo( pNtk, pObj, i )
00331             pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
00332         // assign PI values
00333         Abc_NtkForEachPi( pNtk, pObj, i )
00334             pObj->pCopy = (void *)(rand() & 1);
00335         // transfer the latch values
00336         Abc_NtkForEachLatch( pNtk, pObj, i )
00337             Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
00338     }
00339     Vec_PtrFree( vNodes );
00340     // set the final values
00341     Abc_NtkForEachLatch( pNtk, pObj, i )
00342         pObj->pData = (void *)(Abc_ObjFanout0(pObj)->pCopy ? ABC_INIT_ONE : ABC_INIT_ZERO);
00343 }

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 }

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 }

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_NtkRetimeVerifyModel ( Abc_Ntk_t *  pNtkCone,
Vec_Int_t *  vValues,
int *  pModel 
) [static]

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

FileName [retInit.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Retiming package.]

Synopsis [Initial state computation for backward retiming.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
retInit.c,v 1.00 2006/10/31 00:00:00 alanmi Exp

] DECLARATIONS ///

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

Synopsis [Verifies the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file retInit.c.

00130 {
00131     Vec_Ptr_t * vNodes;
00132     Abc_Obj_t * pObj;
00133     int i, Counter = 0;
00134     assert( Abc_NtkIsSopLogic(pNtkCone) );
00135     // set the PIs
00136     Abc_NtkForEachPi( pNtkCone, pObj, i )
00137         pObj->pCopy = (void *)pModel[i];
00138     // simulate the internal nodes
00139     vNodes = Abc_NtkDfs( pNtkCone, 0 );
00140     Vec_PtrForEachEntry( vNodes, pObj, i )
00141         pObj->pCopy = (void *)Abc_ObjSopSimulate( pObj );
00142     Vec_PtrFree( vNodes );
00143     // compare the outputs
00144     Abc_NtkForEachPo( pNtkCone, pObj, i )
00145         pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
00146     Abc_NtkForEachPo( pNtkCone, pObj, i )
00147         Counter += (Vec_IntEntry(vValues, i) != (int)pObj->pCopy);
00148     if ( Counter > 0 )
00149         printf( "%d outputs (out of %d) have a value mismatch.\n", Counter, Abc_NtkPoNum(pNtkCone) );
00150     return 1;
00151 }

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:32 2010 for abc70930 by  doxygen 1.6.1