summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcVerify.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2006-10-07 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2006-10-07 08:01:00 -0700
commit73bb7932f7edad95086d67a795444537c438309e (patch)
tree43ce6255913e15ecb3f4f8a41ac531d6679ddcf1 /src/base/abci/abcVerify.c
parent0da555cb481696efd78d9c5dc6293b6a95d1ffd5 (diff)
downloadabc-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.c22
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 )