diff options
Diffstat (limited to 'abc70930/src/base/abci/abcVerify.c')
| -rw-r--r-- | abc70930/src/base/abci/abcVerify.c | 1018 |
1 files changed, 1018 insertions, 0 deletions
diff --git a/abc70930/src/base/abci/abcVerify.c b/abc70930/src/base/abci/abcVerify.c new file mode 100644 index 00000000..9c9bbcfd --- /dev/null +++ b/abc70930/src/base/abci/abcVerify.c @@ -0,0 +1,1018 @@ +/**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 /// +//////////////////////////////////////////////////////////////////////// + + |