+#include "satSolver.h"

+#include "cnf.h"

+ Synopsis [Counts the number of nodes to get registers after retiming.]

+int Saig_ManRetimeCountCut( Aig_Man_t * p, Vec_Ptr_t * vCut )

+ Vec_Ptr_t * vNodes;

+ Aig_Obj_t * pObj, * pFanin;

+ int i, RetValue;

+ // mark the cones

+ Vec_PtrForEachEntry( vCut, pObj, i )

+ // collect the new cut

+ vNodes = Vec_PtrAlloc( 1000 );

+ Aig_ManForEachObj( p, pObj, i )

+ {

+ if ( Aig_ObjIsTravIdCurrent(p, pObj) )

+ continue;

+ pFanin = Aig_ObjFanin0( pObj );

+ if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )

+ {

+ Vec_PtrPush( vNodes, pFanin );

+ pFanin->fMarkA = 1;

+ }

+ pFanin = Aig_ObjFanin1( pObj );

+ if ( pFanin && !pFanin->fMarkA && Aig_ObjIsTravIdCurrent(p, pFanin) )

+ {

+ Vec_PtrPush( vNodes, pFanin );

+ pFanin->fMarkA = 1;

+ }

+ }

+ Vec_PtrForEachEntry( vNodes, pObj, i )

+ pObj->fMarkA = 0;

+ RetValue = Vec_PtrSize( vNodes );

+ Vec_PtrFree( vNodes );

+ return RetValue;

+ Synopsis [Computes the new cut after excluding the nodes in the set.]

+Vec_Ptr_t * Saig_ManRetimeExtendCut( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Ptr_t * vToExclude )

+ int i;

+ // mark the cones

+ Aig_ManIncrementTravId( p );

+ Vec_PtrForEachEntry( vCut, pObj, i )

+ Saig_ManMarkCone_rec( p, pObj );

+ Vec_PtrForEachEntry( vToExclude, pObj, i )

+ Saig_ManMarkCone_rec( p, pObj );

+ // collect the new cut

+ return vNodes;

+ Synopsis [Duplicates the AIG recursively.]

+void Saig_ManRetimeDup_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj )

+ Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );

+ Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin1(pObj) );

+ // duplicate logic above the cut

+ Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );

+ if ( Aig_ObjIsNode(pObj) )

+ // duplicate logic below the cut

+ Saig_ManRetimeDup_rec( pNew, pObj );

+ Synopsis [Derives AIG for the initial state computation.]

+Aig_Man_t * Saig_ManRetimeDupInitState( Aig_Man_t * p, Vec_Ptr_t * vCut )

+ Aig_Obj_t * pObj;

+ int i;

+ // mark the cones under the cut

+// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );

+ // create the new manager

+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );

+ // create the true PIs

+ Aig_ManCleanData( p );

+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);

+ // create the registers

+ Vec_PtrForEachEntry( vCut, pObj, i )

+ pObj->pData = Aig_ObjCreatePi(pNew);

+ // duplicate logic above the cut and create POs

+ Saig_ManForEachLi( p, pObj, i )

+ {

+ Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );

+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );

+ }

+ return pNew;

+}

+

+/**Function*************************************************************

+

+ Synopsis [Derives the initial state after backward retiming.]

+

+ Description []

+

+ SideEffects []

+

+ SeeAlso []

+

+***********************************************************************/

+Vec_Int_t * Saig_ManRetimeFindInitState( Aig_Man_t * p )

+{

+ int nConfLimit = 1000000;

+ Vec_Int_t * vCiIds, * vInit = NULL;

+ Cnf_Dat_t * pCnf;

+ sat_solver * pSat;

+ Aig_Obj_t * pObj;

+ int i, RetValue, * pAssumps, * pModel;

+ // solve the SAT problem

+ pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );

+ pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );

+ pAssumps = ALLOC( int, Aig_ManPoNum(p) );

+ Aig_ManForEachPo( p, pObj, i )

+ pAssumps[i] = toLitCond( pCnf->pVarNums[pObj->Id], 1 );

+ RetValue = sat_solver_solve( pSat, pAssumps, pAssumps+Aig_ManPoNum(p), (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );

+ free( pAssumps );

+ if ( RetValue == l_True )

+ {

+ // accumulate SAT variables of the CIs

+ vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) );

+ Aig_ManForEachPi( p, pObj, i )

+ Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );

+ // create the model

+ pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );

+ vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) );

+ Vec_IntFree( vCiIds );

+ }

+ sat_solver_delete( pSat );

+ Cnf_DataFree( pCnf );

+ return vInit;

+}

+

+/**Function*************************************************************

+

+ Synopsis [Returns the array of bad registers.]

+

+ Description []

+

+ SideEffects []

+

+ SeeAlso []

+

+***********************************************************************/

