1 /**CFile****************************************************************
2
3 FileName [intFrames.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Interpolation engine.]
8
9 Synopsis [Sequential AIG unrolling for interpolation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 24, 2008.]
16
17 Revision [$Id: intFrames.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "intInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Create timeframes of the manager for interpolation.]
37
38 Description [The resulting manager is combinational. The primary inputs
39 corresponding to register outputs are ordered first. The only POs of the
40 manager is the property output of the last timeframe.]
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
Inter_ManFramesInter(Aig_Man_t * pAig,int nFrames,int fAddRegOuts,int fUseTwoFrames)47 Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts, int fUseTwoFrames )
48 {
49 Aig_Man_t * pFrames;
50 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
51 Aig_Obj_t * pLastPo = NULL;
52 int i, f;
53 assert( Saig_ManRegNum(pAig) > 0 );
54 assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
55 pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
56 // map the constant node
57 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
58 // create variables for register outputs
59 if ( fAddRegOuts )
60 {
61 Saig_ManForEachLo( pAig, pObj, i )
62 pObj->pData = Aig_ManConst0( pFrames );
63 }
64 else
65 {
66 Saig_ManForEachLo( pAig, pObj, i )
67 pObj->pData = Aig_ObjCreateCi( pFrames );
68 }
69 // add timeframes
70 for ( f = 0; f < nFrames; f++ )
71 {
72 // create PI nodes for this frame
73 Saig_ManForEachPi( pAig, pObj, i )
74 pObj->pData = Aig_ObjCreateCi( pFrames );
75 // add internal nodes of this frame
76 Aig_ManForEachNode( pAig, pObj, i )
77 pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
78 // add outputs for constraints
79 Saig_ManForEachPo( pAig, pObj, i )
80 {
81 if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
82 continue;
83 Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
84 }
85 if ( f == nFrames - 1 )
86 break;
87 // remember the last PO
88 pObj = Aig_ManCo( pAig, 0 );
89 pLastPo = Aig_ObjChild0Copy(pObj);
90 // save register inputs
91 Saig_ManForEachLi( pAig, pObj, i )
92 pObj->pData = Aig_ObjChild0Copy(pObj);
93 // transfer to register outputs
94 Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
95 pObjLo->pData = pObjLi->pData;
96 }
97 // create POs for each register output
98 if ( fAddRegOuts )
99 {
100 Saig_ManForEachLi( pAig, pObj, i )
101 Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
102 }
103 // create the only PO of the manager
104 else
105 {
106 pObj = Aig_ManCo( pAig, 0 );
107 // add the last PO
108 if ( pLastPo == NULL || !fUseTwoFrames )
109 pLastPo = Aig_ObjChild0Copy(pObj);
110 else
111 pLastPo = Aig_Or( pFrames, pLastPo, Aig_ObjChild0Copy(pObj) );
112 Aig_ObjCreateCo( pFrames, pLastPo );
113 }
114 Aig_ManCleanup( pFrames );
115 return pFrames;
116 }
117
118 ////////////////////////////////////////////////////////////////////////
119 /// END OF FILE ///
120 ////////////////////////////////////////////////////////////////////////
121
122
123 ABC_NAMESPACE_IMPL_END
124
125