ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
int.h File Reference
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Inter_ManParams_t_
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Inter_ManParams_t_ Inter_ManParams_t
 INCLUDES ///.
 

Functions

void Inter_ManSetDefaultParams (Inter_ManParams_t *p)
 MACRO DEFINITIONS ///.
 
int Inter_ManPerformInterpolation (Aig_Man_t *pAig, Inter_ManParams_t *pPars, int *piFrame)
 

Typedef Documentation

◆ Inter_ManParams_t

typedef typedefABC_NAMESPACE_HEADER_START struct Inter_ManParams_t_ Inter_ManParams_t

INCLUDES ///.

CFile****************************************************************

FileName [int.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id
int.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 48 of file int.h.

Function Documentation

◆ Inter_ManPerformInterpolation()

int Inter_ManPerformInterpolation ( Aig_Man_t * pAig,
Inter_ManParams_t * pPars,
int * piFrame )
extern

Function*************************************************************

Synopsis [Interplates while the number of conflicts is not exceeded.]

Description [Returns 1 if proven. 0 if failed. -1 if undecided.]

SideEffects [Does not check the property in 0-th frame.]

SeeAlso []

Definition at line 79 of file intCore.c.

80{
81 extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
82 Inter_Man_t * p;
83 Inter_Check_t * pCheck = NULL;
84 Aig_Man_t * pAigTemp;
85 int s, i, RetValue, Status;
86 abctime clk, clk2, clkTotal = Abc_Clock(), timeTemp = 0;
87 abctime nTimeNewOut = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
88
89 // enable ORing of the interpolants, if containment check is performed inductively with K > 1
90 if ( pPars->nFramesK > 1 )
91 pPars->fTransLoop = 1;
92
93 // sanity checks
94 assert( Saig_ManRegNum(pAig) > 0 );
95 assert( Saig_ManPiNum(pAig) > 0 );
96 assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
97 if ( pPars->fVerbose && Saig_ManConstrNum(pAig) )
98 printf( "Performing interpolation with %d constraints...\n", Saig_ManConstrNum(pAig) );
99
100 if ( Inter_ManCheckInitialState(pAig) )
101 {
102 *piFrame = -1;
103 printf( "Property trivially fails in the initial state.\n" );
104 return 0;
105 }
106/*
107 if ( Inter_ManCheckAllStates(pAig) )
108 {
109 printf( "Property trivially holds in all states.\n" );
110 return 1;
111 }
112*/
113 // create interpolation manager
114 // can perform SAT sweeping and/or rewriting of this AIG...
115 p = Inter_ManCreate( pAig, pPars );
116 if ( pPars->fTransLoop )
117 p->pAigTrans = Inter_ManStartOneOutput( pAig, 0 );
118 else
119 p->pAigTrans = Inter_ManStartDuplicated( pAig );
120 // derive CNF for the transformed AIG
121clk = Abc_Clock();
122 p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) );
123p->timeCnf += Abc_Clock() - clk;
124 if ( pPars->fVerbose )
125 {
126 printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d. CNF: Var/Cla = %d/%d.\n",
127 Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
128 Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
129 p->pCnfAig->nVars, p->pCnfAig->nClauses );
130 }
131
132 // derive interpolant
133 *piFrame = -1;
134 p->nFrames = 1;
135 for ( s = 0; ; s++ )
136 {
137 Cnf_Dat_t * pCnfInter2;
138
139clk2 = Abc_Clock();
140 // initial state
141 if ( pPars->fUseBackward )
142 p->pInter = Inter_ManStartOneOutput( pAig, 1 );
143 else
144 p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
145 assert( Aig_ManCoNum(p->pInter) == 1 );
146clk = Abc_Clock();
147 p->pCnfInter = Cnf_Derive( p->pInter, 0 );
148p->timeCnf += Abc_Clock() - clk;
149 // timeframes
150 p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward, pPars->fUseTwoFrames );
151clk = Abc_Clock();
152 if ( pPars->fRewrite )
153 {
154 p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 );
155 Aig_ManStop( pAigTemp );
156// p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 );
157// Aig_ManStop( pAigTemp );
158 }
159p->timeRwr += Abc_Clock() - clk;
160 // can also do SAT sweeping on the timeframes...
161clk = Abc_Clock();
162 if ( pPars->fUseBackward )
163 p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );
164 else
165// p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );
166 p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 );
167p->timeCnf += Abc_Clock() - clk;
168 // report statistics
169 if ( pPars->fVerbose )
170 {
171 printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d. ",
172 s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
173 ABC_PRT( "Time", Abc_Clock() - clk2 );
174 }
175
176
178 // start containment checking
179 if ( !(pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1) )
180 {
181 pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK );
182 // try new containment check for the initial state
183clk = Abc_Clock();
184 pCnfInter2 = Cnf_Derive( p->pInter, 1 );
185p->timeCnf += Abc_Clock() - clk;
186clk = Abc_Clock();
187 RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
188p->timeEqu += Abc_Clock() - clk;
189// assert( RetValue == 0 );
190 Cnf_DataFree( pCnfInter2 );
191 if ( p->vInters )
192 Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) );
193 }
195
196 // iterate the interpolation procedure
197 for ( i = 0; ; i++ )
198 {
199 if ( pPars->nFramesMax && p->nFrames + i >= pPars->nFramesMax )
200 {
201 if ( pPars->fVerbose )
202 printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
203 p->timeTotal = Abc_Clock() - clkTotal;
204 Inter_ManStop( p, 0 );
205 Inter_CheckStop( pCheck );
206 return -1;
207 }
208
209 // perform interpolation
210 clk = Abc_Clock();
211#ifdef ABC_USE_LIBRARIES
212 if ( pPars->fUseMiniSat )
213 {
214 assert( !pPars->fUseBackward );
215 RetValue = Inter_ManPerformOneStepM114p( p, pPars->fUsePudlak, pPars->fUseOther );
216 }
217 else
218#endif
219 RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward, nTimeNewOut );
220
221 if ( pPars->fVerbose )
222 {
223 printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ",
224 i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
225 ABC_PRT( "Time", Abc_Clock() - clk );
226 }
227 // remember the number of timeframes completed
228 pPars->iFrameMax = i - 1 + p->nFrames;
229 if ( RetValue == 0 ) // found a (spurious?) counter-example
230 {
231 if ( i == 0 ) // real counterexample
232 {
233 if ( pPars->fVerbose )
234 printf( "Found a real counterexample in frame %d.\n", p->nFrames );
235 p->timeTotal = Abc_Clock() - clkTotal;
236 *piFrame = p->nFrames;
237// pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
238 {
239 int RetValue;
240 Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
241 Saig_ParBmcSetDefaultParams( pParsBmc );
242 pParsBmc->nConfLimit = 100000000;
243 pParsBmc->nStart = p->nFrames;
244 pParsBmc->fVerbose = pPars->fVerbose;
245 RetValue = Saig_ManBmcScalable( pAig, pParsBmc );
246 if ( RetValue == 1 )
247 printf( "Error: The problem should be SAT but it is UNSAT.\n" );
248 else if ( RetValue == -1 )
249 printf( "Error: The problem timed out.\n" );
250 }
251 Inter_ManStop( p, 0 );
252 Inter_CheckStop( pCheck );
253 return 0;
254 }
255 // likely spurious counter-example
256 p->nFrames += i;
257 Inter_ManClean( p );
258 break;
259 }
260 else if ( RetValue == -1 )
261 {
262 if ( pPars->nSecLimit && Abc_Clock() > nTimeNewOut ) // timed out
263 {
264 if ( pPars->fVerbose )
265 printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
266 }
267 else
268 {
269 assert( p->nConfCur >= p->nConfLimit );
270 if ( pPars->fVerbose )
271 printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
272 }
273 p->timeTotal = Abc_Clock() - clkTotal;
274 Inter_ManStop( p, 0 );
275 Inter_CheckStop( pCheck );
276 return -1;
277 }
278 assert( RetValue == 1 ); // found new interpolant
279 // compress the interpolant
280clk = Abc_Clock();
281 if ( p->pInterNew )
282 {
283 // save the timeout value
284 p->pInterNew->Time2Quit = nTimeNewOut;
285// Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 );
286 p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
287// p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 0 );
288 Aig_ManStop( pAigTemp );
289 if ( p->pInterNew == NULL )
290 {
291 printf( "Reached timeout (%d seconds) during rewriting.\n", pPars->nSecLimit );
292 p->timeTotal = Abc_Clock() - clkTotal;
293 Inter_ManStop( p, 1 );
294 Inter_CheckStop( pCheck );
295 return -1;
296 }
297 }
298p->timeRwr += Abc_Clock() - clk;
299
300 // check if interpolant is trivial
301 if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManCo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
302 {
303// printf( "interpolant is constant 0\n" );
304 if ( pPars->fVerbose )
305 printf( "The problem is trivially true for all states.\n" );
306 p->timeTotal = Abc_Clock() - clkTotal;
307 Inter_ManStop( p, 1 );
308 Inter_CheckStop( pCheck );
309 return 1;
310 }
311
312 // check containment of interpolants
313clk = Abc_Clock();
314 if ( pPars->fCheckKstep ) // k-step unique-state induction
315 {
316 if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
317 {
318 if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 )
319 {
320clk2 = Abc_Clock();
321 Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, Abc_MinInt(i + 1, pPars->nFramesK), pPars->fUseBackward );
322timeTemp = Abc_Clock() - clk2;
323 }
324 else
325 { // new containment check
326clk2 = Abc_Clock();
327 pCnfInter2 = Cnf_Derive( p->pInterNew, 1 );
328p->timeCnf += Abc_Clock() - clk2;
329timeTemp = Abc_Clock() - clk2;
330
331 Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
332 Cnf_DataFree( pCnfInter2 );
333 if ( p->vInters )
334 Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) );
335 }
336 }
337 else
338 Status = 0;
339 }
340 else // combinational containment
341 {
342 if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
343 Status = Inter_ManCheckContainment( p->pInterNew, p->pInter );
344 else
345 Status = 0;
346 }
347p->timeEqu += Abc_Clock() - clk - timeTemp;
348 if ( Status ) // contained
349 {
350 if ( pPars->fVerbose )
351 printf( "Proved containment of interpolants.\n" );
352 p->timeTotal = Abc_Clock() - clkTotal;
353 Inter_ManStop( p, 1 );
354 Inter_CheckStop( pCheck );
355 return 1;
356 }
357 if ( pPars->nSecLimit && Abc_Clock() > nTimeNewOut )
358 {
359 printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
360 p->timeTotal = Abc_Clock() - clkTotal;
361 Inter_ManStop( p, 1 );
362 Inter_CheckStop( pCheck );
363 return -1;
364 }
365 // save interpolant and convert it into CNF
366 if ( pPars->fTransLoop )
367 {
368 Aig_ManStop( p->pInter );
369 p->pInter = p->pInterNew;
370 }
371 else
372 {
373 if ( pPars->fUseBackward )
374 {
375 p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
376 Aig_ManStop( pAigTemp );
377 Aig_ManStop( p->pInterNew );
378 // compress the interpolant
379clk = Abc_Clock();
380 p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
381 Aig_ManStop( pAigTemp );
382p->timeRwr += Abc_Clock() - clk;
383 }
384 else // forward with the new containment checking (using only the frontier)
385 {
386 Aig_ManStop( p->pInter );
387 p->pInter = p->pInterNew;
388 }
389 }
390 p->pInterNew = NULL;
391 Cnf_DataFree( p->pCnfInter );
392clk = Abc_Clock();
393 p->pCnfInter = Cnf_Derive( p->pInter, 0 );
394p->timeCnf += Abc_Clock() - clk;
395 }
396
397 // start containment checking
398 Inter_CheckStop( pCheck );
399 }
400 assert( 0 );
401 return RetValue;
402}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
Dar_ManRwsat
ABC_NAMESPACE_IMPL_START Aig_Man_t * Dar_ManRwsat(Aig_Man_t *pAig, int fBalance, int fVerbose)
DECLARATIONS ///.
Definition darScript.c:71
Aig_ManDupSimple
Aig_Man_t * Aig_ManDupSimple(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigDup.c:46
Aig_ManLevelNum
int Aig_ManLevelNum(Aig_Man_t *p)
Definition aigDfs.c:500
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManCreateMiter
Aig_Man_t * Aig_ManCreateMiter(Aig_Man_t *p1, Aig_Man_t *p2, int fImpl)
Definition aigDup.c:1049
Saig_ParBmcSetDefaultParams
void Saig_ParBmcSetDefaultParams(Saig_ParBmc_t *p)
Definition bmcBmc3.c:1334
Saig_ManBmcScalable
int Saig_ManBmcScalable(Aig_Man_t *pAig, Saig_ParBmc_t *pPars)
Definition bmcBmc3.c:1461
Saig_ParBmc_t
struct Saig_ParBmc_t_ Saig_ParBmc_t
Definition bmc.h:105
Cnf_DeriveSimple
Cnf_Dat_t * Cnf_DeriveSimple(Aig_Man_t *p, int nOutputs)
Definition cnfWrite.c:587
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition cnfCore.c:165
Cnf_Dat_t
struct Cnf_Dat_t_ Cnf_Dat_t
Definition cnf.h:52
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition cnfMan.c:207
p
Cube * p
Definition exorList.c:222
Inter_CheckStop
void Inter_CheckStop(Inter_Check_t *p)
Definition intCheck.c:137
Inter_CheckPerform
int Inter_CheckPerform(Inter_Check_t *p, Cnf_Dat_t *pCnfInt, abctime nTimeNewOut)
Definition intCheck.c:220
Inter_CheckStart
Inter_Check_t * Inter_CheckStart(Aig_Man_t *pTrans, int nFramesK)
MACRO DEFINITIONS ///.
Definition intCheck.c:105
Inter_ManCheckInductiveContainment
int Inter_ManCheckInductiveContainment(Aig_Man_t *pTrans, Aig_Man_t *pInter, int nSteps, int fBackward)
Definition intContain.c:190
Inter_ManCheckContainment
int Inter_ManCheckContainment(Aig_Man_t *pNew, Aig_Man_t *pOld)
FUNCTION DEFINITIONS ///.
Definition intContain.c:47
Inter_ManStartDuplicated
Aig_Man_t * Inter_ManStartDuplicated(Aig_Man_t *p)
Definition intDup.c:73
Inter_ManStartOneOutput
Aig_Man_t * Inter_ManStartOneOutput(Aig_Man_t *p, int fAddFirstPo)
Definition intDup.c:122
Inter_ManStartInitState
ABC_NAMESPACE_IMPL_START Aig_Man_t * Inter_ManStartInitState(int nRegs)
DECLARATIONS ///.
Definition intDup.c:45
Inter_ManFramesInter
ABC_NAMESPACE_IMPL_START Aig_Man_t * Inter_ManFramesInter(Aig_Man_t *pAig, int nFrames, int fAddRegOuts, int fUseTwoFrames)
DECLARATIONS ///.
Definition intFrames.c:47
Inter_ManCheckInitialState
int Inter_ManCheckInitialState(Aig_Man_t *p)
DECLARATIONS ///.
Definition intUtil.c:46
Inter_Man_t
typedefABC_NAMESPACE_HEADER_START struct Inter_Man_t_ Inter_Man_t
INCLUDES ///.
Definition intInt.h:49
Inter_ManPerformOneStep
int Inter_ManPerformOneStep(Inter_Man_t *p, int fUseBias, int fUseBackward, abctime nTimeNewOut)
Definition intM114.c:203
Inter_ManStop
void Inter_ManStop(Inter_Man_t *p, int fProved)
Definition intMan.c:128
Inter_ManClean
void Inter_ManClean(Inter_Man_t *p)
Definition intMan.c:73
Inter_ManCreate
Inter_Man_t * Inter_ManCreate(Aig_Man_t *pAig, Inter_ManParams_t *pPars)
DECLARATIONS ///.
Definition intMan.c:46
Inter_Check_t
struct Inter_Check_t_ Inter_Check_t
Definition intInt.h:84
Saig_ParBmc_t_::fVerbose
int fVerbose
Definition bmc.h:129
Saig_ParBmc_t_::nConfLimit
int nConfLimit
Definition bmc.h:110
Saig_ParBmc_t_::nStart
int nStart
Definition bmc.h:108
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Inter_ManSetDefaultParams()

void Inter_ManSetDefaultParams ( Inter_ManParams_t * p)
extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

CFile****************************************************************

FileName [intCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Core procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id
intCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] ` DECLARATIONS /// Function*************************************************************

Synopsis [This procedure sets default values of interpolation parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file intCore.c.

47{
48 memset( p, 0, sizeof(Inter_ManParams_t) );
49 p->nBTLimit = 0; // limit on the number of conflicts
50 p->nFramesMax = 0; // the max number timeframes to unroll
51 p->nSecLimit = 0; // time limit in seconds
52 p->nFramesK = 1; // the number of timeframes to use in induction
53 p->fRewrite = 0; // use additional rewriting to simplify timeframes
54 p->fTransLoop = 0; // add transition into the init state under new PI var
55 p->fUsePudlak = 0; // use Pudluk interpolation procedure
56 p->fUseOther = 0; // use other undisclosed option
57 p->fUseMiniSat = 0; // use MiniSat-1.14p instead of internal proof engine
58 p->fCheckKstep = 1; // check using K-step induction
59 p->fUseBias = 0; // bias decisions to global variables
60 p->fUseBackward = 0; // perform backward interpolation
61 p->fUseSeparate = 0; // solve each output separately
62 p->fUseTwoFrames = 0; // create OR of two last timeframes
63 p->fDropSatOuts = 0; // replace by 1 the solved outputs
64 p->fVerbose = 0; // print verbose statistics
65 p->iFrameMax =-1;
66}
Inter_ManParams_t
typedefABC_NAMESPACE_HEADER_START struct Inter_ManParams_t_ Inter_ManParams_t
INCLUDES ///.
Definition int.h:48
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function: