ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mapperSuper.c
Go to the documentation of this file.
1
18
19#include "mapperInt.h"
20
22
23
27
28static int Map_LibraryReadFile( Map_SuperLib_t * pLib, FILE * pFile );
29static Map_Super_t * Map_LibraryReadGate( Map_SuperLib_t * pLib, char * pBuffer, int nVars );
30static int Map_LibraryTruthVerify( Map_SuperLib_t * pLib, Map_Super_t * pGate );
31static void Map_LibraryComputeTruth( Map_SuperLib_t * pLib, char * pFormula, unsigned uTruthRes[] );
32static void Map_LibraryComputeTruth_rec( Map_SuperLib_t * pLib, char * pFormula, unsigned uTruthsIn[][2], unsigned uTruthRes[] );
33static void Map_LibraryPrintClasses( Map_SuperLib_t * p );
34
38
50int Map_LibraryRead( Map_SuperLib_t * pLib, char * pFileName )
51{
52 FILE * pFile;
53 int Status;
54 // read the beginning of the file
55 assert( pLib->pGenlib == NULL );
56 pFile = fopen( pFileName, "r" );
57 if ( pFile == NULL )
58 {
59 printf( "Cannot open input file \"%s\".\n", pFileName );
60 return 0;
61 }
62 Status = Map_LibraryReadFile( pLib, pFile );
63 fclose( pFile );
64// Map_LibraryPrintClasses( pLib );
65 return Status;
66}
67
68
80int Map_LibraryReadFile( Map_SuperLib_t * pLib, FILE * pFile )
81{
82 ProgressBar * pProgress;
83 char pBuffer[5000];
84 FILE * pFileGen;
85 Map_Super_t * pGate;
86 char * pTemp = NULL; // Suppress "might be used uninitialized"
87 char * pLibName;
88 int nCounter, nGatesTotal;
89 unsigned uCanon[2];
90 int RetValue;
91
92 // skip empty and comment lines
93 while ( fgets( pBuffer, 2000, pFile ) != NULL )
94 {
95 // skip leading spaces
96 for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ );
97 // skip comment lines and empty lines
98 if ( *pTemp != 0 && *pTemp != '#' )
99 break;
100 }
101
102 // get the genlib file name
103 pLibName = strtok( pTemp, " \t\r\n" );
104 if ( strcmp( pLibName, "GATE" ) == 0 )
105 {
106 printf( "The input file \"%s\" looks like a genlib file and not a supergate library file.\n", pLib->pName );
107 return 0;
108 }
109 pFileGen = fopen( pLibName, "r" );
110 if ( pFileGen == NULL )
111 {
112 printf( "Cannot open the genlib file \"%s\".\n", pLibName );
113 return 0;
114 }
115 fclose( pFileGen );
116
117 // read the genlib library
118 pLib->pGenlib = Mio_LibraryRead( pLibName, NULL, 0, 0, 0 );
119 if ( pLib->pGenlib == NULL )
120 {
121 printf( "Cannot read genlib file \"%s\".\n", pLibName );
122 return 0;
123 }
124
125 // read the number of variables
126 RetValue = fscanf( pFile, "%d\n", &pLib->nVarsMax );
127 if ( pLib->nVarsMax < 2 || pLib->nVarsMax > 10 )
128 {
129 printf( "Suspicious number of variables (%d).\n", pLib->nVarsMax );
130 return 0;
131 }
132
133 // read the number of gates
134 RetValue = fscanf( pFile, "%d\n", &nGatesTotal );
135 if ( nGatesTotal < 1 || nGatesTotal > 10000000 )
136 {
137 printf( "Suspicious number of gates (%d).\n", nGatesTotal );
138 return 0;
139 }
140
141 // read the lines
142 nCounter = 0;
143 pProgress = Extra_ProgressBarStart( stdout, nGatesTotal );
144 while ( fgets( pBuffer, 5000, pFile ) != NULL )
145 {
146 for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ );
147 if ( pTemp[0] == '\0' )
148 continue;
149 // get the gate
150 pGate = Map_LibraryReadGate( pLib, pTemp, pLib->nVarsMax );
151 assert( pGate->Num == nCounter + 1 );
152 // count the number of parentheses in the formula - this is the number of gates
153 for ( pTemp = pGate->pFormula; *pTemp; pTemp++ )
154 pGate->nGates += (*pTemp == '(');
155 // verify the truth table
156 assert( Map_LibraryTruthVerify(pLib, pGate) );
157
158 // find the N-canonical form of this supergate
159 pGate->nPhases = Map_CanonComputeSlow( pLib->uTruths, pLib->nVarsMax, pLib->nVarsMax, pGate->uTruth, pGate->uPhases, uCanon );
160 // add the supergate into the table by its N-canonical table
161 Map_SuperTableInsertC( pLib->tTableC, uCanon, pGate );
162 // update the progress bar
163 Extra_ProgressBarUpdate( pProgress, ++nCounter, NULL );
164 }
165 Extra_ProgressBarStop( pProgress );
166 pLib->nSupersAll = nCounter;
167 if ( nCounter != nGatesTotal )
168 printf( "The number of gates read (%d) is different what the file says (%d).\n", nGatesTotal, nCounter );
169 return 1;
170}
171
183Map_Super_t * Map_LibraryReadGate( Map_SuperLib_t * pLib, char * pBuffer, int nVars )
184{
185 Map_Super_t * pGate;
186 char * pTemp;
187 int i;
188
189 // start and clean the gate
190 pGate = (Map_Super_t *)Extra_MmFixedEntryFetch( pLib->mmSupers );
191 memset( pGate, 0, sizeof(Map_Super_t) );
192
193 // read the number
194 pTemp = strtok( pBuffer, " " );
195 pGate->Num = atoi(pTemp);
196
197 // read the signature
198 pTemp = strtok( NULL, " " );
199 if ( pLib->nVarsMax < 6 )
200 {
201 pGate->uTruth[0] = Extra_ReadBinary(pTemp);
202 pGate->uTruth[1] = 0;
203 }
204 else
205 {
206 pGate->uTruth[0] = Extra_ReadBinary(pTemp+32);
207 pTemp[32] = 0;
208 pGate->uTruth[1] = Extra_ReadBinary(pTemp);
209 }
210
211 // read the max delay
212 pTemp = strtok( NULL, " " );
213 pGate->tDelayMax.Rise = (float)atof(pTemp);
214 pGate->tDelayMax.Fall = pGate->tDelayMax.Rise;
215
216 // read the pin-to-pin delay
217 for ( i = 0; i < nVars; i++ )
218 {
219 pTemp = strtok( NULL, " " );
220 pGate->tDelaysR[i].Rise = (float)atof(pTemp);
221 pGate->tDelaysF[i].Fall = pGate->tDelaysR[i].Rise;
222 }
223
224 // read the area
225 pTemp = strtok( NULL, " " );
226 pGate->Area = (float)atof(pTemp);
227
228 // the rest is the gate name
229 pTemp = strtok( NULL, " \r\n" );
230 if ( strlen(pTemp) == 0 )
231 printf( "A gate name is empty.\n" );
232
233 // save the gate name
234 pGate->pFormula = Extra_MmFlexEntryFetch( pLib->mmForms, strlen(pTemp) + 1 );
235 strcpy( pGate->pFormula, pTemp );
236
237 // the rest is the gate name
238 pTemp = strtok( NULL, " \n\0" );
239 if ( pTemp != NULL )
240 printf( "The following trailing symbols found \"%s\".\n", pTemp );
241 return pGate;
242}
243
256char * Map_LibraryReadFormulaStep( char * pFormula, char * pStrings[], int * pnStrings )
257{
258 char * pName, * pPar1, * pPar2, * pCur;
259 int nStrings, CountPars;
260
261 // skip leading spaces
262 for ( pName = pFormula; *pName && *pName == ' '; pName++ );
263 assert( *pName );
264 // find the first opening parenthesis
265 for ( pPar1 = pName; *pPar1 && *pPar1 != '('; pPar1++ );
266 if ( *pPar1 == 0 )
267 {
268 *pnStrings = 0;
269 return pName;
270 }
271 // overwrite it with space
272 assert( *pPar1 == '(' );
273 *pPar1 = 0;
274 // find the corresponding closing parenthesis
275 for ( CountPars = 1, pPar2 = pPar1 + 1; *pPar2 && CountPars; pPar2++ )
276 if ( *pPar2 == '(' )
277 CountPars++;
278 else if ( *pPar2 == ')' )
279 CountPars--;
280 pPar2--;
281 assert( CountPars == 0 );
282 // overwrite it with space
283 assert( *pPar2 == ')' );
284 *pPar2 = 0;
285 // save the intervals between the commas
286 nStrings = 0;
287 pCur = pPar1 + 1;
288 while ( 1 )
289 {
290 // save the current string
291 pStrings[ nStrings++ ] = pCur;
292 // find the beginning of the next string
293 for ( CountPars = 0; *pCur && (CountPars || *pCur != ','); pCur++ )
294 if ( *pCur == '(' )
295 CountPars++;
296 else if ( *pCur == ')' )
297 CountPars--;
298 if ( *pCur == 0 )
299 break;
300 assert( *pCur == ',' );
301 *pCur = 0;
302 pCur++;
303 }
304 // save the results and return
305 *pnStrings = nStrings;
306 return pName;
307}
308
309
321int Map_LibraryTruthVerify( Map_SuperLib_t * pLib, Map_Super_t * pGate )
322{
323 unsigned uTruthRes[2];
324 Map_LibraryComputeTruth( pLib, pGate->pFormula, uTruthRes );
325 if ( uTruthRes[0] != pGate->uTruth[0] || uTruthRes[1] != pGate->uTruth[1] )
326 return 0;
327 return 1;
328}
329
330
344void Map_LibraryComputeTruth( Map_SuperLib_t * pLib, char * pFormula, unsigned uTruthRes[] )
345{
346 char Buffer[1000];
347 strcpy( Buffer, pFormula );
348 Map_LibraryComputeTruth_rec( pLib, Buffer, pLib->uTruths, uTruthRes );
349}
350
364void Map_LibraryComputeTruth_rec( Map_SuperLib_t * pLib, char * pFormula, unsigned uTruthsIn[][2], unsigned uTruthRes[] )
365{
366 Mio_Gate_t * pMioGate;
367 char * pGateName, * pStrings[6];
368 unsigned uTruthsFanins[6][2];
369 int nStrings, i;
370
371 // perform one step parsing of the formula
372 // detect the root gate name, the next-step strings, and their number
373 pGateName = Map_LibraryReadFormulaStep( pFormula, pStrings, &nStrings );
374 if ( nStrings == 0 ) // elementary variable
375 {
376 assert( pGateName[0] - 'a' < pLib->nVarsMax );
377 uTruthRes[0] = uTruthsIn[pGateName[0] - 'a'][0];
378 uTruthRes[1] = uTruthsIn[pGateName[0] - 'a'][1];
379 return;
380 }
381 // derive the functionality of the fanins
382 for ( i = 0; i < nStrings; i++ )
383 Map_LibraryComputeTruth_rec( pLib, pStrings[i], uTruthsIn, uTruthsFanins[i] );
384 // get the root supergate
385 pMioGate = Mio_LibraryReadGateByName( pLib->pGenlib, pGateName, NULL );
386 if ( pMioGate == NULL )
387 printf( "A supergate contains gate \"%s\" that is not in \"%s\".\n", pGateName, Mio_LibraryReadName(pLib->pGenlib) );
388 // derive the functionality of the output of the supergate
389 Mio_DeriveTruthTable( pMioGate, uTruthsFanins, nStrings, pLib->nVarsMax, uTruthRes );
390}
391
404{
405 printf( "%5d : ", pGate->nUsed );
406 printf( "%5d ", pGate->Num );
407 printf( "A = %5.2f ", pGate->Area );
408 printf( "D = %5.2f/%5.2f/%5.2f ", pGate->tDelayMax.Rise, pGate->tDelayMax.Fall, pGate->tDelayMax.Worst );
409 printf( "%s", pGate->pFormula );
410 printf( "\n" );
411}
412
413
425void Map_LibraryPrintClasses( Map_SuperLib_t * p )
426{
427/*
428 st__generator * gen;
429 Map_Super_t * pSuper, * pSuper2;
430 unsigned Key, uTruth;
431 int Counter = 0;
432 // copy all the supergates into one array
433 st__foreach_item( p->tSuplib, gen, (char **)&Key, (char **)&pSuper )
434 {
435 for ( pSuper2 = pSuper; pSuper2; pSuper2 = pSuper2->pNext )
436 {
437 uTruth = pSuper2->Phase;
438 Extra_PrintBinary( stdout, &uTruth, 5 );
439 printf( " %5d ", pSuper2->Num );
440 printf( "%s", pSuper2->pFormula );
441 printf( "\n" );
442 }
443 printf( "\n" );
444 if ( ++ Counter == 100 )
445 break;
446 }
447*/
448}
449
453
454
456
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
ABC_NAMESPACE_IMPL_START typedef char ProgressBar
Definition bbrNtbdd.c:27
Cube * p
Definition exorList.c:222
char * Extra_MmFixedEntryFetch(Extra_MmFixed_t *p)
void Extra_ProgressBarStop(ProgressBar *p)
unsigned Extra_ReadBinary(char *Buffer)
char * Extra_MmFlexEntryFetch(Extra_MmFlex_t *p, int nBytes)
ProgressBar * Extra_ProgressBarStart(FILE *pFile, int nItemsTotal)
FUNCTION DEFINITIONS ///.
int Map_SuperTableInsertC(Map_HashTable_t *pLib, unsigned uTruthC[], Map_Super_t *pGate)
Definition mapperTable.c:92
char * Map_LibraryReadFormulaStep(char *pFormula, char *pStrings[], int *pnStrings)
int Map_LibraryRead(Map_SuperLib_t *pLib, char *pFileName)
FUNCTION DEFINITIONS ///.
Definition mapperSuper.c:50
void Map_LibraryPrintSupergate(Map_Super_t *pGate)
int Map_CanonComputeSlow(unsigned uTruths[][2], int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char *puPhases, unsigned uTruthRes[])
FUNCTION DEFINITIONS ///.
Definition mapperCanon.c:48
struct Map_SuperStruct_t_ Map_Super_t
Definition mapper.h:45
struct Map_SuperLibStruct_t_ Map_SuperLib_t
Definition mapper.h:46
char * Mio_LibraryReadName(Mio_Library_t *pLib)
DECLARATIONS ///.
Definition mioApi.c:43
void Mio_DeriveTruthTable(Mio_Gate_t *pGate, unsigned uTruthsIn[][2], int nSigns, int nInputs, unsigned uTruthRes[])
Definition mioUtils.c:1036
Mio_Gate_t * Mio_LibraryReadGateByName(Mio_Library_t *pLib, char *pName, char *pOutName)
Definition mioApi.c:105
Mio_Library_t * Mio_LibraryRead(char *FileName, char *pBuffer, char *ExcludeFile, int nFaninLimit, int fVerbose)
Definition mioRead.c:54
struct Mio_GateStruct_t_ Mio_Gate_t
Definition mio.h:43
unsigned uTruths[6][2]
Definition mapperInt.h:188
Mio_Library_t * pGenlib
Definition mapperInt.h:173
Map_HashTable_t * tTableC
Definition mapperInt.h:184
Extra_MmFixed_t * mmSupers
Definition mapperInt.h:199
Extra_MmFlex_t * mmForms
Definition mapperInt.h:201
unsigned uTruth[2]
Definition mapperInt.h:293
Map_Time_t tDelayMax
Definition mapperInt.h:296
Map_Time_t tDelaysF[6]
Definition mapperInt.h:295
Map_Time_t tDelaysR[6]
Definition mapperInt.h:294
unsigned char uPhases[4]
Definition mapperInt.h:289
#define assert(ex)
Definition util_old.h:213
char * memset()
int strlen()
int strcmp()
char * strtok()
char * strcpy()
double atof()