From 765a21240891735a844dd64d1d73789ae6e55bc6 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 2 Oct 2007 08:01:00 -0700 Subject: Version abc71002 --- src/aig/fra/fra.h | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) (limited to 'src/aig/fra/fra.h') diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 0de803ed..8cd677d1 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -53,6 +53,7 @@ typedef struct Fra_Par_t_ Fra_Par_t; typedef struct Fra_Man_t_ Fra_Man_t; typedef struct Fra_Cla_t_ Fra_Cla_t; typedef struct Fra_Sml_t_ Fra_Sml_t; +typedef struct Fra_Cex_t_ Fra_Cex_t; typedef struct Fra_Bmc_t_ Fra_Bmc_t; // FRAIG parameters @@ -118,6 +119,17 @@ struct Fra_Sml_t_ unsigned pData[0]; // simulation data for the nodes }; +// simulation manager +struct Fra_Cex_t_ +{ + int iPo; // the zero-based number of PO, for which verification failed + int iFrame; // the zero-based number of the time-frame, for which verificaiton failed + int nRegs; // the number of registers in the miter + int nPis; // the number of primary inputs in the miter + int nBits; // the number of words of bit data used + unsigned pData[0]; // the cex bit data (the number of bits: nRegs + (iFrame+1) * nPis) +}; + // FRAIG manager struct Fra_Man_t_ { @@ -227,6 +239,7 @@ extern int Fra_BmcNodeIsConst( Aig_Obj_t * pObj ); extern int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); extern void Fra_BmcStop( Fra_Bmc_t * p ); extern void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth ); +extern void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRewrite, int fVerbose ); /*=== fraClass.c ========================================================*/ extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ); extern void Fra_ClassesStop( Fra_Cla_t * p ); @@ -247,9 +260,10 @@ extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pO /*=== fraCore.c ========================================================*/ extern void Fra_FraigSweep( Fra_Man_t * pManAig ); extern int Fra_FraigMiterStatus( Aig_Man_t * p ); +extern int Fra_FraigMiterAssertedOutput( Aig_Man_t * p ); extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax ); -extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax ); +extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve ); /*=== fraImp.c ========================================================*/ extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr ); extern void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums ); @@ -291,7 +305,11 @@ extern Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrame extern void Fra_SmlStop( Fra_Sml_t * p ); extern Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords ); extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords ); - +extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ); +extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel ); +extern void Fra_SmlFreeCounterExample( Fra_Cex_t * p ); +extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p ); +extern Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut ); #ifdef __cplusplus } -- cgit v1.2.3