mfsStrash.c File Reference

#include "mfsInt.h"
#include "proof/fra/fra.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Abc_MfsConvertAigToHop_rec (Aig_Obj_t *pObj, Hop_Man_t *pHop)
	DECLARATIONS ///. More...
Hop_Obj_t *	Abc_MfsConvertAigToHop (Aig_Man_t *pMan, Hop_Man_t *pHop)
void	Abc_MfsConvertHopToAig_rec (Hop_Obj_t *pObj, Aig_Man_t *pMan)
void	Abc_MfsConvertHopToAig (Abc_Obj_t *pObjOld, Aig_Man_t *pMan)
Aig_Obj_t *	Abc_NtkConstructAig_rec (Mfs_Man_t *p, Abc_Obj_t *pNode, Aig_Man_t *pMan)
Aig_Obj_t *	Abc_NtkConstructCare_rec (Aig_Man_t *pCare, Aig_Obj_t *pObj, Aig_Man_t *pMan)
Aig_Man_t *	Abc_NtkConstructAig (Mfs_Man_t *p, Abc_Obj_t *pNode)
Aig_Man_t *	Abc_NtkAigForConstraints (Mfs_Man_t *p, Abc_Obj_t *pNode)
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START double	Abc_NtkConstraintRatio (Mfs_Man_t *p, Abc_Obj_t *pNode)

Function Documentation

Hop_Obj_t* Abc_MfsConvertAigToHop	(	Aig_Man_t *	pMan,
		Hop_Man_t *	pHop
	)

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

Synopsis [Converts AIG from Aig_Man_t into Hop_Obj_t.]

Description [Assumes that Aig_Man_t has exactly one primary outputs. Returns the pointer to the root node (Hop_Obj_t) in Hop_Man_t.]

SideEffects []

SeeAlso []

Definition at line 67 of file mfsStrash.c.

{
    Aig_Obj_t * pRoot, * pObj;
    int i;
    assert( Aig_ManCoNum(pMan) == 1 );
    pRoot = Aig_ManCo( pMan, 0 );
    // check the case of a constant
    if ( Aig_ObjIsConst1( Aig_ObjFanin0(pRoot) ) )
        return Hop_NotCond( Hop_ManConst1(pHop), Aig_ObjFaninC0(pRoot) );
    // set the PI mapping
    Aig_ManCleanData( pMan );
    Aig_ManForEachCi( pMan, pObj, i )
        pObj->pData = Hop_IthVar( pHop, i );
    // construct the AIG
    Abc_MfsConvertAigToHop_rec( Aig_ObjFanin0(pRoot), pHop );
    return Hop_NotCond( (Hop_Obj_t *)Aig_ObjFanin0(pRoot)->pData, Aig_ObjFaninC0(pRoot) );
}

ABC_NAMESPACE_IMPL_START void Abc_MfsConvertAigToHop_rec	(	Aig_Obj_t *	pObj,
		Hop_Man_t *	pHop
	)

DECLARATIONS ///.

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

FileName [mfsStrash.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The good old minimization with complete don't-cares.]

Synopsis [Structural hashing of the window with ODCs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

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

Synopsis [Recursively converts AIG from Aig_Man_t into Hop_Obj_t.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file mfsStrash.c.

{
    assert( !Aig_IsComplement(pObj) );
    if ( pObj->pData )
        return;
    Abc_MfsConvertAigToHop_rec( Aig_ObjFanin0(pObj), pHop ); 
    Abc_MfsConvertAigToHop_rec( Aig_ObjFanin1(pObj), pHop );
    pObj->pData = Hop_And( pHop, (Hop_Obj_t *)Aig_ObjChild0Copy(pObj), (Hop_Obj_t *)Aig_ObjChild1Copy(pObj) ); 
    assert( !Hop_IsComplement((Hop_Obj_t *)pObj->pData) );
}

void Abc_MfsConvertHopToAig	(	Abc_Obj_t *	pObjOld,
		Aig_Man_t *	pMan
	)

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

Synopsis [Converts the network from AIG to BDD representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file mfsStrash.c.

{
    Hop_Man_t * pHopMan;
    Hop_Obj_t * pRoot;
    Abc_Obj_t * pFanin;
    int i;
    // get the local AIG
    pHopMan = (Hop_Man_t *)pObjOld->pNtk->pManFunc;
    pRoot = (Hop_Obj_t *)pObjOld->pData;
    // check the case of a constant
    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
    {
        pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Aig_ManConst1(pMan), Hop_IsComplement(pRoot) );
        pObjOld->pNext = pObjOld->pCopy;
        return;
    }

    // assign the fanin nodes
    Abc_ObjForEachFanin( pObjOld, pFanin, i )
        Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
    // construct the AIG
    Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
    pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( (Aig_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );

    // assign the fanin nodes
    Abc_ObjForEachFanin( pObjOld, pFanin, i )
        Hop_ManPi(pHopMan, i)->pData = pFanin->pNext;
    // construct the AIG
    Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
    pObjOld->pNext = (Abc_Obj_t *)Aig_NotCond( (Aig_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
}

void Abc_MfsConvertHopToAig_rec	(	Hop_Obj_t *	pObj,
		Aig_Man_t *	pMan
	)

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

Synopsis [Construct BDDs and mark AIG nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file mfsStrash.c.

{
    assert( !Hop_IsComplement(pObj) );
    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
        return;
    Abc_MfsConvertHopToAig_rec( Hop_ObjFanin0(pObj), pMan ); 
    Abc_MfsConvertHopToAig_rec( Hop_ObjFanin1(pObj), pMan );
    pObj->pData = Aig_And( pMan, (Aig_Obj_t *)Hop_ObjChild0Copy(pObj), (Aig_Obj_t *)Hop_ObjChild1Copy(pObj) ); 
    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
    Hop_ObjSetMarkA( pObj );
}

Aig_Man_t* Abc_NtkAigForConstraints	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Creates AIG for the window with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 325 of file mfsStrash.c.

{
    Abc_Obj_t * pFanin;
    Aig_Man_t * pMan;
    Aig_Obj_t * pPi, * pPo, * pObjAig, * pObjRoot;
    Vec_Int_t * vOuts;
    int i, k, iOut;
    if ( p->pCare == NULL )
        return NULL;
    pMan = Aig_ManStart( 1000 );
    // mark the care set
    Aig_ManIncrementTravId( p->pCare );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
    {
        pPi = Aig_ManCi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
        Aig_ObjSetTravIdCurrent( p->pCare, pPi );
        pPi->pData = Aig_ObjCreateCi(pMan);
    }
    // construct the constraints
    pObjRoot = Aig_ManConst1(pMan);
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
    {
        vOuts = (Vec_Int_t *)Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
        Vec_IntForEachEntry( vOuts, iOut, k )
        {
            pPo = Aig_ManCo( p->pCare, iOut );
            if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
                continue;
            Aig_ObjSetTravIdCurrent( p->pCare, pPo );
            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
                continue;
            pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
            if ( pObjAig == NULL )
                continue;
            pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
            pObjRoot = Aig_And( pMan, pObjRoot, pObjAig );
        }
    }
    Aig_ObjCreateCo( pMan, pObjRoot );
    Aig_ManCleanup( pMan );
    return pMan;
}

ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START double Abc_NtkConstraintRatio	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Compute the ratio of don't-cares.]

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file mfsStrash.c.

{
    int nSimWords = 256;
    Aig_Man_t * pMan;
    Fra_Sml_t * pSim;
    int Counter;
    pMan = Abc_NtkAigForConstraints( p, pNode );
    pSim = Fra_SmlSimulateComb( pMan, nSimWords, 0 );
    Counter = Fra_SmlNodeCountOnes( pSim, Aig_ManCo(pMan, 0) );
    Aig_ManStop( pMan );
    Fra_SmlStop( pSim );
    return 1.0 * Counter / (32 * nSimWords);
}

Aig_Man_t* Abc_NtkConstructAig	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode
	)

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

Synopsis [Creates AIG for the window with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file mfsStrash.c.

{
    Aig_Man_t * pMan;
    Abc_Obj_t * pFanin;
    Aig_Obj_t * pObjAig, * pPi, * pPo;
    Vec_Int_t * vOuts;
    int i, k, iOut;
    // start the new manager
    pMan = Aig_ManStart( 1000 );
    // construct the root node's AIG cone
    pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
//    assert( Aig_ManConst1(pMan) == pObjAig );
    Aig_ObjCreateCo( pMan, pObjAig );
    if ( p->pCare )
    {
        // mark the care set
        Aig_ManIncrementTravId( p->pCare );
        Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
        {
            pPi = Aig_ManCi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
            Aig_ObjSetTravIdCurrent( p->pCare, pPi );
            pPi->pData = pFanin->pCopy;
        }
        // construct the constraints
        Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
        {
            vOuts = (Vec_Int_t *)Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
            Vec_IntForEachEntry( vOuts, iOut, k )
            {
                pPo = Aig_ManCo( p->pCare, iOut );
                if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
                    continue;
                Aig_ObjSetTravIdCurrent( p->pCare, pPo );
                if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
                    continue;
                pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
                if ( pObjAig == NULL )
                    continue;
                pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
                Aig_ObjCreateCo( pMan, pObjAig );
            }
        }
/*
        Aig_ManForEachCo( p->pCare, pPo, i )
        {
//            assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
                continue;
            pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
            if ( pObjAig == NULL )
                continue;
            pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
            Aig_ObjCreateCo( pMan, pObjAig );
        }
*/
    }
    if ( p->pPars->fResub )
    {
        // construct the node
        pObjAig = (Aig_Obj_t *)pNode->pCopy;
        Aig_ObjCreateCo( pMan, pObjAig );
        // construct the divisors
        Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pFanin, i )
        {
            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
            Aig_ObjCreateCo( pMan, pObjAig );
        }
    }
    else
    {
        // construct the fanins
        Abc_ObjForEachFanin( pNode, pFanin, i )
        {
            pObjAig = (Aig_Obj_t *)pFanin->pCopy;
            Aig_ObjCreateCo( pMan, pObjAig );
        }
    }
    Aig_ManCleanup( pMan );
    return pMan;
}

Aig_Obj_t* Abc_NtkConstructAig_rec	(	Mfs_Man_t *	p,
		Abc_Obj_t *	pNode,
		Aig_Man_t *	pMan
	)

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

Synopsis [Computes the care set of the node under ODCs.]

Description []

SideEffects []

SeeAlso []

Definition at line 166 of file mfsStrash.c.

{
    Aig_Obj_t * pRoot, * pExor;
    Abc_Obj_t * pObj;
    int i;
    // assign AIG nodes to the leaves
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pObj, i )
        pObj->pCopy = pObj->pNext = (Abc_Obj_t *)Aig_ObjCreateCi( pMan );
    // strash intermediate nodes
    Abc_NtkIncrementTravId( pNode->pNtk );
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pObj, i )
    {
        Abc_MfsConvertHopToAig( pObj, pMan );
        if ( pObj == pNode )
            pObj->pNext = Abc_ObjNot(pObj->pNext);
    }
    // create the observability condition
    pRoot = Aig_ManConst0(pMan);
    Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
    {
        pExor = Aig_Exor( pMan, (Aig_Obj_t *)pObj->pCopy, (Aig_Obj_t *)pObj->pNext );
        pRoot = Aig_Or( pMan, pRoot, pExor );
    }
    return pRoot;
}

Aig_Obj_t* Abc_NtkConstructCare_rec	(	Aig_Man_t *	pCare,
		Aig_Obj_t *	pObj,
		Aig_Man_t *	pMan
	)

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

Synopsis [Adds relevant constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file mfsStrash.c.

{
    Aig_Obj_t * pObj0, * pObj1;
    if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
        return (Aig_Obj_t *)pObj->pData;
    Aig_ObjSetTravIdCurrent( pCare, pObj );
    if ( Aig_ObjIsCi(pObj) )
        return (Aig_Obj_t *)(pObj->pData = NULL);
    pObj0 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan );
    if ( pObj0 == NULL )
        return (Aig_Obj_t *)(pObj->pData = NULL);
    pObj1 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan );
    if ( pObj1 == NULL )
        return (Aig_Obj_t *)(pObj->pData = NULL);
    pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
    pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) );
    return (Aig_Obj_t *)(pObj->pData = Aig_And( pMan, pObj0, pObj1 ));
}