/**CFile****************************************************************
FileName [llbInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [BDD-based reachability.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - May 8, 2010.]
Revision [$Id: llbInt.h,v 1.00 2010/05/08 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__aig__llb__llbInt_h
#define ABC__aig__llb__llbInt_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include "proof/ssw/ssw.h"
#include "misc/extra/extraBdd.h"
#include "llb.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Llb_Man_t_ Llb_Man_t;
typedef struct Llb_Mtr_t_ Llb_Mtr_t;
typedef struct Llb_Grp_t_ Llb_Grp_t;
struct Llb_Man_t_
{
Gia_ParLlb_t * pPars; // parameters
Aig_Man_t * pAigGlo; // initial AIG manager (owned by the caller)
Aig_Man_t * pAig; // derived AIG manager (created in this package)
DdManager * dd; // BDD manager
DdManager * ddG; // BDD manager
DdManager * ddR; // BDD manager
Vec_Int_t * vObj2Var; // mapping AIG ObjId into BDD var index
Vec_Int_t * vVar2Obj; // mapping BDD var index into AIG ObjId
Vec_Ptr_t * vGroups; // group Id into group pointer
Llb_Mtr_t * pMatrix; // dependency matrix
// image computation
Vec_Ptr_t * vRings; // onion rings
Vec_Int_t * vVarBegs; // the first group where the var appears
Vec_Int_t * vVarEnds; // the last group where the var appears
// variable mapping
Vec_Int_t * vNs2Glo; // next state variables into global variables
Vec_Int_t * vCs2Glo; // next state variables into global variables
Vec_Int_t * vGlo2Cs; // global variables into current state variables
Vec_Int_t * vGlo2Ns; // global variables into current state variables
// flow computation
// Vec_Int_t * vMem;
// Vec_Ptr_t * vTops;
// Vec_Ptr_t * vBots;
// Vec_Ptr_t * vCuts;
};
struct Llb_Mtr_t_
{
int nPis; // number of primary inputs
int nFfs; // number of flip-flops
int nRows; // number of rows
int nCols; // number of columns
int * pColSums; // sum of values in a column
Llb_Grp_t ** pColGrps; // group structure for each col
int * pRowSums; // sum of values in a row
char ** pMatrix; // dependency matrix
Llb_Man_t * pMan; // manager
// partial product
char * pProdVars; // variables in the partial product
int * pProdNums; // var counts in the remaining partitions
};
struct Llb_Grp_t_
{
int Id; // group ID
Vec_Ptr_t * vIns; // input AIG objs
Vec_Ptr_t * vOuts; // output AIG objs
Vec_Ptr_t * vNodes; // internal AIG objs
Llb_Man_t * pMan; // manager
Llb_Grp_t * pPrev; // previous group
Llb_Grp_t * pNext; // next group
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Llb_ObjBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== llbConstr.c ======================================================*/
extern Vec_Int_t * Llb_ManDeriveConstraints( Aig_Man_t * p );
extern void Llb_ManPrintEntries( Aig_Man_t * p, Vec_Int_t * vCands );
/*=== llbCore.c ======================================================*/
extern int Llb_ManModelCheckAig( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars, Vec_Int_t * vHints, DdManager ** pddGlo );
/*=== llbCluster.c ======================================================*/
extern void Llb_ManCluster( Llb_Mtr_t * p );
/*=== llbDump.c ======================================================*/
extern void Llb_ManDumpReached( DdManager * ddG, DdNode * bReached, char * pModel, char * pFileName );
/*=== llbFlow.c ======================================================*/
extern Vec_Ptr_t * Llb_ManFlow( Aig_Man_t * p, Vec_Ptr_t * vSources, int * pnFlow );
/*=== llbHint.c ======================================================*/
extern int Llb_ManReachabilityWithHints( Llb_Man_t * p );
extern int Llb_ManModelCheckAigWithHints( Aig_Man_t * pAigGlo, Gia_ParLlb_t * pPars );
/*=== llbMan.c =======================================================*/
extern void Llb_ManPrepareVarMap( Llb_Man_t * p );
extern Llb_Man_t * Llb_ManStart( Aig_Man_t * pAigGlo, Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
extern void Llb_ManStop( Llb_Man_t * p );
/*=== llbMatrix.c ====================================================*/
extern void Llb_MtrVerifyMatrix( Llb_Mtr_t * p );
extern Llb_Mtr_t * Llb_MtrCreate( Llb_Man_t * p );
extern void Llb_MtrFree( Llb_Mtr_t * p );
extern void Llb_MtrPrint( Llb_Mtr_t * p, int fOrder );
extern void Llb_MtrPrintMatrixStats( Llb_Mtr_t * p );
/*=== llbPart.c ======================================================*/
extern Llb_Grp_t * Llb_ManGroupAlloc( Llb_Man_t * pMan );
extern void Llb_ManGroupStop( Llb_Grp_t * p );
extern void Llb_ManPrepareGroups( Llb_Man_t * pMan );
extern Llb_Grp_t * Llb_ManGroupsCombine( Llb_Grp_t * p1, Llb_Grp_t * p2 );
extern Llb_Grp_t * Llb_ManGroupCreateFromCuts( Llb_Man_t * pMan, Vec_Int_t * vCut1, Vec_Int_t * vCut2 );
extern void Llb_ManPrepareVarLimits( Llb_Man_t * p );
/*=== llbPivot.c =====================================================*/
extern int Llb_ManTracePaths( Aig_Man_t * p, Aig_Obj_t * pPivot );
extern Vec_Int_t * Llb_ManMarkPivotNodes( Aig_Man_t * p, int fUseInternal );
/*=== llbReach.c =====================================================*/
extern int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo );
/*=== llbSched.c =====================================================*/
extern void Llb_MtrSchedule( Llb_Mtr_t * p );
/*=== llb2Bad.c ======================================================*/
extern DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, clock_t TimeOut );
extern DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc );
/*=== llb2Core.c ======================================================*/
extern DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues );
extern int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, clock_t TimeTarget );
/*=== llb2Driver.c ======================================================*/
extern Vec_Int_t * Llb_DriverCountRefs( Aig_Man_t * p );
extern Vec_Int_t * Llb_DriverCollectNs( Aig_Man_t * pAig, Vec_Int_t * vDriRefs );
extern Vec_Int_t * Llb_DriverCollectCs( Aig_Man_t * pAig );
extern DdNode * Llb_DriverPhaseCube( Aig_Man_t * pAig, Vec_Int_t * vDriRefs, DdManager * dd );
extern DdManager * Llb_DriverLastPartition( Aig_Man_t * p, Vec_Int_t * vVarsNs, clock_t TimeTarget );
/*=== llb2Image.c ======================================================*/
extern Vec_Ptr_t * Llb_ImgSupports( Aig_Man_t * p, Vec_Ptr_t * vDdMans, Vec_Int_t * vStart, Vec_Int_t * vStop, int fAddPis, int fVerbose );
extern void Llb_ImgSchedule( Vec_Ptr_t * vSupps, Vec_Ptr_t ** pvQuant0, Vec_Ptr_t ** pvQuant1, int fVerbose );
extern DdManager * Llb_ImgPartition( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, clock_t TimeTarget );
extern void Llb_ImgQuantifyFirst( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, Vec_Ptr_t * vQuant0, int fVerbose );
extern void Llb_ImgQuantifyReset( Vec_Ptr_t * vDdMans );
extern DdNode * Llb_ImgComputeImage( Aig_Man_t * pAig, Vec_Ptr_t * vDdMans, DdManager * dd, DdNode * bInit,
Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1, Vec_Int_t * vDriRefs,
clock_t TimeTarget, int fBackward, int fReorder, int fVerbose );
extern DdManager * Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, int * pOrder, int fFirst, clock_t TimeTarget );
extern DdNode * Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder );
extern void Llb_NonlinImageQuit();
/*=== llb3Image.c =======================================================*/
extern DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q,
DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder );
/*=== llb3Nonlin.c ======================================================*/
extern DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
/*=== llb4Cex.c =======================================================*/
extern Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int iCexPo, int fVerbose );
/*=== llb4Cluster.c =======================================================*/
//extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose );
/*=== llb4Image.c =======================================================*/
extern DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q );
extern Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax );
/*=== llb4Map.c =========================================================*/
//extern Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin );
/*=== llb4Nonlin.c ======================================================*/
//extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
/*=== llb4Sweep.c ======================================================*/
extern void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int fVerbose );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////