mirror of https://github.com/YosysHQ/abc.git
136 lines
6.3 KiB
C
136 lines
6.3 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [sscInt.h]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [Choice computation for tech-mapping.]
|
|
|
|
Synopsis [Internal declarations.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - June 29, 2008.]
|
|
|
|
Revision [$Id: sscInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#ifndef ABC__aig__ssc__sscInt_h
|
|
#define ABC__aig__ssc__sscInt_h
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// INCLUDES ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
#include "aig/gia/gia.h"
|
|
#include "sat/bsat/satSolver.h"
|
|
#include "ssc.h"
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// PARAMETERS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
ABC_NAMESPACE_HEADER_START
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// BASIC TYPES ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
// choicing manager
|
|
typedef struct Ssc_Man_t_ Ssc_Man_t;
|
|
struct Ssc_Man_t_
|
|
{
|
|
// user data
|
|
Ssc_Pars_t * pPars; // choicing parameters
|
|
Gia_Man_t * pAig; // subject AIG
|
|
Gia_Man_t * pCare; // care set AIG
|
|
// internal data
|
|
Gia_Man_t * pFraig; // resulting AIG
|
|
sat_solver * pSat; // recyclable SAT solver
|
|
Vec_Int_t * vId2Var; // mapping of each node into its SAT var
|
|
Vec_Int_t * vVar2Id; // mapping of each SAT var into its node
|
|
Vec_Int_t * vPivot; // one SAT pattern
|
|
int nSatVarsPivot; // the number of variables for constraints
|
|
int nSatVars; // the current number of variables
|
|
// temporary storage
|
|
Vec_Int_t * vFront; // supergate fanins
|
|
Vec_Int_t * vFanins; // supergate fanins
|
|
Vec_Int_t * vPattern; // counter-example
|
|
Vec_Int_t * vDisPairs; // disproved pairs
|
|
// SAT calls statistics
|
|
int nSimRounds; // the number of simulation rounds
|
|
int nRecycles; // the number of times SAT solver was recycled
|
|
int nCallsSince; // the number of calls since the last recycle
|
|
int nSatCalls; // the number of SAT calls
|
|
int nSatCallsUnsat; // the number of unsat SAT calls
|
|
int nSatCallsSat; // the number of sat SAT calls
|
|
int nSatCallsUndec; // the number of undec SAT calls
|
|
// runtime stats
|
|
abctime timeSimInit; // simulation and class computation
|
|
abctime timeSimSat; // simulation of the counter-examples
|
|
abctime timeCnfGen; // generation of CNF
|
|
abctime timeSat; // total SAT time
|
|
abctime timeSatSat; // sat
|
|
abctime timeSatUnsat; // unsat
|
|
abctime timeSatUndec; // undecided
|
|
abctime timeOther; // other runtime
|
|
abctime timeTotal; // total runtime
|
|
};
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// MACRO DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
static inline int Ssc_ObjSatVar( Ssc_Man_t * p, int iObj ) { return Vec_IntEntry(p->vId2Var, iObj); }
|
|
static inline void Ssc_ObjSetSatVar( Ssc_Man_t * p, int iObj, int Num ) { Vec_IntWriteEntry(p->vId2Var, iObj, Num); Vec_IntWriteEntry(p->vVar2Id, Num, iObj); }
|
|
static inline void Ssc_ObjCleanSatVar( Ssc_Man_t * p, int Num ) { Vec_IntWriteEntry(p->vId2Var, Vec_IntEntry(p->vVar2Id, Num), Num); Vec_IntWriteEntry(p->vVar2Id, Num, 0); }
|
|
|
|
static inline int Ssc_ObjFraig( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return pObj->Value; }
|
|
static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode ) { pObj->Value = iNode; }
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/*=== sscClass.c =================================================*/
|
|
extern void Ssc_GiaClassesInit( Gia_Man_t * p );
|
|
extern int Ssc_GiaClassesRefine( Gia_Man_t * p );
|
|
extern void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs );
|
|
extern int Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i );
|
|
/*=== sscCnf.c ===================================================*/
|
|
extern void Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj );
|
|
/*=== sscCore.c ==================================================*/
|
|
/*=== sscSat.c ===================================================*/
|
|
extern void Ssc_ManSatSolverRecycle( Ssc_Man_t * p );
|
|
extern void Ssc_ManStartSolver( Ssc_Man_t * p );
|
|
extern Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p );
|
|
extern int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iObj, int fCompl );
|
|
/*=== sscSim.c ===================================================*/
|
|
extern void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords );
|
|
extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot );
|
|
extern int Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot );
|
|
extern void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat );
|
|
extern void Ssc_GiaSimRound( Gia_Man_t * p );
|
|
extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p );
|
|
extern int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords );
|
|
/*=== sscUtil.c ===================================================*/
|
|
extern Gia_Man_t * Ssc_GenerateOneHot( int nVars );
|
|
|
|
|
|
ABC_NAMESPACE_HEADER_END
|
|
|
|
|
|
|
|
#endif
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|