ivyDsd.c File Reference

#include "ivy.h"

Include dependency graph for ivyDsd.c:

Go to the source code of this file.

Classes
struct	Ivy_Dec_t_

Typedefs
typedef struct Ivy_Dec_t_	Ivy_Dec_t

Enumerations
enum	Ivy_DecType_t {   IVY_DEC_PI , IVY_DEC_CONST1 , IVY_DEC_BUF , IVY_DEC_AND ,   IVY_DEC_EXOR , IVY_DEC_MUX , IVY_DEC_MAJ , IVY_DEC_PRIME }
	DECLARATIONS ///. More...

Functions
int	Ivy_TruthDsd (unsigned uTruth, Vec_Int_t *vTree)
	FUNCTION DEFINITIONS ///.
unsigned	Ivy_TruthDsdCompute_rec (int iNode, Vec_Int_t *vTree)
unsigned	Ivy_TruthDsdCompute (Vec_Int_t *vTree)
void	Ivy_TruthDsdPrint_rec (FILE *pFile, int iNode, Vec_Int_t *vTree)
void	Ivy_TruthDsdPrint (FILE *pFile, Vec_Int_t *vTree)
Ivy_Obj_t *	Ivy_ManDsdConstruct_rec (Ivy_Man_t *p, Vec_Int_t *vFront, int iNode, Vec_Int_t *vTree)
Ivy_Obj_t *	Ivy_ManDsdConstruct (Ivy_Man_t *p, Vec_Int_t *vFront, Vec_Int_t *vTree)
void	Ivy_TruthDsdComputePrint (unsigned uTruth)
void	Ivy_TruthTestOne (unsigned uTruth)

Typedef Documentation

Ivy_Dec_t

typedef struct Ivy_Dec_t_ Ivy_Dec_t

Definition at line 42 of file ivyDsd.c.

Enumeration Type Documentation

Ivy_DecType_t

enum Ivy_DecType_t

DECLARATIONS ///.

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

FileName [ivyDsd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [And-Inverter Graph package.]

Synopsis [Disjoint-support decomposition.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - May 11, 2006.]

Revision [

Id

ivyDsd.c,v 1.00 2006/05/11 00:00:00 alanmi Exp

]

Enumerator
IVY_DEC_PI
IVY_DEC_CONST1
IVY_DEC_BUF
IVY_DEC_AND
IVY_DEC_EXOR
IVY_DEC_MUX
IVY_DEC_MAJ
IVY_DEC_PRIME

Definition at line 31 of file ivyDsd.c.

             { 
    IVY_DEC_PI,             // 0: var
    IVY_DEC_CONST1,         // 1: CONST1
    IVY_DEC_BUF,            // 2: BUF
    IVY_DEC_AND,            // 3: AND
    IVY_DEC_EXOR,           // 4: EXOR
    IVY_DEC_MUX,            // 5: MUX
    IVY_DEC_MAJ,            // 6: MAJ
    IVY_DEC_PRIME           // 7: undecomposable
} Ivy_DecType_t;

Function Documentation

Ivy_ManDsdConstruct()

Ivy_Obj_t * Ivy_ManDsdConstruct	(	Ivy_Man_t *	p,
		Vec_Int_t *	vFront,
		Vec_Int_t *	vTree )

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

Synopsis [Implement DSD in the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 655 of file ivyDsd.c.

{
    int Entry, i;
    // implement latches on the frontier (TEMPORARY!!!)
    Vec_IntForEachEntry( vFront, Entry, i )
        Vec_IntWriteEntry( vFront, i, Ivy_LeafId(Entry) );
    // recursively construct the tree
    return Ivy_ManDsdConstruct_rec( p, vFront, Vec_IntSize(vTree)-1, vTree );
}

Here is the call graph for this function:

Ivy_ManDsdConstruct_rec()

Ivy_Obj_t * Ivy_ManDsdConstruct_rec	(	Ivy_Man_t *	p,
		Vec_Int_t *	vFront,
		int	iNode,
		Vec_Int_t *	vTree )

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

Synopsis [Implement DSD in the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 586 of file ivyDsd.c.

{
    Ivy_Obj_t * pResult, * pChild, * pNodes[16];
    int Var, i;
    // get the node
    Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
    // compute the node function
    if ( Node.Type == IVY_DEC_CONST1 )
        return Ivy_NotCond( Ivy_ManConst1(p), Node.fCompl );
    if ( Node.Type == IVY_DEC_PI )
    {
        pResult = Ivy_ManObj( p, Vec_IntEntry(vFront, iNode) );
        return Ivy_NotCond( pResult, Node.fCompl );
    }
    if ( Node.Type == IVY_DEC_BUF )
    {
        pResult = Ivy_ManDsdConstruct_rec( p, vFront, Node.Fan0 >> 1, vTree );
        return Ivy_NotCond( pResult, Node.fCompl );
    }
    if ( Node.Type == IVY_DEC_AND || Node.Type == IVY_DEC_EXOR )
    {
        for ( i = 0; i < (int)Node.nFans; i++ )
        {
            Var = Ivy_DecGetVar( &Node, i );
            assert( Node.Type == IVY_DEC_AND || (Var & 1) == 0 );
            pChild = Ivy_ManDsdConstruct_rec( p, vFront, Var >> 1, vTree );
            pChild = Ivy_NotCond( pChild, (Var & 1) );
            pNodes[i] = pChild;
        }
 
//        Ivy_MultiEval( pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
 
        pResult = Ivy_Multi( p, pNodes, Node.nFans, Node.Type == IVY_DEC_AND ? IVY_AND : IVY_EXOR );
        return Ivy_NotCond( pResult, Node.fCompl );
    }
    assert( Node.fCompl == 0 );
    if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
    {
        int VarC, Var1, Var0;
        VarC = Ivy_DecGetVar( &Node, 0 );
        Var1 = Ivy_DecGetVar( &Node, 1 );
        Var0 = Ivy_DecGetVar( &Node, 2 );
        pNodes[0] = Ivy_ManDsdConstruct_rec( p, vFront, VarC >> 1, vTree );
        pNodes[1] = Ivy_ManDsdConstruct_rec( p, vFront, Var1 >> 1, vTree );
        pNodes[2] = Ivy_ManDsdConstruct_rec( p, vFront, Var0 >> 1, vTree );
        assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
        pNodes[0] = Ivy_NotCond( pNodes[0], (VarC & 1) );
        pNodes[1] = Ivy_NotCond( pNodes[1], (Var1 & 1) );
        pNodes[2] = Ivy_NotCond( pNodes[2], (Var0 & 1) );
        if ( Node.Type == IVY_DEC_MUX )
            return Ivy_Mux( p, pNodes[0], pNodes[1], pNodes[2] );
        else
            return Ivy_Maj( p, pNodes[0], pNodes[1], pNodes[2] );
    }
    assert( 0 );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_TruthDsd()

int Ivy_TruthDsd	(	unsigned	uTruth,
		Vec_Int_t *	vTree )

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes DSD of truth table of 5 variables or less.]

Description [Returns 1 if the function is a constant or is fully DSD decomposable using AND/EXOR/MUX gates.]

SideEffects []

SeeAlso []

Definition at line 166 of file ivyDsd.c.

{
    Ivy_Dec_t Node;
    int i, RetValue;
    // set the PI variables
    Vec_IntClear( vTree );
    for ( i = 0; i < 5; i++ )
        Vec_IntPush( vTree, 0 );
    // check if it is a constant
    if ( uTruth == 0 || ~uTruth == 0 )
    {
        Ivy_DecClear( &Node );
        Node.Type = IVY_DEC_CONST1;
        Node.fCompl = (uTruth == 0);
        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
        return 1;
    }
    // perform the decomposition
    RetValue = Ivy_TruthDecompose_rec( uTruth, vTree );
    if ( RetValue == -1 )
        return 0;
    // get the topmost node
    if ( (RetValue >> 1) < 5 )
    { // add buffer
        Ivy_DecClear( &Node );
        Node.Type = IVY_DEC_BUF;
        Node.fCompl = (RetValue & 1);
        Node.Fan0 = ((RetValue >> 1) << 1);
        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
    }
    else if ( RetValue & 1 )
    { // check if the topmost node has to be complemented
        Node = Ivy_IntToDec( Vec_IntPop(vTree) );
        assert( Node.fCompl == 0 );
        Node.fCompl = (RetValue & 1);
        Vec_IntPush( vTree, Ivy_DecToInt(Node) );
    }
    if ( uTruth != Ivy_TruthDsdCompute(vTree) )
        printf( "Verification failed.\n" );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_TruthDsdCompute()

unsigned Ivy_TruthDsdCompute

(

Vec_Int_t *

vTree

)

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

Synopsis [Computes truth table of decomposition tree for verification.]

Description []

SideEffects []

SeeAlso []

Definition at line 478 of file ivyDsd.c.

{
    return Ivy_TruthDsdCompute_rec( Vec_IntSize(vTree)-1, vTree );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_TruthDsdCompute_rec()

unsigned Ivy_TruthDsdCompute_rec	(	int	iNode,
		Vec_Int_t *	vTree )

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

Synopsis [Computes truth table of decomposition tree for verification.]

Description []

SideEffects []

SeeAlso []

Definition at line 404 of file ivyDsd.c.

{
    unsigned uTruthChild, uTruthTotal;
    int Var, i;
    // get the node
    Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
    // compute the node function
    if ( Node.Type == IVY_DEC_CONST1 )
        return s_Masks[5][ !Node.fCompl ];
    if ( Node.Type == IVY_DEC_PI )
        return s_Masks[iNode][ !Node.fCompl ];
    if ( Node.Type == IVY_DEC_BUF )
    {
        uTruthTotal = Ivy_TruthDsdCompute_rec( Node.Fan0 >> 1, vTree );
        return Node.fCompl? ~uTruthTotal : uTruthTotal;
    }
    if ( Node.Type == IVY_DEC_AND )
    {
        uTruthTotal = s_Masks[5][1];
        for ( i = 0; i < (int)Node.nFans; i++ )
        {
            Var = Ivy_DecGetVar( &Node, i );
            uTruthChild = Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
            uTruthTotal = (Var & 1)? uTruthTotal & ~uTruthChild : uTruthTotal & uTruthChild;
        }
        return Node.fCompl? ~uTruthTotal : uTruthTotal;
    }
    if ( Node.Type == IVY_DEC_EXOR )
    {
        uTruthTotal = 0;
        for ( i = 0; i < (int)Node.nFans; i++ )
        {
            Var = Ivy_DecGetVar( &Node, i );
            uTruthTotal ^= Ivy_TruthDsdCompute_rec( Var >> 1, vTree );
            assert( (Var & 1) == 0 );
        }
        return Node.fCompl? ~uTruthTotal : uTruthTotal;
    }
    assert( Node.fCompl == 0 );
    if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
    {
        unsigned uTruthChildC, uTruthChild1, uTruthChild0;
        int VarC, Var1, Var0;
        VarC = Ivy_DecGetVar( &Node, 0 );
        Var1 = Ivy_DecGetVar( &Node, 1 );
        Var0 = Ivy_DecGetVar( &Node, 2 );
        uTruthChildC = Ivy_TruthDsdCompute_rec( VarC >> 1, vTree );
        uTruthChild1 = Ivy_TruthDsdCompute_rec( Var1 >> 1, vTree );
        uTruthChild0 = Ivy_TruthDsdCompute_rec( Var0 >> 1, vTree );
        assert( Node.Type == IVY_DEC_MAJ || (VarC & 1) == 0 );
        uTruthChildC = (VarC & 1)? ~uTruthChildC : uTruthChildC;
        uTruthChild1 = (Var1 & 1)? ~uTruthChild1 : uTruthChild1;
        uTruthChild0 = (Var0 & 1)? ~uTruthChild0 : uTruthChild0;
        if ( Node.Type == IVY_DEC_MUX )
            return (uTruthChildC & uTruthChild1) | (~uTruthChildC & uTruthChild0);
        else
            return (uTruthChildC & uTruthChild1) | (uTruthChildC & uTruthChild0) | (uTruthChild1 & uTruthChild0);
    }
    assert( 0 );
    return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_TruthDsdComputePrint()

void Ivy_TruthDsdComputePrint

(

unsigned

uTruth

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 678 of file ivyDsd.c.

{
    static Vec_Int_t * vTree = NULL;
    if ( vTree == NULL )
        vTree = Vec_IntAlloc( 12 );
    if ( Ivy_TruthDsd( uTruth, vTree ) )
        Ivy_TruthDsdPrint( stdout, vTree );
    else
        printf( "Undecomposable\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_TruthDsdPrint()

void Ivy_TruthDsdPrint	(	FILE *	pFile,
		Vec_Int_t *	vTree )

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

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 568 of file ivyDsd.c.

{
    fprintf( pFile, "F = " );
    Ivy_TruthDsdPrint_rec( pFile, Vec_IntSize(vTree)-1, vTree );
    fprintf( pFile, "\n" );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_TruthDsdPrint_rec()

void Ivy_TruthDsdPrint_rec	(	FILE *	pFile,
		int	iNode,
		Vec_Int_t *	vTree )

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

Synopsis [Prints the decomposition tree.]

Description []

SideEffects []

SeeAlso []

Definition at line 494 of file ivyDsd.c.

{
    int Var, i;
    // get the node
    Ivy_Dec_t Node = Ivy_IntToDec( Vec_IntEntry(vTree, iNode) );
    // compute the node function
    if ( Node.Type == IVY_DEC_CONST1 )
        fprintf( pFile, "Const1%s", (Node.fCompl? "\'" : "") );
    else if ( Node.Type == IVY_DEC_PI )
        fprintf( pFile, "%c%s", 'a' + iNode, (Node.fCompl? "\'" : "") );
    else if ( Node.Type == IVY_DEC_BUF )
    {
        Ivy_TruthDsdPrint_rec( pFile, Node.Fan0 >> 1, vTree );
        fprintf( pFile, "%s", (Node.fCompl? "\'" : "") );
    }
    else if ( Node.Type == IVY_DEC_AND )
    {
        fprintf( pFile, "AND(" );
        for ( i = 0; i < (int)Node.nFans; i++ )
        {
            Var = Ivy_DecGetVar( &Node, i );
            Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
            fprintf( pFile, "%s", (Var & 1)? "\'" : "" );
            if ( i != (int)Node.nFans-1 )
                fprintf( pFile, "," );
        }
        fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
    }
    else if ( Node.Type == IVY_DEC_EXOR )
    {
        fprintf( pFile, "EXOR(" );
        for ( i = 0; i < (int)Node.nFans; i++ )
        {
            Var = Ivy_DecGetVar( &Node, i );
            Ivy_TruthDsdPrint_rec( pFile, Var >> 1, vTree );
            if ( i != (int)Node.nFans-1 )
                fprintf( pFile, "," );
            assert( (Var & 1) == 0 );
        }
        fprintf( pFile, ")%s", (Node.fCompl? "\'" : "") );
    }
    else if ( Node.Type == IVY_DEC_MUX || Node.Type == IVY_DEC_MAJ )
    {
        int VarC, Var1, Var0;
        assert( Node.fCompl == 0 );
        VarC = Ivy_DecGetVar( &Node, 0 );
        Var1 = Ivy_DecGetVar( &Node, 1 );
        Var0 = Ivy_DecGetVar( &Node, 2 );
        fprintf( pFile, "%s", (Node.Type == IVY_DEC_MUX)? "MUX(" : "MAJ(" );
        Ivy_TruthDsdPrint_rec( pFile, VarC >> 1, vTree );
        fprintf( pFile, "%s", (VarC & 1)? "\'" : "" );
        fprintf( pFile, "," );
        Ivy_TruthDsdPrint_rec( pFile, Var1 >> 1, vTree );
        fprintf( pFile, "%s", (Var1 & 1)? "\'" : "" );
        fprintf( pFile, "," );
        Ivy_TruthDsdPrint_rec( pFile, Var0 >> 1, vTree );
        fprintf( pFile, "%s", (Var0 & 1)? "\'" : "" );
        fprintf( pFile, ")" );
    }
    else assert( 0 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Ivy_TruthTestOne()

void Ivy_TruthTestOne

(

unsigned

uTruth

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 700 of file ivyDsd.c.

{
    static int Counter = 0;
    static Vec_Int_t * vTree = NULL;
    // decompose
    if ( vTree == NULL )
        vTree = Vec_IntAlloc( 12 );
 
    if ( !Ivy_TruthDsd( uTruth, vTree ) )
    {
//        printf( "Undecomposable\n" );
    }
    else
    {
//        nTruthDsd++;
        printf( "%5d : ", Counter++ );
        Extra_PrintBinary( stdout, &uTruth, 32 );
        printf( "  " );
        Ivy_TruthDsdPrint( stdout, vTree );
        if ( uTruth != Ivy_TruthDsdCompute(vTree) )
            printf( "Verification failed.\n" );
    }
//    Vec_IntFree( vTree );
}

Here is the call graph for this function: