saigRetMin.c File Reference

#include "saig.h"
#include "opt/nwk/nwk.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "sat/bsat/satStore.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Vec_Int_t *	Saig_ManRetimeInitState (Aig_Man_t *p)
	DECLARATIONS ///. More...
int	Saig_ManRetimeUnsatCore (Aig_Man_t *p, int fVerbose)
void	Saig_ManMarkCone_rec (Aig_Man_t *p, Aig_Obj_t *pObj)
int	Saig_ManRetimeCountCut (Aig_Man_t *p, Vec_Ptr_t *vCut)
void	Saig_ManRetimeDup_rec (Aig_Man_t *pNew, Aig_Obj_t *pObj)
Aig_Man_t *	Saig_ManRetimeDupForward (Aig_Man_t *p, Vec_Ptr_t *vCut)
Aig_Man_t *	Saig_ManRetimeDupBackward (Aig_Man_t *p, Vec_Ptr_t *vCut, Vec_Int_t *vInit)
Aig_Man_t *	Saig_ManRetimeDupInitState (Aig_Man_t *p, Vec_Ptr_t *vCut)
Vec_Ptr_t *	Saig_ManGetRegistersToExclude (Aig_Man_t *p)
int	Saig_ManHideBadRegs (Aig_Man_t *p, Vec_Ptr_t *vBadRegs)
void	Saig_ManExposeBadRegs (Aig_Man_t *p, int nBadRegs)
Aig_Man_t *	Saig_ManRetimeMinAreaBackward (Aig_Man_t *pNew, int fVerbose)
Aig_Man_t *	Saig_ManRetimeMinArea (Aig_Man_t *p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose)

Function Documentation

void Saig_ManExposeBadRegs	(	Aig_Man_t *	p,
		int	nBadRegs
	)

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

Synopsis [Exposes bad registers.]

Description []

SideEffects []

SeeAlso []

Definition at line 549 of file saigRetMin.c.

{
    p->nRegs += nBadRegs;
    p->nTruePis -= nBadRegs;
    p->nTruePos -= nBadRegs;
}

Vec_Ptr_t* Saig_ManGetRegistersToExclude

(

Aig_Man_t *

p

)

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

Synopsis [Returns the array of bad registers.]

Description []

SideEffects []

SeeAlso []

Definition at line 441 of file saigRetMin.c.

{
    Vec_Ptr_t * vNodes;
    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;
    }
    vNodes = Vec_PtrAlloc( 100 );
    if ( Diffs > 0 )
    {
        Saig_ManForEachLi( p, pObj, i )
        {
            pFanin = Aig_ObjFanin0(pObj);
            if ( pFanin->fMarkA && pFanin->fMarkB )
                Vec_PtrPush( vNodes, pObj );
        }
        assert( Vec_PtrSize(vNodes) == Diffs );
    }
    Saig_ManForEachLi( p, pObj, i )
    {
        pFanin = Aig_ObjFanin0(pObj);
        pFanin->fMarkA = pFanin->fMarkB = 0;
    }
    return vNodes;
}

int Saig_ManHideBadRegs	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vBadRegs
	)

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

Synopsis [Hides the registers that cannot be backward retimed.]

Description []

SideEffects []

SeeAlso []

Definition at line 491 of file saigRetMin.c.

{
    Vec_Ptr_t * vPisNew, * vPosNew;
    Aig_Obj_t * pObjLi, * pObjLo;
    int nTruePi, nTruePo, nBadRegs, i;
    if ( Vec_PtrSize(vBadRegs) == 0 )
        return 0;
    // attached LOs to LIs
    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
        pObjLi->pData = pObjLo;
    // reorder them by putting bad registers first
    vPisNew = Vec_PtrDup( p->vCis );
    vPosNew = Vec_PtrDup( p->vCos );
    nTruePi = Aig_ManCiNum(p) - Aig_ManRegNum(p);
    nTruePo = Aig_ManCoNum(p) - Aig_ManRegNum(p);
    assert( nTruePi == p->nTruePis );
    assert( nTruePo == p->nTruePos );
    Vec_PtrForEachEntry( Aig_Obj_t *, vBadRegs, pObjLi, i )
    {
        Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLi->pData );
        Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi );
        pObjLi->fMarkA = 1;
    }
    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
    {
        if ( pObjLi->fMarkA )
        {
            pObjLi->fMarkA = 0;
            continue;
        }
        Vec_PtrWriteEntry( vPisNew, nTruePi++, pObjLo );
        Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi );
    }
    // check the sizes
    assert( nTruePi == Aig_ManCiNum(p) );
    assert( nTruePo == Aig_ManCoNum(p) );
    // transfer the arrays
    Vec_PtrFree( p->vCis ); p->vCis = vPisNew;
    Vec_PtrFree( p->vCos ); p->vCos = vPosNew;
    // update the PIs
    nBadRegs = Vec_PtrSize(vBadRegs);
    p->nRegs -= nBadRegs;
    p->nTruePis += nBadRegs;
    p->nTruePos += nBadRegs;
    return nBadRegs;
}

