summaryrefslogtreecommitdiffstats
path: root/src/base/abci/abcVerify.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci/abcVerify.c')
-rw-r--r--src/base/abci/abcVerify.c97
1 files changed, 76 insertions, 21 deletions
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 424c26ec..58b8fbb8 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -19,8 +19,16 @@
***********************************************************************/
#include "abc.h"
+#include "main.h"
+#include "cmd.h"
#include "fraig.h"
#include "sim.h"
+#include "aig.h"
+#include "gia.h"
+#include "ssw.h"
+
+ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -151,7 +159,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
// Params.fFuncRed = 0;
// Params.nPatsRand = 0;
// Params.nPatsDyna = 0;
- pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 );
+ pMan = (Fraig_Man_t *)Abc_NtkToFraig( pMiter, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
// analyze the result
@@ -209,9 +217,6 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
***********************************************************************/
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;
@@ -327,8 +332,6 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
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;
@@ -375,7 +378,7 @@ void Abc_NtkCecFraigPartAuto( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds
Status = 1;
nOutputs = 0;
vOnePtr = Vec_PtrAlloc( 1000 );
- Vec_PtrForEachEntry( vParts, vOne, i )
+ Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i )
{
// get this part of the miter
Abc_NtkConvertCos( pMiter, vOne, vOnePtr );
@@ -596,7 +599,7 @@ int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFr
// Params.fFuncRed = 0;
// Params.nPatsRand = 0;
// Params.nPatsDyna = 0;
- pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 );
+ pMan = (Fraig_Man_t *)Abc_NtkToFraig( pFrames, &Params, 0, 0 );
Fraig_ManProveMiter( pMan );
// analyze the result
@@ -667,20 +670,20 @@ 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_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)1;
Abc_NtkForEachCi( pNtk, pNode, i )
- pNode->pCopy = (void *)(ABC_PTRINT_T)pModel[i];
+ pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)pModel[i];
// simulate in the topological order
Abc_NtkForEachNode( pNtk, pNode, i )
{
- Value0 = ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
- Value1 = ((int)(ABC_PTRINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode);
- pNode->pCopy = (void *)(ABC_PTRINT_T)(Value0 & Value1);
+ Value0 = ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ (int)Abc_ObjFaninC0(pNode);
+ Value1 = ((int)(ABC_PTRINT_T)Abc_ObjFanin1(pNode)->pCopy) ^ (int)Abc_ObjFaninC1(pNode);
+ pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)(Value0 & Value1);
}
// fill the output values
pValues = ABC_ALLOC( int, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
- pValues[i] = ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode);
+ pValues[i] = ((int)(ABC_PTRINT_T)Abc_ObjFanin0(pNode)->pCopy) ^ (int)Abc_ObjFaninC0(pNode);
if ( fStrashed )
Abc_NtkDelete( pNtk );
return pValues;
@@ -740,12 +743,12 @@ void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pMode
vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 );
// set the PI numbers
Abc_NtkForEachCi( pNtk1, pNode, i )
- pNode->pCopy = (void*)(ABC_PTRINT_T)i;
+ pNode->pCopy = (Abc_Obj_t *)(ABC_PTRINT_T)i;
// print the model
- pNode = Vec_PtrEntry( vNodes, 0 );
+ pNode = (Abc_Obj_t *)Vec_PtrEntry( vNodes, 0 );
if ( Abc_ObjIsCi(pNode) )
{
- Vec_PtrForEachEntry( vNodes, pNode, i )
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
assert( Abc_ObjIsCi(pNode) );
printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)(ABC_PTRINT_T)pNode->pCopy] );
@@ -787,18 +790,18 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo )
// mark the support of the frames
Abc_NtkForEachCi( pFrames, pObj, i )
pObj->pCopy = NULL;
- Vec_PtrForEachEntry( vSupp, pObj, i )
- pObj->pCopy = (void *)1;
+ Vec_PtrForEachEntry( Abc_Obj_t *, vSupp, pObj, i )
+ pObj->pCopy = (Abc_Obj_t *)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;
+ pObj->pCopy = (Abc_Obj_t *)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;
+ pObj->pCopy = (Abc_Obj_t *)1;
// free stuff
Vec_PtrFree( vSupp );
Abc_NtkDelete( pFrames );
@@ -1012,8 +1015,60 @@ void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
}
+/**Function*************************************************************
+
+ Synopsis [Returns the PO values under the given input pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkIsTrueCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
+{
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+// extern int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Abc_Cex_t * p );
+ Aig_Man_t * pMan;
+ int status, fStrashed = 0;
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ pNtk = Abc_NtkStrash(pNtk, 0, 0, 0);
+ fStrashed = 1;
+ }
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan )
+ {
+ status = Ssw_SmlRunCounterExample( pMan, pCex );
+ Aig_ManStop( pMan );
+ }
+ if ( fStrashed )
+ Abc_NtkDelete( pNtk );
+ return status;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if the number of PIs matches.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkIsValidCex( Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
+{
+ return Abc_NtkPiNum(pNtk) == pCex->nPis;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 17:44:03 +0000