1 /**CFile****************************************************************
2
3 FileName [saigConstr2.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Sequential AIG package.]
8
9 Synopsis [Functional constraint detection.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: saigConstr2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "saig.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver.h"
24 #include "bool/kit/kit.h"
25 #include "misc/bar/bar.h"
26
27 ABC_NAMESPACE_IMPL_START
28
29
30
31 ////////////////////////////////////////////////////////////////////////
32 /// DECLARATIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
Aig_ObjFrames(Aig_Obj_t ** pObjMap,int nFs,Aig_Obj_t * pObj,int i)35 static inline Aig_Obj_t * Aig_ObjFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return pObjMap[nFs*pObj->Id + i]; }
Aig_ObjSetFrames(Aig_Obj_t ** pObjMap,int nFs,Aig_Obj_t * pObj,int i,Aig_Obj_t * pNode)36 static inline void Aig_ObjSetFrames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { pObjMap[nFs*pObj->Id + i] = pNode; }
37
Aig_ObjChild0Frames(Aig_Obj_t ** pObjMap,int nFs,Aig_Obj_t * pObj,int i)38 static inline Aig_Obj_t * Aig_ObjChild0Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; }
Aig_ObjChild1Frames(Aig_Obj_t ** pObjMap,int nFs,Aig_Obj_t * pObj,int i)39 static inline Aig_Obj_t * Aig_ObjChild1Frames( Aig_Obj_t ** pObjMap, int nFs, Aig_Obj_t * pObj, int i ) { return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_ObjFrames(pObjMap,nFs,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; }
40
41 ////////////////////////////////////////////////////////////////////////
42 /// FUNCTION DEFINITIONS ///
43 ////////////////////////////////////////////////////////////////////////
44
45 /**Function*************************************************************
46
47 Synopsis [Returns the probability of POs being 1 under rand seq sim.]
48
49 Description []
50
51 SideEffects []
52
53 SeeAlso []
54
55 ***********************************************************************/
Ssw_ManProfileConstraints(Aig_Man_t * p,int nWords,int nFrames,int fVerbose)56 int Ssw_ManProfileConstraints( Aig_Man_t * p, int nWords, int nFrames, int fVerbose )
57 {
58 Vec_Ptr_t * vInfo;
59 Vec_Int_t * vProbs, * vProbs2;
60 Aig_Obj_t * pObj, * pObjLi;
61 unsigned * pInfo, * pInfo0, * pInfo1, * pInfoMask, * pInfoMask2;
62 int i, w, f, RetValue = 1;
63 abctime clk = Abc_Clock();
64 if ( fVerbose )
65 printf( "Simulating %d nodes and %d flops for %d frames with %d words... ",
66 Aig_ManNodeNum(p), Aig_ManRegNum(p), nFrames, nWords );
67 Aig_ManRandom( 1 );
68 vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p)+2, nWords );
69 Vec_PtrCleanSimInfo( vInfo, 0, nWords );
70 vProbs = Vec_IntStart( Saig_ManPoNum(p) );
71 vProbs2 = Vec_IntStart( Saig_ManPoNum(p) );
72 // start the constant
73 pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(Aig_ManConst1(p)) );
74 for ( w = 0; w < nWords; w++ )
75 pInfo[w] = ~0;
76 // start the flop inputs
77 Saig_ManForEachLi( p, pObj, i )
78 {
79 pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
80 for ( w = 0; w < nWords; w++ )
81 pInfo[w] = 0;
82 }
83 // get the info mask
84 pInfoMask = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p) ); // PO failed
85 pInfoMask2 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ManObjNumMax(p)+1 ); // constr failed
86 for ( f = 0; f < nFrames; f++ )
87 {
88 // assign primary inputs
89 Saig_ManForEachPi( p, pObj, i )
90 {
91 pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
92 for ( w = 0; w < nWords; w++ )
93 pInfo[w] = Aig_ManRandom( 0 );
94 }
95 // move the flop values
96 Saig_ManForEachLiLo( p, pObjLi, pObj, i )
97 {
98 pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
99 pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObjLi) );
100 for ( w = 0; w < nWords; w++ )
101 pInfo[w] = pInfo0[w];
102 }
103 // simulate the nodes
104 Aig_ManForEachNode( p, pObj, i )
105 {
106 pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
107 pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) );
108 pInfo1 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId1(pObj) );
109 if ( Aig_ObjFaninC0(pObj) )
110 {
111 if ( Aig_ObjFaninC1(pObj) )
112 for ( w = 0; w < nWords; w++ )
113 pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
114 else
115 for ( w = 0; w < nWords; w++ )
116 pInfo[w] = ~pInfo0[w] & pInfo1[w];
117 }
118 else
119 {
120 if ( Aig_ObjFaninC1(pObj) )
121 for ( w = 0; w < nWords; w++ )
122 pInfo[w] = pInfo0[w] & ~pInfo1[w];
123 else
124 for ( w = 0; w < nWords; w++ )
125 pInfo[w] = pInfo0[w] & pInfo1[w];
126 }
127 }
128 // clean the mask
129 for ( w = 0; w < nWords; w++ )
130 pInfoMask[w] = pInfoMask2[w] = 0;
131 // simulate the primary outputs
132 Aig_ManForEachCo( p, pObj, i )
133 {
134 pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
135 pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjFaninId0(pObj) );
136 if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) || i >= Saig_ManPoNum(p) )
137 {
138 if ( Aig_ObjFaninC0(pObj) )
139 {
140 for ( w = 0; w < nWords; w++ )
141 pInfo[w] = ~pInfo0[w];
142 }
143 else
144 {
145 for ( w = 0; w < nWords; w++ )
146 pInfo[w] = pInfo0[w];
147 }
148 }
149 else
150 {
151 if ( Aig_ObjFaninC0(pObj) )
152 {
153 for ( w = 0; w < nWords; w++ )
154 pInfo[w] |= ~pInfo0[w];
155 }
156 else
157 {
158 for ( w = 0; w < nWords; w++ )
159 pInfo[w] |= pInfo0[w];
160 }
161 }
162 // collect patterns when one of the outputs fails
163 if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
164 {
165 for ( w = 0; w < nWords; w++ )
166 pInfoMask[w] |= pInfo[w];
167 }
168 else if ( i < Saig_ManPoNum(p) )
169 {
170 for ( w = 0; w < nWords; w++ )
171 pInfoMask2[w] |= pInfo[w];
172 }
173 }
174 // compare the PO values (mask=1 => out=0) or UNSAT(mask=1 & out=1)
175 Saig_ManForEachPo( p, pObj, i )
176 {
177 pInfo = (unsigned *)Vec_PtrEntry( vInfo, Aig_ObjId(pObj) );
178 for ( w = 0; w < nWords; w++ )
179 Vec_IntAddToEntry( vProbs, i, Aig_WordCountOnes(pInfo[w]) );
180 if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
181 {
182 // chek the output
183 for ( w = 0; w < nWords; w++ )
184 if ( pInfo[w] & ~pInfoMask2[w] )
185 break;
186 if ( w == nWords )
187 continue;
188 printf( "Primary output %d fails on some input patterns.\n", i );
189 }
190 else
191 {
192 // collect patterns that block the POs
193 for ( w = 0; w < nWords; w++ )
194 Vec_IntAddToEntry( vProbs2, i, Aig_WordCountOnes(pInfo[w] & pInfoMask[w]) );
195 }
196 }
197 }
198 if ( fVerbose )
199 Abc_PrintTime( 1, "T", Abc_Clock() - clk );
200 // print the state
201 if ( fVerbose )
202 {
203 Saig_ManForEachPo( p, pObj, i )
204 {
205 if ( i < Saig_ManPoNum(p) - Saig_ManConstrNum(p) )
206 printf( "Primary output : " );
207 else
208 printf( "Constraint %3d : ", i-(Saig_ManPoNum(p) - Saig_ManConstrNum(p)) );
209 printf( "ProbOne = %f ", (float)Vec_IntEntry(vProbs, i)/(32*nWords*nFrames) );
210 printf( "ProbOneC = %f ", (float)Vec_IntEntry(vProbs2, i)/(32*nWords*nFrames) );
211 printf( "AllZeroValue = %d ", Aig_ObjPhase(pObj) );
212 printf( "\n" );
213 }
214 }
215
216 // print the states
217 Vec_PtrFree( vInfo );
218 Vec_IntFree( vProbs );
219 Vec_IntFree( vProbs2 );
220 return RetValue;
221 }
222
223 /**Function*************************************************************
224
225 Synopsis [Creates COI of the property output.]
226
227 Description []
228
229 SideEffects []
230
231 SeeAlso []
232
233 ***********************************************************************/
Saig_ManCreateIndMiter(Aig_Man_t * pAig,Vec_Vec_t * vCands)234 Aig_Man_t * Saig_ManCreateIndMiter( Aig_Man_t * pAig, Vec_Vec_t * vCands )
235 {
236 int nFrames = 2;
237 Vec_Ptr_t * vNodes;
238 Aig_Man_t * pFrames;
239 Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
240 Aig_Obj_t ** pObjMap;
241 int i, f, k;
242
243 // create mapping for the frames nodes
244 pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
245
246 // start the fraig package
247 pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
248 pFrames->pName = Abc_UtilStrsav( pAig->pName );
249 pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
250 // map constant nodes
251 for ( f = 0; f < nFrames; f++ )
252 Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
253 // create PI nodes for the frames
254 for ( f = 0; f < nFrames; f++ )
255 Aig_ManForEachPiSeq( pAig, pObj, i )
256 Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
257 // set initial state for the latches
258 Aig_ManForEachLoSeq( pAig, pObj, i )
259 Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
260
261 // add timeframes
262 for ( f = 0; f < nFrames; f++ )
263 {
264 // add internal nodes of this frame
265 Aig_ManForEachNode( pAig, pObj, i )
266 {
267 pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
268 Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
269 }
270 // set the latch inputs and copy them into the latch outputs of the next frame
271 Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
272 {
273 pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
274 if ( f < nFrames - 1 )
275 Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
276 }
277 }
278
279 // go through the candidates
280 Vec_VecForEachLevel( vCands, vNodes, i )
281 {
282 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
283 {
284 Aig_Obj_t * pObjR = Aig_Regular(pObj);
285 Aig_Obj_t * pNode0 = pObjMap[nFrames*Aig_ObjId(pObjR)+0];
286 Aig_Obj_t * pNode1 = pObjMap[nFrames*Aig_ObjId(pObjR)+1];
287 Aig_Obj_t * pFan0 = Aig_NotCond( pNode0, Aig_IsComplement(pObj) );
288 Aig_Obj_t * pFan1 = Aig_NotCond( pNode1, !Aig_IsComplement(pObj) );
289 Aig_Obj_t * pMiter = Aig_And( pFrames, pFan0, pFan1 );
290 Aig_ObjCreateCo( pFrames, pMiter );
291 }
292 }
293 Aig_ManCleanup( pFrames );
294 ABC_FREE( pObjMap );
295
296 //Aig_ManShow( pAig, 0, NULL );
297 //Aig_ManShow( pFrames, 0, NULL );
298 return pFrames;
299 }
300
301 /**Function*************************************************************
302
303 Synopsis [Performs inductive check for one of the constraints.]
304
305 Description []
306
307 SideEffects []
308
309 SeeAlso []
310
311 ***********************************************************************/
Saig_ManFilterUsingIndOne_new(Aig_Man_t * p,Aig_Man_t * pFrame,sat_solver * pSat,Cnf_Dat_t * pCnf,int nConfs,int nProps,int Counter)312 int Saig_ManFilterUsingIndOne_new( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver * pSat, Cnf_Dat_t * pCnf, int nConfs, int nProps, int Counter )
313 {
314 Aig_Obj_t * pObj;
315 int Lit, status;
316 pObj = Aig_ManCo( pFrame, Counter );
317 Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 );
318 status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
319 if ( status == l_False )
320 return 1;
321 if ( status == l_Undef )
322 {
323 // printf( "Solver returned undecided.\n" );
324 return 0;
325 }
326 assert( status == l_True );
327 return 0;
328 }
329
330 /**Function*************************************************************
331
332 Synopsis [Detects constraints functionally.]
333
334 Description []
335
336 SideEffects []
337
338 SeeAlso []
339
340 ***********************************************************************/
Saig_ManFilterUsingInd(Aig_Man_t * p,Vec_Vec_t * vCands,int nConfs,int nProps,int fVerbose)341 void Saig_ManFilterUsingInd( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int nProps, int fVerbose )
342 {
343 Vec_Ptr_t * vNodes;
344 Aig_Man_t * pFrames;
345 sat_solver * pSat;
346 Cnf_Dat_t * pCnf;
347 Aig_Obj_t * pObj;
348 int i, k, k2, Counter;
349 /*
350 Vec_VecForEachLevel( vCands, vNodes, i )
351 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
352 printf( "%d ", Aig_ObjId(Aig_Regular(pObj)) );
353 printf( "\n" );
354 */
355 // create timeframes
356 // pFrames = Saig_ManUnrollInd( p );
357 pFrames = Saig_ManCreateIndMiter( p, vCands );
358 assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands) );
359 // start the SAT solver
360 pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
361 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
362 // check candidates
363 if ( fVerbose )
364 printf( "Filtered cands: " );
365 Counter = 0;
366 Vec_VecForEachLevel( vCands, vNodes, i )
367 {
368 k2 = 0;
369 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
370 {
371 if ( Saig_ManFilterUsingIndOne_new( p, pFrames, pSat, pCnf, nConfs, nProps, Counter++ ) )
372 // if ( Saig_ManFilterUsingIndOne_old( p, pSat, pCnf, nConfs, pObj ) )
373 {
374 Vec_PtrWriteEntry( vNodes, k2++, pObj );
375 if ( fVerbose )
376 printf( "%d:%s%d ", i, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
377 }
378 }
379 Vec_PtrShrink( vNodes, k2 );
380 }
381 if ( fVerbose )
382 printf( "\n" );
383 // clean up
384 Cnf_DataFree( pCnf );
385 sat_solver_delete( pSat );
386 if ( fVerbose )
387 Aig_ManPrintStats( pFrames );
388 Aig_ManStop( pFrames );
389 }
390
391
392
393
394 /**Function*************************************************************
395
396 Synopsis [Creates COI of the property output.]
397
398 Description []
399
400 SideEffects []
401
402 SeeAlso []
403
404 ***********************************************************************/
Saig_ManUnrollCOI_(Aig_Man_t * p,int nFrames)405 Aig_Man_t * Saig_ManUnrollCOI_( Aig_Man_t * p, int nFrames )
406 {
407 Aig_Man_t * pFrames;
408 Aig_Obj_t ** pObjMap;
409 int i;
410 //Aig_Man_t * Aig_ManFrames( Aig_Man_t * pAig, int nFrames, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap )
411 pFrames = Aig_ManFrames( p, nFrames, 0, 1, 1, 0, &pObjMap );
412 for ( i = 0; i < nFrames * Aig_ManObjNumMax(p); i++ )
413 if ( pObjMap[i] && Aig_ObjIsNone( Aig_Regular(pObjMap[i]) ) )
414 pObjMap[i] = NULL;
415 assert( p->pObjCopies == NULL );
416 p->pObjCopies = pObjMap;
417 return pFrames;
418 }
419
420 /**Function*************************************************************
421
422 Synopsis [Creates COI of the property output.]
423
424 Description []
425
426 SideEffects []
427
428 SeeAlso []
429
430 ***********************************************************************/
Saig_ManUnrollCOI(Aig_Man_t * pAig,int nFrames)431 Aig_Man_t * Saig_ManUnrollCOI( Aig_Man_t * pAig, int nFrames )
432 {
433 Aig_Man_t * pFrames;
434 Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
435 Aig_Obj_t ** pObjMap;
436 int i, f;
437 // create mapping for the frames nodes
438 pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) );
439 // start the fraig package
440 pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
441 pFrames->pName = Abc_UtilStrsav( pAig->pName );
442 pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
443 // map constant nodes
444 for ( f = 0; f < nFrames; f++ )
445 Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) );
446 // create PI nodes for the frames
447 for ( f = 0; f < nFrames; f++ )
448 Aig_ManForEachPiSeq( pAig, pObj, i )
449 Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, Aig_ObjCreateCi(pFrames) );
450 // set initial state for the latches
451 Aig_ManForEachLoSeq( pAig, pObj, i )
452 Aig_ObjSetFrames( pObjMap, nFrames, pObj, 0, Aig_ObjCreateCi(pFrames) );
453 // add timeframes
454 for ( f = 0; f < nFrames; f++ )
455 {
456 Aig_ManForEachNode( pAig, pObj, i )
457 {
458 pObjNew = Aig_And( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f), Aig_ObjChild1Frames(pObjMap,nFrames,pObj,f) );
459 Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
460 }
461 // set the latch inputs and copy them into the latch outputs of the next frame
462 Aig_ManForEachLiLoSeq( pAig, pObjLi, pObjLo, i )
463 {
464 pObjNew = Aig_ObjChild0Frames(pObjMap,nFrames,pObjLi,f);
465 if ( f < nFrames - 1 )
466 Aig_ObjSetFrames( pObjMap, nFrames, pObjLo, f+1, pObjNew );
467 }
468 }
469 // create the only output
470 for ( f = nFrames-1; f < nFrames; f++ )
471 {
472 Aig_ManForEachPoSeq( pAig, pObj, i )
473 {
474 pObjNew = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Frames(pObjMap,nFrames,pObj,f) );
475 Aig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew );
476 }
477 }
478 // created lots of dangling nodes - no sweeping!
479 //Aig_ManCleanup( pFrames );
480 assert( pAig->pObjCopies == NULL );
481 pAig->pObjCopies = pObjMap;
482 return pFrames;
483 }
484
485
486 /**Function*************************************************************
487
488 Synopsis [Collects and saves values of the SAT variables.]
489
490 Description []
491
492 SideEffects []
493
494 SeeAlso []
495
496 ***********************************************************************/
Saig_CollectSatValues(sat_solver * pSat,Cnf_Dat_t * pCnf,Vec_Ptr_t * vInfo,int * piPat)497 void Saig_CollectSatValues( sat_solver * pSat, Cnf_Dat_t * pCnf, Vec_Ptr_t * vInfo, int * piPat )
498 {
499 Aig_Obj_t * pObj;
500 unsigned * pInfo;
501 int i;
502 Aig_ManForEachObj( pCnf->pMan, pObj, i )
503 {
504 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
505 continue;
506 assert( pCnf->pVarNums[i] > 0 );
507 pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
508 if ( Abc_InfoHasBit(pInfo, *piPat) != sat_solver_var_value(pSat, pCnf->pVarNums[i]) )
509 Abc_InfoXorBit(pInfo, *piPat);
510 }
511 }
512
513 /**Function*************************************************************
514
515 Synopsis [Runs the SAT test for the node in one polarity.]
516
517 Description []
518
519 SideEffects []
520
521 SeeAlso []
522
523 ***********************************************************************/
Saig_DetectTryPolarity(sat_solver * pSat,int nConfs,int nProps,Cnf_Dat_t * pCnf,Aig_Obj_t * pObj,int iPol,Vec_Ptr_t * vInfo,int * piPat,int fVerbose)524 int Saig_DetectTryPolarity( sat_solver * pSat, int nConfs, int nProps, Cnf_Dat_t * pCnf, Aig_Obj_t * pObj, int iPol, Vec_Ptr_t * vInfo, int * piPat, int fVerbose )
525 {
526 Aig_Obj_t * pOut = Aig_ManCo( pCnf->pMan, 0 );
527 int status, Lits[2];
528 // ABC_INT64_T nOldConfs = pSat->stats.conflicts;
529 // ABC_INT64_T nOldImps = pSat->stats.propagations;
530 Lits[0] = toLitCond( pCnf->pVarNums[Aig_ObjId(pOut)], 0 );
531 Lits[1] = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !iPol );
532 status = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nConfs, (ABC_INT64_T)nProps, 0, 0 );
533 if ( status == l_False )
534 {
535 // printf( "u%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) );
536 return 1;
537 }
538 if ( status == l_Undef )
539 {
540 // printf( "Solver returned undecided.\n" );
541 return 0;
542 }
543 // printf( "s%d(%d) ", (int)(pSat->stats.conflicts-nOldConfs), (int)(pSat->stats.propagations-nOldImps) );
544 assert( status == l_True );
545 Saig_CollectSatValues( pSat, pCnf, vInfo, piPat );
546 (*piPat)++;
547 if ( *piPat == Vec_PtrReadWordsSimInfo(vInfo) * 32 )
548 {
549 if ( fVerbose )
550 printf( "Warning: Reached the limit on the number of patterns.\n" );
551 *piPat = 0;
552 }
553 return 0;
554 }
555
556 /**Function*************************************************************
557
558 Synopsis [Returns the number of variables implied by the output.]
559
560 Description []
561
562 SideEffects []
563
564 SeeAlso []
565
566 ***********************************************************************/
Ssw_ManFindDirectImplications(Aig_Man_t * p,int nFrames,int nConfs,int nProps,int fVerbose)567 Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
568 {
569 Vec_Vec_t * vCands = NULL;
570 Vec_Ptr_t * vNodes;
571 Cnf_Dat_t * pCnf;
572 sat_solver * pSat;
573 Aig_Man_t * pFrames;
574 Aig_Obj_t * pObj, * pRepr, * pReprR;
575 int i, f, k, value;
576 vCands = Vec_VecAlloc( nFrames );
577
578 // perform unrolling
579 pFrames = Saig_ManUnrollCOI( p, nFrames );
580 assert( Aig_ManCoNum(pFrames) == 1 );
581 // start the SAT solver
582 pCnf = Cnf_DeriveSimple( pFrames, 0 );
583 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
584 if ( pSat != NULL )
585 {
586 Aig_ManIncrementTravId( p );
587 for ( f = 0; f < nFrames; f++ )
588 {
589 Aig_ManForEachObj( p, pObj, i )
590 {
591 if ( !Aig_ObjIsCand(pObj) )
592 continue;
593 if ( Aig_ObjIsTravIdCurrent(p, pObj) )
594 continue;
595 // get the node from timeframes
596 pRepr = p->pObjCopies[nFrames*i + nFrames-1-f];
597 pReprR = Aig_Regular(pRepr);
598 if ( pCnf->pVarNums[Aig_ObjId(pReprR)] < 0 )
599 continue;
600 // value = pSat->assigns[ pCnf->pVarNums[Aig_ObjId(pReprR)] ];
601 value = sat_solver_get_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pReprR)] );
602 if ( value == l_Undef )
603 continue;
604 // label this node as taken
605 Aig_ObjSetTravIdCurrent(p, pObj);
606 if ( Saig_ObjIsLo(p, pObj) )
607 Aig_ObjSetTravIdCurrent( p, Aig_ObjFanin0(Saig_ObjLoToLi(p, pObj)) );
608 // remember the node
609 Vec_VecPush( vCands, f, Aig_NotCond( pObj, (value == l_True) ^ Aig_IsComplement(pRepr) ) );
610 // printf( "%s%d ", (value == l_False)? "":"!", i );
611 }
612 }
613 // printf( "\n" );
614 sat_solver_delete( pSat );
615 }
616 Aig_ManStop( pFrames );
617 Cnf_DataFree( pCnf );
618
619 if ( fVerbose )
620 {
621 printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
622 Vec_VecForEachLevel( vCands, vNodes, k )
623 {
624 printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
625 // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
626 // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
627 printf( "\n" );
628 }
629 }
630
631 ABC_FREE( p->pObjCopies );
632 Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose );
633 if ( Vec_VecSizeSize(vCands) )
634 printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
635 if ( fVerbose )
636 {
637 Vec_VecForEachLevel( vCands, vNodes, k )
638 {
639 printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
640 // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
641 // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
642 printf( "\n" );
643 }
644 }
645
646 return vCands;
647 }
648
649
650 /**Function*************************************************************
651
652 Synopsis [Detects constraints functionally.]
653
654 Description []
655
656 SideEffects []
657
658 SeeAlso []
659
660 ***********************************************************************/
Saig_ManDetectConstrFunc(Aig_Man_t * p,int nFrames,int nConfs,int nProps,int fVerbose)661 Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fVerbose )
662 {
663 int iPat = 0, nWordsAlloc = 16;
664 Bar_Progress_t * pProgress = NULL;
665 Vec_Vec_t * vCands = NULL;
666 Vec_Ptr_t * vInfo, * vNodes;
667 Aig_Obj_t * pObj, * pRepr, * pObjNew;
668 Aig_Man_t * pFrames;
669 sat_solver * pSat;
670 Cnf_Dat_t * pCnf;
671 unsigned * pInfo;
672 int i, j, k, Lit, status, nCands = 0;
673 assert( Saig_ManPoNum(p) == 1 );
674 if ( Saig_ManPoNum(p) != 1 )
675 {
676 printf( "The number of outputs is different from 1.\n" );
677 return NULL;
678 }
679 //printf( "Implications = %d.\n", Ssw_ManCountImplications(p, nFrames) );
680
681 // perform unrolling
682 pFrames = Saig_ManUnrollCOI( p, nFrames );
683 assert( Aig_ManCoNum(pFrames) == 1 );
684 if ( fVerbose )
685 {
686 printf( "Detecting constraints with %d frames, %d conflicts, and %d propagations.\n", nFrames, nConfs, nProps );
687 printf( "Frames: " );
688 Aig_ManPrintStats( pFrames );
689 }
690 // Aig_ManShow( pFrames, 0, NULL );
691
692 // start the SAT solver
693 pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
694 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
695 //printf( "Implications = %d.\n", pSat->qhead );
696
697 // solve the original problem
698 Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(Aig_ManCo(pFrames,0))], 0 );
699 status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 );
700 if ( status == l_False )
701 {
702 printf( "The problem is trivially UNSAT (inductive with k=%d).\n", nFrames-1 );
703 Cnf_DataFree( pCnf );
704 sat_solver_delete( pSat );
705 Aig_ManStop( pFrames );
706 return NULL;
707 }
708 if ( status == l_Undef )
709 {
710 printf( "Solver could not solve the original problem.\n" );
711 Cnf_DataFree( pCnf );
712 sat_solver_delete( pSat );
713 Aig_ManStop( pFrames );
714 return NULL;
715 }
716 assert( status == l_True );
717
718 // create simulation info
719 vInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pFrames), nWordsAlloc );
720 Vec_PtrCleanSimInfo( vInfo, 0, nWordsAlloc );
721 Saig_CollectSatValues( pSat, pCnf, vInfo, &iPat );
722 Aig_ManForEachObj( pFrames, pObj, i )
723 {
724 pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
725 if ( pInfo[0] & 1 )
726 memset( (char*)pInfo, 0xff, 4*nWordsAlloc );
727 }
728 // Aig_ManShow( pFrames, 0, NULL );
729 // Aig_ManShow( p, 0, NULL );
730
731 // consider the nodes for ci=>!Out and label when it holds
732 pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pFrames) );
733 Aig_ManCleanMarkAB( pFrames );
734 Aig_ManForEachObj( pFrames, pObj, i )
735 {
736 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
737 continue;
738 Bar_ProgressUpdate( pProgress, i, NULL );
739 // check if the node is available in both polarities
740 pInfo = (unsigned *)Vec_PtrEntry( vInfo, i );
741 for ( k = 0; k < nWordsAlloc; k++ )
742 if ( pInfo[k] != ~0 )
743 break;
744 if ( k == nWordsAlloc )
745 {
746 if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 0, vInfo, &iPat, fVerbose) ) // !pObj is a constr
747 {
748 pObj->fMarkA = 1, nCands++;
749 // printf( "!%d ", Aig_ObjId(pObj) );
750 }
751 continue;
752 }
753 for ( k = 0; k < nWordsAlloc; k++ )
754 if ( pInfo[k] != 0 )
755 break;
756 if ( k == nWordsAlloc )
757 {
758 if ( Saig_DetectTryPolarity(pSat, nConfs, nProps, pCnf, pObj, 1, vInfo, &iPat, fVerbose) ) // pObj is a constr
759 {
760 pObj->fMarkB = 1, nCands++;
761 // printf( "%d ", Aig_ObjId(pObj) );
762 }
763 continue;
764 }
765 }
766 Bar_ProgressStop( pProgress );
767 if ( nCands )
768 {
769
770 // printf( "\n" );
771 if ( fVerbose )
772 printf( "Found %3d classes of candidates.\n", nCands );
773 vCands = Vec_VecAlloc( nFrames );
774 for ( k = 0; k < nFrames; k++ )
775 {
776 Aig_ManForEachObj( p, pObj, i )
777 {
778 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
779 continue;
780 pRepr = p->pObjCopies[nFrames*i + nFrames-1-k];
781 // pRepr = p->pObjCopies[nFrames*i + k];
782 if ( pRepr == NULL )
783 continue;
784 if ( Aig_Regular(pRepr)->fMarkA ) // !pObj is a constr
785 {
786 pObjNew = Aig_NotCond(pObj, !Aig_IsComplement(pRepr));
787
788 for ( j = 0; j < k; j++ )
789 if ( Vec_PtrFind( Vec_VecEntry(vCands, j), pObjNew ) >= 0 )
790 break;
791 if ( j == k )
792 Vec_VecPush( vCands, k, pObjNew );
793 // printf( "%d->!%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) );
794 }
795 else if ( Aig_Regular(pRepr)->fMarkB ) // pObj is a constr
796 {
797 pObjNew = Aig_NotCond(pObj, Aig_IsComplement(pRepr));
798
799 for ( j = 0; j < k; j++ )
800 if ( Vec_PtrFind( Vec_VecEntry(vCands, j), pObjNew ) >= 0 )
801 break;
802 if ( j == k )
803 Vec_VecPush( vCands, k, pObjNew );
804 // printf( "%d->%d ", Aig_ObjId(Aig_Regular(pRepr)), Aig_ObjId(pObj) );
805 }
806 }
807 }
808
809 // printf( "\n" );
810 if ( fVerbose )
811 {
812 printf( "Found %3d candidates.\n", Vec_VecSizeSize(vCands) );
813 Vec_VecForEachLevel( vCands, vNodes, k )
814 {
815 printf( "Level %d. Cands =%d ", k, Vec_PtrSize(vNodes) );
816 // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
817 // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
818 printf( "\n" );
819 }
820 }
821
822 ABC_FREE( p->pObjCopies );
823 Saig_ManFilterUsingInd( p, vCands, nConfs, nProps, fVerbose );
824 if ( Vec_VecSizeSize(vCands) )
825 printf( "Found %3d constraints after filtering.\n", Vec_VecSizeSize(vCands) );
826 if ( fVerbose )
827 {
828 Vec_VecForEachLevel( vCands, vNodes, k )
829 {
830 printf( "Level %d. Constr =%d ", k, Vec_PtrSize(vNodes) );
831 // Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
832 // printf( "%d:%s%d ", k, Aig_IsComplement(pObj)? "!":"", Aig_ObjId(Aig_Regular(pObj)) );
833 printf( "\n" );
834 }
835 }
836 }
837 Vec_PtrFree( vInfo );
838 Cnf_DataFree( pCnf );
839 sat_solver_delete( pSat );
840 Aig_ManCleanMarkAB( pFrames );
841 Aig_ManStop( pFrames );
842 return vCands;
843 }
844
845 /**Function*************************************************************
846
847 Synopsis [Experimental procedure.]
848
849 Description []
850
851 SideEffects []
852
853 SeeAlso []
854
855 ***********************************************************************/
Saig_ManDetectConstrFuncTest(Aig_Man_t * p,int nFrames,int nConfs,int nProps,int fOldAlgo,int fVerbose)856 void Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
857 {
858 Vec_Vec_t * vCands;
859 if ( fOldAlgo )
860 vCands = Saig_ManDetectConstrFunc( p, nFrames, nConfs, nProps, fVerbose );
861 else
862 vCands = Ssw_ManFindDirectImplications( p, nFrames, nConfs, nProps, fVerbose );
863 Vec_VecFreeP( &vCands );
864 }
865
866 /**Function*************************************************************
867
868 Synopsis [Duplicates the AIG while unfolding constraints.]
869
870 Description []
871
872 SideEffects []
873
874 SeeAlso []
875
876 ***********************************************************************/
Saig_ManDupUnfoldConstrsFunc(Aig_Man_t * pAig,int nFrames,int nConfs,int nProps,int fOldAlgo,int fVerbose)877 Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose )
878 {
879 Aig_Man_t * pNew;
880 Vec_Vec_t * vCands;
881 Vec_Ptr_t * vNodes, * vNewFlops;
882 Aig_Obj_t * pObj;
883 int i, j, k, nNewFlops;
884 if ( fOldAlgo )
885 vCands = Saig_ManDetectConstrFunc( pAig, nFrames, nConfs, nProps, fVerbose );
886 else
887 vCands = Ssw_ManFindDirectImplications( pAig, nFrames, nConfs, nProps, fVerbose );
888 if ( vCands == NULL || Vec_VecSizeSize(vCands) == 0 )
889 {
890 Vec_VecFreeP( &vCands );
891 return Aig_ManDupDfs( pAig );
892 }
893 // create new manager
894 pNew = Aig_ManDupWithoutPos( pAig );
895 pNew->nConstrs = pAig->nConstrs + Vec_VecSizeSize(vCands);
896 // add normal POs
897 Saig_ManForEachPo( pAig, pObj, i )
898 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
899 // create constraint outputs
900 vNewFlops = Vec_PtrAlloc( 100 );
901 Vec_VecForEachLevel( vCands, vNodes, i )
902 {
903 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
904 {
905 Vec_PtrPush( vNewFlops, Aig_ObjRealCopy(pObj) );
906 for ( j = 0; j < i; j++ )
907 Vec_PtrPush( vNewFlops, Aig_ObjCreateCi(pNew) );
908 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrPop(vNewFlops) );
909 }
910 }
911 // add latch outputs
912 Saig_ManForEachLi( pAig, pObj, i )
913 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
914 // add new latch outputs
915 nNewFlops = 0;
916 Vec_VecForEachLevel( vCands, vNodes, i )
917 {
918 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, k )
919 {
920 for ( j = 0; j < i; j++ )
921 Aig_ObjCreateCo( pNew, (Aig_Obj_t *)Vec_PtrEntry(vNewFlops, nNewFlops++) );
922 }
923 }
924 assert( nNewFlops == Vec_PtrSize(vNewFlops) );
925 Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) + nNewFlops );
926 Vec_VecFreeP( &vCands );
927 Vec_PtrFree( vNewFlops );
928 return pNew;
929 }
930
931 /**Function*************************************************************
932
933 Synopsis [Duplicates the AIG while unfolding constraints.]
934
935 Description []
936
937 SideEffects []
938
939 SeeAlso []
940
941 ***********************************************************************/
Saig_ManDupFoldConstrsFunc(Aig_Man_t * pAig,int fCompl,int fVerbose)942 Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose )
943 {
944 Aig_Man_t * pAigNew;
945 Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
946 int i;
947 if ( Aig_ManConstrNum(pAig) == 0 )
948 return Aig_ManDupDfs( pAig );
949 assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) );
950 // start the new manager
951 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
952 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
953 pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec );
954 // map the constant node
955 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
956 // create variables for PIs
957 Aig_ManForEachCi( pAig, pObj, i )
958 pObj->pData = Aig_ObjCreateCi( pAigNew );
959 // add internal nodes of this frame
960 Aig_ManForEachNode( pAig, pObj, i )
961 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
962
963 // OR the constraint outputs
964 pMiter = Aig_ManConst0( pAigNew );
965 Saig_ManForEachPo( pAig, pObj, i )
966 {
967 if ( i < Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
968 continue;
969 pMiter = Aig_Or( pAigNew, pMiter, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
970 }
971
972 // create additional flop
973 if ( Saig_ManRegNum(pAig) > 0 )
974 {
975 pFlopOut = Aig_ObjCreateCi( pAigNew );
976 pFlopIn = Aig_Or( pAigNew, pMiter, pFlopOut );
977 }
978 else
979 pFlopIn = pMiter;
980
981 // create primary output
982 Saig_ManForEachPo( pAig, pObj, i )
983 {
984 if ( i >= Saig_ManPoNum(pAig)-Aig_ManConstrNum(pAig) )
985 continue;
986 pMiter = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_Not(pFlopIn) );
987 Aig_ObjCreateCo( pAigNew, pMiter );
988 }
989
990 // transfer to register outputs
991 Saig_ManForEachLi( pAig, pObj, i )
992 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
993
994 // create additional flop
995 if ( Saig_ManRegNum(pAig) > 0 )
996 {
997 Aig_ObjCreateCo( pAigNew, pFlopIn );
998 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 );
999 }
1000
1001 // perform cleanup
1002 Aig_ManCleanup( pAigNew );
1003 Aig_ManSeqCleanup( pAigNew );
1004 return pAigNew;
1005 }
1006
1007 ////////////////////////////////////////////////////////////////////////
1008 /// END OF FILE ///
1009 ////////////////////////////////////////////////////////////////////////
1010
1011 #include "saigUnfold2.c"
1012 ABC_NAMESPACE_IMPL_END
1013
1014