void Saig_ManMarkCone_rec	(	Aig_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Marks the TFI cone with the current traversal ID.]

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file saigRetMin.c.

{
    if ( pObj == NULL )
        return;
    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
        return;
    Aig_ObjSetTravIdCurrent( p, pObj );
    Saig_ManMarkCone_rec( p, Aig_ObjFanin0(pObj) );
    Saig_ManMarkCone_rec( p, Aig_ObjFanin1(pObj) );
}

int Saig_ManRetimeCountCut	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vCut
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file saigRetMin.c.

{
    Vec_Ptr_t * vNodes;
    Aig_Obj_t * pObj, * pFanin;
    int i, RetValue;
    // mark the cones
    Aig_ManIncrementTravId( p );
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
        Saig_ManMarkCone_rec( p, pObj );
    // 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( Aig_Obj_t *, vNodes, pObj, i )
        pObj->fMarkA = 0;
    RetValue = Vec_PtrSize( vNodes );
    Vec_PtrFree( vNodes );
    return RetValue;
}

void Saig_ManRetimeDup_rec	(	Aig_Man_t *	pNew,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Duplicates the AIG recursively.]

Description []

SideEffects []

SeeAlso []

Definition at line 260 of file saigRetMin.c.

{
    if ( pObj->pData )
        return;
    assert( Aig_ObjIsNode(pObj) );
    Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
    Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin1(pObj) );
    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}

Aig_Man_t* Saig_ManRetimeDupBackward	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vCut,
		Vec_Int_t *	vInit
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 340 of file saigRetMin.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    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) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_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_ObjCreateCi( pNew );
    // create the registers
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
        pObj->pData = Aig_NotCond( Aig_ObjCreateCi(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( Aig_Obj_t *, vCut, pObj, i )
        if ( Aig_ObjIsNode(pObj) )
            pObj->pData = NULL;
    // replicate the data on the constant node and the PIs
    pObj = Aig_ManConst1(p);
    pObj->pData = Aig_ManConst1(pNew);
    Saig_ManForEachPi( p, pObj, i )
        pObj->pData = Aig_ManCi( pNew, i );
    // duplicate logic below the cut
    Saig_ManForEachPo( p, pObj, i )
    {
        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
    {
        Saig_ManRetimeDup_rec( pNew, pObj );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)pObj->pData, vInit?Vec_IntEntry(vInit,i):0) );
    }
    Aig_ManCleanup( pNew );
    return pNew;
}

Aig_Man_t* Saig_ManRetimeDupForward	(	Aig_Man_t *	p,
		Vec_Ptr_t *	vCut
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 281 of file saigRetMin.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    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) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_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_ObjCreateCi( pNew );
    // create the registers
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
        pObj->pData = Aig_NotCond( Aig_ObjCreateCi(pNew), pObj->fPhase );
    // duplicate logic above the cut
    Aig_ManForEachCo( p, pObj, i )
        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
    // create the true POs
    Saig_ManForEachPo( p, pObj, i )
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    // remember value in LI
    Saig_ManForEachLi( p, pObj, i )
        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( Aig_Obj_t *, vCut, pObj, i )
        if ( Aig_ObjIsNode(pObj) )
            pObj->pData = NULL;
    // duplicate logic below the cut
    Vec_PtrForEachEntry( Aig_Obj_t *, vCut, pObj, i )
    {
        Saig_ManRetimeDup_rec( pNew, pObj );
        Aig_ObjCreateCo( pNew, Aig_NotCond((Aig_Obj_t *)pObj->pData, pObj->fPhase) );
    }
    Aig_ManCleanup( pNew );
    return pNew;
}

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

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

Synopsis [Derives AIG for the initial state computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 406 of file saigRetMin.c.

{
    Aig_Man_t * pNew;
    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( Aig_Obj_t *, vCut, pObj, i )
        pObj->pData = Aig_ObjCreateCi(pNew);
    // duplicate logic above the cut and create POs
    Saig_ManForEachLi( p, pObj, i )
    {
        Saig_ManRetimeDup_rec( pNew, Aig_ObjFanin0(pObj) );
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    return pNew;
}

ABC_NAMESPACE_IMPL_START Vec_Int_t* Saig_ManRetimeInitState

(

Aig_Man_t *

p

)

DECLARATIONS ///.

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

FileName [saigRetMin.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Min-area retiming for the AIG.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

saigRetMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis [Derives the initial state after backward retiming.]

Description []

SideEffects []

SeeAlso []

Definition at line 50 of file saigRetMin.c.

{
    int nConfLimit = 1000000;
    Vec_Int_t * vCiIds, * vInit = NULL;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Aig_Obj_t * pObj;
    int i, RetValue, * pModel;
    // solve the SAT problem
    pCnf = Cnf_DeriveSimpleForRetiming( p );
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    if ( pSat == NULL )
    {
        Cnf_DataFree( pCnf );
        return NULL;
    }
    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    assert( RetValue != l_Undef );
    // create counter-example
    if ( RetValue == l_True )
    {
        // accumulate SAT variables of the CIs
        vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
        Aig_ManForEachCi( 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_ManCiNum(p) );
        Vec_IntFree( vCiIds );
    }
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    return vInit;
}

Aig_Man_t* Saig_ManRetimeMinArea	(	Aig_Man_t *	p,
		int	nMaxIters,
		int	fForwardOnly,
		int	fBackwardOnly,
		int	fInitial,
		int	fVerbose
	)

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

Synopsis [Performs min-area retiming.]

Description []

SideEffects []

SeeAlso []

Definition at line 623 of file saigRetMin.c.

{
    Vec_Ptr_t * vCut;
    Aig_Man_t * pNew, * pTemp, * pCopy;
    int i, fChanges;
    pNew = Aig_ManDupSimple( p );
    // perform several iterations of forward retiming
    fChanges = 0;
    if ( !fBackwardOnly )
    for ( i = 0; i < nMaxIters; i++ )
    {
        if ( Saig_ManRegNum(pNew) == 0 )
            break;
        vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
        if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
        {
            if ( fVerbose && !fChanges )
                printf( "Forward retiming cannot reduce registers.\n" );
            Vec_PtrFree( vCut );
            break;
        }
        pNew = Saig_ManRetimeDupForward( pTemp = pNew, vCut );
        Aig_ManStop( pTemp );
        Vec_PtrFree( vCut );
        if ( fVerbose )
            Aig_ManReportImprovement( p, pNew );
        fChanges = 1;
    }
    // perform several iterations of backward retiming
    fChanges = 0;
    if ( !fForwardOnly && !fInitial )
    for ( i = 0; i < nMaxIters; i++ )
    {
        if ( Saig_ManRegNum(pNew) == 0 )
            break;
        vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
        if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
        {
            if ( fVerbose && !fChanges )
                printf( "Backward retiming cannot reduce registers.\n" );
            Vec_PtrFree( vCut );
            break;
        }
        pNew = Saig_ManRetimeDupBackward( pTemp = pNew, vCut, NULL );
        Aig_ManStop( pTemp );
        Vec_PtrFree( vCut );
        if ( fVerbose )
            Aig_ManReportImprovement( p, pNew );
        fChanges = 1;
    }
    else if ( !fForwardOnly && fInitial )
    for ( i = 0; i < nMaxIters; i++ )
    {
        if ( Saig_ManRegNum(pNew) == 0 )
            break;
        pCopy = Aig_ManDupSimple( pNew );
        pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
        Aig_ManStop( pCopy );
        if ( pTemp == NULL )
        {
            if ( fVerbose && !fChanges )
                printf( "Backward retiming cannot reduce registers.\n" );
            break;
        }
        Saig_ManExposeBadRegs( pTemp, Saig_ManPoNum(pTemp) - Saig_ManPoNum(pNew) );
        Aig_ManStop( pNew );
        pNew = pTemp;
        if ( fVerbose )
            Aig_ManReportImprovement( p, pNew );
        fChanges = 1;
    }
    if ( !fForwardOnly && !fInitial && fChanges )
        printf( "Assuming const-0 init-state after backward retiming. Result will not verify.\n" );
    return pNew;
}

Aig_Man_t* Saig_ManRetimeMinAreaBackward	(	Aig_Man_t *	pNew,
		int	fVerbose
	)

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

Synopsis [Performs min-area retiming backward with initial state.]

Description []

SideEffects []

SeeAlso []

Definition at line 567 of file saigRetMin.c.

{
    Aig_Man_t * pInit, * pFinal;
    Vec_Ptr_t * vBadRegs, * vCut;
    Vec_Int_t * vInit;
    int iBadReg;
    // transform the AIG to have no bad registers
    vBadRegs = Saig_ManGetRegistersToExclude( pNew );
    if ( fVerbose && Vec_PtrSize(vBadRegs) )
        printf( "Excluding %d registers that cannot be backward retimed.\n", Vec_PtrSize(vBadRegs) ); 
    while ( 1 )
    {
        Saig_ManHideBadRegs( pNew, vBadRegs );
        Vec_PtrFree( vBadRegs );
        // compute cut
        vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
        if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
        {
            Vec_PtrFree( vCut );
            return NULL;
        }
        // derive the initial state
        pInit = Saig_ManRetimeDupInitState( pNew, vCut );
        vInit = Saig_ManRetimeInitState( pInit );
        if ( vInit != NULL )
        {
            pFinal = Saig_ManRetimeDupBackward( pNew, vCut, vInit );
            Vec_IntFree( vInit );
            Vec_PtrFree( vCut );
            Aig_ManStop( pInit );
            return pFinal;
        }
        Vec_PtrFree( vCut );
        // there is no initial state - find the offending output
        iBadReg = Saig_ManRetimeUnsatCore( pInit, fVerbose );
        Aig_ManStop( pInit );
        if ( fVerbose )
            printf( "Excluding register %d.\n", iBadReg ); 
        // prepare to remove this output
        vBadRegs = Vec_PtrAlloc( 1 );
        Vec_PtrPush( vBadRegs, Aig_ManCo( pNew, Saig_ManPoNum(pNew) + iBadReg ) );
    }
    return NULL;
}

int Saig_ManRetimeUnsatCore	(	Aig_Man_t *	p,
		int	fVerbose
	)

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

Synopsis [Uses UNSAT core to find the part of AIG to be excluded.]

Description [Returns the number of the PO that appears in the UNSAT core.]

SideEffects []

SeeAlso []

Definition at line 96 of file saigRetMin.c.

{
    int fVeryVerbose = 0;
    int nConfLimit = 1000000;
    void * pSatCnf = NULL; 
    Intp_Man_t * pManProof;
    Vec_Int_t * vCore = NULL;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    Aig_Obj_t * pObj;
    int * pClause1, * pClause2, * pLit, * pVars;
    int i, RetValue, iBadPo, iClause, nVars, nPos;
    // create the SAT solver
    pCnf = Cnf_DeriveSimpleForRetiming( p );
    pSat = sat_solver_new();
    sat_solver_store_alloc( pSat ); 
    sat_solver_setnvars( pSat, pCnf->nVars );
    for ( i = 0; i < pCnf->nClauses; i++ )
    {
        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
        {
            Cnf_DataFree( pCnf );
            sat_solver_delete( pSat );
            return -1;
        }
    }
    sat_solver_store_mark_roots( pSat ); 
    // solve the problem
    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    assert( RetValue != l_Undef );
    assert( RetValue == l_False );
    pSatCnf = sat_solver_store_release( pSat ); 
    sat_solver_delete( pSat );
    // derive the UNSAT core
    pManProof = Intp_ManAlloc();
    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, fVeryVerbose );
    Intp_ManFree( pManProof );
    Sto_ManFree( (Sto_Man_t *)pSatCnf );
    // derive the set of variables on which the core depends
    // collect the variable numbers
    nVars = 0;
    pVars = ABC_ALLOC( int, pCnf->nVars );
    memset( pVars, 0, sizeof(int) * pCnf->nVars );
    Vec_IntForEachEntry( vCore, iClause, i )
    {
        pClause1 = pCnf->pClauses[iClause];
        pClause2 = pCnf->pClauses[iClause+1];
        for ( pLit = pClause1; pLit < pClause2; pLit++ )
        {
            if ( pVars[ (*pLit) >> 1 ] == 0 )
                nVars++;
            pVars[ (*pLit) >> 1 ] = 1;
            if ( fVeryVerbose )
            printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
        }
        if ( fVeryVerbose )
        printf( "\n" );
    }
    // collect the nodes
    if ( fVeryVerbose ) {
      Aig_ManForEachObj( p, pObj, i )
          if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
          {
              Aig_ObjPrint( p, pObj );
              printf( "\n" );
          }
    }
    // pick the first PO in the list
    nPos = 0;
    iBadPo = -1;
    Aig_ManForEachCo( p, pObj, i )
        if ( pCnf->pVarNums[pObj->Id] >= 0 && pVars[ pCnf->pVarNums[pObj->Id] ] == 1 )
        {
            if ( iBadPo == -1 )
                iBadPo = i;
            nPos++;
        }
    if ( fVerbose )
        printf( "UNSAT core: %d clauses, %d variables, %d POs.  ", Vec_IntSize(vCore), nVars, nPos );
    ABC_FREE( pVars );
    Vec_IntFree( vCore );
    Cnf_DataFree( pCnf );
    return iBadPo;
}