1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
|
/**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 ///
////////////////////////////////////////////////////////////////////////
|
