ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
saigTrans.c File Reference
#include "saig.h"
#include "proof/fra/fra.h"
Include dependency graph for saigTrans.c:

Go to the source code of this file.

Functions

void Saig_ManCreateMapping (Aig_Man_t *pAig, Aig_Man_t *pFrames, int nFrames)
 
Aig_Man_t * Saig_ManFramesNonInitial (Aig_Man_t *pAig, int nFrames)
 
Aig_Man_t * Saig_ManFramesInitialMapped (Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit)
 
Aig_Man_t * Saig_ManTimeframeSimplify (Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit, int fVerbose)
 

Function Documentation

◆ Saig_ManCreateMapping()

void Saig_ManCreateMapping ( Aig_Man_t * pAig,
Aig_Man_t * pFrames,
int nFrames )

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

Synopsis [Create mapping for the first nFrames timeframes of pAig.]

Description []

SideEffects []

SeeAlso []

Definition at line 148 of file saigTrans.c.

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}
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
assert
#define assert(ex)
Definition util_old.h:213
Here is the caller graph for this function:

◆ Saig_ManFramesInitialMapped()

Aig_Man_t * Saig_ManFramesInitialMapped ( Aig_Man_t * pAig,
int nFrames,
int nFramesMax,
int fInit )

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

Synopsis [Unroll with initialization and mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 256 of file saigTrans.c.

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}
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition aigMan.c:438
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition aigMan.c:265
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManFramesNonInitial()

Aig_Man_t * Saig_ManFramesNonInitial ( Aig_Man_t * pAig,
int nFrames )

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

Synopsis [Unroll without initialization.]

Description []

SideEffects []

SeeAlso []

Definition at line 195 of file saigTrans.c.

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}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManTimeframeSimplify()

Aig_Man_t * Saig_ManTimeframeSimplify ( Aig_Man_t * pAig,
int nFrames,
int nFramesMax,
int fInit,
int fVerbose )

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

Synopsis [Implements dynamic simplification.]

Description []

SideEffects []

SeeAlso []

Definition at line 378 of file saigTrans.c.

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
386clk = 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 );
393ABC_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
402clk = Abc_Clock();
403 pRes2 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
404ABC_PRT( "Mapped", Abc_Clock() - clk );
405 // free mapping
406 Saig_ManStopMap2( pAig );
407clk = Abc_Clock();
408 pRes1 = Saig_ManFramesInitialMapped( pAig, nFrames, nFramesMax, fInit );
409ABC_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}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition aigMan.c:379
Fra_FraigEquivence
Aig_Man_t * Fra_FraigEquivence(Aig_Man_t *pManAig, int nConfMax, int fProve)
Definition fraCore.c:468
Saig_ManCreateMapping
void Saig_ManCreateMapping(Aig_Man_t *pAig, Aig_Man_t *pFrames, int nFrames)
Definition saigTrans.c:148
Saig_ManFramesInitialMapped
Aig_Man_t * Saig_ManFramesInitialMapped(Aig_Man_t *pAig, int nFrames, int nFramesMax, int fInit)
Definition saigTrans.c:256
Saig_ManFramesNonInitial
Aig_Man_t * Saig_ManFramesNonInitial(Aig_Man_t *pAig, int nFrames)
Definition saigTrans.c:195
Here is the call graph for this function:
Here is the caller graph for this function: