abcScorr.c File Reference

#include "base/abc/abc.h"
#include "base/io/ioAbc.h"
#include "aig/saig/saig.h"
#include "proof/ssw/ssw.h"
#include "aig/gia/gia.h"
#include "proof/cec/cec.h"
#include "aig/gia/giaAig.h"

Include dependency graph for abcScorr.c:

Go to the source code of this file.

Classes
struct	Tst_Dat_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Tst_Dat_t_	Tst_Dat_t
	DECLARATIONS ///.

Functions
Vec_Int_t *	Abc_NtkMapGiaIntoNameId (Abc_Ntk_t *pNetlist, Aig_Man_t *pAig, Gia_Man_t *pGia)
	FUNCTION DEFINITIONS ///.
char *	Abc_NtkTestScorrGetName (Abc_Ntk_t *pNetlist, Vec_Int_t *vId2Name, int Id)
int	Abc_NtkTestScorrWriteEquivPair (Abc_Ntk_t *pNetlist, Vec_Int_t *vId2Name, int Id1, int Id2, FILE *pFile, int fPol)
int	Abc_NtkTestScorrWriteEquivConst (Abc_Ntk_t *pNetlist, Vec_Int_t *vId2Name, int Id1, FILE *pFile, int fPol)
char *	Abc_NtkBmcFileName (char *pName)
int	Abc_NtkTestScorrWriteEquivGia (Tst_Dat_t *pData)
int	Abc_NtkTestScorrWriteEquivAig (Tst_Dat_t *pData)
Abc_Ntk_t *	Abc_NtkTestScorr (char *pFileNameIn, char *pFileNameOut, int nStepsMax, int nBTLimit, int fNewAlgo, int fFlopOnly, int fFfNdOnly, int fVerbose)
Gia_Man_t *	Cec_ManScorrCorrespondence (Gia_Man_t *p, Cec_ParCor_t *pCorPars)

Typedef Documentation

Tst_Dat_t

typedef typedefABC_NAMESPACE_IMPL_START struct Tst_Dat_t_ Tst_Dat_t

DECLARATIONS ///.

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

FileName [abcScorr.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Signal correspondence testing procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 36 of file abcScorr.c.

Function Documentation

Abc_NtkBmcFileName()

char * Abc_NtkBmcFileName

(

char *

pName

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 194 of file abcScorr.c.

{
    static char Buffer[1000];
    char * pNameGeneric = Extra_FileNameGeneric( pName );
    sprintf( Buffer, "%s_bmc%s", pNameGeneric, pName + strlen(pNameGeneric) );
    ABC_FREE( pNameGeneric );
    return Buffer;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkMapGiaIntoNameId()

Vec_Int_t * Abc_NtkMapGiaIntoNameId	(	Abc_Ntk_t *	pNetlist,
		Aig_Man_t *	pAig,
		Gia_Man_t *	pGia )

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file abcScorr.c.

{
    Vec_Int_t * vId2Name;
    Abc_Obj_t * pNet, * pNode, * pAnd;
    Aig_Obj_t * pObjAig;
    int i;
    vId2Name = Vec_IntAlloc( 0 );
    Vec_IntFill( vId2Name, pGia ? Gia_ManObjNum(pGia) : Aig_ManObjNumMax(pAig), ~0 );
    // copy all names
    Abc_NtkForEachNet( pNetlist, pNet, i )
    {
        pNode = Abc_ObjFanin0(pNet)->pCopy; 
        if ( pNode && (pAnd = Abc_ObjRegular(pNode->pCopy)) && 
            (pObjAig = (Aig_Obj_t *)Abc_ObjRegular(pAnd->pCopy)) && 
             Aig_ObjType(pObjAig) != AIG_OBJ_NONE )
        {
            if ( pGia == NULL )
                Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) );
            else
                Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
        }
    }
    // overwrite CO names
    Abc_NtkForEachCo( pNetlist, pNode, i )
    {
        pNet = Abc_ObjFanin0(pNode);
        pNode = pNode->pCopy;
        if ( pNode && (pAnd = Abc_ObjRegular(pNode->pCopy)) && 
            (pObjAig = (Aig_Obj_t *)Abc_ObjRegular(pAnd->pCopy)) && 
             Aig_ObjType(pObjAig) != AIG_OBJ_NONE )
        {
            if ( pGia == NULL )
                Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) );
            else
                Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
        }
    }
    // overwrite CI names
    Abc_NtkForEachCi( pNetlist, pNode, i )
    {
        pNet = Abc_ObjFanout0(pNode);
        pNode = pNode->pCopy;
        if ( pNode && (pAnd = Abc_ObjRegular(pNode->pCopy)) && 
            (pObjAig = (Aig_Obj_t *)Abc_ObjRegular(pAnd->pCopy)) && 
             Aig_ObjType(pObjAig) != AIG_OBJ_NONE )
        {
            if ( pGia == NULL )
                Vec_IntWriteEntry( vId2Name, Aig_ObjId(pObjAig), Abc_ObjId(pNet) );
            else
                Vec_IntWriteEntry( vId2Name, Abc_Lit2Var(pObjAig->iData), Abc_ObjId(pNet) );
        }
    }
    return vId2Name;
}

