1 /**CFile****************************************************************
2
3 FileName [saigTempor.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Sequential AIG package.]
8
9 Synopsis [Temporal decomposition.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: saigTempor.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "saig.h"
22 #include "sat/bmc/bmc.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis [Creates initialized timeframes for temporal decomposition.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Saig_ManTemporFrames(Aig_Man_t * pAig,int nFrames)46 Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames )
47 {
48 Aig_Man_t * pFrames;
49 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
50 int i, f;
51 // start the frames package
52 Aig_ManCleanData( pAig );
53 pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames );
54 pFrames->pName = Abc_UtilStrsav( pAig->pName );
55 // initiliaze the flops
56 Saig_ManForEachLo( pAig, pObj, i )
57 pObj->pData = Aig_ManConst0(pFrames);
58 // for each timeframe
59 for ( f = 0; f < nFrames; f++ )
60 {
61 Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames);
62 Saig_ManForEachPi( pAig, pObj, i )
63 pObj->pData = Aig_ObjCreateCi(pFrames);
64 Aig_ManForEachNode( pAig, pObj, i )
65 pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
66 Aig_ManForEachCo( pAig, pObj, i )
67 pObj->pData = Aig_ObjChild0Copy(pObj);
68 Saig_ManForEachLiLo( pAig, pObjLi, pObjLo, i )
69 pObjLo->pData = pObjLi->pData;
70 }
71 // create POs for the flop inputs
72 Saig_ManForEachLi( pAig, pObj, i )
73 Aig_ObjCreateCo( pFrames, (Aig_Obj_t *)pObj->pData );
74 Aig_ManCleanup( pFrames );
75 return pFrames;
76 }
77
78
79 /**Function*************************************************************
80
81 Synopsis []
82
83 Description []
84
85 SideEffects []
86
87 SeeAlso []
88
89 ***********************************************************************/
Saig_ManTemporDecompose(Aig_Man_t * pAig,int nFrames)90 Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
91 {
92 Aig_Man_t * pAigNew, * pFrames;
93 Aig_Obj_t * pObj, * pReset;
94 int i;
95 if ( pAig->nConstrs > 0 )
96 {
97 printf( "The AIG manager should have no constraints.\n" );
98 return NULL;
99 }
100 // create initialized timeframes
101 pFrames = Saig_ManTemporFrames( pAig, nFrames );
102 assert( Aig_ManCoNum(pFrames) == Aig_ManRegNum(pAig) );
103
104 // start the new manager
105 Aig_ManCleanData( pAig );
106 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
107 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
108 // map the constant node and primary inputs
109 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
110 Saig_ManForEachPi( pAig, pObj, i )
111 pObj->pData = Aig_ObjCreateCi( pAigNew );
112
113 // insert initialization logic
114 Aig_ManConst1(pFrames)->pData = Aig_ManConst1( pAigNew );
115 Aig_ManForEachCi( pFrames, pObj, i )
116 pObj->pData = Aig_ObjCreateCi( pAigNew );
117 Aig_ManForEachNode( pFrames, pObj, i )
118 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
119 Aig_ManForEachCo( pFrames, pObj, i )
120 pObj->pData = Aig_ObjChild0Copy(pObj);
121
122 // create reset latch (the first one among the latches)
123 pReset = Aig_ObjCreateCi( pAigNew );
124
125 // create flop output values
126 Saig_ManForEachLo( pAig, pObj, i )
127 pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreateCi(pAigNew), (Aig_Obj_t *)Aig_ManCo(pFrames, i)->pData );
128 Aig_ManStop( pFrames );
129
130 // add internal nodes of this frame
131 Aig_ManForEachNode( pAig, pObj, i )
132 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
133 // create primary outputs
134 Saig_ManForEachPo( pAig, pObj, i )
135 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
136
137 // create reset latch (the first one among the latches)
138 Aig_ObjCreateCo( pAigNew, Aig_ManConst1(pAigNew) );
139 // create latch inputs
140 Saig_ManForEachLi( pAig, pObj, i )
141 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
142
143 // finalize
144 Aig_ManCleanup( pAigNew );
145 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig)+1 ); // + reset latch (011111...)
146 return pAigNew;
147 }
148
149 /**Function*************************************************************
150
151 Synopsis [Find index of first non-zero entry.]
152
153 Description []
154
155 SideEffects []
156
157 SeeAlso []
158
159 ***********************************************************************/
Vec_IntLastNonZeroBeforeLimit(Vec_Int_t * vTemp,int Limit)160 int Vec_IntLastNonZeroBeforeLimit( Vec_Int_t * vTemp, int Limit )
161 {
162 int Entry, i;
163 if ( vTemp == NULL )
164 return -1;
165 Vec_IntForEachEntryReverse( vTemp, Entry, i )
166 {
167 if ( i >= Limit )
168 continue;
169 if ( Entry )
170 return i;
171 }
172 return -1;
173 }
174
175 /**Function*************************************************************
176
177 Synopsis []
178
179 Description []
180
181 SideEffects []
182
183 SeeAlso []
184
185 ***********************************************************************/
Saig_ManTempor(Aig_Man_t * pAig,int nFrames,int TimeOut,int nConfLimit,int fUseBmc,int fUseTransSigs,int fVerbose,int fVeryVerbose)186 Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
187 {
188 extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans );
189
190 Vec_Int_t * vTransSigs = NULL;
191 int RetValue, nFramesFinished = -1;
192 assert( nFrames >= 0 );
193 if ( nFrames == 0 )
194 {
195 nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose, &vTransSigs );
196 if ( nFrames == 0 )
197 {
198 Vec_IntFreeP( &vTransSigs );
199 printf( "The leading sequence has length 0. Temporal decomposition is not performed.\n" );
200 return NULL;
201 }
202 if ( nFrames == 1 )
203 {
204 Vec_IntFreeP( &vTransSigs );
205 printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" );
206 return NULL;
207 }
208 if ( fUseTransSigs )
209 {
210 int Entry, i, iLast = -1;
211 Vec_IntForEachEntry( vTransSigs, Entry, i )
212 iLast = Entry ? i :iLast;
213 if ( iLast > 0 && iLast < nFrames )
214 {
215 Abc_Print( 1, "Reducing frame count from %d to %d to fit the last transient.\n", nFrames, iLast );
216 nFrames = iLast;
217 }
218 }
219 Abc_Print( 1, "Using computed frame number (%d).\n", nFrames );
220 }
221 else
222 Abc_Print( 1, "Using user-given frame number (%d).\n", nFrames );
223 // run BMC2
224 if ( fUseBmc )
225 {
226 RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0, 0 );
227 if ( RetValue == 0 )
228 {
229 Vec_IntFreeP( &vTransSigs );
230 printf( "A cex found in the first %d frames.\n", nFrames );
231 return NULL;
232 }
233 if ( nFramesFinished + 1 < nFrames )
234 {
235 int iLastBefore = Vec_IntLastNonZeroBeforeLimit( vTransSigs, nFramesFinished );
236 if ( iLastBefore < 1 || !fUseTransSigs )
237 {
238 Vec_IntFreeP( &vTransSigs );
239 printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
240 return NULL;
241 }
242 assert( iLastBefore < nFramesFinished );
243 printf( "BMC succeeded to frame %d. Adjusting frame count to be (%d) based on the last transient signal.\n", nFramesFinished, iLastBefore );
244 nFrames = iLastBefore;
245 }
246 }
247 Vec_IntFreeP( &vTransSigs );
248 return Saig_ManTemporDecompose( pAig, nFrames );
249 }
250
251 ////////////////////////////////////////////////////////////////////////
252 /// END OF FILE ///
253 ////////////////////////////////////////////////////////////////////////
254
255 ABC_NAMESPACE_IMPL_END
256
257