1 /*////////////////////////////////////////////////////////////////////////////
2
3 ABC: System for Sequential Synthesis and Verification
4
5 http://www.eecs.berkeley.edu/~alanmi/abc/
6
7 Copyright (c) The Regents of the University of California. All rights reserved.
8
9 Permission is hereby granted, without written agreement and without license or
10 royalty fees, to use, copy, modify, and distribute this software and its
11 documentation for any purpose, provided that the above copyright notice and
12 the following two paragraphs appear in all copies of this software.
13
14 IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
15 DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
16 THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
17 CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
18
19 THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
20 BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
21 A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
22 AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
23 SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
24
25 ////////////////////////////////////////////////////////////////////////////*/
26
27 /**CFile****************************************************************
28
29 FileName [main.c]
30
31 SystemName [ABC: Logic synthesis and verification system.]
32
33 PackageName [The main package.]
34
35 Synopsis [Here everything starts.]
36
37 Author [Alan Mishchenko]
38
39 Affiliation [UC Berkeley]
40
41 Date [Ver. 1.0. Started - June 20, 2005.]
42
43 Revision [$Id: main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
44
45 ***********************************************************************/
46
47 #ifndef WIN32
48 #include <sys/time.h>
49 #include <sys/times.h>
50 #include <sys/resource.h>
51 #include <unistd.h>
52 #include <signal.h>
53 #include <stdlib.h>
54 #endif
55
56 #include "base/abc/abc.h"
57 #include "mainInt.h"
58 #include "base/wlc/wlc.h"
59
60 ABC_NAMESPACE_IMPL_START
61
62
63 ////////////////////////////////////////////////////////////////////////
64 /// DECLARATIONS ///
65 ////////////////////////////////////////////////////////////////////////
66
67 static int TypeCheck( Abc_Frame_t * pAbc, const char * s);
68
69 ////////////////////////////////////////////////////////////////////////
70 /// FUNCTION DEFINITIONS ///
71 ////////////////////////////////////////////////////////////////////////
72
73 unsigned enable_dbg_outs = 1;
74
75 /**Function*************************************************************
76
77 Synopsis [The main() procedure.]
78
79 Description []
80
81 SideEffects []
82
83 SeeAlso []
84
85 ***********************************************************************/
Abc_RealMain(int argc,char * argv[])86 int Abc_RealMain( int argc, char * argv[] )
87 {
88 Abc_Frame_t * pAbc;
89 Vec_Str_t* sCommandUsr = Vec_StrAlloc(1000);
90 char sCommandTmp[ABC_MAX_STR], sReadCmd[1000], sWriteCmd[1000];
91 const char * sOutFile, * sInFile;
92 char * sCommand;
93 int fStatus = 0;
94 int c, fInitSource, fInitRead, fFinalWrite;
95
96 enum {
97 INTERACTIVE, // interactive mode
98 BATCH, // batch mode, run a command and quit
99 BATCH_THEN_INTERACTIVE, // run a command, then back to interactive mode
100 BATCH_QUIET, // as in batch mode, but don't echo the command
101 BATCH_QUIET_THEN_INTERACTIVE, // as in batch then interactive mode, but don't echo the command
102 BATCH_SMT // special batch mode, which expends SMTLIB problem via stdin
103 } fBatch;
104
105 // added to detect memory leaks
106 // watch for {,,msvcrtd.dll}*__p__crtBreakAlloc()
107 // (http://support.microsoft.com/kb/151585)
108 #if defined(_DEBUG) && defined(_MSC_VER)
109 _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
110 #endif
111
112 // get global frame (singleton pattern)
113 // will be initialized on first call
114 pAbc = Abc_FrameGetGlobalFrame();
115 pAbc->sBinary = argv[0];
116
117 // default options
118 fBatch = INTERACTIVE;
119 fInitSource = 1;
120 fInitRead = 0;
121 fFinalWrite = 0;
122 sInFile = sOutFile = NULL;
123 sprintf( sReadCmd, "read" );
124 sprintf( sWriteCmd, "write" );
125
126 Extra_UtilGetoptReset();
127 while ((c = Extra_UtilGetopt(argc, argv, "dm:l:c:q:C:Q:S:hf:F:o:st:T:xb")) != EOF) {
128 switch(c) {
129
130 case 'd':
131 enable_dbg_outs ^= 1;
132 break;
133
134 case 'm': {
135 #ifndef WIN32
136 int maxMb = atoi(globalUtilOptarg);
137 printf("Limiting memory use to %d MB\n", maxMb);
138 struct rlimit limit = {
139 maxMb * (1llu << 20), /* soft limit */
140 maxMb * (1llu << 20) /* hard limit */
141 };
142 setrlimit(RLIMIT_AS, &limit);
143 #endif
144 break;
145 }
146 case 'l': {
147 #ifndef WIN32
148 int maxTime = atoi(globalUtilOptarg);
149 printf("Limiting time to %d seconds\n", maxTime);
150 struct rlimit limit = {
151 maxTime, /* soft limit */
152 maxTime /* hard limit */
153 };
154 setrlimit(RLIMIT_CPU, &limit);
155 #endif
156 break;
157 }
158 case 'c':
159 if( Vec_StrSize(sCommandUsr) > 0 )
160 {
161 Vec_StrAppend(sCommandUsr, " ; ");
162 }
163 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
164 fBatch = BATCH;
165 break;
166
167 case 'q':
168 if( Vec_StrSize(sCommandUsr) > 0 )
169 {
170 Vec_StrAppend(sCommandUsr, " ; ");
171 }
172 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
173 fBatch = BATCH_QUIET;
174 break;
175
176 case 'Q':
177 if( Vec_StrSize(sCommandUsr) > 0 )
178 {
179 Vec_StrAppend(sCommandUsr, " ; ");
180 }
181 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
182 fBatch = BATCH_QUIET_THEN_INTERACTIVE;
183 break;
184
185 case 'C':
186 if( Vec_StrSize(sCommandUsr) > 0 )
187 {
188 Vec_StrAppend(sCommandUsr, " ; ");
189 }
190 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
191 fBatch = BATCH_THEN_INTERACTIVE;
192 break;
193
194 case 'S':
195 if( Vec_StrSize(sCommandUsr) > 0 )
196 {
197 Vec_StrAppend(sCommandUsr, " ; ");
198 }
199 Vec_StrAppend(sCommandUsr, globalUtilOptarg );
200 fBatch = BATCH_SMT;
201 break;
202
203 case 'f':
204 if( Vec_StrSize(sCommandUsr) > 0 )
205 {
206 Vec_StrAppend(sCommandUsr, " ; ");
207 }
208 Vec_StrPrintF(sCommandUsr, "source %s", globalUtilOptarg );
209 fBatch = BATCH;
210 break;
211
212 case 'F':
213 if( Vec_StrSize(sCommandUsr) > 0 )
214 {
215 Vec_StrAppend(sCommandUsr, " ; ");
216 }
217 Vec_StrPrintF(sCommandUsr, "source -x %s", globalUtilOptarg );
218 fBatch = BATCH;
219 break;
220
221 case 'h':
222 goto usage;
223 break;
224
225 case 'o':
226 sOutFile = globalUtilOptarg;
227 fFinalWrite = 1;
228 break;
229
230 case 's':
231 fInitSource = 0;
232 break;
233
234 case 't':
235 if ( TypeCheck( pAbc, globalUtilOptarg ) )
236 {
237 if ( (!strcmp(globalUtilOptarg, "none")) == 0 )
238 {
239 fInitRead = 1;
240 sprintf( sReadCmd, "read_%s", globalUtilOptarg );
241 }
242 }
243 else {
244 goto usage;
245 }
246 fBatch = BATCH;
247 break;
248
249 case 'T':
250 if ( TypeCheck( pAbc, globalUtilOptarg ) )
251 {
252 if ( (!strcmp(globalUtilOptarg, "none")) == 0)
253 {
254 fFinalWrite = 1;
255 sprintf( sWriteCmd, "write_%s", globalUtilOptarg);
256 }
257 }
258 else {
259 goto usage;
260 }
261 fBatch = BATCH;
262 break;
263
264 case 'x':
265 fFinalWrite = 0;
266 fInitRead = 0;
267 fBatch = BATCH;
268 break;
269
270 case 'b':
271 Abc_FrameSetBridgeMode();
272 break;
273
274 default:
275 goto usage;
276 }
277 }
278
279 Vec_StrPush(sCommandUsr, '\0');
280
281 if ( fBatch == BATCH_SMT )
282 {
283 Wlc_StdinProcessSmt( pAbc, Vec_StrArray(sCommandUsr) );
284 Abc_Stop();
285 return 0;
286 }
287
288 if ( Abc_FrameIsBridgeMode() )
289 {
290 extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit );
291 pAbc->pGia = Gia_ManFromBridge( stdin, NULL );
292 }
293 else if ( fBatch!=INTERACTIVE && fBatch!=BATCH_QUIET && fBatch!=BATCH_QUIET_THEN_INTERACTIVE && Vec_StrSize(sCommandUsr)>0 )
294 Abc_Print( 1, "ABC command line: \"%s\".\n\n", Vec_StrArray(sCommandUsr) );
295
296 if ( fBatch!=INTERACTIVE )
297 {
298 pAbc->fBatchMode = 1;
299
300 if (argc - globalUtilOptind == 0)
301 {
302 sInFile = NULL;
303 }
304 else if (argc - globalUtilOptind == 1)
305 {
306 fInitRead = 1;
307 sInFile = argv[globalUtilOptind];
308 }
309 else
310 {
311 Abc_UtilsPrintUsage( pAbc, argv[0] );
312 }
313
314 // source the resource file
315 if ( fInitSource )
316 {
317 Abc_UtilsSource( pAbc );
318 }
319
320 fStatus = 0;
321 if ( fInitRead && sInFile )
322 {
323 sprintf( sCommandTmp, "%s %s", sReadCmd, sInFile );
324 fStatus = Cmd_CommandExecute( pAbc, sCommandTmp );
325 }
326
327 if ( fStatus == 0 )
328 {
329 /* cmd line contains `source <file>' */
330 fStatus = Cmd_CommandExecute( pAbc, Vec_StrArray(sCommandUsr) );
331 if ( (fStatus == 0 || fStatus == -1) && fFinalWrite && sOutFile )
332 {
333 sprintf( sCommandTmp, "%s %s", sWriteCmd, sOutFile );
334 fStatus = Cmd_CommandExecute( pAbc, sCommandTmp );
335 }
336 }
337
338 if (fBatch == BATCH_THEN_INTERACTIVE || fBatch == BATCH_QUIET_THEN_INTERACTIVE){
339 fBatch = INTERACTIVE;
340 pAbc->fBatchMode = 0;
341 }
342 }
343
344 Vec_StrFreeP(&sCommandUsr);
345
346 if ( fBatch==INTERACTIVE )
347 {
348 // start interactive mode
349
350 // print the hello line
351 Abc_UtilsPrintHello( pAbc );
352 // print history of the recent commands
353 Cmd_HistoryPrint( pAbc, 10 );
354
355 // source the resource file
356 if ( fInitSource )
357 {
358 Abc_UtilsSource( pAbc );
359 }
360
361 // execute commands given by the user
362 while ( !feof(stdin) )
363 {
364 // print command line prompt and
365 // get the command from the user
366 sCommand = Abc_UtilsGetUsersInput( pAbc );
367
368 // execute the user's command
369 fStatus = Cmd_CommandExecute( pAbc, sCommand );
370
371 // stop if the user quitted or an error occurred
372 if ( fStatus == -1 || fStatus == -2 )
373 break;
374 }
375 }
376
377 // if the memory should be freed, quit packages
378 // if ( fStatus < 0 )
379 {
380 Abc_Stop();
381 }
382 return 0;
383
384 usage:
385 Abc_UtilsPrintHello( pAbc );
386 Abc_UtilsPrintUsage( pAbc, argv[0] );
387 return 1;
388 }
389
390 /**Function********************************************************************
391
392 Synopsis [Returns 1 if s is a file type recognized, else returns 0.]
393
394 Description [Returns 1 if s is a file type recognized by ABC, else returns 0.
395 Recognized types are "blif", "bench", "pla", and "none".]
396
397 SideEffects []
398
399 ******************************************************************************/
TypeCheck(Abc_Frame_t * pAbc,const char * s)400 static int TypeCheck( Abc_Frame_t * pAbc, const char * s )
401 {
402 if (strcmp(s, "blif") == 0)
403 return 1;
404 else if (strcmp(s, "bench") == 0)
405 return 1;
406 else if (strcmp(s, "pla") == 0)
407 return 1;
408 else if (strcmp(s, "none") == 0)
409 return 1;
410 else {
411 fprintf( pAbc->Err, "unknown type %s\n", s );
412 return 0;
413 }
414 }
415
416
417
418
419 ////////////////////////////////////////////////////////////////////////
420 /// END OF FILE ///
421 ////////////////////////////////////////////////////////////////////////
422
423
424 ABC_NAMESPACE_IMPL_END
425