covCore.c File Reference

#include "cov.h"

Go to the source code of this file.

Functions
static ABC_NAMESPACE_IMPL_START void	Abc_NtkCovCovers (Cov_Man_t *p, Abc_Ntk_t *pNtk, int fVerbose)
	DECLARATIONS ///. More...
static int	Abc_NtkCovCoversOne (Cov_Man_t *p, Abc_Ntk_t *pNtk, int fVerbose)
static void	Abc_NtkCovCovers_rec (Cov_Man_t *p, Abc_Obj_t *pObj, Vec_Ptr_t *vBoundary)
static int	Abc_NodeCovPropagate (Cov_Man_t *p, Abc_Obj_t *pObj)
static Min_Cube_t *	Abc_NodeCovProduct (Cov_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1, int fEsop, int nSupp)
static Min_Cube_t *	Abc_NodeCovSum (Cov_Man_t *p, Min_Cube_t *pCover0, Min_Cube_t *pCover1, int fEsop, int nSupp)
Abc_Ntk_t *	Abc_NtkSopEsopCover (Abc_Ntk_t *pNtk, int nFaninMax, int fUseEsop, int fUseSop, int fUseInvs, int fVerbose)
	FUNCTION DEFINITIONS ///. More...
Vec_Int_t *	Abc_NodeCovSupport (Cov_Man_t *p, Vec_Int_t *vSupp0, Vec_Int_t *vSupp1)

Function Documentation

Min_Cube_t * Abc_NodeCovProduct ( Cov_Man_t *  p, Min_Cube_t *  pCover0, Min_Cube_t *  pCover1, int  fEsop, int  nSupp  )

static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 469 of file covCore.c.

{
    Min_Cube_t * pCube, * pCube0, * pCube1;
    Min_Cube_t * pCover;
    int i, Val0, Val1;
    assert( pCover0 && pCover1 );

    // clean storage
    Min_ManClean( p->pManMin, nSupp );
    // go through the cube pairs
    Min_CoverForEachCube( pCover0, pCube0 )
    Min_CoverForEachCube( pCover1, pCube1 )
    {
        // go through the support variables of the cubes
        for ( i = 0; i < p->vPairs0->nSize; i++ )
        {
            Val0 = Min_CubeGetVar( pCube0, p->vPairs0->pArray[i] );
            Val1 = Min_CubeGetVar( pCube1, p->vPairs1->pArray[i] );
            if ( (Val0 & Val1) == 0 )
                break;
        }
        // check disjointness
        if ( i < p->vPairs0->nSize )
            continue;

        if ( p->pManMin->nCubes > p->nCubesMax )
        {
            pCover = Min_CoverCollect( p->pManMin, nSupp );
//Min_CoverWriteFile( pCover, "large", 1 );
            Min_CoverRecycle( p->pManMin, pCover );
            return NULL;
        }

        // create the product cube
        pCube = Min_CubeAlloc( p->pManMin );

        // add the literals
        pCube->nLits = 0;
        for ( i = 0; i < nSupp; i++ )
        {
            if ( p->vComTo0->pArray[i] == -1 )
                Val0 = 3;
            else
                Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );

            if ( p->vComTo1->pArray[i] == -1 )
                Val1 = 3;
            else
                Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );

            if ( (Val0 & Val1) == 3 )
                continue;

            Min_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 );
            pCube->nLits++;
        }
        // add the cube to storage
        if ( fEsop ) 
            Min_EsopAddCube( p->pManMin, pCube );
        else
            Min_SopAddCube( p->pManMin, pCube );
    }

    // minimize the cover
    if ( fEsop ) 
        Min_EsopMinimize( p->pManMin );
    else
        Min_SopMinimize( p->pManMin );
    pCover = Min_CoverCollect( p->pManMin, nSupp );

    // quit if the cover is too large
    if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
    {
/*        
Min_CoverWriteFile( pCover, "large", 1 );
        Min_CoverExpand( p->pManMin, pCover );
        Min_EsopMinimize( p->pManMin );
        Min_EsopMinimize( p->pManMin );
        Min_EsopMinimize( p->pManMin );
        Min_EsopMinimize( p->pManMin );
        Min_EsopMinimize( p->pManMin );
        Min_EsopMinimize( p->pManMin );
        Min_EsopMinimize( p->pManMin );
        Min_EsopMinimize( p->pManMin );
        Min_EsopMinimize( p->pManMin );
        pCover = Min_CoverCollect( p->pManMin, nSupp );
*/
        Min_CoverRecycle( p->pManMin, pCover );
        return NULL;
    }
    return pCover;
}

