abc/src/opt/ret/retInit.c - third_party/vtr-verilog-to-routing - Git at Google


            
            /**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"


            ABC_NAMESPACE_IMPL_START


            ////////////////////////////////////////////////////////////////////////

            
            ///                        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;

            
                abctime 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 = Abc_Clock();

            
                RetValue = Abc_NtkMiterSat( pNtkMiter, (ABC_INT64_T)500000, (ABC_INT64_T)50000000, 0, NULL, NULL );

            
                if ( fVerbose )

            
                    { ABC_PRT( "SAT solving time", Abc_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 = (char *)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_PTRUINT_T)Abc_ObjFanin(pObj, v)->pCopy);

            
                        else if ( Value == '1' )

            
                            ResVar = (int)(ABC_PTRUINT_T)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 = (Abc_Obj_t *)(ABC_PTRUINT_T)pModel[i];

            
                // simulate the internal nodes

            
                vNodes = Abc_NtkDfs( pNtkCone, 0 );

            
                Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )

            
                    pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)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)(ABC_PTRUINT_T)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 = (Abc_Obj_t *)(ABC_PTRUINT_T)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 *)(ABC_PTRUINT_T)(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 = (Abc_Obj_t *)(ABC_PTRUINT_T)Counter++;

            
                Abc_NtkForEachObj( pNtk, pObj, i )

            
                    if ( Abc_ObjIsLatch(pObj) )

            
                        pObj->pData = (Abc_Obj_t *)(ABC_PTRUINT_T)(vValues? (Vec_IntEntry(vValues,(int)(ABC_PTRUINT_T)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 = (Abc_Obj_t *)(ABC_PTRUINT_T)(rand() & 1);

            
                Abc_NtkForEachLatch( pNtk, pObj, i )

            
                    pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)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( Abc_Obj_t *, vNodes, pObj, i )

            
                        pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)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 = (Abc_Obj_t *)(ABC_PTRUINT_T)(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_PTRUINT_T)(Abc_ObjFanout0(pObj)->pCopy ? ABC_INIT_ONE : ABC_INIT_ZERO);

            
            }


            ////////////////////////////////////////////////////////////////////////

            
            ///                       END OF FILE                                ///

            
            ////////////////////////////////////////////////////////////////////////


            ABC_NAMESPACE_IMPL_END
	/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"

	ABC_NAMESPACE_IMPL_START


	////////////////////////////////////////////////////////////////////////
	/// 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;
	abctime 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 = Abc_Clock();
	RetValue = Abc_NtkMiterSat( pNtkMiter, (ABC_INT64_T)500000, (ABC_INT64_T)50000000, 0, NULL, NULL );
	if ( fVerbose )
	{ ABC_PRT( "SAT solving time", Abc_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 = (char *)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_PTRUINT_T)Abc_ObjFanin(pObj, v)->pCopy);
	else if ( Value == '1' )
	ResVar = (int)(ABC_PTRUINT_T)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 = (Abc_Obj_t *)(ABC_PTRUINT_T)pModel[i];
	// simulate the internal nodes
	vNodes = Abc_NtkDfs( pNtkCone, 0 );
	Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
	pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)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)(ABC_PTRUINT_T)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 = (Abc_Obj_t *)(ABC_PTRUINT_T)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 *)(ABC_PTRUINT_T)(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 = (Abc_Obj_t *)(ABC_PTRUINT_T)Counter++;
	Abc_NtkForEachObj( pNtk, pObj, i )
	if ( Abc_ObjIsLatch(pObj) )
	pObj->pData = (Abc_Obj_t *)(ABC_PTRUINT_T)(vValues? (Vec_IntEntry(vValues,(int)(ABC_PTRUINT_T)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 = (Abc_Obj_t *)(ABC_PTRUINT_T)(rand() & 1);
	Abc_NtkForEachLatch( pNtk, pObj, i )
	pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)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( Abc_Obj_t *, vNodes, pObj, i )
	pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)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 = (Abc_Obj_t *)(ABC_PTRUINT_T)(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_PTRUINT_T)(Abc_ObjFanout0(pObj)->pCopy ? ABC_INIT_ONE : ABC_INIT_ZERO);
	}

	////////////////////////////////////////////////////////////////////////
	/// END OF FILE ///
	////////////////////////////////////////////////////////////////////////


	ABC_NAMESPACE_IMPL_END