summaryrefslogtreecommitdiffstats
path: root/src/proof/abs/abs.h
blob: 1c31e7cc63ca4d7820786a0281f17c57b9fc92a3 (plain)
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
/**CFile****************************************************************

  FileName    [abs.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Abstraction package.]

  Synopsis    [External declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: abs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/
 
#ifndef ABC__proof_abs__Abs_h
#define ABC__proof_abs__Abs_h


////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#include "aig/saig/saig.h"

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_HEADER_START


////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

// abstraction parameters
typedef struct Abs_Par_t_ Abs_Par_t;
struct Abs_Par_t_
{
    int            nFramesMax;         // maximum frames
    int            nFramesStart;       // starting frame 
    int            nFramesPast;        // overlap frames
    int            nConfLimit;         // conflict limit
    int            nLearnedMax;        // max number of learned clauses
    int            nLearnedStart;      // max number of learned clauses
    int            nLearnedDelta;      // delta increase of learned clauses
    int            nLearnedPerce;      // percentage of clauses to leave
    int            nTimeOut;           // timeout in seconds
    int            nRatioMin;          // stop when less than this % of object is unabstracted
    int            nRatioMin2;         // stop when less than this % of object is unabstracted during refinement
    int            nRatioMax;          // restart when the number of abstracted object is more than this
    int            fUseTermVars;       // use terminal variables
    int            fUseRollback;       // use rollback to the starting number of frames
    int            fPropFanout;        // propagate fanout implications
    int            fAddLayer;          // refinement strategy by adding layers
    int            fNewRefine;         // uses new refinement heuristics
    int            fUseSkip;           // skip proving intermediate timeframes
    int            fUseSimple;         // use simple CNF construction
    int            fSkipHash;          // skip hashing CNF while unrolling
    int            fUseFullProof;      // use full proof for UNSAT cores
    int            fDumpVabs;          // dumps the abstracted model
    int            fDumpMabs;          // dumps the original AIG with abstraction map
    int            fCallProver;        // calls the prover
    int            fSimpProver;        // calls simplification before prover
    char *         pFileVabs;          // dumps the abstracted model into this file
    int            fVerbose;           // verbose flag
    int            fVeryVerbose;       // print additional information
    int            iFrame;             // the number of frames covered
    int            iFrameProved;       // the number of frames proved
    int            nFramesNoChange;    // the number of last frames without changes
    int            nFramesNoChangeLim; // the number of last frames without changes to dump abstraction
};

// old abstraction parameters
typedef struct Gia_ParAbs_t_ Gia_ParAbs_t;
struct Gia_ParAbs_t_
{
    int            Algo;               // the algorithm to be used
    int            nFramesMax;         // timeframes for PBA
    int            nConfMax;           // conflicts for PBA
    int            fDynamic;           // dynamic unfolding for PBA
    int            fConstr;            // use constraints
    int            nFramesBmc;         // timeframes for BMC
    int            nConfMaxBmc;        // conflicts for BMC
    int            nStableMax;         // the number of stable frames to quit
    int            nRatio;             // ratio of flops to quit
    int            TimeOut;            // approximate timeout in seconds
    int            TimeOutVT;          // approximate timeout in seconds
    int            nBobPar;            // Bob's parameter
    int            fUseBdds;           // use BDDs to refine abstraction
    int            fUseDprove;         // use 'dprove' to refine abstraction
    int            fUseStart;          // use starting frame
    int            fVerbose;           // verbose output
    int            fVeryVerbose;       // printing additional information
    int            Status;             // the problem status
    int            nFramesDone;        // the number of frames covered
};

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

static inline int         Ga2_ObjOffset( Gia_Man_t * p, Gia_Obj_t * pObj )          { return Vec_IntEntry(p->vMapping, Gia_ObjId(p, pObj));                                                         }
static inline int         Ga2_ObjLeaveNum( Gia_Man_t * p, Gia_Obj_t * pObj )        { return Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj));                                                     }
static inline int *       Ga2_ObjLeavePtr( Gia_Man_t * p, Gia_Obj_t * pObj )        { return Vec_IntEntryP(p->vMapping, Ga2_ObjOffset(p, pObj) + 1);                                                }
static inline unsigned    Ga2_ObjTruth( Gia_Man_t * p, Gia_Obj_t * pObj )           { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 1);            }
static inline int         Ga2_ObjRefNum( Gia_Man_t * p, Gia_Obj_t * pObj )          { return (unsigned)Vec_IntEntry(p->vMapping, Ga2_ObjOffset(p, pObj) + Ga2_ObjLeaveNum(p, pObj) + 2);            }
static inline Vec_Int_t * Ga2_ObjLeaves( Gia_Man_t * p, Gia_Obj_t * pObj )          { static Vec_Int_t v; v.nSize = Ga2_ObjLeaveNum(p, pObj), v.pArray = Ga2_ObjLeavePtr(p, pObj); return &v;       }

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== abs.c =========================================================*/
/*=== absDup.c =========================================================*/
extern Gia_Man_t *       Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses );
extern Gia_Man_t *       Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses );
extern void              Gia_ManGlaCollect( Gia_Man_t * p, Vec_Int_t * vGateClasses, Vec_Int_t ** pvPis, Vec_Int_t ** pvPPis, Vec_Int_t ** pvFlops, Vec_Int_t ** pvNodes );
extern void              Gia_ManPrintFlopClasses( Gia_Man_t * p );
extern void              Gia_ManPrintObjClasses( Gia_Man_t * p );
extern void              Gia_ManPrintGateClasses( Gia_Man_t * p );
/*=== absGla.c =========================================================*/
extern int               Gia_ManPerformGla( Gia_Man_t * p, Abs_Par_t * pPars );
/*=== absGlaOld.c =========================================================*/
extern int               Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, int fStartVta );
/*=== absIter.c =========================================================*/
extern Gia_Man_t *       Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose );
/*=== absPth.c =========================================================*/
extern void              Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose );
extern void              Gia_GlaProveCancel( int fVerbose );
extern int               Gia_GlaProveCheck( int fVerbose );
/*=== absVta.c =========================================================*/
extern int               Gia_VtaPerform( Gia_Man_t * pAig, Abs_Par_t * pPars );
/*=== absUtil.c =========================================================*/
extern void              Abs_ParSetDefaults( Abs_Par_t * p );
extern Vec_Int_t *       Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vVta );
extern Vec_Int_t *       Gia_VtaConvertFromGla( Gia_Man_t * p, Vec_Int_t * vGla, int nFrames );
extern Vec_Int_t *       Gia_FlaConvertToGla( Gia_Man_t * p, Vec_Int_t * vFla );
extern Vec_Int_t *       Gia_GlaConvertToFla( Gia_Man_t * p, Vec_Int_t * vGla );
extern int               Gia_GlaCountFlops( Gia_Man_t * p, Vec_Int_t * vGla );
extern int               Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla );

/*=== absRpm.c =========================================================*/
extern Gia_Man_t *       Abs_RpmPerform( Gia_Man_t * p, int nCutMax, int fVerbose, int fVeryVerbose );
/*=== absRpmOld.c =========================================================*/
extern Gia_Man_t *       Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose );
extern void              Gia_ManAbsSetDefaultParams( Gia_ParAbs_t * p );
extern Vec_Int_t *       Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );

/*=== absOldCex.c ==========================================================*/
extern Vec_Int_t *       Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect );
extern Abc_Cex_t *       Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
/*=== absOldRef.c ==========================================================*/
extern int               Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int nFfToAddMax, int fTryFour, int fSensePath, int fVerbose );
/*=== absOldSat.c ==========================================================*/
extern Vec_Int_t *       Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
/*=== absOldSim.c ==========================================================*/
extern Vec_Int_t *       Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );


ABC_NAMESPACE_HEADER_END

#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////