1 /*------------------------------------------------------------\
2 | |
3 | This file is part of the Alliance CAD System Copyright |
4 | (C) Laboratoire LIP6 - D�partement ASIM Universite P&M Curie|
5 | |
6 | Home page : http://www-asim.lip6.fr/alliance/ |
7 | E-mail : mailto:alliance-users@asim.lip6.fr |
8 | |
9 | This progam is free software; you can redistribute it |
10 | and/or modify it under the terms of the GNU Library General|
11 | Public License as published by the Free Software Foundation |
12 | either version 2 of the License, or (at your option) any |
13 | later version. |
14 | |
15 | Alliance VLSI CAD System is distributed in the hope that |
16 | it will be useful, but WITHOUT ANY WARRANTY; |
17 | without even the implied warranty of MERCHANTABILITY or |
18 | FITNESS FOR A PARTICULAR PURPOSE. See the GNU General |
19 | Public License for more details. |
20 | |
21 | You should have received a copy of the GNU General Public |
22 | License along with the GNU C Library; see the file COPYING. |
23 | If not, write to the Free Software Foundation, Inc., |
24 | 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. |
25 | |
26 \------------------------------------------------------------*/
27 /*------------------------------------------------------------\
28 | |
29 | Tool : Bdd |
30 | |
31 | File : bddsystem.c |
32 | |
33 | Date : 03.12.96 |
34 | |
35 | Author : Jacomme Ludovic |
36 | |
37 \------------------------------------------------------------*/
38 /*------------------------------------------------------------\
39 | |
40 | Include Files |
41 | |
42 \------------------------------------------------------------*/
43
44 # include "mut.h"
45 # include "aut.h"
46 # include "abl.h"
47 # include "bdd.h"
48
49 # include <stdio.h>
50 # include "bddsystem.h"
51 # include "bdderror.h"
52
53 /*------------------------------------------------------------\
54 | |
55 | Constants |
56 | |
57 \------------------------------------------------------------*/
58 /*------------------------------------------------------------\
59 | |
60 | Types |
61 | |
62 \------------------------------------------------------------*/
63 /*------------------------------------------------------------\
64 | |
65 | Variables |
66 | |
67 \------------------------------------------------------------*/
68
69 bddsystem *BddLocalSystem = (bddsystem *)0;
70
71 /*------------------------------------------------------------\
72 | |
73 | Functions |
74 | |
75 \------------------------------------------------------------*/
76 /*------------------------------------------------------------\
77 | |
78 | Bdd Create System |
79 | |
80 \------------------------------------------------------------*/
81
createbddsystem(ModelVar,ModelOper,MaxVar,MaxNode)82 bddsystem *createbddsystem( ModelVar, ModelOper, MaxVar, MaxNode )
83
84 long ModelVar;
85 long ModelOper;
86 long MaxVar;
87 long MaxNode;
88 {
89 bddsystem *BddSystem;
90 bddnode *BddOne;
91 bddnode *BddZero;
92 long MaxIndex;
93
94 MaxIndex = BDD_INDEX_MIN + MaxVar;
95
96 if ( ModelVar <= 0 )
97 {
98 bdderror( BDD_MODEL_VAR_ERROR, ModelVar );
99 }
100
101 if ( MaxVar >= BDD_MAX_VAR )
102 {
103 bdderror( BDD_BAD_VAR_ERROR, MaxVar );
104 }
105
106 if ( ModelOper <= 0 )
107 {
108 bdderror( BDD_MODEL_OPER_ERROR, ModelOper );
109 }
110
111 BddSystem = allocbddsystem();
112
113 BddSystem->HASH_OPER = createbddhopertable( ModelOper );
114 BddSystem->OPER_MODEL = ModelOper;
115
116 BddSystem->MAX_VAR = MaxVar;
117 BddSystem->MAX_INDEX = MaxIndex;
118 BddSystem->MAX_NODE = MaxNode;
119 BddSystem->VAR_NODE = allocbddvarnode( MaxIndex );
120 BddSystem->VAR_MODEL = ModelVar;
121
122 BddSystem->INDEX_NODE = allocbddindexnode( MaxIndex );
123 BddSystem->INDEX_NODE[ BDD_INDEX_ZERO ] = createbddhnodetable( ModelVar );
124 BddSystem->INDEX_NODE[ BDD_INDEX_ONE ] = BddSystem->INDEX_NODE[ BDD_INDEX_ZERO ];
125
126 BddSystem->VAR_TO_INDEX = allocbddindex( MaxVar );
127 BddSystem->INDEX_TO_VAR = allocbddvar( MaxIndex );
128 BddSystem->INDEX_TO_VAR[ BDD_INDEX_ZERO ] = BDD_MAX_VAR;
129 BddSystem->INDEX_TO_VAR[ BDD_INDEX_ONE ] = BDD_MAX_VAR;
130
131 BddSystem->NUMBER_VAR = 0;
132 BddSystem->NUMBER_INDEX = BDD_INDEX_MIN;
133
134 setbddlocalsystem( BddSystem );
135
136 createbddblock( (bddsystem *)0 );
137
138 BddOne = addbddnode( (bddsystem *)0, BDD_INDEX_ONE , (bddnode *)0, (bddnode *)0 );
139 BddZero = addbddnode( (bddsystem *)0, BDD_INDEX_ZERO, (bddnode *)0, (bddnode *)0 );
140
141 BddOne->REF_EXT = BDD_MAX_REF;
142 BddOne->REF_INT = BDD_MAX_REF;
143 BddZero->REF_EXT = BDD_MAX_REF;
144 BddZero->REF_INT = BDD_MAX_REF;
145
146 BddSystem->ONE = BddOne;
147 BddSystem->ZERO = BddZero;
148
149 BddSystem->VAR_NODE[ BDD_INDEX_ZERO ] = BddZero;
150 BddSystem->VAR_NODE[ BDD_INDEX_ONE ] = BddOne;
151
152 return( BddSystem );
153 }
154
155 /*------------------------------------------------------------\
156 | |
157 | Bdd Reset System |
158 | |
159 \------------------------------------------------------------*/
160
resetbddsystem(BddSystem)161 void resetbddsystem( BddSystem )
162
163 bddsystem *BddSystem;
164 {
165 bddindexnode *IndexNode;
166 bddnode *BddOne;
167 bddnode *BddZero;
168 bddindex NumberIndex;
169 bddindex Index;
170
171 setbddlocalsystem( BddSystem );
172
173 resetbddblock( (bddsystem *)0 );
174 destroybddassoc( (bddsystem *)0 );
175
176 resetbddhopertable( BddLocalSystem->HASH_OPER );
177
178 NumberIndex = BddLocalSystem->NUMBER_INDEX;
179 IndexNode = BddLocalSystem->INDEX_NODE;
180
181 resetbddhnodetable( IndexNode[ BDD_INDEX_ZERO ] );
182
183 for ( Index = BDD_INDEX_MIN; Index < NumberIndex; Index++ )
184 {
185 resetbddhnodetable( IndexNode[ Index ] );
186 }
187
188 BddLocalSystem->NUMBER_VAR = 0;
189 BddLocalSystem->NUMBER_INDEX = BDD_INDEX_MIN;
190 BddLocalSystem->FLAGS = 0;
191 BddLocalSystem->MARK = 0;
192
193 BddOne = addbddnode( (bddsystem *)0, BDD_INDEX_ONE , (bddnode *)0, (bddnode *)0 );
194 BddZero = addbddnode( (bddsystem *)0, BDD_INDEX_ZERO, (bddnode *)0, (bddnode *)0 );
195
196 BddOne->REF_EXT = BDD_MAX_REF;
197 BddOne->REF_INT = BDD_MAX_REF;
198 BddZero->REF_EXT = BDD_MAX_REF;
199 BddZero->REF_INT = BDD_MAX_REF;
200
201 BddLocalSystem->ONE = BddOne;
202 BddLocalSystem->ZERO = BddZero;
203
204 BddLocalSystem->VAR_NODE[ BDD_INDEX_ZERO ] = BddZero;
205 BddLocalSystem->VAR_NODE[ BDD_INDEX_ONE ] = BddOne;
206
207 BddLocalSystem->REORDER_LIMIT = BddLocalSystem->REORDER_LOW;
208 }
209
210 /*------------------------------------------------------------\
211 | |
212 | Bdd Destroy System |
213 | |
214 \------------------------------------------------------------*/
215
destroybddsystem(BddSystem)216 void destroybddsystem( BddSystem )
217
218 bddsystem *BddSystem;
219 {
220 bddindexnode *IndexNode;
221 bddindex NumberIndex;
222 bddindex Index;
223
224 setbddlocalsystem( BddSystem );
225
226 destroybddblock( (bddsystem *)0 );
227 destroybddassoc( (bddsystem *)0 );
228 destroybdduserfunc( (bddsystem *)0 );
229
230 destroybddhopertable( BddLocalSystem->HASH_OPER );
231
232 NumberIndex = BddLocalSystem->NUMBER_INDEX;
233 IndexNode = BddLocalSystem->INDEX_NODE;
234
235 destroybddhnodetable( IndexNode[ BDD_INDEX_ZERO ] );
236
237 for ( Index = BDD_INDEX_MIN; Index < NumberIndex; Index++ )
238 {
239 destroybddhnodetable( IndexNode[ Index ] );
240 }
241
242 freebddvar( BddLocalSystem->INDEX_TO_VAR );
243 freebddindex( BddLocalSystem->VAR_TO_INDEX );
244
245 freebddindexnode( BddLocalSystem->INDEX_NODE );
246 freebddvarnode( BddLocalSystem->VAR_NODE );
247
248 freebddsystem( BddLocalSystem );
249
250 BddLocalSystem = (bddsystem *)0;
251 }
252
253 /*------------------------------------------------------------\
254 | |
255 | View Functions |
256 | |
257 \------------------------------------------------------------*/
258 /*------------------------------------------------------------\
259 | |
260 | Bdd View System |
261 | |
262 \------------------------------------------------------------*/
263
viewbddsystem(BddSystem,ViewIndex)264 void viewbddsystem( BddSystem, ViewIndex )
265
266 bddsystem *BddSystem;
267 char ViewIndex;
268 {
269 bddvar *IndexToVar;
270 bddindex *VarToIndex;
271 bddvar Variable;
272 bddindex Index;
273
274 if ( BddSystem == (bddsystem *)0 )
275 {
276 BddSystem = BddLocalSystem;
277 }
278
279 fprintf( stdout, "--> BddSystem\n" );
280
281 fprintf( stdout, " NUMBER_NODE : %ld\n", BddSystem->NUMBER_NODE );
282 fprintf( stdout, " NUMBER_FREE : %ld\n", BddSystem->NUMBER_FREE );
283 fprintf( stdout, " MAX_NODE : %ld\n", BddSystem->MAX_NODE );
284 fprintf( stdout, " TOP_NODE : %ld\n", BddSystem->TOP_NODE );
285 fprintf( stdout, " NUMBER_VAR : %ld\n", BddSystem->NUMBER_VAR );
286 fprintf( stdout, " MAX_VAR : %ld\n", BddSystem->MAX_VAR );
287 fprintf( stdout, " NUMBER_INDEX : %ld\n", BddSystem->NUMBER_INDEX );
288 fprintf( stdout, " MAX_INDEX : %ld\n", BddSystem->MAX_INDEX );
289 fprintf( stdout, " ASSOC_RESET : %d\n" , BddSystem->ASSOC_RESET );
290 fprintf( stdout, " FLAGS : %lx\n", BddSystem->FLAGS );
291 fprintf( stdout, " REORDER_LOW : %ld\n", BddSystem->REORDER_LOW );
292 fprintf( stdout, " REORDER_LIMIT : %ld\n", BddSystem->REORDER_LIMIT );
293 fprintf( stdout, " REORDER_RATIO : %ld\n", BddSystem->REORDER_RATIO );
294 fprintf( stdout, " EXPLOSION_LIMIT : %ld\n", BddSystem->EXPLOSION_LIMIT );
295 fprintf( stdout, " VAR_MODEL : %ld\n", BddSystem->VAR_MODEL );
296 fprintf( stdout, " OPER_MODEL : %ld\n", BddSystem->OPER_MODEL );
297
298 if ( ViewIndex )
299 {
300 IndexToVar = BddSystem->INDEX_TO_VAR;
301 VarToIndex = BddSystem->VAR_TO_INDEX;
302
303 for ( Index = 0; Index < BddSystem->NUMBER_INDEX; Index++ )
304 {
305 fprintf( stdout, " INDEX_TO_VAR[ %u ] = %d\n",
306 Index, IndexToVar[ Index ] );
307 }
308
309 for ( Variable = 0; Variable < BddSystem->NUMBER_VAR; Variable++ )
310 {
311 fprintf( stdout, " VAR_TO_INDEX[ %u ] = %d\n",
312 Variable, VarToIndex[ Variable ] );
313 }
314 }
315
316 fprintf( stdout, "<-- BddSystem\n" );
317 }
318
319 /*------------------------------------------------------------\
320 | |
321 | Bdd View System Info |
322 | |
323 \------------------------------------------------------------*/
324
viewbddsysteminfo(BddSystem)325 void viewbddsysteminfo( BddSystem )
326
327 bddsystem *BddSystem;
328 {
329 bddhopertable *HashOper;
330 bddindexnode *IndexNode;
331 bddhnodetable *HashTable;
332 long NumberIndex;
333 long Index;
334 long Sum;
335 long Slot;
336 long Fill;
337 long Hit;
338 long Miss;
339 long Stretch;
340 long Resize;
341 long Scan;
342
343 if ( BddSystem == (bddsystem *)0 )
344 {
345 BddSystem = BddLocalSystem;
346 }
347
348 HashOper = BddSystem->HASH_OPER;
349 IndexNode = BddSystem->INDEX_NODE;
350
351 fprintf( stdout, "--> BddSystem Info\n" );
352
353 Slot = HashOper->TABLE_SIZE;
354 Fill = ( HashOper->NUMBER_OPER * 100 ) / Slot;
355 Sum = HashOper->NUMBER_HIT + HashOper->NUMBER_MISS;
356
357 if ( Sum != 0 )
358 {
359 Hit = ( 100 * HashOper->NUMBER_HIT ) / Sum;
360 Miss = ( 100 * HashOper->NUMBER_MISS ) / Sum;
361 }
362 else
363 {
364 Hit = Miss = -1;
365 }
366
367 fprintf( stdout, " HASH_OPER SLOTS : %ld \n", Slot );
368 fprintf( stdout, " HASH_OPER FILL RATE : %ld %%\n", Fill );
369 fprintf( stdout, " HASH_OPER HIT RATE : %ld %%\n", Hit );
370 fprintf( stdout, " HASH_OPER MISS RATE : %ld %%\n", Miss );
371
372 Slot = 0;
373 Fill = 0;
374 Scan = 0;
375 Stretch = 0;
376 Resize = 0;
377
378 NumberIndex = BddLocalSystem->NUMBER_INDEX;
379
380 for ( Index = BDD_INDEX_MIN; Index < NumberIndex; Index++ )
381 {
382 HashTable = IndexNode[ Index ];
383
384 Slot += HashTable->TABLE_SIZE;
385 Fill += ( HashTable->NUMBER_NODE * 100 ) / HashTable->TABLE_SIZE;
386 Scan += HashTable->NUMBER_SCAN;
387 Stretch += HashTable->NUMBER_STRETCH;
388 Resize += HashTable->NUMBER_RESIZE;
389 }
390
391 NumberIndex -= BDD_INDEX_MIN;
392
393 Slot /= NumberIndex;
394 Fill /= NumberIndex;
395 Scan /= NumberIndex;
396 Stretch /= NumberIndex;
397 Resize /= NumberIndex;
398
399 fprintf( stdout, " HASH_NODE SLOTS AVERAGE : %ld \n", Slot );
400 fprintf( stdout, " HASH_NODE FILL RATE : %ld %%\n", Fill );
401 fprintf( stdout, " HASH_NODE SCAN AVERAGE : %ld \n", Scan );
402 fprintf( stdout, " HASH_OPER STRETCH AVERAGE : %ld \n", Stretch );
403 fprintf( stdout, " HASH_OPER RESIZE AVERAGE : %ld \n", Resize );
404
405 fprintf( stdout, "<-- BddSystem Info\n" );
406 }
407