1 /**CFile****************************************************************
2
3 FileName [retInit.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Retiming package.]
8
9 Synopsis [Initial state computation for backward retiming.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - Oct 31, 2006.]
16
17 Revision [$Id: retInit.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "retInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 static int Abc_NtkRetimeVerifyModel( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int * pModel );
31
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 /**Function*************************************************************
37
38 Synopsis [Computes initial values of the new latches.]
39
40 Description []
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
Abc_NtkRetimeInitialValues(Abc_Ntk_t * pNtkCone,Vec_Int_t * vValues,int fVerbose)47 Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int fVerbose )
48 {
49 Vec_Int_t * vSolution;
50 Abc_Ntk_t * pNtkMiter, * pNtkLogic;
51 int RetValue;
52 abctime clk;
53 if ( pNtkCone == NULL )
54 return Vec_IntDup( vValues );
55 // convert the target network to AIG
56 pNtkLogic = Abc_NtkDup( pNtkCone );
57 Abc_NtkToAig( pNtkLogic );
58 // get the miter
59 pNtkMiter = Abc_NtkCreateTarget( pNtkLogic, pNtkLogic->vCos, vValues );
60 if ( fVerbose )
61 printf( "The miter for initial state computation has %d AIG nodes. ", Abc_NtkNodeNum(pNtkMiter) );
62 // solve the miter
63 clk = Abc_Clock();
64 RetValue = Abc_NtkMiterSat( pNtkMiter, (ABC_INT64_T)500000, (ABC_INT64_T)50000000, 0, NULL, NULL );
65 if ( fVerbose )
66 { ABC_PRT( "SAT solving time", Abc_Clock() - clk ); }
67 // analyze the result
68 if ( RetValue == 1 )
69 printf( "Abc_NtkRetimeInitialValues(): The problem is unsatisfiable. DC latch values are used.\n" );
70 else if ( RetValue == -1 )
71 printf( "Abc_NtkRetimeInitialValues(): The SAT problem timed out. DC latch values are used.\n" );
72 else if ( !Abc_NtkRetimeVerifyModel( pNtkCone, vValues, pNtkMiter->pModel ) )
73 printf( "Abc_NtkRetimeInitialValues(): The computed counter-example is incorrect.\n" );
74 // set the values of the latches
75 vSolution = RetValue? NULL : Vec_IntAllocArray( pNtkMiter->pModel, Abc_NtkPiNum(pNtkLogic) );
76 pNtkMiter->pModel = NULL;
77 Abc_NtkDelete( pNtkMiter );
78 Abc_NtkDelete( pNtkLogic );
79 return vSolution;
80 }
81
82 /**Function*************************************************************
83
84 Synopsis [Computes the results of simulating one node.]
85
86 Description [Assumes that fanins have pCopy set to the input values.]
87
88 SideEffects []
89
90 SeeAlso []
91
92 ***********************************************************************/
Abc_ObjSopSimulate(Abc_Obj_t * pObj)93 int Abc_ObjSopSimulate( Abc_Obj_t * pObj )
94 {
95 char * pCube, * pSop = (char *)pObj->pData;
96 int nVars, Value, v, ResOr, ResAnd, ResVar;
97 assert( pSop && !Abc_SopIsExorType(pSop) );
98 // simulate the SOP of the node
99 ResOr = 0;
100 nVars = Abc_SopGetVarNum(pSop);
101 Abc_SopForEachCube( pSop, nVars, pCube )
102 {
103 ResAnd = 1;
104 Abc_CubeForEachVar( pCube, Value, v )
105 {
106 if ( Value == '0' )
107 ResVar = 1 ^ ((int)(ABC_PTRUINT_T)Abc_ObjFanin(pObj, v)->pCopy);
108 else if ( Value == '1' )
109 ResVar = (int)(ABC_PTRUINT_T)Abc_ObjFanin(pObj, v)->pCopy;
110 else
111 continue;
112 ResAnd &= ResVar;
113 }
114 ResOr |= ResAnd;
115 }
116 // complement the result if necessary
117 if ( !Abc_SopGetPhase(pSop) )
118 ResOr ^= 1;
119 return ResOr;
120 }
121
122 /**Function*************************************************************
123
124 Synopsis [Verifies the counter-example.]
125
126 Description []
127
128 SideEffects []
129
130 SeeAlso []
131
132 ***********************************************************************/
Abc_NtkRetimeVerifyModel(Abc_Ntk_t * pNtkCone,Vec_Int_t * vValues,int * pModel)133 int Abc_NtkRetimeVerifyModel( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int * pModel )
134 {
135 Vec_Ptr_t * vNodes;
136 Abc_Obj_t * pObj;
137 int i, Counter = 0;
138 assert( Abc_NtkIsSopLogic(pNtkCone) );
139 // set the PIs
140 Abc_NtkForEachPi( pNtkCone, pObj, i )
141 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)pModel[i];
142 // simulate the internal nodes
143 vNodes = Abc_NtkDfs( pNtkCone, 0 );
144 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
145 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)Abc_ObjSopSimulate( pObj );
146 Vec_PtrFree( vNodes );
147 // compare the outputs
148 Abc_NtkForEachPo( pNtkCone, pObj, i )
149 pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
150 Abc_NtkForEachPo( pNtkCone, pObj, i )
151 Counter += (Vec_IntEntry(vValues, i) != (int)(ABC_PTRUINT_T)pObj->pCopy);
152 if ( Counter > 0 )
153 printf( "%d outputs (out of %d) have a value mismatch.\n", Counter, Abc_NtkPoNum(pNtkCone) );
154 return 1;
155 }
156
157 /**Function*************************************************************
158
159 Synopsis [Transfer latch initial values to pCopy.]
160
161 Description []
162
163 SideEffects []
164
165 SeeAlso []
166
167 ***********************************************************************/
Abc_NtkRetimeTranferToCopy(Abc_Ntk_t * pNtk)168 void Abc_NtkRetimeTranferToCopy( Abc_Ntk_t * pNtk )
169 {
170 Abc_Obj_t * pObj;
171 int i;
172 Abc_NtkForEachObj( pNtk, pObj, i )
173 if ( Abc_ObjIsLatch(pObj) )
174 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)Abc_LatchIsInit1(pObj);
175 }
176
177 /**Function*************************************************************
178
179 Synopsis [Transfer latch initial values from pCopy.]
180
181 Description []
182
183 SideEffects []
184
185 SeeAlso []
186
187 ***********************************************************************/
Abc_NtkRetimeTranferFromCopy(Abc_Ntk_t * pNtk)188 void Abc_NtkRetimeTranferFromCopy( Abc_Ntk_t * pNtk )
189 {
190 Abc_Obj_t * pObj;
191 int i;
192 Abc_NtkForEachObj( pNtk, pObj, i )
193 if ( Abc_ObjIsLatch(pObj) )
194 pObj->pData = (void *)(ABC_PTRUINT_T)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO);
195 }
196
197 /**Function*************************************************************
198
199 Synopsis [Transfer latch initial values to pCopy.]
200
201 Description []
202
203 SideEffects []
204
205 SeeAlso []
206
207 ***********************************************************************/
Abc_NtkRetimeCollectLatchValues(Abc_Ntk_t * pNtk)208 Vec_Int_t * Abc_NtkRetimeCollectLatchValues( Abc_Ntk_t * pNtk )
209 {
210 Vec_Int_t * vValues;
211 Abc_Obj_t * pObj;
212 int i;
213 vValues = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) );
214 Abc_NtkForEachObj( pNtk, pObj, i )
215 if ( Abc_ObjIsLatch(pObj) )
216 Vec_IntPush( vValues, Abc_LatchIsInit1(pObj) );
217 return vValues;
218 }
219
220 /**Function*************************************************************
221
222 Synopsis [Transfer latch initial values from pCopy.]
223
224 Description []
225
226 SideEffects []
227
228 SeeAlso []
229
230 ***********************************************************************/
Abc_NtkRetimeInsertLatchValues(Abc_Ntk_t * pNtk,Vec_Int_t * vValues)231 void Abc_NtkRetimeInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues )
232 {
233 Abc_Obj_t * pObj;
234 int i, Counter = 0;
235 Abc_NtkForEachObj( pNtk, pObj, i )
236 if ( Abc_ObjIsLatch(pObj) )
237 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)Counter++;
238 Abc_NtkForEachObj( pNtk, pObj, i )
239 if ( Abc_ObjIsLatch(pObj) )
240 pObj->pData = (Abc_Obj_t *)(ABC_PTRUINT_T)(vValues? (Vec_IntEntry(vValues,(int)(ABC_PTRUINT_T)pObj->pCopy)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC);
241 }
242
243 /**Function*************************************************************
244
245 Synopsis [Transfer latch initial values to pCopy.]
246
247 Description []
248
249 SideEffects []
250
251 SeeAlso []
252
253 ***********************************************************************/
Abc_NtkRetimeBackwardInitialStart(Abc_Ntk_t * pNtk)254 Abc_Ntk_t * Abc_NtkRetimeBackwardInitialStart( Abc_Ntk_t * pNtk )
255 {
256 Abc_Ntk_t * pNtkNew;
257 Abc_Obj_t * pObj;
258 int i;
259 // create the network used for the initial state computation
260 pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
261 // create POs corresponding to the initial values
262 Abc_NtkForEachObj( pNtk, pObj, i )
263 if ( Abc_ObjIsLatch(pObj) )
264 pObj->pCopy = Abc_NtkCreatePo(pNtkNew);
265 return pNtkNew;
266 }
267
268 /**Function*************************************************************
269
270 Synopsis [Transfer latch initial values to pCopy.]
271
272 Description []
273
274 SideEffects []
275
276 SeeAlso []
277
278 ***********************************************************************/
Abc_NtkRetimeBackwardInitialFinish(Abc_Ntk_t * pNtk,Abc_Ntk_t * pNtkNew,Vec_Int_t * vValuesOld,int fVerbose)279 void Abc_NtkRetimeBackwardInitialFinish( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, Vec_Int_t * vValuesOld, int fVerbose )
280 {
281 Vec_Int_t * vValuesNew;
282 Abc_Obj_t * pObj;
283 int i;
284 // create PIs corresponding to the initial values
285 Abc_NtkForEachObj( pNtk, pObj, i )
286 if ( Abc_ObjIsLatch(pObj) )
287 Abc_ObjAddFanin( pObj->pCopy, Abc_NtkCreatePi(pNtkNew) );
288 // assign dummy node names
289 Abc_NtkAddDummyPiNames( pNtkNew );
290 Abc_NtkAddDummyPoNames( pNtkNew );
291 // check the network
292 if ( !Abc_NtkCheck( pNtkNew ) )
293 fprintf( stdout, "Abc_NtkRetimeBackwardInitialFinish(): Network check has failed.\n" );
294 // derive new initial values
295 vValuesNew = Abc_NtkRetimeInitialValues( pNtkNew, vValuesOld, fVerbose );
296 // insert new initial values
297 Abc_NtkRetimeInsertLatchValues( pNtk, vValuesNew );
298 if ( vValuesNew ) Vec_IntFree( vValuesNew );
299 }
300
301
302 /**Function*************************************************************
303
304 Synopsis [Cycles the circuit to create a new initial state.]
305
306 Description [Simulates the circuit with random input for the given
307 number of timeframes to get a better initial state.]
308
309 SideEffects []
310
311 SeeAlso []
312
313 ***********************************************************************/
Abc_NtkCycleInitStateSop(Abc_Ntk_t * pNtk,int nFrames,int fVerbose)314 void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
315 {
316 Vec_Ptr_t * vNodes;
317 Abc_Obj_t * pObj;
318 int i, f;
319 assert( Abc_NtkIsSopLogic(pNtk) );
320 srand( 0x12341234 );
321 // initialize the values
322 Abc_NtkForEachPi( pNtk, pObj, i )
323 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)(rand() & 1);
324 Abc_NtkForEachLatch( pNtk, pObj, i )
325 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)Abc_LatchIsInit1(pObj);
326 // simulate for the given number of timeframes
327 vNodes = Abc_NtkDfs( pNtk, 0 );
328 for ( f = 0; f < nFrames; f++ )
329 {
330 // simulate internal nodes
331 Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
332 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)Abc_ObjSopSimulate( pObj );
333 // bring the results to the COs
334 Abc_NtkForEachCo( pNtk, pObj, i )
335 pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy;
336 // assign PI values
337 Abc_NtkForEachPi( pNtk, pObj, i )
338 pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)(rand() & 1);
339 // transfer the latch values
340 Abc_NtkForEachLatch( pNtk, pObj, i )
341 Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
342 }
343 Vec_PtrFree( vNodes );
344 // set the final values
345 Abc_NtkForEachLatch( pNtk, pObj, i )
346 pObj->pData = (void *)(ABC_PTRUINT_T)(Abc_ObjFanout0(pObj)->pCopy ? ABC_INIT_ONE : ABC_INIT_ZERO);
347 }
348
349 ////////////////////////////////////////////////////////////////////////
350 /// END OF FILE ///
351 ////////////////////////////////////////////////////////////////////////
352
353
354 ABC_NAMESPACE_IMPL_END
355
356