ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
casDec.c
Go to the documentation of this file.
1
20
21#include <stdio.h>
22#include <string.h>
23#include <stdlib.h>
24
25#include "bdd/extrab/extraBdd.h"
26#include "cas.h"
27
29
30
34
35typedef struct
36{
37 int nIns; // the number of LUT variables
38 int nInsP; // the number of inputs coming from the previous LUT
39 int nCols; // the number of columns in this LUT
40 int nMulti; // the column multiplicity, [log2(nCols)]
41 int nSimple; // the number of outputs implemented as direct connections to inputs of the previous block
42 int Level; // the starting level in the ADD in this LUT
43
44// DdNode ** pbVarsIn[32]; // the BDDs of the elementary input variables
45// DdNode ** pbVarsOut[32]; // the BDDs of the elementary output variables
46
47// char * pNamesIn[32]; // the names of input variables
48// char * pNamesOut[32]; // the names of output variables
49
50 DdNode ** pbCols; // the array of columns represented by BDDs
51 DdNode ** pbCodes; // the array of codes (in terms of pbVarsOut)
52 DdNode ** paNodes; // the array of starting ADD nodes on the next level (also referenced)
53
54 DdNode * bRelation; // the relation after encoding
55
56 // the relation depends on the three groups of variables:
57 // (1) variables on top represent the outputs of the previous cascade
58 // (2) variables in the middle represent the primary inputs
59 // (3) variables below (CVars) represent the codes
60 //
61 // the replacement is done after computing the relation
62} LUT;
63
64
68
69// the LUT-2-BLIF writing function
70void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName );
71
72// the function to write a DD (BDD or ADD) as a network of MUXES
73extern void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
74extern void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
75
79
80static int s_LutSize = 15;
81static int s_nFuncVars;
82
84
87
89// temporary output variables
90//FILE * pTable;
91//long s_ReadingTime;
92//long s_RemappingTime;
94
98
99#define PRB_(f) printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
100#define PRK(f,n) Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
101#define PRK2(f,g,n) Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" )
102
103
107
108int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose )
109// aFunc is a 0-1 ADD for the given function
110// pNames (nNames) are the input variable names
111// FileName is the name of the output file for the LUT network
112// dynamic variable reordering should be disabled when this function is running
113{
114 static LUT * pLuts[MAXINPUTS]; // the LUT cascade
115 static int Profile[MAXINPUTS]; // the profile filled in with the info about the BDD width
116 static int Permute[MAXINPUTS]; // the array to store a temporary permutation of variables
117
118 LUT * p; // the current LUT
119 int i, v;
120
121 DdNode * bCVars[32]; // these are variables for the codes
122
123 int nVarsRem; // the number of remaining variables
124 int PrevMulti; // column multiplicity on the previous level
125 int fLastLut; // flag to signal the last LUT
126 int nLuts;
127 int nLutsTotal = 0;
128 int nLutOutputs = 0;
129 int nLutOutputsOrig = 0;
130
131 abctime clk1;
132
133 s_LutSize = nLutSize;
134
135 s_nFuncVars = nNames;
136
137 // get the profile
138 clk1 = Abc_Clock();
139 Extra_ProfileWidth( dd, aFunc, Profile, -1 );
140
141
142// for ( v = 0; v < nNames; v++ )
143// printf( "Level = %2d, Width = %2d\n", v+1, Profile[v] );
144
145
146//printf( "\n" );
147
148 // mark-up the LUTs
149 // assuming that the manager has exactly nNames vars (new vars have not been introduced yet)
150 nVarsRem = nNames; // the number of remaining variables
151 PrevMulti = 0; // column multiplicity on the previous level
152 fLastLut = 0;
153 nLuts = 0;
154 do
155 {
156 p = (LUT*) ABC_ALLOC( char, sizeof(LUT) );
157 memset( p, 0, sizeof(LUT) );
158
159 if ( nVarsRem + PrevMulti <= s_LutSize ) // this is the last LUT
160 {
161 p->nIns = nVarsRem + PrevMulti;
162 p->nInsP = PrevMulti;
163 p->nCols = 2;
164 p->nMulti = 1;
165 p->Level = nNames-nVarsRem;
166
167 nVarsRem = 0;
168 PrevMulti = 1;
169
170 fLastLut = 1;
171 }
172 else // this is not the last LUT
173 {
174 p->nIns = s_LutSize;
175 p->nInsP = PrevMulti;
176 p->nCols = Profile[nNames-(nVarsRem-(s_LutSize-PrevMulti))];
177 p->nMulti = Abc_Base2Log(p->nCols);
178 p->Level = nNames-nVarsRem;
179
180 nVarsRem = nVarsRem-(s_LutSize-PrevMulti);
181 PrevMulti = p->nMulti;
182 }
183
184 if ( p->nMulti >= s_LutSize )
185 {
186 printf( "The LUT size is too small\n" );
187 return 0;
188 }
189
190 nLutOutputsOrig += p->nMulti;
191
192
193//if ( fVerbose )
194//printf( "Stage %2d: In = %3d, InP = %3d, Cols = %5d, Multi = %2d, Level = %2d\n",
195// nLuts+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->Level );
196
197
198 // there should be as many columns, codes, and nodes, as there are columns on this level
199 p->pbCols = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
200 p->pbCodes = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
201 p->paNodes = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
202
203 pLuts[nLuts] = p;
204 nLuts++;
205 }
206 while ( !fLastLut );
207
208
209//if ( fVerbose )
210//printf( "The number of cascades = %d\n", nLuts );
211
212
213//fprintf( pTable, "%d ", nLuts );
214
215
216 // add the new variables at the bottom
217 for ( i = 0; i < s_LutSize; i++ )
218 bCVars[i] = Cudd_bddNewVar(dd);
219
220 // for each LUT - assign the LUT and encode the columns
221 s_EncodingTime = 0;
222 for ( i = 0; i < nLuts; i++ )
223 {
224 int RetValue;
225 DdNode * bVars[32];
226 int nVars;
227 DdNode * bVarsInCube;
228 DdNode * bVarsCCube;
229 DdNode * bVarsCube;
230 int CutLevel;
231
232 p = pLuts[i];
233
234 // compute the columns of this LUT starting from the given set of nodes with the given codes
235 // (these codes have been remapped to depend on the topmost variables in the manager)
236 // for the first LUT, start with the constant 1 BDD
237 CutLevel = p->Level + p->nIns - p->nInsP;
238 if ( i == 0 )
240 dd, &aFunc, &(b1), 1,
241 p->paNodes, p->pbCols, CutLevel );
242 else
244 dd, pLuts[i-1]->paNodes, pLuts[i-1]->pbCodes, pLuts[i-1]->nCols,
245 p->paNodes, p->pbCols, CutLevel );
246 assert( RetValue == p->nCols );
247 // at this point, we have filled out p->paNodes[] and p->pbCols[] of this LUT
248 // pLuts[i-1]->paNodes depended on normal vars
249 // pLuts[i-1]->pbCodes depended on the topmost variables
250 // the resulting p->paNodes depend on normal ADD nodes
251 // the resulting p->pbCols depend on normal vars and topmost variables in the manager
252
253 // perform the encoding
254
255 // create the cube of these variables
256 // collect the topmost variables of the manager
257 nVars = p->nInsP;
258 for ( v = 0; v < nVars; v++ )
259 bVars[v] = dd->vars[ dd->invperm[v] ];
260 bVarsCCube = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 ); Cudd_Ref( bVarsCCube );
261
262 // collect the primary input variables involved in this LUT
263 nVars = p->nIns - p->nInsP;
264 for ( v = 0; v < nVars; v++ )
265 bVars[v] = dd->vars[ dd->invperm[p->Level+v] ];
266 bVarsInCube = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 ); Cudd_Ref( bVarsInCube );
267
268 // get the cube
269 bVarsCube = Cudd_bddAnd( dd, bVarsInCube, bVarsCCube ); Cudd_Ref( bVarsCube );
270 Cudd_RecursiveDeref( dd, bVarsInCube );
271 Cudd_RecursiveDeref( dd, bVarsCCube );
272
273 // get the encoding relation
274 if ( i == nLuts -1 )
275 {
276 DdNode * bVar;
277 assert( p->nMulti == 1 );
278 assert( p->nCols == 2 );
279 assert( Cudd_IsConstant( p->paNodes[0] ) );
280 assert( Cudd_IsConstant( p->paNodes[1] ) );
281
282 bVar = ( p->paNodes[0] == a1 )? bCVars[0]: Cudd_Not( bCVars[0] );
283 p->bRelation = Cudd_bddIte( dd, bVar, p->pbCols[0], p->pbCols[1] ); Cudd_Ref( p->bRelation );
284 }
285 else
286 {
287 abctime clk2 = Abc_Clock();
288// p->bRelation = PerformTheEncoding( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple ); Cudd_Ref( p->bRelation );
289 p->bRelation = Extra_bddEncodingNonStrict( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple ); Cudd_Ref( p->bRelation );
290 s_EncodingTime += Abc_Clock() - clk2;
291 }
292
293 // update the number of LUT outputs
294 nLutOutputs += (p->nMulti - p->nSimple);
295 nLutsTotal += p->nMulti;
296
297//if ( fVerbose )
298//printf( "Stage %2d: Simple = %d\n", i+1, p->nSimple );
299
300if ( fVerbose )
301printf( "Stage %3d: In = %3d InP = %3d Cols = %5d Multi = %2d Simple = %2d Level = %3d\n",
302 i+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->nSimple, p->Level );
303
304 // get the codes from the relation (these are not necessarily cubes)
305 {
306 int c;
307 for ( c = 0; c < p->nCols; c++ )
308 {
309 p->pbCodes[c] = Cudd_bddAndAbstract( dd, p->bRelation, p->pbCols[c], bVarsCube ); Cudd_Ref( p->pbCodes[c] );
310 }
311 }
312
313 Cudd_RecursiveDeref( dd, bVarsCube );
314
315 // remap the codes to depend on the topmost varibles of the manager
316 // useful as a preparation for the next step
317 {
318 DdNode ** pbTemp;
319 int k, v;
320
321 pbTemp = (DdNode **) ABC_ALLOC( char, p->nCols * sizeof(DdNode *) );
322
323 // create the identical permutation
324 for ( v = 0; v < dd->size; v++ )
325 Permute[v] = v;
326
327 // use the topmost variables of the manager
328 // to represent the previous level codes
329 for ( v = 0; v < p->nMulti; v++ )
330 Permute[bCVars[v]->index] = dd->invperm[v];
331
332 Extra_bddPermuteArray( dd, p->pbCodes, pbTemp, p->nCols, Permute );
333 // the array pbTemp comes already referenced
334
335 // deref the old codes and assign the new ones
336 for ( k = 0; k < p->nCols; k++ )
337 {
338 Cudd_RecursiveDeref( dd, p->pbCodes[k] );
339 p->pbCodes[k] = pbTemp[k];
340 }
341 ABC_FREE( pbTemp );
342 }
343 }
344 if ( fVerbose )
345 printf( "LUTs: Total = %5d. Final = %5d. Simple = %5d. (%6.2f %%) ",
346 nLutsTotal, nLutOutputs, nLutsTotal-nLutOutputs, 100.0*(nLutsTotal-nLutOutputs)/nLutsTotal );
347 if ( fVerbose )
348 printf( "Memory = %6.2f MB\n", 1.0*nLutOutputs*(1<<nLutSize)/(1<<20) );
349// printf( "\n" );
350
351//fprintf( pTable, "%d ", nLutOutputsOrig );
352//fprintf( pTable, "%d ", nLutOutputs );
353
354 if ( fVerbose )
355 {
356 printf( "Pure decomposition time = %.2f sec\n", (float)(Abc_Clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
357 printf( "Encoding time = %.2f sec\n", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
358// printf( "Encoding search time = %.2f sec\n", (float)(s_EncSearchTime)/(float)(CLOCKS_PER_SEC) );
359// printf( "Encoding compute time = %.2f sec\n", (float)(s_EncComputeTime)/(float)(CLOCKS_PER_SEC) );
360 }
361
362
363//fprintf( pTable, "%.2f ", (float)(s_ReadingTime)/(float)(CLOCKS_PER_SEC) );
364//fprintf( pTable, "%.2f ", (float)(Abc_Clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
365//fprintf( pTable, "%.2f ", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
366//fprintf( pTable, "%.2f ", (float)(s_RemappingTime)/(float)(CLOCKS_PER_SEC) );
367
368
369 // write LUTs into the BLIF file
370 clk1 = Abc_Clock();
371 if ( fCheck )
372 {
373 FILE * pFile;
374 // start the file
375 pFile = fopen( FileName, "w" );
376 fprintf( pFile, ".model %s\n", FileName );
377
378 fprintf( pFile, ".inputs" );
379 for ( i = 0; i < nNames; i++ )
380 fprintf( pFile, " %s", pNames[i] );
381 fprintf( pFile, "\n" );
382 fprintf( pFile, ".outputs F" );
383 fprintf( pFile, "\n" );
384
385 // write the DD into the file
386 WriteLUTSintoBLIFfile( pFile, dd, pLuts, nLuts, bCVars, pNames, nNames, FileName );
387
388 fprintf( pFile, ".end\n" );
389 fclose( pFile );
390 if ( fVerbose )
391 printf( "Output file writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
392 }
393
394
395 // updo the LUT cascade
396 for ( i = 0; i < nLuts; i++ )
397 {
398 p = pLuts[i];
399 for ( v = 0; v < p->nCols; v++ )
400 {
401 Cudd_RecursiveDeref( dd, p->pbCols[v] );
402 Cudd_RecursiveDeref( dd, p->pbCodes[v] );
403 Cudd_RecursiveDeref( dd, p->paNodes[v] );
404 }
405 Cudd_RecursiveDeref( dd, p->bRelation );
406
407 ABC_FREE( p->pbCols );
408 ABC_FREE( p->pbCodes );
409 ABC_FREE( p->paNodes );
410 ABC_FREE( p );
411 }
412
413 return 1;
414}
415
416void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName )
417{
418 int i, v, o;
419 static char * pNamesLocalIn[MAXINPUTS];
420 static char * pNamesLocalOut[MAXINPUTS];
421 static char Buffer[100];
422 DdNode * bCube, * bCof, * bFunc;
423 LUT * p;
424
425 // go through all the LUTs
426 for ( i = 0; i < nLuts; i++ )
427 {
428 // get the pointer to the LUT
429 p = pLuts[i];
430
431 if ( i == nLuts -1 )
432 {
433 assert( p->nMulti == 1 );
434 }
435
436
437 fprintf( pFile, "#----------------- LUT #%d ----------------------\n", i );
438
439
440 // fill in the names for the current LUT
441
442 // write the outputs of the previous LUT
443 if ( i != 0 )
444 for ( v = 0; v < p->nInsP; v++ )
445 {
446 sprintf( Buffer, "LUT%02d_%02d", i-1, v );
447 pNamesLocalIn[dd->invperm[v]] = Extra_UtilStrsav( Buffer );
448 }
449 // write the primary inputs of the current LUT
450 for ( v = 0; v < p->nIns - p->nInsP; v++ )
451 pNamesLocalIn[dd->invperm[p->Level+v]] = Extra_UtilStrsav( pNames[dd->invperm[p->Level+v]] );
452 // write the outputs of the current LUT
453 for ( v = 0; v < p->nMulti; v++ )
454 {
455 sprintf( Buffer, "LUT%02d_%02d", i, v );
456 if ( i != nLuts - 1 )
457 pNamesLocalOut[v] = Extra_UtilStrsav( Buffer );
458 else
459 pNamesLocalOut[v] = Extra_UtilStrsav( "F" );
460 }
461
462
463 // write LUT outputs
464
465 // get the prefix
466 sprintf( Buffer, "L%02d_", i );
467
468 // get the cube of encoding variables
469 bCube = Extra_bddBitsToCube( dd, (1<<p->nMulti)-1, p->nMulti, bCVars, 1 ); Cudd_Ref( bCube );
470
471 // write each output of the LUT
472 for ( o = 0; o < p->nMulti; o++ )
473 {
474 // get the cofactor of this output
475 bCof = Cudd_Cofactor( dd, p->bRelation, bCVars[o] ); Cudd_Ref( bCof );
476 // quantify the remaining variables to get the function
477 bFunc = Cudd_bddExistAbstract( dd, bCof, bCube ); Cudd_Ref( bFunc );
478 Cudd_RecursiveDeref( dd, bCof );
479
480 // write BLIF
481 sprintf( Buffer, "L%02d_%02d_", i, o );
482
483// WriteDDintoBLIFfileReorder( dd, pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn );
484 // does not work well; the advantage is marginal (30%), the run time is huge...
485
486 WriteDDintoBLIFfile( pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn );
487 Cudd_RecursiveDeref( dd, bFunc );
488 }
489 Cudd_RecursiveDeref( dd, bCube );
490
491 // clean up the previous local names
492 for ( v = 0; v < dd->size; v++ )
493 {
494 if ( pNamesLocalIn[v] )
495 ABC_FREE( pNamesLocalIn[v] );
496 pNamesLocalIn[v] = NULL;
497 }
498 for ( v = 0; v < p->nMulti; v++ )
499 ABC_FREE( pNamesLocalOut[v] );
500 }
501}
502
503
507
508
509
510
512
ABC_INT64_T abctime
Definition abc_global.h:332
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
#define ABC_FREE(obj)
Definition abc_global.h:267
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
#define b1
Definition bbrImage.c:97
long s_EncodingTime
Definition casDec.c:83
void WriteLUTSintoBLIFfile(FILE *pFile, DdManager *dd, LUT **pLuts, int nLuts, DdNode **bCVars, char **pNames, int nNames, char *FileName)
static functions ///
Definition casDec.c:416
int CreateDecomposedNetwork(DdManager *dd, DdNode *aFunc, char **pNames, int nNames, char *FileName, int nLutSize, int fCheck, int fVerbose)
EXTERNAL FUNCTIONS ///.
Definition casDec.c:108
long s_EncComputeTime
Definition casDec.c:86
void WriteDDintoBLIFfile(FILE *pFile, DdNode *Func, char *OutputName, char *Prefix, char **InputNames)
BLIF WRITING FUNCTIONS ///.
Definition casCore.c:803
void WriteDDintoBLIFfileReorder(DdManager *dd, FILE *pFile, DdNode *Func, char *OutputName, char *Prefix, char **InputNames)
Definition casCore.c:928
long s_EncSearchTime
Definition casDec.c:85
#define MAXINPUTS
INCLUDES ///.
Definition cas.h:38
Cube * p
Definition exorList.c:222
DdNode * Extra_bddBitsToCube(DdManager *dd, int Code, int CodeWidth, DdNode **pbVars, int fMsbFirst)
void Extra_bddPermuteArray(DdManager *dd, DdNode **bNodesIn, DdNode **bNodesOut, int nNodes, int *permut)
int Extra_ProfileWidth(DdManager *dd, DdNode *F, int *Profile, int CutLevel)
int Extra_bddNodePathsUnderCutArray(DdManager *dd, DdNode **paNodes, DdNode **pbCubes, int nNodes, DdNode **paNodesRes, DdNode **pbCubesRes, int CutLevel)
#define a1
Definition extraBdd.h:80
DdNode * Extra_bddEncodingNonStrict(DdManager *dd, DdNode **pbColumns, int nColumns, DdNode *bVarsCol, DdNode **pCVars, int nMulti, int *pSimple)
char * Extra_UtilStrsav(const char *s)
type definitions ///
Definition casDec.c:36
int Level
Definition casDec.c:42
int nCols
Definition casDec.c:39
int nSimple
Definition casDec.c:41
int nMulti
Definition casDec.c:40
DdNode ** pbCols
Definition casDec.c:50
int nInsP
Definition casDec.c:38
DdNode ** paNodes
Definition casDec.c:52
DdNode ** pbCodes
Definition casDec.c:51
DdNode * bRelation
Definition casDec.c:54
int nIns
Definition casDec.c:37
#define assert(ex)
Definition util_old.h:213
char * memset()
char * sprintf()