abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
saigTrans.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigTrans.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Dynamic simplication of the transition relation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigTrans.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "saig.h"
22 #include "proof/fra/fra.h"
23 
25 
26 
27 /*
28  A similar approach is presented in the his paper:
29  A. Kuehlmann. Dynamic transition relation simplification for
30  bounded property checking. ICCAD'04, pp. 50-57.
31 */
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// DECLARATIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 ////////////////////////////////////////////////////////////////////////
38 /// FUNCTION DEFINITIONS ///
39 ////////////////////////////////////////////////////////////////////////
40 
41 /**Function*************************************************************
42 
43  Synopsis [Maps a node/frame into a node of a different manager.]
44 
45  Description []
46 
47  SideEffects []
48 
49  SeeAlso []
50 
51 ***********************************************************************/
52 static inline void Saig_ManStartMap1( Aig_Man_t * p, int nFrames )
53 {
54  Vec_Int_t * vMap;
55  int i;
56  assert( p->pData == NULL );
57  vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames );
58  for ( i = 0; i < vMap->nCap; i++ )
59  vMap->pArray[i] = -1;
60  vMap->nSize = vMap->nCap;
61  p->pData = vMap;
62 }
63 static inline void Saig_ManStopMap1( Aig_Man_t * p )
64 {
65  assert( p->pData != NULL );
66  Vec_IntFree( (Vec_Int_t *)p->pData );
67  p->pData = NULL;
68 }
69 static inline int Saig_ManHasMap1( Aig_Man_t * p )
70 {
71  return (int)(p->pData != NULL);
72 }
73 static inline void Saig_ManSetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew )
74 {
75  Vec_Int_t * vMap = (Vec_Int_t *)p->pData;
76  int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
77  assert( !Aig_IsComplement(pOld) );
78  assert( !Aig_IsComplement(pNew) );
79  Vec_IntWriteEntry( vMap, nOffset, pNew->Id );
80 }
81 static inline int Saig_ManGetMap1( Aig_Man_t * p, Aig_Obj_t * pOld, int f1 )
82 {
83  Vec_Int_t * vMap = (Vec_Int_t *)p->pData;
84  int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
85  return Vec_IntEntry( vMap, nOffset );
86 }
87 
88 /**Function*************************************************************
89 
90  Synopsis [Maps a node/frame into a node/frame of a different manager.]
91 
92  Description []
93 
94  SideEffects []
95 
96  SeeAlso []
97 
98 ***********************************************************************/
99 static inline void Saig_ManStartMap2( Aig_Man_t * p, int nFrames )
100 {
101  Vec_Int_t * vMap;
102  int i;
103  assert( p->pData2 == NULL );
104  vMap = Vec_IntAlloc( Aig_ManObjNumMax(p) * nFrames * 2 );
105  for ( i = 0; i < vMap->nCap; i++ )
106  vMap->pArray[i] = -1;
107  vMap->nSize = vMap->nCap;
108  p->pData2 = vMap;
109 }
110 static inline void Saig_ManStopMap2( Aig_Man_t * p )
111 {
112  assert( p->pData2 != NULL );
113  Vec_IntFree( (Vec_Int_t *)p->pData2 );
114  p->pData2 = NULL;
115 }
116 static inline int Saig_ManHasMap2( Aig_Man_t * p )
117 {
118  return (int)(p->pData2 != NULL);
119 }
120 static inline void Saig_ManSetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, Aig_Obj_t * pNew, int f2 )
121 {
122  Vec_Int_t * vMap = (Vec_Int_t *)p->pData2;
123  int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
124  assert( !Aig_IsComplement(pOld) );
125  assert( !Aig_IsComplement(pNew) );
126  Vec_IntWriteEntry( vMap, 2*nOffset + 0, pNew->Id );
127  Vec_IntWriteEntry( vMap, 2*nOffset + 1, f2 );
128 }
129 static inline int Saig_ManGetMap2( Aig_Man_t * p, Aig_Obj_t * pOld, int f1, int * pf2 )
130 {
131  Vec_Int_t * vMap = (Vec_Int_t *)p->pData2;
132  int nOffset = f1 * Aig_ManObjNumMax(p) + pOld->Id;
133  *pf2 = Vec_IntEntry( vMap, 2*nOffset + 1 );
134  return Vec_IntEntry( vMap, 2*nOffset );
135 }
136 
137 /**Function*************************************************************
138 
139  Synopsis [Create mapping for the first nFrames timeframes of pAig.]
140 
141  Description []
142 
143  SideEffects []
144 
145  SeeAlso []
146 
147 ***********************************************************************/
148 void Saig_ManCreateMapping( Aig_Man_t * pAig, Aig_Man_t * pFrames, int nFrames )
149 {
150  Aig_Obj_t * pObj, * pObjFrame, * pObjRepr;
151  int i, f, iNum, iFrame;
152  assert( pFrames->pReprs != NULL ); // mapping from nodes into their representatives
153  // start step mapping for both orignal manager and fraig
154  Saig_ManStartMap2( pAig, nFrames );
155  Saig_ManStartMap2( pFrames, 1 );
156  // for each object in each frame
157  for ( f = 0; f < nFrames; f++ )
158  Aig_ManForEachObj( pAig, pObj, i )
159  {
160  // get the frame object
161  iNum = Saig_ManGetMap1( pAig, pObj, f );
162  pObjFrame = Aig_ManObj( pFrames, iNum );
163  // if the node has no prototype, map it into itself
164  if ( pObjFrame == NULL )
165  {
166  Saig_ManSetMap2( pAig, pObj, f, pObj, f );
167  continue;
168  }
169  // get the representative object
170  pObjRepr = Aig_ObjRepr( pFrames, pObjFrame );
171  if ( pObjRepr == NULL )
172  pObjRepr = pObjFrame;
173  // check if this is the first time this object is reached
174  if ( Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame ) == -1 )
175  Saig_ManSetMap2( pFrames, pObjRepr, 0, pObj, f );
176  // set the map for the main object
177  iNum = Saig_ManGetMap2( pFrames, pObjRepr, 0, &iFrame );
178  Saig_ManSetMap2( pAig, pObj, f, Aig_ManObj(pAig, iNum), iFrame );
179  }
180  Saig_ManStopMap2( pFrames );
181  assert( Saig_ManHasMap2(pAig) );
182 }
183 
184 /**Function*************************************************************
185 
186  Synopsis [Unroll without initialization.]
187 
188  Description []
189 
190  SideEffects []
191 
192  SeeAlso []
193 
194 ***********************************************************************/
196 {
197  Aig_Man_t * pFrames;
198  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
199  int i, f;
200  assert( Saig_ManRegNum(pAig) > 0 );
201  // start node map
202  Saig_ManStartMap1( pAig, nFrames );
203  // start the new manager
204  pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
205  // map the constant node
206  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
207  // create variables for register outputs
208  Saig_ManForEachLo( pAig, pObj, i )
209  pObj->pData = Aig_ObjCreateCi( pFrames );
210  // add timeframes
211  for ( f = 0; f < nFrames; f++ )
212  {
213  // create PI nodes for this frame
214  Saig_ManForEachPi( pAig, pObj, i )
215  pObj->pData = Aig_ObjCreateCi( pFrames );
216  // add internal nodes of this frame
217  Aig_ManForEachNode( pAig, pObj, i )
218  pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
219  // create POs for this frame
220  Saig_ManForEachPo( pAig, pObj, i )
221  pObj->pData = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
222  // save register inputs
223  Saig_ManForEachLi( pAig, pObj, i )
224  pObj->pData = Aig_ObjChild0Copy(pObj);
225  // save the mapping
226  Aig_ManForEachObj( pAig, pObj, i )
227  {
228  assert( pObj->pData != NULL );
229  Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) );
230  }
231  // quit if the last frame
232  if ( f == nFrames - 1 )
233  break;
234  // transfer to register outputs
235  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
236  pObjLo->pData = pObjLi->pData;
237  }
238  // remember register outputs
239  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
240  Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLi->pData );
241  Aig_ManCleanup( pFrames );
242  return pFrames;
243 }
244 
245 /**Function*************************************************************
246 
247  Synopsis [Unroll with initialization and mapping.]
248 
249  Description []
250 
251  SideEffects []
252 
253  SeeAlso []
254 
255 ***********************************************************************/
256 Aig_Man_t * Saig_ManFramesInitialMapped( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit )
257 {
258  Aig_Man_t * pFrames;
259  Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pRepr;
260  int i, f, iNum1, iNum2, iFrame2;
261  assert( nFrames <= nFramesMax );
262  assert( Saig_ManRegNum(pAig) > 0 );
263  // start node map
264  Saig_ManStartMap1( pAig, nFramesMax );
265  // start the new manager
266  pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFramesMax );
267  // create variables for register outputs
268  if ( fInit )
269  {
270  Saig_ManForEachLo( pAig, pObj, i )
271  {
272  pObj->pData = Aig_ManConst0( pFrames );
273  Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular((Aig_Obj_t *)pObj->pData) );
274  }
275  }
276  else
277  {
278  // create PIs first
279  for ( f = 0; f < nFramesMax; f++ )
280  Saig_ManForEachPi( pAig, pObj, i )
281  Aig_ObjCreateCi( pFrames );
282  // create registers second
283  Saig_ManForEachLo( pAig, pObj, i )
284  {
285  pObj->pData = Aig_ObjCreateCi( pFrames );
286  Saig_ManSetMap1( pAig, pObj, 0, Aig_Regular((Aig_Obj_t *)pObj->pData) );
287  }
288  }
289  // add timeframes
290  for ( f = 0; f < nFramesMax; f++ )
291  {
292  // map the constant node
293  pObj = Aig_ManConst1(pAig);
294  pObj->pData = Aig_ManConst1( pFrames );
295  Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) );
296  // create PI nodes for this frame
297  Saig_ManForEachPi( pAig, pObj, i )
298  {
299  if ( fInit )
300  pObj->pData = Aig_ObjCreateCi( pFrames );
301  else
302  pObj->pData = Aig_ManCi( pFrames, f * Saig_ManPiNum(pAig) + i );
303  Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) );
304  }
305  // add internal nodes of this frame
306  Aig_ManForEachNode( pAig, pObj, i )
307  {
308  pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
309  Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) );
310  if ( !Saig_ManHasMap2(pAig) )
311  continue;
312  if ( f < nFrames )
313  {
314  // get the mapping for this node
315  iNum2 = Saig_ManGetMap2( pAig, pObj, f, &iFrame2 );
316  }
317  else
318  {
319  // get the mapping for this node
320  iNum2 = Saig_ManGetMap2( pAig, pObj, nFrames-1, &iFrame2 );
321  iFrame2 += f - (nFrames-1);
322  }
323  assert( iNum2 != -1 );
324  assert( f >= iFrame2 );
325  // get the corresponding frames node
326  iNum1 = Saig_ManGetMap1( pAig, Aig_ManObj(pAig, iNum2), iFrame2 );
327  pRepr = Aig_ManObj( pFrames, iNum1 );
328  // compare the phases of these nodes
329  pObj->pData = Aig_NotCond( pRepr, pRepr->fPhase ^ Aig_ObjPhaseReal((Aig_Obj_t *)pObj->pData) );
330  }
331  // create POs for this frame
332  Saig_ManForEachPo( pAig, pObj, i )
333  {
334  pObj->pData = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
335  Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) );
336  }
337  // save register inputs
338  Saig_ManForEachLi( pAig, pObj, i )
339  {
340  pObj->pData = Aig_ObjChild0Copy(pObj);
341  Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) );
342  }
343  // quit if the last frame
344  if ( f == nFramesMax - 1 )
345  break;
346  // transfer to register outputs
347  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
348  {
349  pObjLo->pData = pObjLi->pData;
350  if ( !fInit )
351  Saig_ManSetMap1( pAig, pObjLo, f+1, Aig_Regular((Aig_Obj_t *)pObjLo->pData) );
352  }
353  }
354  if ( !fInit )
355  {
356  // create registers
357  Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
358  Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObjLi->pData );
359  // set register number
360  Aig_ManSetRegNum( pFrames, pAig->nRegs );
361  }
362  Aig_ManCleanup( pFrames );
363  Saig_ManStopMap1( pAig );
364  return pFrames;
365 }
366 
367 /**Function*************************************************************
368 
369  Synopsis [Implements dynamic simplification.]
370 
371  Description []
372 
373  SideEffects []
374 
375  SeeAlso []
376 
377 ***********************************************************************/
378 Aig_Man_t * Saig_ManTimeframeSimplify( Aig_Man_t * pAig, int nFrames, int nFramesMax, int fInit, int fVerbose )
379 {
380 // extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
381  Aig_Man_t * pFrames, * pFraig, * pRes1, * pRes2;
382  abctime clk;
383  // create uninitialized timeframes with map1
384  pFrames = Saig_ManFramesNonInitial( pAig, nFrames );
385  // perform fraiging for the unrolled timeframes
386 clk = Abc_Clock();
387  pFraig = Fra_FraigEquivence( pFrames, 1000, 0 );
388  // report the results
389  if ( fVerbose )
390  {
391  Aig_ManPrintStats( pFrames );
392  Aig_ManPrintStats( pFraig );
393 ABC_PRT( "Fraiging", Abc_Clock() - clk );
394  }
395  Aig_ManStop( pFraig );
396  assert( pFrames->pReprs != NULL );
397  // create AIG with map2
398  Saig_ManCreateMapping( pAig, pFrames, nFrames );
399  Aig_ManStop( pFrames );
400  Saig_ManStopMap1( pAig );
401  // create reduced initialized timeframes
402 clk = Abc_Clock();
403  pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
404 ABC_PRT( "Mapped", Abc_Clock() - clk );
405  // free mapping
406  Saig_ManStopMap2( pAig );
407 clk = Abc_Clock();
408  pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
409 ABC_PRT( "Normal", Abc_Clock() - clk );
410  // report the results
411  if ( fVerbose )
412  {
413  Aig_ManPrintStats( pRes1 );
414  Aig_ManPrintStats( pRes2 );
415  }
416  Aig_ManStop( pRes1 );
417  assert( !Saig_ManHasMap1(pAig) );
418  assert( !Saig_ManHasMap2(pAig) );
419  return pRes2;
420 }
421 
422 ////////////////////////////////////////////////////////////////////////
423 /// END OF FILE ///
424 ////////////////////////////////////////////////////////////////////////
425 
426 
428 
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
static Aig_Obj_t * Aig_ObjRepr(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:330
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Aig_Man_t * Fra_FraigEquivence(Aig_Man_t *pManAig, int nConfMax, int fProve)
Definition: fraCore.c:468
void * pData
Definition: aig.h:87
static int Saig_ManHasMap2(Aig_Man_t *p)
Definition: saigTrans.c:116
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
void Aig_ManPrintStats(Aig_Man_t *p)
Definition: aigMan.c:379
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Saig_ManHasMap1(Aig_Man_t *p)
Definition: saigTrans.c:69
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static void Saig_ManStartMap2(Aig_Man_t *p, int nFrames)
Definition: saigTrans.c:99
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Saig_ManGetMap2(Aig_Man_t *p, Aig_Obj_t *pOld, int f1, int *pf2)
Definition: saigTrans.c:129
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Aig_Man_t * Saig_ManTimeframeSimplify(Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit, int fVerbose)
Definition: saigTrans.c:378
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
Definition: aig.h:69
static void Saig_ManSetMap1(Aig_Man_t *p, Aig_Obj_t *pOld, int f1, Aig_Obj_t *pNew)
Definition: saigTrans.c:73
Aig_Man_t * Saig_ManFramesInitialMapped(Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit)
Definition: saigTrans.c:256
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static void Saig_ManSetMap2(Aig_Man_t *p, Aig_Obj_t *pOld, int f1, Aig_Obj_t *pNew, int f2)
Definition: saigTrans.c:120
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
unsigned int fPhase
Definition: aig.h:78
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Aig_Man_t * Saig_ManFramesNonInitial(Aig_Man_t *pAig, int nFrames)
Definition: saigTrans.c:195
void Saig_ManCreateMapping(Aig_Man_t *pAig, Aig_Man_t *pFrames, int nFrames)
Definition: saigTrans.c:148
#define ABC_PRT(a, t)
Definition: abc_global.h:220
static void Saig_ManStopMap2(Aig_Man_t *p)
Definition: saigTrans.c:110
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
ABC_INT64_T abctime
Definition: abc_global.h:278
static int Saig_ManGetMap1(Aig_Man_t *p, Aig_Obj_t *pOld, int f1)
Definition: saigTrans.c:81
int Id
Definition: aig.h:85
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
static void Saig_ManStopMap1(Aig_Man_t *p)
Definition: saigTrans.c:63
static ABC_NAMESPACE_IMPL_START void Saig_ManStartMap1(Aig_Man_t *p, int nFrames)
DECLARATIONS ///.
Definition: saigTrans.c:52
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91