diff options
Diffstat (limited to 'src/base/abci/abcVerify.c')
| -rw-r--r-- | src/base/abci/abcVerify.c | 110 |
1 files changed, 106 insertions, 4 deletions
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index c891772f..05bd021d 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -52,7 +52,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -120,7 +120,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 1, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -198,6 +198,108 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV /**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 ) + { + // 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 %d (out of %d)\r", i+1, Abc_NtkPoNum(pMiter) ); + nOutputs += nPartSize; + } +// if ( pMiter->pModel ) +// Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); + 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 brute-force SAT.] Description [] @@ -216,7 +318,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); @@ -298,7 +400,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr int RetValue; // get the miter of the two networks - pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0 ); + pMiter = Abc_NtkMiter( pNtk1, pNtk2, 0, 0 ); if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); |