diff options
Diffstat (limited to 'src/opt/ret/retInit.c')
-rw-r--r-- | src/opt/ret/retInit.c | 349 |
1 files changed, 0 insertions, 349 deletions
diff --git a/src/opt/ret/retInit.c b/src/opt/ret/retInit.c deleted file mode 100644 index dcb71c60..00000000 --- a/src/opt/ret/retInit.c +++ /dev/null @@ -1,349 +0,0 @@ -/**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 $] - -***********************************************************************/ - -#include "retInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static int Abc_NtkRetimeVerifyModel( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int * pModel ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Computes initial values of the new latches.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int fVerbose ) -{ - Vec_Int_t * vSolution; - Abc_Ntk_t * pNtkMiter, * pNtkLogic; - int RetValue, clk; - if ( pNtkCone == NULL ) - return Vec_IntDup( vValues ); - // convert the target network to AIG - pNtkLogic = Abc_NtkDup( pNtkCone ); - Abc_NtkToAig( pNtkLogic ); - // get the miter - pNtkMiter = Abc_NtkCreateTarget( pNtkLogic, pNtkLogic->vCos, vValues ); - if ( fVerbose ) - printf( "The miter for initial state computation has %d AIG nodes. ", Abc_NtkNodeNum(pNtkMiter) ); - // solve the miter - clk = clock(); - RetValue = Abc_NtkMiterSat( pNtkMiter, (sint64)500000, (sint64)50000000, 0, NULL, NULL ); - if ( fVerbose ) - { PRT( "SAT solving time", clock() - clk ); } - // analyze the result - if ( RetValue == 1 ) - printf( "Abc_NtkRetimeInitialValues(): The problem is unsatisfiable. DC latch values are used.\n" ); - else if ( RetValue == -1 ) - printf( "Abc_NtkRetimeInitialValues(): The SAT problem timed out. DC latch values are used.\n" ); - else if ( !Abc_NtkRetimeVerifyModel( pNtkCone, vValues, pNtkMiter->pModel ) ) - printf( "Abc_NtkRetimeInitialValues(): The computed counter-example is incorrect.\n" ); - // set the values of the latches - vSolution = RetValue? NULL : Vec_IntAllocArray( pNtkMiter->pModel, Abc_NtkPiNum(pNtkLogic) ); - pNtkMiter->pModel = NULL; - Abc_NtkDelete( pNtkMiter ); - Abc_NtkDelete( pNtkLogic ); - return vSolution; -} - -/**Function************************************************************* - - Synopsis [Computes the results of simulating one node.] - - Description [Assumes that fanins have pCopy set to the input values.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_ObjSopSimulate( Abc_Obj_t * pObj ) -{ - char * pCube, * pSop = pObj->pData; - int nVars, Value, v, ResOr, ResAnd, ResVar; - assert( pSop && !Abc_SopIsExorType(pSop) ); - // simulate the SOP of the node - ResOr = 0; - nVars = Abc_SopGetVarNum(pSop); - Abc_SopForEachCube( pSop, nVars, pCube ) - { - ResAnd = 1; - Abc_CubeForEachVar( pCube, Value, v ) - { - if ( Value == '0' ) - ResVar = 1 ^ ((int)Abc_ObjFanin(pObj, v)->pCopy); - else if ( Value == '1' ) - ResVar = (int)Abc_ObjFanin(pObj, v)->pCopy; - else - continue; - ResAnd &= ResVar; - } - ResOr |= ResAnd; - } - // complement the result if necessary - if ( !Abc_SopGetPhase(pSop) ) - ResOr ^= 1; - return ResOr; -} - -/**Function************************************************************* - - Synopsis [Verifies the counter-example.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkRetimeVerifyModel( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int * pModel ) -{ - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj; - int i, Counter = 0; - assert( Abc_NtkIsSopLogic(pNtkCone) ); - // set the PIs - Abc_NtkForEachPi( pNtkCone, pObj, i ) - pObj->pCopy = (void *)pModel[i]; - // simulate the internal nodes - vNodes = Abc_NtkDfs( pNtkCone, 0 ); - Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pCopy = (void *)Abc_ObjSopSimulate( pObj ); - Vec_PtrFree( vNodes ); - // compare the outputs - Abc_NtkForEachPo( pNtkCone, pObj, i ) - pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy; - Abc_NtkForEachPo( pNtkCone, pObj, i ) - Counter += (Vec_IntEntry(vValues, i) != (int)pObj->pCopy); - if ( Counter > 0 ) - printf( "%d outputs (out of %d) have a value mismatch.\n", Counter, Abc_NtkPoNum(pNtkCone) ); - return 1; -} - -/**Function************************************************************* - - Synopsis [Transfer latch initial values to pCopy.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkRetimeTranferToCopy( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pObj; - int i; - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( Abc_ObjIsLatch(pObj) ) - pObj->pCopy = (void *)Abc_LatchIsInit1(pObj); -} - -/**Function************************************************************* - - Synopsis [Transfer latch initial values from pCopy.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkRetimeTranferFromCopy( Abc_Ntk_t * pNtk ) -{ - Abc_Obj_t * pObj; - int i; - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( Abc_ObjIsLatch(pObj) ) - pObj->pData = (void *)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO); -} - -/**Function************************************************************* - - Synopsis [Transfer latch initial values to pCopy.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkRetimeCollectLatchValues( Abc_Ntk_t * pNtk ) -{ - Vec_Int_t * vValues; - Abc_Obj_t * pObj; - int i; - vValues = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( Abc_ObjIsLatch(pObj) ) - Vec_IntPush( vValues, Abc_LatchIsInit1(pObj) ); - return vValues; -} - -/**Function************************************************************* - - Synopsis [Transfer latch initial values from pCopy.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkRetimeInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues ) -{ - Abc_Obj_t * pObj; - int i, Counter = 0; - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( Abc_ObjIsLatch(pObj) ) - pObj->pCopy = (void *)Counter++; - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( Abc_ObjIsLatch(pObj) ) - pObj->pData = (void *)(vValues? (Vec_IntEntry(vValues,(int)pObj->pCopy)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC); -} - -/**Function************************************************************* - - Synopsis [Transfer latch initial values to pCopy.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkRetimeBackwardInitialStart( Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj; - int i; - // create the network used for the initial state computation - pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); - // create POs corresponding to the initial values - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( Abc_ObjIsLatch(pObj) ) - pObj->pCopy = Abc_NtkCreatePo(pNtkNew); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Transfer latch initial values to pCopy.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkRetimeBackwardInitialFinish( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, Vec_Int_t * vValuesOld, int fVerbose ) -{ - Vec_Int_t * vValuesNew; - Abc_Obj_t * pObj; - int i; - // create PIs corresponding to the initial values - Abc_NtkForEachObj( pNtk, pObj, i ) - if ( Abc_ObjIsLatch(pObj) ) - Abc_ObjAddFanin( pObj->pCopy, Abc_NtkCreatePi(pNtkNew) ); - // assign dummy node names - Abc_NtkAddDummyPiNames( pNtkNew ); - Abc_NtkAddDummyPoNames( pNtkNew ); - // check the network - if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkRetimeBackwardInitialFinish(): Network check has failed.\n" ); - // derive new initial values - vValuesNew = Abc_NtkRetimeInitialValues( pNtkNew, vValuesOld, fVerbose ); - // insert new initial values - Abc_NtkRetimeInsertLatchValues( pNtk, vValuesNew ); - if ( vValuesNew ) Vec_IntFree( vValuesNew ); -} - - -/**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 [] - -***********************************************************************/ -void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) -{ - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj; - int i, f; - assert( Abc_NtkIsSopLogic(pNtk) ); - srand( 0x12341234 ); - // initialize the values - Abc_NtkForEachPi( pNtk, pObj, i ) - pObj->pCopy = (void *)(rand() & 1); - Abc_NtkForEachLatch( pNtk, pObj, i ) - pObj->pCopy = (void *)Abc_LatchIsInit1(pObj); - // simulate for the given number of timeframes - vNodes = Abc_NtkDfs( pNtk, 0 ); - for ( f = 0; f < nFrames; f++ ) - { - // simulate internal nodes - Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pCopy = (void *)Abc_ObjSopSimulate( pObj ); - // bring the results to the COs - Abc_NtkForEachCo( pNtk, pObj, i ) - pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy; - // assign PI values - Abc_NtkForEachPi( pNtk, pObj, i ) - pObj->pCopy = (void *)(rand() & 1); - // transfer the latch values - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin0(pObj)->pCopy; - } - Vec_PtrFree( vNodes ); - // set the final values - Abc_NtkForEachLatch( pNtk, pObj, i ) - pObj->pData = (void *)(Abc_ObjFanout0(pObj)->pCopy ? ABC_INIT_ONE : ABC_INIT_ZERO); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |