/**CFile****************************************************************
FileName [cecInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Combinational equivalence checking.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__aig__cec__cecInt_h
#define ABC__aig__cec__cecInt_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "sat/bsat/satSolver.h"
#include "misc/bar/bar.h"
#include "aig/gia/gia.h"
#include "cec.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// simulation pattern manager
typedef struct Cec_ManPat_t_ Cec_ManPat_t;
struct Cec_ManPat_t_
{
Vec_Int_t * vPattern1; // pattern in terms of primary inputs
Vec_Int_t * vPattern2; // pattern in terms of primary inputs
Vec_Str_t * vStorage; // storage for compressed patterns
int iStart; // position in the array where recent patterns begin
int nPats; // total number of recent patterns
int nPatsAll; // total number of all patterns
int nPatLits; // total number of literals in recent patterns
int nPatLitsAll; // total number of literals in all patterns
int nPatLitsMin; // total number of literals in minimized recent patterns
int nPatLitsMinAll; // total number of literals in minimized all patterns
int nSeries; // simulation series
int fVerbose; // verbose stats
// runtime statistics
abctime timeFind; // detecting the pattern
abctime timeShrink; // minimizing the pattern
abctime timeVerify; // verifying the result of minimisation
abctime timeSort; // sorting literals
abctime timePack; // packing into sim info structures
abctime timeTotal; // total runtime
abctime timeTotalSave; // total runtime for saving
};
// SAT solving manager
typedef struct Cec_ManSat_t_ Cec_ManSat_t;
struct Cec_ManSat_t_
{
// parameters
Cec_ParSat_t * pPars;
// AIGs used in the package
Gia_Man_t * pAig; // the AIG whose outputs are considered
Vec_Int_t * vStatus; // status for each output
// SAT solving
sat_solver * pSat; // recyclable SAT solver
int nSatVars; // the counter of SAT variables
int * pSatVars; // mapping of each node into its SAT var
Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned
int nRecycles; // the number of times SAT solver was recycled
int nCallsSince; // the number of calls since the last recycle
Vec_Ptr_t * vFanins; // fanins of the CNF node
// counter-examples
Vec_Int_t * vCex; // the latest counter-example
Vec_Int_t * vVisits; // temporary array for visited nodes
// SAT calls statistics
int nSatUnsat; // the number of proofs
int nSatSat; // the number of failure
int nSatUndec; // the number of timeouts
int nSatTotal; // the number of calls
int nCexLits;
// conflicts
int nConfUnsat; // conflicts in unsat problems
int nConfSat; // conflicts in sat problems
int nConfUndec; // conflicts in undec problems
// runtime stats
int timeSatUnsat; // unsat
int timeSatSat; // sat
int timeSatUndec; // undecided
int timeTotal; // total runtime
};
// combinational simulation manager
typedef struct Cec_ManSim_t_ Cec_ManSim_t;
struct Cec_ManSim_t_
{
// parameters
Gia_Man_t * pAig; // the AIG to be used for simulation
Cec_ParSim_t * pPars; // simulation parameters
int nWords; // the number of simulation words
// recycable memory
int * pSimInfo; // simulation information offsets
unsigned * pMems; // allocated simulaton memory
int nWordsAlloc; // the number of allocated entries
int nMems; // the number of used entries
int nMemsMax; // the max number of used entries
int MemFree; // next free entry
int nWordsOld; // the number of simulation words after previous relink
// internal simulation info
Vec_Ptr_t * vCiSimInfo; // CI simulation info
Vec_Ptr_t * vCoSimInfo; // CO simulation info
// counter examples
void ** pCexes; // counter-examples for each output
int iOut; // first failed output
int nOuts; // the number of failed outputs
Abc_Cex_t * pCexComb; // counter-example for the first failed output
Abc_Cex_t * pBestState; // the state that led to most of the refinements
// scoring simulation patterns
int * pScores; // counters of refinement for each pattern
// temporaries
Vec_Int_t * vClassOld; // old class numbers
Vec_Int_t * vClassNew; // new class numbers
Vec_Int_t * vClassTemp; // temporary storage
Vec_Int_t * vRefinedC; // refined const reprs
};
// combinational simulation manager
typedef struct Cec_ManFra_t_ Cec_ManFra_t;
struct Cec_ManFra_t_
{
// parameters
Gia_Man_t * pAig; // the AIG to be used for simulation
Cec_ParFra_t * pPars; // SAT sweeping parameters
// simulation patterns
Vec_Int_t * vXorNodes; // nodes used in speculative reduction
int nAllProved; // total number of proved nodes
int nAllDisproved; // total number of disproved nodes
int nAllFailed; // total number of failed nodes
// runtime stats
abctime timeSim; // unsat
abctime timePat; // unsat
abctime timeSat; // sat
abctime timeTotal; // total runtime
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cecCorr.c ============================================================*/
extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time );
/*=== cecClass.c ============================================================*/
extern int Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
extern int Cec_ManSimClassesPrepare( Cec_ManSim_t * p, int LevelMax );
extern int Cec_ManSimClassesRefine( Cec_ManSim_t * p );
extern int Cec_ManSimSimulateRound( Cec_ManSim_t * p, Vec_Ptr_t * vInfoCis, Vec_Ptr_t * vInfoCos );
/*=== cecIso.c ============================================================*/
extern int * Cec_ManDetectIsomorphism( Gia_Man_t * p );
/*=== cecMan.c ============================================================*/
extern Cec_ManSat_t * Cec_ManSatCreate( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern void Cec_ManSatPrintStats( Cec_ManSat_t * p );
extern void Cec_ManSatStop( Cec_ManSat_t * p );
extern Cec_ManPat_t * Cec_ManPatStart();
extern void Cec_ManPatPrintStats( Cec_ManPat_t * p );
extern void Cec_ManPatStop( Cec_ManPat_t * p );
extern Cec_ManSim_t * Cec_ManSimStart( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
extern void Cec_ManSimStop( Cec_ManSim_t * p );
extern Cec_ManFra_t * Cec_ManFraStart( Gia_Man_t * pAig, Cec_ParFra_t * pPars );
extern void Cec_ManFraStop( Cec_ManFra_t * p );
/*=== cecPat.c ============================================================*/
extern void Cec_ManPatSavePattern( Cec_ManPat_t * pPat, Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat );
extern Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nWords );
extern Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
/*=== cecSeq.c ============================================================*/
extern int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo );
extern int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter );
extern void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Abc_Cex_t * pCex );
extern int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
/*=== cecSolve.c ============================================================*/
extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs );
extern void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj );
extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p );
/*=== ceFraeep.c ============================================================*/
extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p );
extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
