luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity
abc/src/base/abci/abcScorr.c

455 lines
14 KiB
C
Raw Blame History

/**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 $]
***********************************************************************/
#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"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Tst_Dat_t_ Tst_Dat_t;
struct Tst_Dat_t_
{
Abc_Ntk_t * pNetlist;
Aig_Man_t * pAig;
Gia_Man_t * pGia;
Vec_Int_t * vId2Name;
char * pFileNameOut;
int fFlopOnly;
int fFfNdOnly;
int fDumpBmc;
};
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_NtkMapGiaIntoNameId( Abc_Ntk_t * pNetlist, Aig_Man_t * pAig, Gia_Man_t * pGia )
{
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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_NtkTestScorrGetName( Abc_Ntk_t * pNetlist, Vec_Int_t * vId2Name, int Id )
{
// 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) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkTestScorrWriteEquivPair( Abc_Ntk_t * pNetlist, Vec_Int_t * vId2Name, int Id1, int Id2, FILE * pFile, int fPol )
{
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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkTestScorrWriteEquivConst( Abc_Ntk_t * pNetlist, Vec_Int_t * vId2Name, int Id1, FILE * pFile, int fPol )
{
char * pName1 = Abc_NtkTestScorrGetName( pNetlist, vId2Name, Id1 );
if ( pName1 == NULL )
return 0;
fprintf( pFile, "%s=%s%s\n", pName1, fPol? "~": "", "const0" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Abc_NtkBmcFileName( char * pName )
{
static char Buffer[1000];
char * pNameGeneric = Extra_FileNameGeneric( pName );
sprintf( Buffer, "%s_bmc%s", pNameGeneric, pName + strlen(pNameGeneric) );
ABC_FREE( pNameGeneric );
return Buffer;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkTestScorrWriteEquivGia( Tst_Dat_t * pData )
{
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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkTestScorrWriteEquivAig( Tst_Dat_t * pData )
{
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;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkTestScorr( char * pFileNameIn, char * pFileNameOut, int nStepsMax, int nBTLimit, int fNewAlgo, int fFlopOnly, int fFfNdOnly, int fVerbose )
{
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;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
Reference in New Issue View Git Blame Copy Permalink