giaResub6.c File Reference

#include "gia.h"
#include "misc/util/utilTruth.h"
#include "base/io/ioResub.h"

Include dependency graph for giaResub6.c:

Go to the source code of this file.

Classes
struct	Res6_Man_t_

Macros
#define	MAX_NODE   100
	DECLARATIONS ///.

Typedefs
typedef struct Res6_Man_t_	Res6_Man_t

Functions
void	Dau_DsdPrintFromTruth2 (word *pTruth, int nVarsInit)
Res6_Man_t *	Res6_ManReadPla (char *pFileName)
Res6_Man_t *	Res6_ManRead (char *pFileName)
void	Res6_ManWrite (char *pFileName, Res6_Man_t *p)
void	Res6_ManPrintProblem (Res6_Man_t *p, int fVerbose)
Vec_Int_t *	Res6_FindSupport (Vec_Int_t *vSol, int nDivs)
void	Res6_PrintSuppSims (Vec_Int_t *vSol, word **ppLits, int nWords, int nDivs)
int	Res6_FindSupportSize (Vec_Int_t *vSol, int nDivs)
void	Res6_PrintSolution (Vec_Int_t *vSol, int nDivs)
int	Res6_FindGetCost (Res6_Man_t *p, int iDiv)
int	Res6_FindBestDiv (Res6_Man_t *p, int *pCost)
int	Res6_FindBestEval (Res6_Man_t *p, Vec_Int_t *vSol, int Start)
void	Res6_ManResubVerify (Res6_Man_t *p, Vec_Int_t *vSol)
void	Res6_ManResubCheck (char *pFileNameRes, char *pFileNameSol, int fVerbose)
int	Res6_FindBestEvalPla (Res6_Man_t *p, Vec_Int_t *vSol)
void	Res6_ManResubVerifyPla (Res6_Man_t *p, Vec_Int_t *vSol)
void	Res6_PrintSolutionPla (Vec_Int_t *vSol, int nSuppSize, int nDivs)
void	Res6_ManResubCheckPla (char *pFileName, int fVerbose)

Macro Definition Documentation

MAX_NODE

#define MAX_NODE   100

DECLARATIONS ///.

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

FileName [giaResub6.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Resubstitution.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 31 of file giaResub6.c.

Typedef Documentation

Res6_Man_t

typedef struct Res6_Man_t_ Res6_Man_t

Definition at line 33 of file giaResub6.c.

Function Documentation

Dau_DsdPrintFromTruth2()

void Dau_DsdPrintFromTruth2 ( word * pTruth, int nVarsInit )

extern

Definition at line 1976 of file dauDsd.c.

{
    char pRes[DAU_MAX_STR];
    word pTemp[DAU_MAX_WORD];
    Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
    Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
    fprintf( stdout, "%s", pRes );
}

Here is the caller graph for this function:

Res6_FindBestDiv()

int Res6_FindBestDiv	(	Res6_Man_t *	p,
		int *	pCost )

Definition at line 397 of file giaResub6.c.

{
    int d, dBest = -1, CostBest = ABC_INFINITY;
    for ( d = 0; d < 2*p->nDivs; d++ )
    {
        int Cost = Res6_FindGetCost( p, d );
        printf( "Div = %d  Cost = %d\n", d, Cost );
        if ( CostBest >= Cost )
            CostBest = Cost, dBest = d;
    }
    if ( pCost )
        *pCost = CostBest;
    return dBest;
}

Here is the call graph for this function:

Res6_FindBestEval()

int Res6_FindBestEval	(	Res6_Man_t *	p,
		Vec_Int_t *	vSol,
		int	Start )

Definition at line 411 of file giaResub6.c.

{
    int i, iLit0, iLit1;
    assert( Vec_IntSize(vSol) % 2 == 0 );
    Vec_IntForEachEntryDoubleStart( vSol, iLit0, iLit1, i, 2*Start )
    {
        if ( iLit0 > iLit1 )
        {
            Abc_TtXor( p->ppLits[2*p->nDivs+i+0], p->ppLits[iLit0],   p->ppLits[iLit1],   p->nWords, 0 );
            Abc_TtXor( p->ppLits[2*p->nDivs+i+1], p->ppLits[iLit0],   p->ppLits[iLit1],   p->nWords, 1 );
        }
        else
        {
            Abc_TtAnd( p->ppLits[2*p->nDivs+i+0], p->ppLits[iLit0],   p->ppLits[iLit1],   p->nWords, 0 );
            Abc_TtOr ( p->ppLits[2*p->nDivs+i+1], p->ppLits[iLit0^1], p->ppLits[iLit1^1], p->nWords );
        }
 
        //printf( "Node %d\n", i/2 );
        //Abc_TtPrintBinary1( stdout, p->ppLits[2*p->nDivs+i+0], 6 ); printf( "\n" );
        //Abc_TtPrintBinary1( stdout, p->ppLits[2*p->nDivs+i+1], 6 ); printf( "\n" );
    }
    return Res6_FindGetCost( p, Vec_IntEntryLast(vSol) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Res6_FindBestEvalPla()

int Res6_FindBestEvalPla	(	Res6_Man_t *	p,
		Vec_Int_t *	vSol )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 493 of file giaResub6.c.

{
    int i, n, iObj, iLit0, iLit1, iOffset = 2*(1+Vec_IntSize(&p->vSupp));
    assert( Vec_IntSize(vSol) % 2 == 0 );
    Vec_IntForEachEntry( &p->vSupp, iObj, i )
        for ( n = 0; n < 2; n++ )
            Abc_TtCopy( p->ppLits[2*(1+i)+n], p->ppLits[2*iObj+n], p->nWords, 0 );
    Vec_IntForEachEntryDouble( vSol, iLit0, iLit1, i )
    {
        if ( iLit0 > iLit1 )
        {
            Abc_TtXor( p->ppLits[iOffset+i+0], p->ppLits[iLit0],   p->ppLits[iLit1],   p->nWords, 0 );
            Abc_TtXor( p->ppLits[iOffset+i+1], p->ppLits[iLit0],   p->ppLits[iLit1],   p->nWords, 1 );
        }
        else
        {
            Abc_TtAnd( p->ppLits[iOffset+i+0], p->ppLits[iLit0],   p->ppLits[iLit1],   p->nWords, 0 );
            Abc_TtOr ( p->ppLits[iOffset+i+1], p->ppLits[iLit0^1], p->ppLits[iLit1^1], p->nWords );
        }
    }
    return Res6_FindGetCost( p, Vec_IntEntryLast(vSol) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Res6_FindGetCost()

int Res6_FindGetCost	(	Res6_Man_t *	p,
		int	iDiv )

Definition at line 384 of file giaResub6.c.

{
    int w, Cost = 0;
    //printf( "DivLit = %d\n", iDiv );
    //Abc_TtPrintBinary1( stdout, p->ppLits[iDiv], p->nIns ); printf( "\n" );
    //printf( "Set0\n" );
    //Abc_TtPrintBinary1( stdout, p->ppSets[0], p->nIns ); printf( "\n" );
    //printf( "Set1\n" );
    //Abc_TtPrintBinary1( stdout, p->ppSets[1], p->nIns ); printf( "\n" );
    for ( w = 0; w < p->nWords; w++ )
        Cost += Abc_TtCountOnes( (p->ppLits[iDiv][w] & p->ppSets[0][w]) | (p->ppLits[iDiv^1][w] & p->ppSets[1][w]) );
    return Cost;
}

Here is the caller graph for this function:

Res6_FindSupport()

Vec_Int_t * Res6_FindSupport	(	Vec_Int_t *	vSol,
		int	nDivs )

Definition at line 320 of file giaResub6.c.

{
    int i, iLit;
    Vec_Int_t * vSupp = Vec_IntAlloc( 10 );
    Vec_IntForEachEntry( vSol, iLit, i )
        if ( iLit >= 2 && iLit < 2*nDivs )
            Vec_IntPushUnique( vSupp, Abc_Lit2Var(iLit) );
    return vSupp;
}

Here is the caller graph for this function:

Res6_FindSupportSize()

int Res6_FindSupportSize	(	Vec_Int_t *	vSol,
		int	nDivs )

Definition at line 359 of file giaResub6.c.

{
    Vec_Int_t * vSupp = Res6_FindSupport( vSol, nDivs );
    int Res = Vec_IntSize(vSupp);
    Vec_IntFree( vSupp );
    return Res;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Res6_ManPrintProblem()

void Res6_ManPrintProblem	(	Res6_Man_t *	p,
		int	fVerbose )

Definition at line 235 of file giaResub6.c.

{
    int i, nInputs = (p->nIns && p->nIns < 6) ? p->nIns : 6;
    printf( "Problem:   In = %d  Div = %d  Out  = %d  Pat = %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats );
    if ( !fVerbose )
        return;
    printf( "%02d : %s\n", 0, "const0" );
    printf( "%02d : %s\n", 1, "const1" );
    for ( i = 1; i < p->nDivs; i++ )
    {
        if ( nInputs < 6 )
        {
            *p->ppLits[2*i+0] = Abc_Tt6Stretch( *p->ppLits[2*i+0], nInputs );
            *p->ppLits[2*i+1] = Abc_Tt6Stretch( *p->ppLits[2*i+1], nInputs );
        }
        printf("%02d : ", 2*i+0), Dau_DsdPrintFromTruth2(p->ppLits[2*i+0], nInputs), printf( "\n" );
        printf("%02d : ", 2*i+1), Dau_DsdPrintFromTruth2(p->ppLits[2*i+1], nInputs), printf( "\n" );
    }
    for ( i = 0; i < (1 << p->nOuts); i++ )
    {
        if ( nInputs < 6 )
            *p->ppSets[i] = Abc_Tt6Stretch( *p->ppSets[i], nInputs );
        printf("%02d : ", i), Dau_DsdPrintFromTruth2(p->ppSets[i], nInputs), printf( "\n" );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Res6_ManRead()

Res6_Man_t * Res6_ManRead

(

char *

pFileName

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 152 of file giaResub6.c.

{
    Res6_Man_t * p = NULL;
    FILE * pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
        printf( "Cannot open input file \"%s\".\n", pFileName );
    else
    {
        int i, k, nIns, nNodes, nOuts, nPats;
        char Temp[100], Buffer[100];
        char * pLine = fgets( Buffer, 100, pFile );
        if ( pLine == NULL )
        {
            printf( "Cannot read the header line of input file \"%s\".\n", pFileName );
            return NULL;
        }
        if ( 5 != sscanf(pLine, "%s %d %d %d %d", Temp, &nIns, &nNodes, &nOuts, &nPats) )
        {
            printf( "Cannot read the parameters from the header of input file \"%s\".\n", pFileName );
            return NULL;
        }
        p = Res6_ManStart( nIns, nNodes, nOuts, nPats );
        pLine = ABC_ALLOC( char, nPats + 100 );
        for ( i = 1; i < p->nDivs; i++ )
        {
            char * pNext = fgets( pLine, nPats + 100, pFile );
            if ( pNext == NULL )
            {
                printf( "Cannot read line %d of input file \"%s\".\n", i, pFileName );
                Res6_ManStop( p );
                ABC_FREE( pLine );
                fclose( pFile );
                return NULL;
            }
            for ( k = 0; k < p->nPats; k++ )
                if ( pNext[k] == '0' )
                    Abc_TtSetBit( p->ppLits[2*i+1], k );
                else if ( pNext[k] == '1' )
                    Abc_TtSetBit( p->ppLits[2*i], k );
        }
        for ( i = 0; i < (1 << p->nOuts); i++ )
        {
            char * pNext = fgets( pLine, nPats + 100, pFile );
            if ( pNext == NULL )
            {
                printf( "Cannot read line %d of input file \"%s\".\n", i, pFileName );
                Res6_ManStop( p );
                ABC_FREE( pLine );
                fclose( pFile );
                return NULL;
            }
            for ( k = 0; k < p->nPats; k++ )
                if ( pNext[k] == '1' )
                    Abc_TtSetBit( p->ppSets[i], k );
        }
        ABC_FREE( pLine );
        fclose( pFile );
    }
    return p;
}

Here is the caller graph for this function:

Res6_ManReadPla()

Res6_Man_t * Res6_ManReadPla

(

char *

pFileName

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file giaResub6.c.

{
    int i, n;
    Abc_RData_t * pData = Abc_ReadPla( pFileName ); assert( pData->nOuts == 1 );
    Res6_Man_t * p = pData ? Res6_ManStart( 0, pData->nIns, pData->nOuts, pData->nPats ) : NULL;
    if ( p == NULL ) return NULL;
    assert( pData->nSimWords == p->nWords );
    for ( i = 1; i < p->nDivs; i++ )
        for ( n = 0; n < 2; n++ )
            Abc_TtCopy( p->ppLits[2*i+n], Vec_WrdEntryP(pData->vSimsIn, (i-1)*pData->nSimWords), pData->nSimWords, n );
    for ( i = 0; i < (1 << p->nOuts); i++ )
        Abc_TtCopy( p->ppSets[i], Vec_WrdEntryP(pData->vSimsOut, i*pData->nSimWords), pData->nSimWords, 0 );
    if ( pData->vDivs )
        Vec_IntForEachEntry( pData->vDivs, n, i )
            Vec_IntPush( &p->vSupp, 1+n );
    if ( pData->vSol ) {
        Vec_IntForEachEntry( pData->vSol, n, i )
            Vec_IntPush( &p->vSol, n );
        Vec_IntPush( &p->vSol, Vec_IntEntryLast(&p->vSol) );
    }
    Abc_RDataStop( pData );
    return p;
}

Here is the caller graph for this function:

Res6_ManResubCheck()

void Res6_ManResubCheck	(	char *	pFileNameRes,
		char *	pFileNameSol,
		int	fVerbose )

Definition at line 454 of file giaResub6.c.

{
    char FileNameSol[1000];
    if ( pFileNameSol )
        strcpy( FileNameSol, pFileNameSol );
    else
    {
        strcpy( FileNameSol, pFileNameRes );
        strcpy( FileNameSol + strlen(FileNameSol) - strlen(".resub"), ".sol" );
    }
    {
        Res6_Man_t * p = Res6_ManRead( pFileNameRes );
        Vec_Int_t * vSol = Res6_ManReadSol( FileNameSol );
        //Vec_IntPrint( vSol );        
        if ( p == NULL || vSol == NULL )
            return;
        if ( fVerbose )
            Res6_ManPrintProblem( p, 0 );
        if ( fVerbose )
            Res6_PrintSolution( vSol, p->nDivs );
        //if ( fVerbose )
        //    Res6_PrintSuppSims( vSol, p->ppLits, p->nWords, p->nDivs );
        Res6_ManResubVerify( p, vSol );
        Vec_IntFree( vSol );
        Res6_ManStop( p );
    }
}

Here is the call graph for this function:

Res6_ManResubCheckPla()

void Res6_ManResubCheckPla	(	char *	pFileName,
		int	fVerbose )

Definition at line 541 of file giaResub6.c.

{
    Res6_Man_t * p = Res6_ManReadPla( pFileName );
    if ( p == NULL ) return;
    //Vec_IntPrint( &p->vSupp );
    //Vec_IntPrint( &p->vSol );
    if ( fVerbose )
        Res6_ManPrintProblem( p, 0 );
    if ( fVerbose )
        Res6_PrintSolutionPla( &p->vSol, Vec_IntSize(&p->vSupp), p->nDivs );
    //if ( fVerbose )
    //    Res6_PrintSuppSims( vSol, p->ppLits, p->nWords, p->nDivs );
    Res6_ManResubVerifyPla( p, &p->vSol );
    Res6_ManStop( p );    
}

Here is the call graph for this function:

Res6_ManResubVerify()

void Res6_ManResubVerify	(	Res6_Man_t *	p,
		Vec_Int_t *	vSol )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 446 of file giaResub6.c.

{
    int Cost = Res6_FindBestEval( p, vSol, 0 );
    if ( Cost == 0 )
        printf( "Verification successful.\n" );
    else
        printf( "Verification FAILED with %d errors on %d patterns.\n", Cost, p->nPats );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Res6_ManResubVerifyPla()

void Res6_ManResubVerifyPla	(	Res6_Man_t *	p,
		Vec_Int_t *	vSol )

Definition at line 515 of file giaResub6.c.

{
    int Cost = Res6_FindBestEvalPla( p, vSol );
    if ( Cost == 0 )
        printf( "Verification successful.\n" );
    else
        printf( "Verification FAILED with %d errors on %d patterns.\n", Cost, p->nPats );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Res6_ManWrite()

void Res6_ManWrite	(	char *	pFileName,
		Res6_Man_t *	p )

Definition at line 212 of file giaResub6.c.

{
    FILE * pFile = fopen( pFileName, "wb" ); 
    if ( pFile == NULL )
        printf( "Cannot open output file \"%s\".\n", pFileName );
    else
    {
        int i, k;
        fprintf( pFile, "resyn %d %d %d %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats );
        for ( i = 1; i < p->nDivs; i++, fputc('\n', pFile) )
            for ( k = 0; k < p->nPats; k++ )
                if ( Abc_TtGetBit(p->ppLits[2*i+1], k) )
                    fputc( '0', pFile );
                else if ( Abc_TtGetBit(p->ppLits[2*i], k) )
                    fputc( '1', pFile );
                else
                    fputc( '-', pFile );
        for ( i = 0; i < (1 << p->nOuts); i++, fputc('\n', pFile) )
            for ( k = 0; k < p->nPats; k++ )
                fputc( '0' + Abc_TtGetBit(p->ppSets[i], k), pFile );
        fclose( pFile );
    }
}

Res6_PrintSolution()

void Res6_PrintSolution	(	Vec_Int_t *	vSol,
		int	nDivs )

Definition at line 366 of file giaResub6.c.

{
    int iNode, nNodes = Vec_IntSize(vSol)/2-1;
    assert( Vec_IntSize(vSol) % 2 == 0 );
    printf( "Solution:  In = %d  Div = %d  Node = %d  Out = %d\n", Res6_FindSupportSize(vSol, nDivs), nDivs-1, nNodes, 1 );
    for ( iNode = 0; iNode <= nNodes; iNode++ )
    {
        int * pLits = Vec_IntEntryP( vSol, 2*iNode );
        printf( "x%-2d = ", nDivs + iNode );
        Res6_LitPrint( pLits[0], nDivs );
        if ( pLits[0] != pLits[1] )
        {
            printf( "  %c ", pLits[0] < pLits[1] ? '&' : '^' );
            Res6_LitPrint( pLits[1], nDivs );
        }
        printf( "\n" );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Res6_PrintSolutionPla()

void Res6_PrintSolutionPla	(	Vec_Int_t *	vSol,
		int	nSuppSize,
		int	nDivs )

Definition at line 523 of file giaResub6.c.

{
    int iNode, nNodes = Vec_IntSize(vSol)/2-1;
    assert( Vec_IntSize(vSol) % 2 == 0 );
    printf( "Solution:  In = %d  Div = %d  Node = %d  Out = %d\n", nSuppSize, nDivs-1, nNodes, 1 );
    for ( iNode = 0; iNode <= nNodes; iNode++ )
    {
        int * pLits = Vec_IntEntryP( vSol, 2*iNode );
        printf( "x%-2d = ", 1+nSuppSize+iNode );
        Res6_LitPrint( pLits[0], 1+nSuppSize );
        if ( pLits[0] != pLits[1] )
        {
            printf( "  %c ", pLits[0] < pLits[1] ? '&' : '^' );
            Res6_LitPrint( pLits[1], 1+nSuppSize );
        }
        printf( "\n" );
    }
}

Here is the caller graph for this function:

Res6_PrintSuppSims()

void Res6_PrintSuppSims	(	Vec_Int_t *	vSol,
		word **	ppLits,
		int	nWords,
		int	nDivs )

Definition at line 329 of file giaResub6.c.

{
    Vec_Int_t * vSupp = Res6_FindSupport( vSol, nDivs );
    int i, k, iObj;
    Vec_IntForEachEntry( vSupp, iObj, i )
    {
        for ( k = 0; k < 64*nWords; k++ )
            if ( Abc_TtGetBit(ppLits[2*iObj+1], k) )
                printf( "0" );
            else if ( Abc_TtGetBit(ppLits[2*iObj], k) )
                printf( "1" );
            else
                printf( "-" );
        printf( "\n" );
    }
    for ( k = 0; k < 64*nWords; k++ )
    {
        Vec_IntForEachEntry( vSupp, iObj, i )
            if ( Abc_TtGetBit(ppLits[2*iObj+1], k) )
                printf( "0" );
            else if ( Abc_TtGetBit(ppLits[2*iObj+0], k) )
                printf( "1" );
            else
                printf( "-" );
        printf( "\n" );
        if ( k == 9 )
            break;
    }
    Vec_IntFree( vSupp );
}                        

Here is the call graph for this function: