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