Here is the caller graph for this function:

Abc_NtkTestScorr()

Abc_Ntk_t * Abc_NtkTestScorr	(	char *	pFileNameIn,
		char *	pFileNameOut,
		int	nStepsMax,
		int	nBTLimit,
		int	fNewAlgo,
		int	fFlopOnly,
		int	fFfNdOnly,
		int	fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file abcScorr.c.

{
    extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
    extern Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
 
    FILE * pFile;
    Tst_Dat_t Data, * pData = &Data;
    Vec_Int_t * vId2Name;
    Abc_Ntk_t * pNetlist, * pLogic, * pStrash, * pResult;
    Aig_Man_t * pAig, * pTempAig;
    Gia_Man_t * pGia, * pTempGia;
//    int Counter = 0;
    // check the files
    pFile = fopen( pFileNameIn, "rb" );
    if ( pFile == NULL )
    {
        printf( "Input file \"%s\" cannot be opened.\n", pFileNameIn );
        return NULL;
    }
    fclose( pFile );
    // check the files
    pFile = fopen( pFileNameOut, "wb" );
    if ( pFile == NULL )
    {
        printf( "Output file \"%s\" cannot be opened.\n", pFileNameOut );
        return NULL;
    }
    fclose( pFile );
    // derive AIG for signal correspondence
    pNetlist = Io_ReadNetlist( pFileNameIn, Io_ReadFileType(pFileNameIn), 1 );
    if ( pNetlist == NULL )
    {
        printf( "Reading input file \"%s\" has failed.\n", pFileNameIn );
        return NULL;
    }
    pLogic = Abc_NtkToLogic( pNetlist );
    if ( pLogic == NULL )
    {
        Abc_NtkDelete( pNetlist );
        printf( "Deriving logic network from input file %s has failed.\n", pFileNameIn );
        return NULL;
    }
    if ( Extra_FileIsType( pFileNameIn, ".bench", ".BENCH", NULL ) )
    {
        // get the init file name
        char * pFileNameInit = Extra_FileNameGenericAppend( pLogic->pSpec, ".init" );
        pFile = fopen( pFileNameInit, "rb" );
        if ( pFile == NULL )
        {
            printf( "Init file \"%s\" cannot be opened.\n", pFileNameInit );
            return NULL;
        }
        Io_ReadBenchInit( pLogic, pFileNameInit );
        Abc_NtkConvertDcLatches( pLogic );
        if ( fVerbose )
            printf( "Initial state was derived from file \"%s\".\n", pFileNameInit );
    }
    pStrash = Abc_NtkStrash( pLogic, 0, 1, 0 );
    if ( pStrash == NULL )
    {
        Abc_NtkDelete( pLogic );
        Abc_NtkDelete( pNetlist );
        printf( "Deriving strashed network from input file %s has failed.\n", pFileNameIn );
        return NULL;
    }
    pAig = Abc_NtkToDar( pStrash, 0, 1 ); // performs "zero" internally
    // the newer computation (&scorr)
    if ( fNewAlgo )
    {
        Cec_ParCor_t CorPars, * pCorPars = &CorPars;
        Cec_ManCorSetDefaultParams( pCorPars );
        pCorPars->nBTLimit  = nBTLimit;
        pCorPars->nStepsMax = nStepsMax;
        pCorPars->fVerbose  = fVerbose;
        pCorPars->fUseCSat  = 1;
        pGia = Gia_ManFromAig( pAig );
        // prepare the data-structure
        memset( pData, 0, sizeof(Tst_Dat_t) );
        pData->pNetlist     = pNetlist;
        pData->pAig         = NULL;
        pData->pGia         = pGia;
        pData->vId2Name     = vId2Name = Abc_NtkMapGiaIntoNameId( pNetlist, pAig, pGia );
        pData->pFileNameOut = pFileNameOut;
        pData->fFlopOnly    = fFlopOnly;
        pData->fFfNdOnly    = fFfNdOnly;
        pData->fDumpBmc     = 1;
        pCorPars->pData     = pData;
        pCorPars->pFunc     = (void *)Abc_NtkTestScorrWriteEquivGia;
        // call signal correspondence
        pTempGia = Cec_ManLSCorrespondence( pGia, pCorPars );
        pTempAig = Gia_ManToAigSimple( pTempGia );
        Gia_ManStop( pTempGia );
        Gia_ManStop( pGia );
    }
    // the older computation (scorr)
    else
    {
        Ssw_Pars_t SswPars, * pSswPars = &SswPars;
        Ssw_ManSetDefaultParams( pSswPars );
        pSswPars->nBTLimit  = nBTLimit;
        pSswPars->nStepsMax = nStepsMax;
        pSswPars->fVerbose  = fVerbose;
        // preSswPare the data-structure
        memset( pData, 0, sizeof(Tst_Dat_t) );
        pData->pNetlist     = pNetlist;
        pData->pAig         = pAig;
        pData->pGia         = NULL;
        pData->vId2Name     = vId2Name = Abc_NtkMapGiaIntoNameId( pNetlist, pAig, NULL );
        pData->pFileNameOut = pFileNameOut;
        pData->fFlopOnly    = fFlopOnly;
        pData->fFfNdOnly    = fFfNdOnly;
        pData->fDumpBmc     = 1;
        pSswPars->pData     = pData;
        pSswPars->pFunc     = (void *)Abc_NtkTestScorrWriteEquivAig;
        // call signal correspondence
        pTempAig = Ssw_SignalCorrespondence( pAig, pSswPars );
    }
    // create the resulting AIG
    pResult = Abc_NtkFromDarSeqSweep( pStrash, pTempAig );
    // cleanup
    Vec_IntFree( vId2Name );
    Aig_ManStop( pAig );
    Aig_ManStop( pTempAig );
    Abc_NtkDelete( pStrash );
    Abc_NtkDelete( pLogic );
    Abc_NtkDelete( pNetlist );
    return pResult;
}

Here is the call graph for this function:

Abc_NtkTestScorrGetName()

char * Abc_NtkTestScorrGetName	(	Abc_Ntk_t *	pNetlist,
		Vec_Int_t *	vId2Name,
		int	Id )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file abcScorr.c.

{
//    Abc_Obj_t * pObj;
//printf( "trying to get name for %d\n", Id );
    if ( Vec_IntEntry(vId2Name, Id) == ~0 )
        return NULL;
//    pObj = Abc_NtkObj( pNetlist, Vec_IntEntry(vId2Name, Id) );
//    pObj = Abc_ObjFanin0(pObj);
//    assert( Abc_ObjIsCi(pObj) );
    return Nm_ManFindNameById( pNetlist->pManName, Vec_IntEntry(vId2Name, Id) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkTestScorrWriteEquivAig()

int Abc_NtkTestScorrWriteEquivAig

(

Tst_Dat_t *

pData

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 267 of file abcScorr.c.

{
    Abc_Ntk_t * pNetlist = pData->pNetlist;
    Vec_Int_t * vId2Name = pData->vId2Name;
    Aig_Man_t * pAig     = pData->pAig;
    char * pFileNameOut  = pData->pFileNameOut;
    FILE * pFile;
    Aig_Obj_t * pObj, * pRepr;
    int i, Counter = 0;
    if ( pData->fDumpBmc )
    {
        pData->fDumpBmc = 0;
        pFileNameOut = Abc_NtkBmcFileName( pFileNameOut );
    }
    pFile = fopen( pFileNameOut, "wb" );
    Aig_ManForEachObj( pAig, pObj, i )
    {
        if ( (pRepr = Aig_ObjRepr(pAig, pObj)) == NULL )
            continue;
        if ( pData->fFlopOnly )
        {
            if ( !Saig_ObjIsLo(pAig, pObj) || !(Saig_ObjIsLo(pAig, pRepr)||pRepr==Aig_ManConst1(pAig)) )
                continue;
        }
        else if ( pData->fFfNdOnly )
        {
            if ( !Saig_ObjIsLo(pAig, pObj) && !(Saig_ObjIsLo(pAig, pRepr)||pRepr==Aig_ManConst1(pAig)) )
                continue;
        }
        if ( pRepr == Aig_ManConst1(pAig) )
            Counter += Abc_NtkTestScorrWriteEquivConst( pNetlist, vId2Name, Aig_ObjId(pObj), pFile, Aig_ObjPhase(pObj) );
        else
            Counter += Abc_NtkTestScorrWriteEquivPair( pNetlist, vId2Name, Aig_ObjId(pRepr), Aig_ObjId(pObj), pFile, 
                Aig_ObjPhase(pRepr) ^ Aig_ObjPhase(pObj) );
    }
    fclose( pFile );
    printf( "%d pairs of sequentially equivalent nodes are written into file \"%s\".\n", Counter, pFileNameOut );
    return Counter;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkTestScorrWriteEquivConst()

int Abc_NtkTestScorrWriteEquivConst	(	Abc_Ntk_t *	pNetlist,
		Vec_Int_t *	vId2Name,
		int	Id1,
		FILE *	pFile,
		int	fPol )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file abcScorr.c.

{
    char * pName1 = Abc_NtkTestScorrGetName( pNetlist, vId2Name, Id1 );
    if ( pName1 == NULL )
        return 0;
    fprintf( pFile, "%s=%s%s\n", pName1, fPol? "~": "", "const0" );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkTestScorrWriteEquivGia()

int Abc_NtkTestScorrWriteEquivGia

(

Tst_Dat_t *

pData

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file abcScorr.c.

{
    Abc_Ntk_t * pNetlist = pData->pNetlist;
    Vec_Int_t * vId2Name = pData->vId2Name;
    Gia_Man_t * pGia     = pData->pGia;
    char * pFileNameOut  = pData->pFileNameOut;
    FILE * pFile;
    Gia_Obj_t * pObj, * pRepr;
    int i, Counter = 0;
    if ( pData->fDumpBmc )
    {
        pData->fDumpBmc = 0;
        pFileNameOut = Abc_NtkBmcFileName( pFileNameOut );
    }
    pFile = fopen( pFileNameOut, "wb" );
    Gia_ManSetPhase( pGia );
    Gia_ManForEachObj( pGia, pObj, i )
    {
        if ( !Gia_ObjHasRepr(pGia, i) )
            continue;
        pRepr = Gia_ManObj( pGia,Gia_ObjRepr(pGia, i) );
        if ( pData->fFlopOnly )
        {
            if ( !Gia_ObjIsRo(pGia, pObj) || !(Gia_ObjIsRo(pGia, pRepr)||Gia_ObjIsConst0(pRepr)) )
                continue;
        }
        else if ( pData->fFfNdOnly )
        {
            if ( !Gia_ObjIsRo(pGia, pObj) && !(Gia_ObjIsRo(pGia, pRepr)||Gia_ObjIsConst0(pRepr)) )
                continue;
        }
        if ( Gia_ObjRepr(pGia, i) == 0 )
            Counter += Abc_NtkTestScorrWriteEquivConst( pNetlist, vId2Name, i, pFile, Gia_ObjPhase(pObj) );
        else
            Counter += Abc_NtkTestScorrWriteEquivPair( pNetlist, vId2Name, Gia_ObjRepr(pGia, i), i, pFile, 
                Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
    }
    fclose( pFile );
    printf( "%d pairs of sequentially equivalent nodes are written into file \"%s\".\n", Counter, pFileNameOut );
    return Counter;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Abc_NtkTestScorrWriteEquivPair()

int Abc_NtkTestScorrWriteEquivPair	(	Abc_Ntk_t *	pNetlist,
		Vec_Int_t *	vId2Name,
		int	Id1,
		int	Id2,
		FILE *	pFile,
		int	fPol )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 153 of file abcScorr.c.

{
    char * pName1 = Abc_NtkTestScorrGetName( pNetlist, vId2Name, Id1 );
    char * pName2 = Abc_NtkTestScorrGetName( pNetlist, vId2Name, Id2 );
    if ( pName1 == NULL || pName2 == NULL )
        return 0;
    fprintf( pFile, "%s=%s%s\n", pName1, fPol? "~": "", pName2 );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Cec_ManScorrCorrespondence()

Gia_Man_t * Cec_ManScorrCorrespondence	(	Gia_Man_t *	p,
		Cec_ParCor_t *	pCorPars )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 458 of file abcScorr.c.

{
    Gia_Man_t * pRes = NULL;
    Aig_Man_t * pOld, * pNew;
    Ssw_Pars_t SswPars, * pSswPars = &SswPars;
    Ssw_ManSetDefaultParams( pSswPars );
    pSswPars->nBTLimit   = pCorPars->nBTLimit;
    pSswPars->nFramesK   = pCorPars->nFrames;
    pSswPars->fLatchCorr = pCorPars->fLatchCorr;
    pSswPars->fVerbose   = pCorPars->fVerbose;
    pOld = Gia_ManToAigSimple( p );
    pNew = Ssw_SignalCorrespondence( pOld, pSswPars );
    pRes = Gia_ManFromAigSimple( pNew );
    Gia_ManReprFromAigRepr( pOld, p );
    Aig_ManStop( pOld );
    Aig_ManStop( pNew );
    return pRes;
}

Here is the call graph for this function: