mirror of https://github.com/YosysHQ/abc.git
165 lines
5.9 KiB
C
165 lines
5.9 KiB
C
/**CFile****************************************************************
|
|
|
|
FileName [int2Int.h]
|
|
|
|
SystemName [ABC: Logic synthesis and verification system.]
|
|
|
|
PackageName [Interpolation engine.]
|
|
|
|
Synopsis [Internal declarations.]
|
|
|
|
Author [Alan Mishchenko]
|
|
|
|
Affiliation [UC Berkeley]
|
|
|
|
Date [Ver. 1.0. Started - Dec 1, 2013.]
|
|
|
|
Revision [$Id: int2Int.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
|
|
|
|
***********************************************************************/
|
|
|
|
#ifndef ABC__Gia__int2__intInt_h
|
|
#define ABC__Gia__int2__intInt_h
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// INCLUDES ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
#include "aig/gia/gia.h"
|
|
#include "sat/bsat/satSolver.h"
|
|
#include "sat/cnf/cnf.h"
|
|
#include "int2.h"
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// PARAMETERS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
ABC_NAMESPACE_HEADER_START
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// BASIC TYPES ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
// interpolation manager
|
|
typedef struct Int2_Man_t_ Int2_Man_t;
|
|
struct Int2_Man_t_
|
|
{
|
|
// parameters
|
|
Int2_ManPars_t * pPars; // parameters
|
|
// GIA managers
|
|
Gia_Man_t * pGia; // original manager
|
|
Gia_Man_t * pGiaPref; // prefix manager
|
|
Gia_Man_t * pGiaSuff; // suffix manager
|
|
// subset of the manager
|
|
Vec_Int_t * vSuffCis; // suffix CIs
|
|
Vec_Int_t * vSuffCos; // suffix COs
|
|
Vec_Int_t * vPrefCos; // suffix POs
|
|
Vec_Int_t * vStack; // temporary stack
|
|
// preimages
|
|
Vec_Int_t * vImageOne; // latest preimage
|
|
Vec_Int_t * vImagesAll; // cumulative preimage
|
|
// variable maps
|
|
Vec_Ptr_t * vMapFrames; // mapping of GIA IDs into frame IDs
|
|
Vec_Int_t * vMapPref; // mapping of flop inputs into SAT variables
|
|
Vec_Int_t * vMapSuff; // mapping of flop outputs into SAT variables
|
|
// initial minimization
|
|
Vec_Int_t * vAssign; // assignment of PIs in pGiaSuff
|
|
Vec_Int_t * vPrio; // priority of PIs in pGiaSuff
|
|
// SAT solving
|
|
sat_solver * pSatPref; // prefix solver
|
|
sat_solver * pSatSuff; // suffix solver
|
|
// runtime
|
|
abctime timeSatPref;
|
|
abctime timeSatSuff;
|
|
abctime timeOther;
|
|
abctime timeTotal;
|
|
};
|
|
|
|
static inline Int2_Man_t * Int2_ManCreate( Gia_Man_t * pGia, Int2_ManPars_t * pPars )
|
|
{
|
|
Int2_Man_t * p;
|
|
p = ABC_CALLOC( Int2_Man_t, 1 );
|
|
p->pPars = pPars;
|
|
p->pGia = pGia;
|
|
p->pGiaPref = Gia_ManStart( 10000 );
|
|
// perform structural hashing
|
|
Gia_ManHashAlloc( pFrames );
|
|
// subset of the manager
|
|
p->vSuffCis = Vec_IntAlloc( Gia_ManCiNum(pGia) );
|
|
p->vSuffCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
|
|
p->vPrefCos = Vec_IntAlloc( Gia_ManCoNum(pGia) );
|
|
p->vStack = Vec_IntAlloc( 10000 );
|
|
// preimages
|
|
p->vImageOne = Vec_IntAlloc( 1000 );
|
|
p->vImagesAll = Vec_IntAlloc( 1000 );
|
|
// variable maps
|
|
p->vMapFrames = Vec_PtrAlloc( 100 );
|
|
p->vMapPref = Vec_IntAlloc( Gia_ManRegNum(pGia) );
|
|
p->vMapSuff = Vec_IntAlloc( Gia_ManRegNum(pGia) );
|
|
// initial minimization
|
|
p->vAssign = Vec_IntAlloc( Gia_ManCiNum(pGia) );
|
|
p->vPrio = Vec_IntAlloc( Gia_ManCiNum(pGia) );
|
|
return p;
|
|
}
|
|
static inline void Int2_ManStop( Int2_Man_t * p )
|
|
{
|
|
// GIA managers
|
|
Gia_ManStopP( &p->pGiaPref );
|
|
Gia_ManStopP( &p->pGiaSuff );
|
|
// subset of the manager
|
|
Vec_IntFreeP( &p->vSuffCis );
|
|
Vec_IntFreeP( &p->vSuffCos );
|
|
Vec_IntFreeP( &p->vPrefCos );
|
|
Vec_IntFreeP( &p->vStack );
|
|
// preimages
|
|
Vec_IntFreeP( &p->vImageOne );
|
|
Vec_IntFreeP( &p->vImagesAll );
|
|
// variable maps
|
|
Vec_VecFree( (Vec_Vec_t *)p->vMapFrames );
|
|
Vec_IntFreeP( &p->vMapPref );
|
|
Vec_IntFreeP( &p->vMapSuff );
|
|
// initial minimization
|
|
Vec_IntFreeP( &p->vAssign );
|
|
Vec_IntFreeP( &p->vPrio );
|
|
// SAT solving
|
|
if ( p->pSatPref )
|
|
sat_solver_delete( p->pSatPref );
|
|
if ( p->timeSatSuff )
|
|
sat_solver_delete( p->pSatSuff );
|
|
ABC_FREE( p );
|
|
}
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// MACRO DEFINITIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// FUNCTION DECLARATIONS ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|
|
/*=== int2Bmc.c =============================================================*/
|
|
extern int Int2_ManCheckInit( Gia_Man_t * p );
|
|
extern Gia_Man_t * Int2_ManDupInit( Gia_Man_t * p, int fVerbose );
|
|
extern sat_solver * Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames );
|
|
extern void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos );
|
|
extern int Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube );
|
|
|
|
/*=== int2Refine.c =============================================================*/
|
|
extern Vec_Int_t * Int2_ManRefineCube( Gia_Man_t * p, Vec_Int_t * vAssign, Vec_Int_t * vPrio );
|
|
|
|
/*=== int2Util.c ============================================================*/
|
|
extern Gia_Man_t * Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop );
|
|
|
|
|
|
ABC_NAMESPACE_HEADER_END
|
|
|
|
|
|
|
|
#endif
|
|
|
|
////////////////////////////////////////////////////////////////////////
|
|
/// END OF FILE ///
|
|
////////////////////////////////////////////////////////////////////////
|
|
|