diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-10-07 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-10-07 08:01:00 -0700 |
| commit | 73bb7932f7edad95086d67a795444537c438309e (patch) | |
| tree | 43ce6255913e15ecb3f4f8a41ac531d6679ddcf1 /src/base/abci/abcVerify.c | |
| parent | 0da555cb481696efd78d9c5dc6293b6a95d1ffd5 (diff) | |
| download | abc-73bb7932f7edad95086d67a795444537c438309e.tar.gz abc-73bb7932f7edad95086d67a795444537c438309e.tar.bz2 abc-73bb7932f7edad95086d67a795444537c438309e.zip | |
Version abc61007
Diffstat (limited to 'src/base/abci/abcVerify.c')
| -rw-r--r-- | src/base/abci/abcVerify.c | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 1fddc8cb..622b4103 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -174,7 +174,8 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV // solve the CNF using the SAT solver Prove_ParamsSetDefault( pParams ); pParams->nItersMax = 5; - RetValue = Abc_NtkMiterProve( &pMiter, pParams ); +// RetValue = Abc_NtkMiterProve( &pMiter, pParams ); + RetValue = Abc_NtkIvyProve( &pMiter, pParams ); if ( RetValue == -1 ) printf( "Networks are undecided (resource limits is reached).\n" ); else if ( RetValue == 0 ) @@ -399,12 +400,11 @@ int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames ) SideEffects [] - SeeAlso [] + SeeAlso [] ***********************************************************************/ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) { - Vec_Ptr_t * vNodes; Abc_Obj_t * pNode; int * pValues, Value0, Value1, i; int fStrashed = 0; @@ -416,22 +416,16 @@ int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) // 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 - vNodes = Abc_NtkDfs( pNtk, 1 ); - Vec_PtrForEachEntry( vNodes, pNode, i ) + Abc_NtkForEachNode( pNtk, pNode, i ) { -// if ( Abc_NodeIsConst(pNode) ) -// pNode->pCopy = NULL; -// else - { - Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); - Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); - pNode->pCopy = (void *)(Value0 & Value1); - } + Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); + Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); + pNode->pCopy = (void *)(Value0 & Value1); } - Vec_PtrFree( vNodes ); // fill the output values pValues = ALLOC( int, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) |