wlcPth.c File Reference

#include "wlc.h"
#include "sat/bmc/bmc.h"

Include dependency graph for wlcPth.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START Abc_Ntk_t *	Abc_NtkFromAigPhase (Aig_Man_t *pAig)
	DECLARATIONS ///.
int	Abc_NtkDarBmc3 (Abc_Ntk_t *pAbcNtk, Saig_ParBmc_t *pBmcPars, int fOrDecomp)
int	Wla_ManShrinkAbs (Wla_Man_t *pWla, int nFrames, int RunId)
int	Wla_CallBackToStop (int RunId)
int	Wla_GetGlobalRunId ()
void	Wla_ManJoinThread (Wla_Man_t *pWla, int RunId)
void	Wla_ManConcurrentBmc3 (Wla_Man_t *pWla, Aig_Man_t *pAig, Abc_Cex_t **ppCex)

Function Documentation

Abc_NtkDarBmc3()

int Abc_NtkDarBmc3 ( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )

extern

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 2449 of file abcDar.c.

{
    Aig_Man_t * pMan;
    Vec_Int_t * vMap = NULL;
    int status, RetValue = -1;
    abctime clk = Abc_Clock();
    abctime nTimeOut = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
    if ( fOrDecomp && !pPars->fSolveAll )
        pMan = Abc_NtkToDarBmc( pNtk, &vMap );
    else
        pMan = Abc_NtkToDar( pNtk, 0, 1 );
    if ( pMan == NULL )
    {
        Abc_Print( 1, "Converting miter into AIG has failed.\n" );
        return RetValue;
    }
    assert( pMan->nRegs > 0 );
    if ( pPars->fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) ) 
        Abc_Print( 1, "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
 
    RetValue = Saig_ManBmcScalable( pMan, pPars );
    ABC_FREE( pNtk->pModel );
    ABC_FREE( pNtk->pSeqModel );
    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
    if ( !pPars->fSilent )
    {
        if ( RetValue == 1 )
        {
            Abc_Print( 1, "Explored all reachable states after completing %d frames.  ", 1<<Aig_ManRegNum(pMan) );
        }
        else if ( RetValue == -1 )
        {
            if ( pPars->nFailOuts == 0 )
            {
                Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame+1,0) );
                if ( nTimeOut && Abc_Clock() > nTimeOut )
                    Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
                else
                    Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
            }
            else
            {
                Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
                if ( Abc_Clock() > nTimeOut )
                    Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
                else
                    Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
            }
        }
        else // if ( RetValue == 0 )
        {
            if ( !pPars->fSolveAll )
            {
                Abc_Cex_t * pCex = pNtk->pSeqModel;
                Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
            }
            else
            {
                int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
                if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
                    Abc_Print( 1, "None of the %d outputs is found to be SAT", nOutputs );
                else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
                    Abc_Print( 1, "All %d outputs are found to be SAT", nOutputs );
                else
                {
                    Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
                    if ( pPars->nDropOuts )
                        Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
                }
                Abc_Print( 1, " after %d frames", pPars->iFrame+2 );
                Abc_Print( 1, ".   " );
            }
        }
        ABC_PRT( "Time", Abc_Clock() - clk );
    }
    if ( RetValue == 0 && pPars->fSolveAll )
    {
        if ( pNtk->vSeqModelVec )
            Vec_PtrFreeFree( pNtk->vSeqModelVec );
        pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
    }
    if ( pNtk->pSeqModel ) 
    {
        status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );
        if ( status == 0 )
            Abc_Print( 1, "Abc_NtkDarBmc3(): Counter-example verification has FAILED.\n" );
    }
    Aig_ManStop( pMan );
    // update the counter-example
    if ( pNtk->pSeqModel && vMap )
        pNtk->pSeqModel->iPo = Vec_IntEntry( vMap, pNtk->pSeqModel->iPo );
    Vec_IntFreeP( &vMap );
    return RetValue;
}

Here is the call graph for this function:

Abc_NtkFromAigPhase()

ABC_NAMESPACE_IMPL_START Abc_Ntk_t * Abc_NtkFromAigPhase ( Aig_Man_t * pMan )

extern

DECLARATIONS ///.

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

FileName [wlcPth.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Verilog parser.]

Synopsis [Abstraction for word-level networks.]

Author [Yen-Sheng Ho, Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

wlcPth.c

]

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

Synopsis [Converts the network from the AIG manager into ABC.]

Description [This procedure should be called after seq sweeping, which changes the number of registers.]

SideEffects []

SeeAlso []

Definition at line 595 of file abcDar.c.

{
    Vec_Ptr_t * vNodes; 
    Abc_Ntk_t * pNtkNew;
    Abc_Obj_t * pObjNew;
    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
    int i; 
    assert( pMan->nAsserts == 0 );
    // perform strashing
    pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
    pNtkNew->nConstrs = pMan->nConstrs;
    pNtkNew->nBarBufs = pMan->nBarBufs;
    // duplicate the name and the spec
//    pNtkNew->pName = Extra_UtilStrsav(pMan->pName);
//    pNtkNew->pSpec = Extra_UtilStrsav(pMan->pSpec);
    Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew);
    // create PIs
    Aig_ManForEachPiSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePi( pNtkNew );
//        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
        pObj->pData = pObjNew;
    }
    // create POs
    Aig_ManForEachPoSeq( pMan, pObj, i )
    {
        pObjNew = Abc_NtkCreatePo( pNtkNew );
//        Abc_ObjAssignName( pObjNew, Abc_ObjName(pObjNew), NULL );
        pObj->pData = pObjNew;
    }
    assert( Abc_NtkCiNum(pNtkNew) == Aig_ManCiNum(pMan) - Aig_ManRegNum(pMan) );
    assert( Abc_NtkCoNum(pNtkNew) == Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) );
    // create as many latches as there are registers in the manager
    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
    {
        pObjNew = Abc_NtkCreateLatch( pNtkNew );
        pObjLi->pData = Abc_NtkCreateBi( pNtkNew );
        pObjLo->pData = Abc_NtkCreateBo( pNtkNew );
        Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)pObjLi->pData );
        Abc_ObjAddFanin( (Abc_Obj_t *)pObjLo->pData, pObjNew );
        Abc_LatchSetInit0( pObjNew );
//        Abc_ObjAssignName( (Abc_Obj_t *)pObjLi->pData, Abc_ObjName((Abc_Obj_t *)pObjLi->pData), NULL );
//        Abc_ObjAssignName( (Abc_Obj_t *)pObjLo->pData, Abc_ObjName((Abc_Obj_t *)pObjLo->pData), NULL );
    }
    // rebuild the AIG
    vNodes = Aig_ManDfs( pMan, 1 );
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
        if ( Aig_ObjIsBuf(pObj) )
            pObj->pData = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        else
            pObj->pData = Abc_AigAnd( (Abc_Aig_t *)pNtkNew->pManFunc, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj), (Abc_Obj_t *)Aig_ObjChild1Copy(pObj) );
    Vec_PtrFree( vNodes );
    // connect the PO nodes
    Aig_ManForEachCo( pMan, pObj, i )
    {
        pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
        Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
    }
 
    Abc_NtkAddDummyPiNames( pNtkNew );
    Abc_NtkAddDummyPoNames( pNtkNew );
    Abc_NtkAddDummyBoxNames( pNtkNew );
 
    // check the resulting AIG
    if ( !Abc_NtkCheck( pNtkNew ) )
        Abc_Print( 1, "Abc_NtkFromAigPhase(): Network check has failed.\n" );
    return pNtkNew;
}

Wla_CallBackToStop()

int Wla_CallBackToStop

(

int

RunId

)

Definition at line 46 of file wlcPth.c.

{ assert( RunId <= g_nRunIds ); return RunId < g_nRunIds; }

Here is the caller graph for this function:

Wla_GetGlobalRunId()

int Wla_GetGlobalRunId

(

)

Definition at line 47 of file wlcPth.c.

{ return g_nRunIds; }

Here is the caller graph for this function:

Wla_ManConcurrentBmc3()

void Wla_ManConcurrentBmc3	(	Wla_Man_t *	pWla,
		Aig_Man_t *	pAig,
		Abc_Cex_t **	ppCex )

Definition at line 52 of file wlcPth.c.

{}

Here is the caller graph for this function:

Wla_ManJoinThread()

void Wla_ManJoinThread	(	Wla_Man_t *	pWla,
		int	RunId )

Definition at line 51 of file wlcPth.c.

{}

Here is the caller graph for this function:

Wla_ManShrinkAbs()

int Wla_ManShrinkAbs ( Wla_Man_t * pWla, int nFrames, int RunId )

extern

Definition at line 1350 of file wlcAbs.c.

{
    int i, Entry;
    int RetValue = 0;
 
    Vec_Int_t * vWhites = Wla_ManCollectNodes( pWla, 0 );
    Vec_Int_t * vBlacks = Wla_ManCollectNodes( pWla, 1 );
    Vec_Bit_t * vCoreMarks = Wlc_NtkProofReduce( pWla->p, pWla->pPars, nFrames, vWhites, vBlacks, RunId );
 
    if ( vCoreMarks == NULL )
    {
        Vec_IntFree( vWhites );
        Vec_IntFree( vBlacks );
        return -1;
    }
 
    RetValue = Vec_IntSize( vWhites ) != Vec_BitCount( vCoreMarks );
 
    Vec_IntForEachEntry( vWhites, Entry, i )
        if ( !Vec_BitEntry( vCoreMarks, i ) )
            Vec_BitWriteEntry( pWla->vUnmark, Entry, 0 );
 
    Vec_IntFree( vWhites );
    Vec_IntFree( vBlacks );
    Vec_BitFree( vCoreMarks );
 
    return RetValue;
}

Here is the call graph for this function: