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/abcVerify.c

1019 lines
32 KiB
C
Raw Blame History

/**CFile****************************************************************
FileName [abcVerify.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Combinational and sequential verification for two networks.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcVerify.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "fraig.h"
#include "sim.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
extern void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Verifies combinational equivalence by brute-force SAT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit )
{
extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pCnf;
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return;
}
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are equivalent after structural hashing.\n" );
return;
}
// convert the miter into a CNF
pCnf = Abc_NtkMulti( pMiter, 0, 100, 1, 0, 0, 0 );
Abc_NtkDelete( pMiter );
if ( pCnf == NULL )
{
printf( "Renoding for CNF has failed.\n" );
return;
}
// solve the CNF using the SAT solver
RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, NULL, NULL );
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out).\n" );
else if ( RetValue == 0 )
printf( "Networks are NOT EQUIVALENT after SAT.\n" );
else
printf( "Networks are equivalent after SAT.\n" );
if ( pCnf->pModel )
Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel );
FREE( pCnf->pModel );
Abc_NtkDelete( pCnf );
}
/**Function*************************************************************
Synopsis [Verifies sequential equivalence by fraiging followed by SAT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
{
Prove_Params_t Params, * pParams = &Params;
// Fraig_Params_t Params;
// Fraig_Man_t * pMan;
Abc_Ntk_t * pMiter;
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return;
}
if ( RetValue == 1 )
{
printf( "Networks are equivalent after structural hashing.\n" );
Abc_NtkDelete( pMiter );
return;
}
/*
// convert the miter into a FRAIG
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
// Params.fFuncRed = 0;
// Params.nPatsRand = 0;
// Params.nPatsDyna = 0;
pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
// analyze the result
RetValue = Fraig_ManCheckMiter( pMan );
// report the result
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out on the final miter).\n" );
else if ( RetValue == 1 )
printf( "Networks are equivalent after fraiging.\n" );
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) );
}
else assert( 0 );
// delete the fraig manager
Fraig_ManFree( pMan );
// delete the miter
Abc_NtkDelete( pMiter );
*/
// solve the CNF using the SAT solver
Prove_ParamsSetDefault( pParams );
pParams->nItersMax = 5;
// RetValue = Abc_NtkMiterProve( &pMiter, pParams );
// pParams->fVerbose = 1;
RetValue = Abc_NtkIvyProve( &pMiter, pParams );
if ( RetValue == -1 )
printf( "Networks are undecided (resource limits is reached).\n" );
else if ( RetValue == 0 )
{
int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel );
if ( pSimInfo[0] != 1 )
printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
else
printf( "Networks are NOT EQUIVALENT.\n" );
free( pSimInfo );
}
else
printf( "Networks are equivalent.\n" );
if ( pMiter->pModel )
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
Abc_NtkDelete( pMiter );
}
/**Function*************************************************************
Synopsis [Verifies sequential equivalence by fraiging followed by SAT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkCecFraigPart( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nPartSize, int fVerbose )
{
extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
extern void * Abc_FrameGetGlobalFrame();
Prove_Params_t Params, * pParams = &Params;
Abc_Ntk_t * pMiter, * pMiterPart;
Abc_Obj_t * pObj;
int i, RetValue, Status, nOutputs;
// solve the CNF using the SAT solver
Prove_ParamsSetDefault( pParams );
pParams->nItersMax = 5;
// pParams->fVerbose = 1;
assert( nPartSize > 0 );
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, nPartSize );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return;
}
if ( RetValue == 1 )
{
printf( "Networks are equivalent after structural hashing.\n" );
Abc_NtkDelete( pMiter );
return;
}
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
// solve the problem iteratively for each output of the miter
Status = 1;
nOutputs = 0;
Abc_NtkForEachPo( pMiter, pObj, i )
{
if ( Abc_ObjFanin0(pObj) == Abc_AigConst1(pMiter) )
{
if ( Abc_ObjFaninC0(pObj) ) // complemented -> const 0
RetValue = 1;
else
RetValue = 0;
pMiterPart = NULL;
}
else
{
// get the cone of this output
pMiterPart = Abc_NtkCreateCone( pMiter, Abc_ObjFanin0(pObj), Abc_ObjName(pObj), 0 );
if ( Abc_ObjFaninC0(pObj) )
Abc_ObjXorFaninC( Abc_NtkPo(pMiterPart,0), 0 );
// solve the cone
// RetValue = Abc_NtkMiterProve( &pMiterPart, pParams );
RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
}
if ( RetValue == -1 )
{
printf( "Networks are undecided (resource limits is reached).\r" );
Status = -1;
}
else if ( RetValue == 0 )
{
int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
if ( pSimInfo[0] != 1 )
printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
else
printf( "Networks are NOT EQUIVALENT. \n" );
free( pSimInfo );
Status = 0;
break;
}
else
{
printf( "Finished part %5d (out of %5d)\r", i+1, Abc_NtkPoNum(pMiter) );
nOutputs += nPartSize;
}
// if ( pMiter->pModel )
// Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
if ( pMiterPart )
Abc_NtkDelete( pMiterPart );
}
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
if ( Status == 1 )
printf( "Networks are equivalent. \n" );
else if ( Status == -1 )
printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
Abc_NtkDelete( pMiter );
}
/**Function*************************************************************
Synopsis [Verifies sequential equivalence by fraiging followed by SAT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose )
{
extern int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd );
extern Vec_Ptr_t * Abc_NtkPartitionSmart( Abc_Ntk_t * pNtk, int nPartSizeLimit, int fVerbose );
extern void Abc_NtkConvertCos( Abc_Ntk_t * pNtk, Vec_Int_t * vOuts, Vec_Ptr_t * vOnePtr );
extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
extern void * Abc_FrameGetGlobalFrame();
Vec_Ptr_t * vParts, * vOnePtr;
Vec_Int_t * vOne;
Prove_Params_t Params, * pParams = &Params;
Abc_Ntk_t * pMiter, * pMiterPart;
int i, RetValue, Status, nOutputs;
// solve the CNF using the SAT solver
Prove_ParamsSetDefault( pParams );
pParams->nItersMax = 5;
// pParams->fVerbose = 1;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 1 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 );
Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return;
}
if ( RetValue == 1 )
{
printf( "Networks are equivalent after structural hashing.\n" );
Abc_NtkDelete( pMiter );
return;
}
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" );
// partition the outputs
vParts = Abc_NtkPartitionSmart( pMiter, 300, 0 );
// fraig each partition
Status = 1;
nOutputs = 0;
vOnePtr = Vec_PtrAlloc( 1000 );
Vec_PtrForEachEntry( vParts, vOne, i )
{
// get this part of the miter
Abc_NtkConvertCos( pMiter, vOne, vOnePtr );
pMiterPart = Abc_NtkCreateConeArray( pMiter, vOnePtr, 0 );
Abc_NtkCombinePos( pMiterPart, 0 );
// check the miter for being constant
RetValue = Abc_NtkMiterIsConstant( pMiterPart );
if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after partitioning.\n" );
Abc_NtkDelete( pMiterPart );
break;
}
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiterPart );
continue;
}
printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
i+1, Vec_PtrSize(vParts), Abc_NtkPiNum(pMiterPart), Abc_NtkPoNum(pMiterPart),
Abc_NtkNodeNum(pMiterPart), Abc_AigLevel(pMiterPart) );
// solve the problem
RetValue = Abc_NtkIvyProve( &pMiterPart, pParams );
if ( RetValue == -1 )
{
printf( "Networks are undecided (resource limits is reached).\r" );
Status = -1;
}
else if ( RetValue == 0 )
{
int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiterPart, pMiterPart->pModel );
if ( pSimInfo[0] != 1 )
printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
else
printf( "Networks are NOT EQUIVALENT. \n" );
free( pSimInfo );
Status = 0;
Abc_NtkDelete( pMiterPart );
break;
}
else
{
// printf( "Finished part %5d (out of %5d)\r", i+1, Vec_PtrSize(vParts) );
nOutputs += Vec_IntSize(vOne);
}
Abc_NtkDelete( pMiterPart );
}
printf( " \r" );
Vec_VecFree( (Vec_Vec_t *)vParts );
Vec_PtrFree( vOnePtr );
Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" );
if ( Status == 1 )
printf( "Networks are equivalent. \n" );
else if ( Status == -1 )
printf( "Timed out after verifying %d outputs (out of %d).\n", nOutputs, Abc_NtkCoNum(pNtk1) );
Abc_NtkDelete( pMiter );
}
/**Function*************************************************************
Synopsis [Verifies sequential equivalence by brute-force SAT.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames )
{
extern Abc_Ntk_t * Abc_NtkMulti( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pFrames;
Abc_Ntk_t * pCnf;
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
return;
}
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are equivalent after structural hashing.\n" );
return;
}
// create the timeframes
pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
Abc_NtkDelete( pMiter );
if ( pFrames == NULL )
{
printf( "Frames computation has failed.\n" );
return;
}
RetValue = Abc_NtkMiterIsConstant( pFrames );
if ( RetValue == 0 )
{
Abc_NtkDelete( pFrames );
printf( "Networks are NOT EQUIVALENT after framing.\n" );
return;
}
if ( RetValue == 1 )
{
Abc_NtkDelete( pFrames );
printf( "Networks are equivalent after framing.\n" );
return;
}
// convert the miter into a CNF
pCnf = Abc_NtkMulti( pFrames, 0, 100, 1, 0, 0, 0 );
Abc_NtkDelete( pFrames );
if ( pCnf == NULL )
{
printf( "Renoding for CNF has failed.\n" );
return;
}
// solve the CNF using the SAT solver
RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, NULL, NULL );
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out).\n" );
else if ( RetValue == 0 )
printf( "Networks are NOT EQUIVALENT after SAT.\n" );
else
printf( "Networks are equivalent after SAT.\n" );
Abc_NtkDelete( pCnf );
}
/**Function*************************************************************
Synopsis [Verifies combinational equivalence by fraiging followed by SAT]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose )
{
Fraig_Params_t Params;
Fraig_Man_t * pMan;
Abc_Ntk_t * pMiter;
Abc_Ntk_t * pFrames;
int RetValue;
// get the miter of the two networks
pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 );
if ( pMiter == NULL )
{
printf( "Miter computation has failed.\n" );
return 0;
}
RetValue = Abc_NtkMiterIsConstant( pMiter );
if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
// report the error
pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, nFrames );
Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames );
FREE( pMiter->pModel );
Abc_NtkDelete( pMiter );
return 0;
}
if ( RetValue == 1 )
{
Abc_NtkDelete( pMiter );
printf( "Networks are equivalent after structural hashing.\n" );
return 1;
}
// create the timeframes
pFrames = Abc_NtkFrames( pMiter, nFrames, 1 );
Abc_NtkDelete( pMiter );
if ( pFrames == NULL )
{
printf( "Frames computation has failed.\n" );
return 0;
}
RetValue = Abc_NtkMiterIsConstant( pFrames );
if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after framing.\n" );
// report the error
pFrames->pModel = Abc_NtkVerifyGetCleanModel( pFrames, 1 );
// Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames );
FREE( pFrames->pModel );
Abc_NtkDelete( pFrames );
return 0;
}
if ( RetValue == 1 )
{
Abc_NtkDelete( pFrames );
printf( "Networks are equivalent after framing.\n" );
return 1;
}
// convert the miter into a FRAIG
Fraig_ParamsSetDefault( &Params );
Params.fVerbose = fVerbose;
Params.nSeconds = nSeconds;
// Params.fFuncRed = 0;
// Params.nPatsRand = 0;
// Params.nPatsDyna = 0;
pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
// analyze the result
RetValue = Fraig_ManCheckMiter( pMan );
// report the result
if ( RetValue == -1 )
printf( "Networks are undecided (SAT solver timed out on the final miter).\n" );
else if ( RetValue == 1 )
printf( "Networks are equivalent after fraiging.\n" );
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT after fraiging.\n" );
// Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, Fraig_ManReadModel(pMan), nFrames );
}
else assert( 0 );
// delete the fraig manager
Fraig_ManFree( pMan );
// delete the miter
Abc_NtkDelete( pFrames );
return RetValue == 1;
}
/**Function*************************************************************
Synopsis [Returns a dummy pattern full of zeros.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames )
{
int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) * nFrames );
memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) * nFrames );
return pModel;
}
/**Function*************************************************************
Synopsis [Returns the PO values under the given input pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel )
{
Abc_Obj_t * pNode;
int * pValues, Value0, Value1, i;
int fStrashed = 0;
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash(pNtk, 0, 0, 0);
fStrashed = 1;
}
/*
printf( "Counter example: " );
Abc_NtkForEachCi( pNtk, pNode, i )
printf( " %d", pModel[i] );
printf( "\n" );
*/
// increment the trav ID
Abc_NtkIncrementTravId( pNtk );
// set the CI values
Abc_AigConst1(pNtk)->pCopy = (void *)1;
Abc_NtkForEachCi( pNtk, pNode, i )
pNode->pCopy = (void *)pModel[i];
// simulate in the topological order
Abc_NtkForEachNode( pNtk, pNode, i )
{
Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
pNode->pCopy = (void *)(Value0 & Value1);
}
// fill the output values
pValues = ALLOC( int, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
if ( fStrashed )
Abc_NtkDelete( pNtk );
return pValues;
}
/**Function*************************************************************
Synopsis [Reports mismatch between the two networks.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
int * pValues1, * pValues2;
int nErrors, nPrinted, i, iNode = -1;
assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) );
assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) );
// get the CO values under this model
pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel );
pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel );
// count the mismatches
nErrors = 0;
for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
nErrors += (int)( pValues1[i] != pValues2[i] );
printf( "Verification failed for at least %d outputs: ", nErrors );
// print the first 3 outputs
nPrinted = 0;
for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ )
if ( pValues1[i] != pValues2[i] )
{
if ( iNode == -1 )
iNode = i;
printf( " %s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) );
if ( ++nPrinted == 3 )
break;
}
if ( nPrinted != nErrors )
printf( " ..." );
printf( "\n" );
// report mismatch for the first output
if ( iNode >= 0 )
{
printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n",
Abc_ObjName(Abc_NtkCo(pNtk1,iNode)), pValues1[iNode], pValues2[iNode] );
printf( "Input pattern: " );
// collect PIs in the cone
pNode = Abc_NtkCo(pNtk1,iNode);
vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
// set the PI numbers
Abc_NtkForEachCi( pNtk1, pNode, i )
pNode->pCopy = (void*)i;
// print the model
pNode = Vec_PtrEntry( vNodes, 0 );
if ( Abc_ObjIsCi(pNode) )
{
Vec_PtrForEachEntry( vNodes, pNode, i )
{
assert( Abc_ObjIsCi(pNode) );
printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] );
}
}
printf( "\n" );
Vec_PtrFree( vNodes );
}
free( pValues1 );
free( pValues2 );
}
/**Function*************************************************************
Synopsis [Computes the COs in the support of the PO in the given frame.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
{
Abc_Ntk_t * pFrames;
Abc_Obj_t * pObj, * pNodePo;
Vec_Ptr_t * vSupp;
int i, k;
// get the timeframes of the network
pFrames = Abc_NtkFrames( pNtk, iFrame + 1, 0 );
//Abc_NtkShowAig( pFrames );
// get the PO of the timeframes
pNodePo = Abc_NtkPo( pFrames, iFrame * Abc_NtkPoNum(pNtk) + iNumPo );
// set the support
vSupp = Abc_NtkNodeSupport( pFrames, &pNodePo, 1 );
// mark the support of the frames
Abc_NtkForEachCi( pFrames, pObj, i )
pObj->pCopy = NULL;
Vec_PtrForEachEntry( vSupp, pObj, i )
pObj->pCopy = (void *)1;
// mark the support of the network if the support of the timeframes is marked
Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pCopy = NULL;
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( Abc_NtkBox(pFrames, i)->pCopy )
pObj->pCopy = (void *)1;
Abc_NtkForEachPi( pNtk, pObj, i )
for ( k = 0; k <= iFrame; k++ )
if ( Abc_NtkPi(pFrames, k*Abc_NtkPiNum(pNtk) + i)->pCopy )
pObj->pCopy = (void *)1;
// free stuff
Vec_PtrFree( vSupp );
Abc_NtkDelete( pFrames );
}
/**Function*************************************************************
Synopsis [Reports mismatch between the two sequential networks.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames )
{
Vec_Ptr_t * vInfo1, * vInfo2;
Abc_Obj_t * pObj, * pObjError, * pObj1, * pObj2;
int ValueError1, ValueError2;
unsigned * pPats1, * pPats2;
int i, o, k, nErrors, iFrameError, iNodePo, nPrinted;
int fRemove1 = 0, fRemove2 = 0;
if ( !Abc_NtkIsStrash(pNtk1) )
fRemove1 = 1, pNtk1 = Abc_NtkStrash( pNtk1, 0, 0, 0 );
if ( !Abc_NtkIsStrash(pNtk2) )
fRemove2 = 1, pNtk2 = Abc_NtkStrash( pNtk2, 0, 0, 0 );
// simulate sequential circuits
vInfo1 = Sim_SimulateSeqModel( pNtk1, nFrames, pModel );
vInfo2 = Sim_SimulateSeqModel( pNtk2, nFrames, pModel );
// look for a discrepancy in the PO values
nErrors = 0;
pObjError = NULL;
for ( i = 0; i < nFrames; i++ )
{
if ( pObjError )
break;
Abc_NtkForEachPo( pNtk1, pObj1, o )
{
pObj2 = Abc_NtkPo( pNtk2, o );
pPats1 = Sim_SimInfoGet(vInfo1, pObj1);
pPats2 = Sim_SimInfoGet(vInfo2, pObj2);
if ( pPats1[i] == pPats2[i] )
continue;
nErrors++;
if ( pObjError == NULL )
{
pObjError = pObj1;
iFrameError = i;
iNodePo = o;
ValueError1 = (pPats1[i] > 0);
ValueError2 = (pPats2[i] > 0);
}
}
}
if ( pObjError == NULL )
{
printf( "No output mismatches detected.\n" );
Sim_UtilInfoFree( vInfo1 );
Sim_UtilInfoFree( vInfo2 );
if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
return;
}
printf( "Verification failed for at least %d output%s of frame %d: ", nErrors, (nErrors>1? "s":""), iFrameError+1 );
// print the first 3 outputs
nPrinted = 0;
Abc_NtkForEachPo( pNtk1, pObj1, o )
{
pObj2 = Abc_NtkPo( pNtk2, o );
pPats1 = Sim_SimInfoGet(vInfo1, pObj1);
pPats2 = Sim_SimInfoGet(vInfo2, pObj2);
if ( pPats1[iFrameError] == pPats2[iFrameError] )
continue;
printf( " %s", Abc_ObjName(pObj1) );
if ( ++nPrinted == 3 )
break;
}
if ( nPrinted != nErrors )
printf( " ..." );
printf( "\n" );
// mark CIs of the networks in the cone of influence of this output
Abc_NtkGetSeqPoSupp( pNtk1, iFrameError, iNodePo );
Abc_NtkGetSeqPoSupp( pNtk2, iFrameError, iNodePo );
// report mismatch for the first output
printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n",
Abc_ObjName(pObjError), ValueError1, ValueError2 );
printf( "The cone of influence of output %s in Network1:\n", Abc_ObjName(pObjError) );
printf( "PIs: " );
Abc_NtkForEachPi( pNtk1, pObj, i )
if ( pObj->pCopy )
printf( "%s ", Abc_ObjName(pObj) );
printf( "\n" );
printf( "Latches: " );
Abc_NtkForEachLatch( pNtk1, pObj, i )
if ( pObj->pCopy )
printf( "%s ", Abc_ObjName(pObj) );
printf( "\n" );
printf( "The cone of influence of output %s in Network2:\n", Abc_ObjName(pObjError) );
printf( "PIs: " );
Abc_NtkForEachPi( pNtk2, pObj, i )
if ( pObj->pCopy )
printf( "%s ", Abc_ObjName(pObj) );
printf( "\n" );
printf( "Latches: " );
Abc_NtkForEachLatch( pNtk2, pObj, i )
if ( pObj->pCopy )
printf( "%s ", Abc_ObjName(pObj) );
printf( "\n" );
// print the patterns
for ( i = 0; i <= iFrameError; i++ )
{
printf( "Frame %d: ", i+1 );
printf( "PI(1):" );
Abc_NtkForEachPi( pNtk1, pObj, k )
if ( pObj->pCopy )
printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 );
printf( " " );
printf( "L(1):" );
Abc_NtkForEachLatch( pNtk1, pObj, k )
if ( pObj->pCopy )
printf( "%d", Sim_SimInfoGet(vInfo1, pObj)[i] > 0 );
printf( " " );
printf( "%s(1):", Abc_ObjName(pObjError) );
printf( "%d", Sim_SimInfoGet(vInfo1, pObjError)[i] > 0 );
printf( " " );
printf( "PI(2):" );
Abc_NtkForEachPi( pNtk2, pObj, k )
if ( pObj->pCopy )
printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 );
printf( " " );
printf( "L(2):" );
Abc_NtkForEachLatch( pNtk2, pObj, k )
if ( pObj->pCopy )
printf( "%d", Sim_SimInfoGet(vInfo2, pObj)[i] > 0 );
printf( " " );
printf( "%s(2):", Abc_ObjName(pObjError) );
printf( "%d", Sim_SimInfoGet(vInfo2, pObjError)[i] > 0 );
printf( "\n" );
}
Abc_NtkForEachCi( pNtk1, pObj, i )
pObj->pCopy = NULL;
Abc_NtkForEachCi( pNtk2, pObj, i )
pObj->pCopy = NULL;
Sim_UtilInfoFree( vInfo1 );
Sim_UtilInfoFree( vInfo2 );
if ( fRemove1 ) Abc_NtkDelete( pNtk1 );
if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
}
/**Function*************************************************************
Synopsis [Simulates buggy miter emailed by Mike.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
{
Abc_Obj_t * pObj;
int i;
int * pModel1, * pModel2, * pResult1, * pResult2;
char * vPiValues1 = "01001011100000000011010110101000000";
char * vPiValues2 = "11001101011101011111110100100010001";
assert( strlen(vPiValues1) == (unsigned)Abc_NtkPiNum(pNtk) );
assert( 1 == Abc_NtkPoNum(pNtk) );
pModel1 = ALLOC( int, Abc_NtkCiNum(pNtk) );
Abc_NtkForEachPi( pNtk, pObj, i )
pModel1[i] = vPiValues1[i] - '0';
Abc_NtkForEachLatch( pNtk, pObj, i )
pModel1[Abc_NtkPiNum(pNtk)+i] = ((int)pObj->pData) - 1;
pResult1 = Abc_NtkVerifySimulatePattern( pNtk, pModel1 );
printf( "Value = %d\n", pResult1[0] );
pModel2 = ALLOC( int, Abc_NtkCiNum(pNtk) );
Abc_NtkForEachPi( pNtk, pObj, i )
pModel2[i] = vPiValues2[i] - '0';
Abc_NtkForEachLatch( pNtk, pObj, i )
pModel2[Abc_NtkPiNum(pNtk)+i] = pResult1[Abc_NtkPoNum(pNtk)+i];
pResult2 = Abc_NtkVerifySimulatePattern( pNtk, pModel2 );
printf( "Value = %d\n", pResult2[0] );
free( pModel1 );
free( pModel2 );
free( pResult1 );
free( pResult2 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
Reference in New Issue View Git Blame Copy Permalink