int Abc_NodeCovPropagate ( Cov_Man_t *  p, Abc_Obj_t *  pObj  )

static

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

Synopsis [Propagates all types of covers.]

Description []

SideEffects []

SeeAlso []

Definition at line 359 of file covCore.c.

{
    Min_Cube_t * pCoverP = NULL, * pCoverN = NULL, * pCoverX = NULL;
    Min_Cube_t * pCov0, * pCov1, * pCover0, * pCover1;
    Vec_Int_t * vSupp, * vSupp0, * vSupp1;
    Abc_Obj_t * pObj0, * pObj1;
    int fCompl0, fCompl1;

    pObj0 = Abc_ObjFanin0( pObj );
    pObj1 = Abc_ObjFanin1( pObj );

    if ( pObj0->fMarkA )  Vec_IntWriteEntry( p->vTriv0, 0, pObj0->Id );
    if ( pObj1->fMarkA )  Vec_IntWriteEntry( p->vTriv1, 0, pObj1->Id );
 
    // get the resulting support
    vSupp0 = pObj0->fMarkA? p->vTriv0 : Abc_ObjGetSupp(pObj0);
    vSupp1 = pObj1->fMarkA? p->vTriv1 : Abc_ObjGetSupp(pObj1);
    vSupp  = Abc_NodeCovSupport( p, vSupp0, vSupp1 );

    // quit if support if too large
    if ( vSupp->nSize > p->nFaninMax )
    {
        Vec_IntFree( vSupp );
        return 0;
    }

    // get the complemented attributes
    fCompl0 = Abc_ObjFaninC0( pObj );
    fCompl1 = Abc_ObjFaninC1( pObj );

    // propagate ESOP
    if ( p->fUseEsop )
    {
        // get the covers
        pCov0 = pObj0->fMarkA? p->pManMin->pTriv0[0] : Abc_ObjGetCover2(pObj0);
        pCov1 = pObj1->fMarkA? p->pManMin->pTriv1[0] : Abc_ObjGetCover2(pObj1);
        if ( pCov0 && pCov1 )
        {
            // complement the first if needed
            if ( !fCompl0 )
                pCover0 = pCov0;
            else if ( pCov0 && pCov0->nLits == 0 ) // topmost one is the tautology cube
                pCover0 = pCov0->pNext;
            else
                pCover0 = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCov0;

            // complement the second if needed
            if ( !fCompl1 )
                pCover1 = pCov1;
            else if ( pCov1 && pCov1->nLits == 0 ) // topmost one is the tautology cube
                pCover1 = pCov1->pNext;
            else
                pCover1 = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCov1;

            // derive the new cover
            pCoverX = Abc_NodeCovProduct( p, pCover0, pCover1, 1, vSupp->nSize );
        }
    }
    // propagate SOPs
    if ( p->fUseSop )
    {
        // get the covers for the direct polarity
        pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[fCompl0] : Abc_ObjGetCover(pObj0, fCompl0);
        pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[fCompl1] : Abc_ObjGetCover(pObj1, fCompl1);
        // derive the new cover
        if ( pCover0 && pCover1 )
            pCoverP = Abc_NodeCovProduct( p, pCover0, pCover1, 0, vSupp->nSize );

        // get the covers for the inverse polarity
        pCover0 = pObj0->fMarkA? p->pManMin->pTriv0[!fCompl0] : Abc_ObjGetCover(pObj0, !fCompl0);
        pCover1 = pObj1->fMarkA? p->pManMin->pTriv1[!fCompl1] : Abc_ObjGetCover(pObj1, !fCompl1);
        // derive the new cover
        if ( pCover0 && pCover1 )
            pCoverN = Abc_NodeCovSum( p, pCover0, pCover1, 0, vSupp->nSize );
    }

    // if none of the covers can be computed quit
    if ( !pCoverX && !pCoverP && !pCoverN )
    {
        Vec_IntFree( vSupp );
        return 0;
    }

    // set the covers
    assert( Abc_ObjGetSupp(pObj) == NULL );
    Abc_ObjSetSupp( pObj, vSupp );
    Abc_ObjSetCover( pObj, pCoverP, 0 );
    Abc_ObjSetCover( pObj, pCoverN, 1 );
    Abc_ObjSetCover2( pObj, pCoverX );
//printf( "%3d : %4d  %4d  %4d\n", pObj->Id, Min_CoverCountCubes(pCoverP), Min_CoverCountCubes(pCoverN), Min_CoverCountCubes(pCoverX) );

    // count statistics
    p->nSupps++;
    p->nSuppsMax = Abc_MaxInt( p->nSuppsMax, p->nSupps );
    return 1;
}