+Vec_Ptr_t * Saig_ManGetRegistersToExclude( Aig_Man_t * p )

+{

+ Vec_Ptr_t * vNodes = NULL;

+ Aig_Obj_t * pObj, * pFanin;

+ int i, Diffs;

+ assert( Saig_ManRegNum(p) > 0 );

+ Saig_ManForEachLi( p, pObj, i )

+ {

+ pFanin = Aig_ObjFanin0(pObj);

+ if ( !Aig_ObjFaninC0(pObj) )

+ pFanin->fMarkA = 1;

+ else

+ pFanin->fMarkB = 1;

+ }

+ Diffs = 0;

+ Saig_ManForEachLi( p, pObj, i )

+ {

+ pFanin = Aig_ObjFanin0(pObj);

+ Diffs += pFanin->fMarkA && pFanin->fMarkB;

+ }

+ if ( Diffs > 0 )

+ vNodes = Vec_PtrAlloc( Diffs );

+ Saig_ManForEachLi( p, pObj, i )

+ {

+ pFanin = Aig_ObjFanin0(pObj);

+ if ( vNodes && pFanin->fMarkA && pFanin->fMarkB )

+ Vec_PtrPush( vNodes, pFanin );

+ pFanin->fMarkA = pFanin->fMarkB = 0;

+ }

+ return vNodes;

+}

+

+/**Function*************************************************************

+

+ Synopsis [Duplicates the AIG while retiming the registers to the cut.]

+

+ Description []

+

+ SideEffects []

+

+ SeeAlso []

+

+***********************************************************************/

+Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCutInit )

+{

+ Vec_Ptr_t * vToExclude, * vCut;

+ Vec_Int_t * vInit = NULL;

+ Aig_Man_t * pNew, * pInit;

+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;

+ int i;

+ // check if there are bad registers

+ vToExclude = Saig_ManGetRegistersToExclude( p );

+ if ( vToExclude )

+ {

+ vCut = Saig_ManRetimeExtendCut( p, vCutInit, vToExclude );

+ printf( "Bad registers = %d. Extended cut from %d to %d nodes.\n",

+ Vec_PtrSize(vToExclude), Vec_PtrSize(vCutInit), Vec_PtrSize(vCut) );

+ Vec_PtrFree( vToExclude );

+ }

+ else

+ vCut = Vec_PtrDup( vCutInit );

+ // mark the cones under the cut

+// assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) );

+ // count if there are registers to disable

+ // derive the initial state

+ pInit = Saig_ManRetimeDupInitState( p, vCut );

+ vInit = Saig_ManRetimeFindInitState( pInit );

+ if ( vInit == NULL )

+ printf( "Initial state computation has failed.\n" );

+ Aig_ManStop( pInit );

+ // create the new manager

+ pNew = Aig_ManStart( Aig_ManObjNumMax(p) );

+ pNew->pName = Aig_UtilStrsav( p->pName );

+ pNew->pSpec = Aig_UtilStrsav( p->pSpec );

+ pNew->nRegs = Vec_PtrSize(vCut);

+ pNew->nTruePis = p->nTruePis;

+ pNew->nTruePos = p->nTruePos;

+ // create the true PIs

+ Aig_ManCleanData( p );

+ Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);

+ Saig_ManForEachPi( p, pObj, i )

+ pObj->pData = Aig_ObjCreatePi( pNew );

+ // create the registers

+ Vec_PtrForEachEntry( vCut, pObj, i )

+ pObj->pData = Aig_NotCond( Aig_ObjCreatePi(pNew), vInit?Vec_IntEntry(vInit,i):0 );

+ // duplicate logic above the cut and remember values

+ Saig_ManForEachLi( p, pObj, i )

+ {

+ Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );

+ pObj->pData = Aig_ObjChild0Copy(pObj);

+ }

+ // transfer values from the LIs to the LOs

+ Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )

+ pObjLo->pData = pObjLi->pData;

+ // erase the data values on the internal nodes of the cut

+ Vec_PtrForEachEntry( vCut, pObj, i )

+ if ( Aig_ObjIsNode(pObj) )

+ pObj->pData = NULL;

+ // replicate the data on the primary inputs

+ Saig_ManForEachPi( p, pObj, i )

+ pObj->pData = Aig_ManPi( pNew, i );

+ // duplicate logic below the cut

+ Saig_ManForEachPo( p, pObj, i )

+ {

+ Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );

+ Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );

+ }

+ Vec_PtrForEachEntry( vCut, pObj, i )

+ {

+ Saig_ManRetimeDup_rec( pNew, pObj );

+ Aig_ObjCreatePo( pNew, Aig_NotCond(pObj->pData, vInit?Vec_IntEntry(vInit,i):0) );

+ }

+ if ( vInit )

+ Vec_IntFree( vInit );

+ Vec_PtrFree( vCut );