1 /**CFile****************************************************************
2
3 FileName [fraMan.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis [Starts the FRAIG manager.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraMan.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.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 [Sets the default solving parameters.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Fra_ParamsDefault(Fra_Par_t * pPars)45 void Fra_ParamsDefault( Fra_Par_t * pPars )
46 {
47 memset( pPars, 0, sizeof(Fra_Par_t) );
48 pPars->nSimWords = 32; // the number of words in the simulation info
49 pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
50 pPars->fPatScores = 0; // enables simulation pattern scoring
51 pPars->MaxScore = 25; // max score after which resimulation is used
52 pPars->fDoSparse = 1; // skips sparse functions
53 // pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped
54 // pPars->dActConeBumpMax = 5.0; // the largest bump of activity
55 pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
56 pPars->dActConeBumpMax = 10.0; // the largest bump of activity
57 pPars->nBTLimitNode = 100; // conflict limit at a node
58 pPars->nBTLimitMiter = 500000; // conflict limit at an output
59 pPars->nFramesK = 0; // the number of timeframes to unroll
60 pPars->fConeBias = 1;
61 pPars->fRewrite = 0;
62 }
63
64 /**Function*************************************************************
65
66 Synopsis [Sets the default solving parameters.]
67
68 Description []
69
70 SideEffects []
71
72 SeeAlso []
73
74 ***********************************************************************/
Fra_ParamsDefaultSeq(Fra_Par_t * pPars)75 void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
76 {
77 memset( pPars, 0, sizeof(Fra_Par_t) );
78 pPars->nSimWords = 1; // the number of words in the simulation info
79 pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached
80 pPars->fPatScores = 0; // enables simulation pattern scoring
81 pPars->MaxScore = 25; // max score after which resimulation is used
82 pPars->fDoSparse = 1; // skips sparse functions
83 pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped
84 pPars->dActConeBumpMax = 10.0; // the largest bump of activity
85 pPars->nBTLimitNode = 10000000; // conflict limit at a node
86 pPars->nBTLimitMiter = 500000; // conflict limit at an output
87 pPars->nFramesK = 1; // the number of timeframes to unroll
88 pPars->fConeBias = 0;
89 pPars->fRewrite = 0;
90 pPars->fLatchCorr = 0;
91 }
92
93 /**Function*************************************************************
94
95 Synopsis [Starts the fraiging manager.]
96
97 Description []
98
99 SideEffects []
100
101 SeeAlso []
102
103 ***********************************************************************/
Fra_ManStart(Aig_Man_t * pManAig,Fra_Par_t * pPars)104 Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
105 {
106 Fra_Man_t * p;
107 Aig_Obj_t * pObj;
108 int i;
109 // allocate the fraiging manager
110 p = ABC_ALLOC( Fra_Man_t, 1 );
111 memset( p, 0, sizeof(Fra_Man_t) );
112 p->pPars = pPars;
113 p->pManAig = pManAig;
114 p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
115 p->nFramesAll = pPars->nFramesK + 1;
116 // allocate storage for sim pattern
117 p->nPatWords = Abc_BitWordNum( (Aig_ManCiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
118 p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords );
119 p->vPiVars = Vec_PtrAlloc( 100 );
120 // equivalence classes
121 p->pCla = Fra_ClassesStart( pManAig );
122 // allocate other members
123 p->pMemFraig = ABC_ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
124 memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
125 // set random number generator
126 // srand( 0xABCABC );
127 Aig_ManRandom(1);
128 // set the pointer to the manager
129 Aig_ManForEachObj( p->pManAig, pObj, i )
130 pObj->pData = p;
131 return p;
132 }
133
134 /**Function*************************************************************
135
136 Synopsis [Starts the fraiging manager.]
137
138 Description []
139
140 SideEffects []
141
142 SeeAlso []
143
144 ***********************************************************************/
Fra_ManClean(Fra_Man_t * p,int nNodesMax)145 void Fra_ManClean( Fra_Man_t * p, int nNodesMax )
146 {
147 int i;
148 // remove old arrays
149 for ( i = 0; i < p->nMemAlloc; i++ )
150 if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
151 Vec_PtrFree( p->pMemFanins[i] );
152 // realloc for the new size
153 if ( p->nMemAlloc < nNodesMax )
154 {
155 int nMemAllocNew = nNodesMax + 5000;
156 p->pMemFanins = ABC_REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
157 p->pMemSatNums = ABC_REALLOC( int, p->pMemSatNums, nMemAllocNew );
158 p->nMemAlloc = nMemAllocNew;
159 }
160 // prepare for the new run
161 memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
162 memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
163 }
164
165 /**Function*************************************************************
166
167 Synopsis [Prepares the new manager to begin fraiging.]
168
169 Description []
170
171 SideEffects []
172
173 SeeAlso []
174
175 ***********************************************************************/
Fra_ManPrepareComb(Fra_Man_t * p)176 Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
177 {
178 Aig_Man_t * pManFraig;
179 Aig_Obj_t * pObj;
180 int i;
181 assert( p->pManFraig == NULL );
182 // start the fraig package
183 pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
184 pManFraig->pName = Abc_UtilStrsav( p->pManAig->pName );
185 pManFraig->pSpec = Abc_UtilStrsav( p->pManAig->pSpec );
186 pManFraig->nRegs = p->pManAig->nRegs;
187 pManFraig->nAsserts = p->pManAig->nAsserts;
188 // set the pointers to the available fraig nodes
189 Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
190 Aig_ManForEachCi( p->pManAig, pObj, i )
191 Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
192 // set the pointers to the manager
193 Aig_ManForEachObj( pManFraig, pObj, i )
194 pObj->pData = p;
195 // allocate memory for mapping FRAIG nodes into SAT numbers and fanins
196 p->nMemAlloc = p->nSizeAlloc;
197 p->pMemFanins = ABC_ALLOC( Vec_Ptr_t *, p->nMemAlloc );
198 memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
199 p->pMemSatNums = ABC_ALLOC( int, p->nMemAlloc );
200 memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
201 // make sure the satisfying assignment is node assigned
202 assert( pManFraig->pData == NULL );
203 return pManFraig;
204 }
205
206 /**Function*************************************************************
207
208 Synopsis [Finalizes the combinational miter after fraiging.]
209
210 Description []
211
212 SideEffects []
213
214 SeeAlso []
215
216 ***********************************************************************/
Fra_ManFinalizeComb(Fra_Man_t * p)217 void Fra_ManFinalizeComb( Fra_Man_t * p )
218 {
219 Aig_Obj_t * pObj;
220 int i;
221 // add the POs
222 Aig_ManForEachCo( p->pManAig, pObj, i )
223 Aig_ObjCreateCo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) );
224 // postprocess
225 Aig_ManCleanMarkB( p->pManFraig );
226 }
227
228
229 /**Function*************************************************************
230
231 Synopsis [Stops the fraiging manager.]
232
233 Description []
234
235 SideEffects []
236
237 SeeAlso []
238
239 ***********************************************************************/
Fra_ManStop(Fra_Man_t * p)240 void Fra_ManStop( Fra_Man_t * p )
241 {
242 if ( p->pPars->fVerbose )
243 Fra_ManPrint( p );
244 // save mapping from original nodes into FRAIG nodes
245 if ( p->pManAig )
246 {
247 if ( p->pManAig->pObjCopies )
248 ABC_FREE( p->pManAig->pObjCopies );
249 p->pManAig->pObjCopies = p->pMemFraig;
250 p->pMemFraig = NULL;
251 }
252 Fra_ManClean( p, 0 );
253 if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
254 if ( p->vPiVars ) Vec_PtrFree( p->vPiVars );
255 if ( p->pSat ) sat_solver_delete( p->pSat );
256 if ( p->pCla ) Fra_ClassesStop( p->pCla );
257 if ( p->pSml ) Fra_SmlStop( p->pSml );
258 if ( p->vCex ) Vec_IntFree( p->vCex );
259 if ( p->vOneHots ) Vec_IntFree( p->vOneHots );
260 ABC_FREE( p->pMemFraig );
261 ABC_FREE( p->pMemFanins );
262 ABC_FREE( p->pMemSatNums );
263 ABC_FREE( p->pPatWords );
264 ABC_FREE( p );
265 }
266
267 /**Function*************************************************************
268
269 Synopsis [Prints stats for the fraiging manager.]
270
271 Description []
272
273 SideEffects []
274
275 SeeAlso []
276
277 ***********************************************************************/
Fra_ManPrint(Fra_Man_t * p)278 void Fra_ManPrint( Fra_Man_t * p )
279 {
280 double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
281 printf( "SimWord = %d. Round = %d. Mem = %0.2f MB. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n",
282 p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
283 printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n",
284 p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
285 printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
286 p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1),
287 p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
288 if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
289 if ( p->pPars->fUse1Hot ) Fra_OneHotEstimateCoverage( p, p->vOneHots );
290 ABC_PRT( "AIG simulation ", p->pSml->timeSim );
291 ABC_PRT( "AIG traversal ", p->timeTrav );
292 if ( p->timeRwr )
293 {
294 ABC_PRT( "AIG rewriting ", p->timeRwr );
295 }
296 ABC_PRT( "SAT solving ", p->timeSat );
297 ABC_PRT( " Unsat ", p->timeSatUnsat );
298 ABC_PRT( " Sat ", p->timeSatSat );
299 ABC_PRT( " Fail ", p->timeSatFail );
300 ABC_PRT( "Class refining ", p->timeRef );
301 ABC_PRT( "TOTAL RUNTIME ", p->timeTotal );
302 if ( p->time1 ) { ABC_PRT( "time1 ", p->time1 ); }
303 if ( p->nSpeculs )
304 printf( "Speculations = %d.\n", p->nSpeculs );
305 fflush( stdout );
306 }
307
308 ////////////////////////////////////////////////////////////////////////
309 /// END OF FILE ///
310 ////////////////////////////////////////////////////////////////////////
311
312
313 ABC_NAMESPACE_IMPL_END
314
315