Min_Cube_t * Abc_NodeCovSum ( Cov_Man_t *  p, Min_Cube_t *  pCover0, Min_Cube_t *  pCover1, int  fEsop, int  nSupp  )

static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 573 of file covCore.c.

{
    Min_Cube_t * pCube, * pCube0, * pCube1;
    Min_Cube_t * pCover;
    int i, Val0, Val1;
    assert( pCover0 && pCover1 );

    // clean storage
    Min_ManClean( p->pManMin, nSupp );
    Min_CoverForEachCube( pCover0, pCube0 )
    {
        // create the cube
        pCube = Min_CubeAlloc( p->pManMin );
        pCube->nLits = 0;
        for ( i = 0; i < p->vComTo0->nSize; i++ )
        {
            if ( p->vComTo0->pArray[i] == -1 )
                continue;
            Val0 = Min_CubeGetVar( pCube0, p->vComTo0->pArray[i] );
            if ( Val0 == 3 )
                continue;
            Min_CubeXorVar( pCube, i, Val0 ^ 3 );
            pCube->nLits++;
        }
        if ( p->pManMin->nCubes > p->nCubesMax )
        {
            pCover = Min_CoverCollect( p->pManMin, nSupp );
            Min_CoverRecycle( p->pManMin, pCover );
            return NULL;
        }
        // add the cube to storage
        if ( fEsop )
            Min_EsopAddCube( p->pManMin, pCube );
        else
            Min_SopAddCube( p->pManMin, pCube );
    }
    Min_CoverForEachCube( pCover1, pCube1 )
    {
        // create the cube
        pCube = Min_CubeAlloc( p->pManMin );
        pCube->nLits = 0;
        for ( i = 0; i < p->vComTo1->nSize; i++ )
        {
            if ( p->vComTo1->pArray[i] == -1 )
                continue;
            Val1 = Min_CubeGetVar( pCube1, p->vComTo1->pArray[i] );
            if ( Val1 == 3 )
                continue;
            Min_CubeXorVar( pCube, i, Val1 ^ 3 );
            pCube->nLits++;
        }
        if ( p->pManMin->nCubes > p->nCubesMax )
        {
            pCover = Min_CoverCollect( p->pManMin, nSupp );
            Min_CoverRecycle( p->pManMin, pCover );
            return NULL;
        }
        // add the cube to storage
        if ( fEsop )
            Min_EsopAddCube( p->pManMin, pCube );
        else
            Min_SopAddCube( p->pManMin, pCube );
    }

    // minimize the cover
    if ( fEsop ) 
        Min_EsopMinimize( p->pManMin );
    else
        Min_SopMinimize( p->pManMin );
    pCover = Min_CoverCollect( p->pManMin, nSupp );

    // quit if the cover is too large
    if ( Min_CoverCountCubes(pCover) > p->nFaninMax )
    {
        Min_CoverRecycle( p->pManMin, pCover );
        return NULL;
    }
    return pCover;
}

Vec_Int_t* Abc_NodeCovSupport	(	Cov_Man_t *	p,
		Vec_Int_t *	vSupp0,
		Vec_Int_t *	vSupp1
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 282 of file covCore.c.

{
    Vec_Int_t * vSupp;
    int k0, k1;

    assert( vSupp0 && vSupp1 );
    Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 );
    Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 );
    Vec_IntClear( p->vPairs0 );
    Vec_IntClear( p->vPairs1 );

    vSupp = Vec_IntAlloc( vSupp0->nSize + vSupp1->nSize );
    for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; )
    {
        if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] )
        {
            Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
            Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
            Vec_IntPush( p->vPairs0, k0 );
            Vec_IntPush( p->vPairs1, k1 );
            Vec_IntPush( vSupp, vSupp0->pArray[k0] );
            k0++; k1++;
        }
        else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] )
        {
            Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
            Vec_IntPush( vSupp, vSupp0->pArray[k0] );
            k0++;
        }
        else 
        {
            Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
            Vec_IntPush( vSupp, vSupp1->pArray[k1] );
            k1++;
        }
    }
    for ( ; k0 < vSupp0->nSize; k0++ )
    {
        Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 );
        Vec_IntPush( vSupp, vSupp0->pArray[k0] );
    }
    for ( ; k1 < vSupp1->nSize; k1++ )
    {
        Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 );
        Vec_IntPush( vSupp, vSupp1->pArray[k1] );
    }
/*
    printf( "Zero : " );
    for ( k0 = 0; k0 < vSupp0->nSize; k0++ )
        printf( "%d ", vSupp0->pArray[k0] );
    printf( "\n" );

    printf( "One  : " );
    for ( k1 = 0; k1 < vSupp1->nSize; k1++ )
        printf( "%d ", vSupp1->pArray[k1] );
    printf( "\n" );

    printf( "Sum  : " );
    for ( k0 = 0; k0 < vSupp->nSize; k0++ )
        printf( "%d ", vSupp->pArray[k0] );
    printf( "\n" );
    printf( "\n" );
*/
    return vSupp;
}

void Abc_NtkCovCovers ( Cov_Man_t *  p, Abc_Ntk_t *  pNtk, int  fVerbose  )

static

DECLARATIONS ///.

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

FileName [covCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Mapping into network of SOPs/ESOPs.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

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

Synopsis [Compute the supports.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file covCore.c.

{
    Abc_Obj_t * pObj;
    int i;
    abctime clk = Abc_Clock();

    // start the manager
    p->vFanCounts = Abc_NtkFanoutCounts(pNtk);

    // set trivial cuts for the constant and the CIs
    pObj = Abc_AigConst1(pNtk);
    pObj->fMarkA = 1;
    Abc_NtkForEachCi( pNtk, pObj, i )
        pObj->fMarkA = 1;

    // perform iterative decomposition
    for ( i = 0; ; i++ )
    {
        if ( fVerbose )
        printf( "Iter %d : ", i+1 );
        if ( Abc_NtkCovCoversOne(p, pNtk, fVerbose) )
            break;
    }

    // clean the cut-point markers
    Abc_NtkForEachObj( pNtk, pObj, i )
        pObj->fMarkA = 0;

if ( fVerbose )
{
ABC_PRT( "Total", Abc_Clock() - clk );
}
}

void Abc_NtkCovCovers_rec ( Cov_Man_t *  p, Abc_Obj_t *  pObj, Vec_Ptr_t *  vBoundary  )

static

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file covCore.c.

{
    Abc_Obj_t * pObj0, * pObj1;
    // return if the support is already computed
    if ( pObj->fMarkB || pObj->fMarkA )//|| Abc_ObjGetSupp(pObj) ) // why do we need Supp check here???
        return;
    // mark as visited
    pObj->fMarkB = 1;
    // get the fanins
    pObj0 = Abc_ObjFanin0(pObj);
    pObj1 = Abc_ObjFanin1(pObj);
    // solve for the fanins
    Abc_NtkCovCovers_rec( p, pObj0, vBoundary );
    Abc_NtkCovCovers_rec( p, pObj1, vBoundary );
    // skip the node that spaced out
    if ( (!pObj0->fMarkA && !Abc_ObjGetSupp(pObj0)) ||  // fanin is not ready
         (!pObj1->fMarkA && !Abc_ObjGetSupp(pObj1)) ||  // fanin is not ready
         !Abc_NodeCovPropagate( p, pObj ) )           // node's support or covers cannot be computed
    {
        // save the nodes of the future boundary
        if ( !pObj0->fMarkA && Abc_ObjGetSupp(pObj0) )
            Vec_PtrPush( vBoundary, pObj0 );
        if ( !pObj1->fMarkA && Abc_ObjGetSupp(pObj1) )
            Vec_PtrPush( vBoundary, pObj1 );
        return;
    }
    // consider dropping the fanin supports
//    Abc_NodeCovDropData( p, pObj0 );
//    Abc_NodeCovDropData( p, pObj1 );
}

int Abc_NtkCovCoversOne ( Cov_Man_t *  p, Abc_Ntk_t *  pNtk, int  fVerbose  )

static

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

Synopsis [Compute the supports.]

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file covCore.c.

{
    ProgressBar * pProgress;
    Abc_Obj_t * pObj;
    Vec_Ptr_t * vBoundary;
    int i;
    abctime clk = Abc_Clock();
    int Counter = 0;
    int fStop = 1;

    // array to collect the nodes in the new boundary
    vBoundary = Vec_PtrAlloc( 100 );

    // start from the COs and mark visited nodes using pObj->fMarkB
    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        // skip the solved nodes (including the CIs)
        pObj = Abc_ObjFanin0(pObj);
        if ( pObj->fMarkA )
        {
            Counter++;
            continue;
        } 

        // traverse the cone starting from this node
        if ( Abc_ObjGetSupp(pObj) == NULL )
            Abc_NtkCovCovers_rec( p, pObj, vBoundary );

        // count the number of solved cones
        if ( Abc_ObjGetSupp(pObj) == NULL )
            fStop = 0;
        else
            Counter++;

/*
        printf( "%-15s : ", Abc_ObjName(pObj) ); 
        printf( "lev = %5d  ", pObj->Level );
        if ( Abc_ObjGetSupp(pObj) == NULL )
        {
            printf( "\n" );
            continue;
        }
        printf( "supp = %3d  ", Abc_ObjGetSupp(pObj)->nSize ); 
        printf( "esop = %3d  ", Min_CoverCountCubes( Abc_ObjGetCover2(pObj) ) ); 
        printf( "\n" );
*/
    }
    Extra_ProgressBarStop( pProgress );

    // clean visited nodes
    Abc_NtkForEachObj( pNtk, pObj, i )
        pObj->fMarkB = 0;

    // create the new boundary
    p->nBoundary = 0;
    Vec_PtrForEachEntry( Abc_Obj_t *, vBoundary, pObj, i )
    {
        if ( !pObj->fMarkA )
        {
            pObj->fMarkA = 1;
            p->nBoundary++;
        }
    }
    Vec_PtrFree( vBoundary );

if ( fVerbose )
{
    printf( "Outs = %4d (%4d) Node = %6d (%6d) Max = %6d  Bound = %4d  ", 
        Counter, Abc_NtkCoNum(pNtk), p->nSupps, Abc_NtkNodeNum(pNtk), p->nSuppsMax, p->nBoundary );
ABC_PRT( "T", Abc_Clock() - clk );
}
    return fStop;
}

Abc_Ntk_t* Abc_NtkSopEsopCover	(	Abc_Ntk_t *	pNtk,
		int	nFaninMax,
		int	fUseEsop,
		int	fUseSop,
		int	fUseInvs,
		int	fVerbose
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Performs decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file covCore.c.

{
    Abc_Ntk_t * pNtkNew;
    Cov_Man_t * p;

    assert( Abc_NtkIsStrash(pNtk) );

    // create the manager
    p = Cov_ManAlloc( pNtk, nFaninMax );
    p->fUseEsop = fUseEsop;
    p->fUseSop  = fUseSop;
    pNtk->pManCut = p;

    // perform mapping
    Abc_NtkCovCovers( p, pNtk, fVerbose );

    // derive the final network
//    if ( fUseInvs )
//        pNtkNew = Abc_NtkCovDeriveClean( p, pNtk );
//      else
//       pNtkNew = Abc_NtkCovDerive( p, pNtk );
//    pNtkNew = NULL;
    pNtkNew = Abc_NtkCovDeriveRegular( p, pNtk );

    Cov_ManFree( p );
    pNtk->pManCut = NULL;

    // make sure that everything is okay
    if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) )
    {
        printf( "Abc_NtkCov: The network check has failed.\n" );
        Abc_NtkDelete( pNtkNew );
        return NULL;
    }
    return pNtkNew;
}