src/opt/lpk/lpkMap.c File Reference

#include "lpkInt.h"

Include dependency graph for lpkMap.c:

Go to the source code of this file.

Functions
If_Obj_t *	Lpk_MapPrimeInternal (If_Man_t *pIfMan, Kit_Graph_t *pGraph)
If_Obj_t *	Lpk_MapPrime (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
If_Obj_t *	Lpk_MapTree_rec (Lpk_Man_t *p, Kit_DsdNtk_t *pNtk, If_Obj_t **ppLeaves, int iLit, If_Obj_t *pResult)

---

Function Documentation

If_Obj_t* Lpk_MapPrime	(	Lpk_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		If_Obj_t **	ppLeaves
	)

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

Synopsis [Strashes one logic node using its SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file lpkMap.c.

{
    Kit_Graph_t * pGraph;
    Kit_Node_t * pNode;
    If_Obj_t * pRes;
    int i;
    // derive the factored form
    pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover );
    if ( pGraph == NULL )
        return NULL;
    // collect the fanins
    Kit_GraphForEachLeaf( pGraph, pNode, i )
        pNode->pFunc = ppLeaves[i];
    // perform strashing
    pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph );
    pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) );
    Kit_GraphFree( pGraph );
    return pRes;
}

If_Obj_t* Lpk_MapPrimeInternal	(	If_Man_t *	pIfMan,
		Kit_Graph_t *	pGraph
	)

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

FileName [lpkMap.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id

lpkMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

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

Synopsis [Transforms the decomposition graph into the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 42 of file lpkMap.c.

{
    Kit_Node_t * pNode;
    If_Obj_t * pAnd0, * pAnd1;
    int i;
    // check for constant function
    if ( Kit_GraphIsConst(pGraph) )
        return If_ManConst1(pIfMan);
    // check for a literal
    if ( Kit_GraphIsVar(pGraph) )
        return Kit_GraphVar(pGraph)->pFunc;
    // build the AIG nodes corresponding to the AND gates of the graph
    Kit_GraphForEachNode( pGraph, pNode, i )
    {
        pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; 
        pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; 
        pNode->pFunc = If_ManCreateAnd( pIfMan, 
            If_NotCond( If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl ), 
            If_NotCond( If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ) );
    }
    return pNode->pFunc;
}

If_Obj_t* Lpk_MapTree_rec	(	Lpk_Man_t *	p,
		Kit_DsdNtk_t *	pNtk,
		If_Obj_t **	ppLeaves,
		int	iLit,
		If_Obj_t *	pResult
	)

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

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file lpkMap.c.

{
    Kit_DsdObj_t * pObj;
    If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
    unsigned i, iLitFanin;

    assert( iLit >= 0 );

    // consider the case of a gate
    pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) );
    if ( pObj == NULL )
    {
        pObjNew = ppLeaves[Kit_DsdLit2Var(iLit)];
        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
    }
    if ( pObj->Type == KIT_DSD_CONST1 )
    {
        return If_NotCond( If_ManConst1(p->pIfMan), Kit_DsdLitIsCompl(iLit) );
    }
    if ( pObj->Type == KIT_DSD_VAR )
    {
        pObjNew = ppLeaves[Kit_DsdLit2Var(pObj->pFans[0])];
        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ^ Kit_DsdLitIsCompl(pObj->pFans[0]) );
    }
    if ( pObj->Type == KIT_DSD_AND )
    {
        assert( pObj->nFans == 2 );
        pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
        pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
            return NULL;
        pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] ); 
        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
    }
    if ( pObj->Type == KIT_DSD_XOR )
    {
        int fCompl = Kit_DsdLitIsCompl(iLit);
        assert( pObj->nFans == 2 );
        pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL );
        pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL );
        if ( pFansNew[0] == NULL || pFansNew[1] == NULL )
            return NULL;
        fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]);
        pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) );
        return If_NotCond( pObjNew, fCompl );
    }
    assert( pObj->Type == KIT_DSD_PRIME );
    p->nBlocks[pObj->nFans]++;

    // solve for the inputs
    Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i )
    {
        if ( i == 0 )
            pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
        else
            pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL );
        if ( pFansNew[i] == NULL )
            return NULL;
    }
/* 
    if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
    {
        pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
        return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
    }
*/
/*
    if ( (int)pObj->nFans > p->pPars->nLutSize )
    {
        pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
//        if ( pObjNew2 )
//            return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
    }
*/

    // find best cofactoring variable
    if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
    {
        pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
        if ( pObjNew2 )
            return If_NotCond( pObjNew2, Kit_DsdLitIsCompl(iLit) );
    }

    pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );

    // add choice
    if ( pObjNew && pObjNew2 )
    {
        If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
        If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
    }
    return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) );
}