/**CFile****************************************************************
FileName [abs.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Abstraction package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__proof_abs__Abs_h
#define ABC__proof_abs__Abs_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#include "aig/saig/saig.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// abstraction parameters
typedef struct Abs_Par_t_ Abs_Par_t;
struct Abs_Par_t_
{
int nFramesMax; // maximum frames
int nFramesStart; // starting frame
int nFramesPast; // overlap frames
int nConfLimit; // conflict limit
int nLearnedMax; // max number of learned clauses
int nLearnedStart; // max number of learned clauses
int nLearnedDelta; // delta increase of learned clauses
int nLearnedPerce; // percentage of clauses to leave
int nTimeOut; // timeout in seconds
int nRatioMin; // stop when less than this % of object is unabstracted
int nRatioMin2; // stop when less than this % of object is unabstracted during refinement
int nRatioMax; // restart when the number of abstracted object is more than this
int fUseTermVars; // use terminal variables
int fUseRollback; // use rollback to the starting number of frames
int fPropFanout; // propagate fanout implications
int fAddLayer; // refinement strategy by adding layers
int fNewRefine; // uses new refinement heuristics
int fUseSkip; // skip proving intermediate timeframes
int fUseSimple; // use simple CNF construction
int fSkipHash; // skip hashing CNF while unrolling
int fUseFullProof; // use full proof for UNSAT cores
int fDumpVabs; // dumps the abstracted model
int fDumpMabs; // dumps the original AIG with abstraction map
int fCallProver; // calls the prover
int fSimpProver; // calls simplification before prover
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
int fVeryVerbose; // print additional information
int iFrame; // the number of frames covered
int iFrameProved; // the number of frames proved
int nFramesNoChange; // the number of last frames without changes
int nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
};
// old abstraction parameters
typedef struct Gia_ParAbs_t_ Gia_ParAbs_t;
struct Gia_ParAbs_t_
{
int Algo; // the algorithm to be used
int nFramesMax; // timeframes for PBA
int nConfMax; // conflicts for PBA
int fDynamic; // dynamic unfolding for PBA
int fConstr; // use constraints
int nFramesBmc; // timeframes for BMC
int nConfMaxBmc; // conflicts for BMC
int nStableMax; // the number of stable frames to quit
int nRatio; // ratio of flops to quit
int TimeOut; // approximate timeout in seconds
int TimeOutVT; // approximate timeout in seconds
int nBobPar; // Bob's parameter
int fUseBdds; // use BDDs to refine abstraction
int fUseDprove; // use 'dprove' to refine abstraction
int fUseStart; // use starting frame
int fVerbose; // verbose output
int fVeryVerbose; // printing additional information
int Status; // the problem status
int nFramesDone; // the number of frames covered
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj)); }
static inline int Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj)); }
static inline int * Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1); }
static inline unsigned Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1); }
static inline int Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2); }
static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj ) { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== abs.c =========================================================*/
/*=== absDup.c =========================================================*/
extern Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
extern Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
extern void Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes );
extern void Gia_ManPrintFlopClasses( Gia_Man_t * p );
extern void Gia_ManPrintObjClasses( Gia_Man_t * p );
extern void Gia_ManPrintGateClasses( Gia_Man_t * p );
/*=== absGla.c =========================================================*/
extern int Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars );
/*=== absGlaOld.c =========================================================*/
extern int Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta );
/*=== absIter.c =========================================================*/
extern Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose );
/*=== absPth.c =========================================================*/
extern void Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose );
extern void Gia_GlaProveCancel( int fVerbose );
extern int Gia_GlaProveCheck( int fVerbose );
/*=== absVta.c =========================================================*/
extern int Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars );
/*=== absUtil.c =========================================================*/
extern void Abs_ParSetDefaults( Abs_Par_t * p );
extern Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
extern Vec_Int_t * Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
extern Vec_Int_t * Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
extern Vec_Int_t * Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
extern int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );
/*=== absRpm.c =========================================================*/
extern Gia_Man_t * Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose );
/*=== absRpmOld.c =========================================================*/
extern Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose );
extern void Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p );
extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
/*=== absOldCex.c ==========================================================*/
extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
/*=== absOldRef.c ==========================================================*/
extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
/*=== absOldSat.c ==========================================================*/
extern Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
/*=== absOldSim.c ==========================================================*/
extern Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////