ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
io.c
Go to the documentation of this file.
1
20
21#include "ioAbc.h"
22#include "base/main/mainInt.h"
23#include "aig/saig/saig.h"
24#include "proof/abs/abs.h"
25#include "sat/bmc/bmc.h"
26
27#ifdef WIN32
28#include <process.h>
29#define unlink _unlink
30#else
31#include <unistd.h>
32#endif
33
34ABC_NAMESPACE_IMPL_START
35
39
40static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
41static int IoCommandReadAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
42static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
43static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
44static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
45static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
46static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
47static int IoCommandReadCex ( Abc_Frame_t * pAbc, int argc, char **argv );
48static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv );
49static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
50static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
51static int IoCommandReadFins ( Abc_Frame_t * pAbc, int argc, char **argv );
52static int IoCommandReadInit ( Abc_Frame_t * pAbc, int argc, char **argv );
53static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
54static int IoCommandReadPlaMo ( Abc_Frame_t * pAbc, int argc, char **argv );
55static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
56static int IoCommandReadCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
57static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
58static int IoCommandReadStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
59static int IoCommandReadGig ( Abc_Frame_t * pAbc, int argc, char **argv );
60static int IoCommandReadJson ( Abc_Frame_t * pAbc, int argc, char **argv );
61static int IoCommandReadSF ( Abc_Frame_t * pAbc, int argc, char **argv );
62static int IoCommandReadRom ( Abc_Frame_t * pAbc, int argc, char **argv );
63static int IoCommandReadMM ( Abc_Frame_t * pAbc, int argc, char **argv );
64static int IoCommandReadMMGia ( Abc_Frame_t * pAbc, int argc, char **argv );
65
66static int IoCommandWrite ( Abc_Frame_t * pAbc, int argc, char **argv );
67static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv );
68static int IoCommandWriteAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
69static int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv );
70static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
71static int IoCommandWriteBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
72static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
73static int IoCommandWriteEdgelist( Abc_Frame_t * pAbc, int argc, char **argv );
74static int IoCommandWriteBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
75static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
76static int IoCommandWriteBook ( Abc_Frame_t * pAbc, int argc, char **argv );
77static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv );
78static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
79static int IoCommandWriteCnf2 ( Abc_Frame_t * pAbc, int argc, char **argv );
80static int IoCommandWriteCex ( Abc_Frame_t * pAbc, int argc, char **argv );
81static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv );
82static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
83static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv );
84static int IoCommandWriteHMetis ( Abc_Frame_t * pAbc, int argc, char **argv );
85static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv );
86static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
87static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
88static int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv );
89static int IoCommandWriteTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
90static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv );
91static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
92static int IoCommandWriteSmv ( Abc_Frame_t * pAbc, int argc, char **argv );
93static int IoCommandWriteJson ( Abc_Frame_t * pAbc, int argc, char **argv );
94static int IoCommandWriteResub ( Abc_Frame_t * pAbc, int argc, char **argv );
95static int IoCommandWriteMM ( Abc_Frame_t * pAbc, int argc, char **argv );
96static int IoCommandWriteMMGia ( Abc_Frame_t * pAbc, int argc, char **argv );
97
98extern void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk );
99
100extern int glo_fMapped;
101
105
117void Io_Init( Abc_Frame_t * pAbc )
118{
119 Cmd_CommandAdd( pAbc, "I/O", "read", IoCommandRead, 1 );
120 Cmd_CommandAdd( pAbc, "I/O", "read_aiger", IoCommandReadAiger, 1 );
121 Cmd_CommandAdd( pAbc, "I/O", "read_baf", IoCommandReadBaf, 1 );
122 Cmd_CommandAdd( pAbc, "I/O", "read_bblif", IoCommandReadBblif, 1 );
123 Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
124 Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 );
125 Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
126 Cmd_CommandAdd( pAbc, "I/O", "read_cex", IoCommandReadCex, 1 );
127 Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 );
128 Cmd_CommandAdd( pAbc, "I/O", "read_formula", IoCommandReadDsd, 1 );
129// Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
130 Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
131 Cmd_CommandAdd( pAbc, "I/O", "read_fins", IoCommandReadFins, 0 );
132 Cmd_CommandAdd( pAbc, "I/O", "read_init", IoCommandReadInit, 1 );
133 Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
134 Cmd_CommandAdd( pAbc, "I/O", "read_plamo", IoCommandReadPlaMo, 1 );
135 Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 );
136 Cmd_CommandAdd( pAbc, "I/O", "read_cnf", IoCommandReadCnf, 1 );
137 Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
138 Cmd_CommandAdd( pAbc, "I/O", "read_status", IoCommandReadStatus, 0 );
139 Cmd_CommandAdd( pAbc, "I/O", "&read_gig", IoCommandReadGig, 0 );
140 Cmd_CommandAdd( pAbc, "I/O", "read_json", IoCommandReadJson, 0 );
141 Cmd_CommandAdd( pAbc, "I/O", "read_sf", IoCommandReadSF, 0 );
142 Cmd_CommandAdd( pAbc, "I/O", "read_rom", IoCommandReadRom, 1 );
143 Cmd_CommandAdd( pAbc, "I/O", "read_mm", IoCommandReadMM, 1 );
144 Cmd_CommandAdd( pAbc, "I/O", "&read_mm", IoCommandReadMMGia, 1 );
145
146 Cmd_CommandAdd( pAbc, "I/O", "write", IoCommandWrite, 0 );
147 Cmd_CommandAdd( pAbc, "I/O", "write_hie", IoCommandWriteHie, 0 );
148 Cmd_CommandAdd( pAbc, "I/O", "write_aiger", IoCommandWriteAiger, 0 );
149 Cmd_CommandAdd( pAbc, "I/O", "write_aiger_cex", IoCommandWriteAigerCex, 0 );
150 Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 );
151 Cmd_CommandAdd( pAbc, "I/O", "write_bblif", IoCommandWriteBblif, 0 );
152 Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
153 Cmd_CommandAdd( pAbc, "I/O", "write_blif_mv", IoCommandWriteBlifMv, 0 );
154 Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
155 Cmd_CommandAdd( pAbc, "I/O", "write_book", IoCommandWriteBook, 0 );
156 Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
157 Cmd_CommandAdd( pAbc, "I/O", "write_cex", IoCommandWriteCex, 0 );
158 Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 );
159 Cmd_CommandAdd( pAbc, "I/O", "&write_cnf", IoCommandWriteCnf2, 0 );
160 Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 );
161 Cmd_CommandAdd( pAbc, "I/O", "write_eqn", IoCommandWriteEqn, 0 );
162 Cmd_CommandAdd( pAbc, "I/O", "write_edgelist",IoCommandWriteEdgelist, 0 );
163 Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 );
164// Cmd_CommandAdd( pAbc, "I/O", "write_list", IoCommandWriteList, 0 );
165 Cmd_CommandAdd( pAbc, "I/O", "write_hmetis", IoCommandWriteHMetis, 0 );
166 Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
167 Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
168// Cmd_CommandAdd( pAbc, "I/O", "write_verlib", IoCommandWriteVerLib, 0 );
169 Cmd_CommandAdd( pAbc, "I/O", "write_sorter_cnf", IoCommandWriteSortCnf, 0 );
170 Cmd_CommandAdd( pAbc, "I/O", "write_truth", IoCommandWriteTruth, 0 );
171 Cmd_CommandAdd( pAbc, "I/O", "&write_truth", IoCommandWriteTruths, 0 );
172 Cmd_CommandAdd( pAbc, "I/O", "&write_truths", IoCommandWriteTruths, 0 );
173 Cmd_CommandAdd( pAbc, "I/O", "write_status", IoCommandWriteStatus, 0 );
174 Cmd_CommandAdd( pAbc, "I/O", "write_smv", IoCommandWriteSmv, 0 );
175 Cmd_CommandAdd( pAbc, "I/O", "write_json", IoCommandWriteJson, 0 );
176 Cmd_CommandAdd( pAbc, "I/O", "&write_resub", IoCommandWriteResub, 0 );
177 Cmd_CommandAdd( pAbc, "I/O", "write_mm", IoCommandWriteMM, 0 );
178 Cmd_CommandAdd( pAbc, "I/O", "&write_mm", IoCommandWriteMMGia, 0 );
179}
180
192void Io_End( Abc_Frame_t * pAbc )
193{
194}
195
207int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
208{
209 char Command[1000];
210 Abc_Ntk_t * pNtk;
211 char * pFileName, * pTemp;
212 int c, fCheck, fBarBufs, fReadGia;
213
214 fCheck = 1;
215 fBarBufs = 0;
216 fReadGia = 0;
217 glo_fMapped = 0;
218 Extra_UtilGetoptReset();
219 while ( ( c = Extra_UtilGetopt( argc, argv, "mcbgh" ) ) != EOF )
220 {
221 switch ( c )
222 {
223 case 'm':
224 glo_fMapped ^= 1;
225 break;
226 case 'c':
227 fCheck ^= 1;
228 break;
229 case 'b':
230 fBarBufs ^= 1;
231 break;
232 case 'g':
233 fReadGia ^= 1;
234 break;
235 case 'h':
236 goto usage;
237 default:
238 goto usage;
239 }
240 }
241 if ( argc != globalUtilOptind + 1 )
242 goto usage;
243 // get the input file name
244 pFileName = argv[globalUtilOptind];
245 // fix the wrong symbol
246 for ( pTemp = pFileName; *pTemp; pTemp++ )
247 if ( *pTemp == '>' || *pTemp == '\\' )
248 *pTemp = '/';
249 // read libraries
250 Command[0] = 0;
251 assert( strlen(pFileName) < 900 );
252 if ( !strcmp( Extra_FileNameExtension(pFileName), "genlib" ) )
253 sprintf( Command, "read_genlib %s", pFileName );
254 else if ( !strcmp( Extra_FileNameExtension(pFileName), "lib" ) )
255 sprintf( Command, "read_lib %s", pFileName );
256 else if ( !strcmp( Extra_FileNameExtension(pFileName), "scl" ) )
257 sprintf( Command, "read_scl %s", pFileName );
258 else if ( !strcmp( Extra_FileNameExtension(pFileName), "super" ) )
259 sprintf( Command, "read_super %s", pFileName );
260 else if ( !strcmp( Extra_FileNameExtension(pFileName), "constr" ) )
261 sprintf( Command, "read_constr %s", pFileName );
262 else if ( !strcmp( Extra_FileNameExtension(pFileName), "c" ) )
263 sprintf( Command, "so %s", pFileName );
264 else if ( !strcmp( Extra_FileNameExtension(pFileName), "script" ) )
265 sprintf( Command, "so %s", pFileName );
266 else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) )
267 sprintf( Command, "dsd_load %s", pFileName );
268 if ( Command[0] )
269 {
270 Cmd_CommandExecute( pAbc, Command );
271 return 0;
272 }
273 if ( fReadGia )
274 {
275 Abc_Ntk_t * pNtk = Io_ReadNetlist( pFileName, Io_ReadFileType(pFileName), fCheck );
276 if ( pNtk )
277 {
278 Gia_Man_t * pGia = Abc_NtkFlattenHierarchyGia( pNtk, NULL, 0 );
279 Abc_NtkDelete( pNtk );
280 if ( pGia == NULL )
281 {
282 Abc_Print( 1, "Abc_CommandBlast(): Bit-blasting has failed.\n" );
283 return 0;
284 }
285 Abc_FrameUpdateGia( pAbc, pGia );
286 }
287 return 0;
288 }
289 // check if the library is available
290 if ( glo_fMapped && Abc_FrameReadLibGen() == NULL )
291 {
292 Abc_Print( 1, "Cannot read mapped design when the library is not given.\n" );
293 return 0;
294 }
295 // read the file using the corresponding file reader
296 if ( strstr(pFileName, ".") && !strcmp(strstr(pFileName, "."), ".s") )
297 {
298 char Command[1000];
299 assert( strlen(pFileName) < 980 );
300 sprintf( Command, "source -x %s", pFileName );
301 if ( Cmd_CommandExecute( pAbc, Command ) )
302 {
303 fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
304 return 1;
305 }
306 return 0;
307 }
308 pNtk = Io_Read( pFileName, Io_ReadFileType(pFileName), fCheck, fBarBufs );
309 if ( pNtk == NULL )
310 return 0;
311 if ( Abc_NtkPiNum(pNtk) == 0 )
312 {
313 Abc_Print( 0, "The new network has no primary inputs. It is recommended\n" );
314 Abc_Print( 1, "to add a dummy PI to make sure all commands work correctly.\n" );
315 }
316 // replace the current network
317 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
318 Abc_FrameCopyLTLDataBase( pAbc, pNtk );
319 Abc_FrameClearVerifStatus( pAbc );
320 return 0;
321
322usage:
323 fprintf( pAbc->Err, "usage: read [-mcbgh] <file>\n" );
324 fprintf( pAbc->Err, "\t replaces the current network by the network read from <file>\n" );
325 fprintf( pAbc->Err, "\t by calling the parser that matches the extension of <file>\n" );
326 fprintf( pAbc->Err, "\t (to read a hierarchical design, use \"read_hie\")\n" );
327 fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
328 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
329 fprintf( pAbc->Err, "\t-b : toggle reading barrier buffers [default = %s]\n", fBarBufs? "yes":"no" );
330 fprintf( pAbc->Err, "\t-g : toggle reading and flattening into &-space [default = %s]\n", fBarBufs? "yes":"no" );
331 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
332 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
333 return 1;
334}
335
347int IoCommandReadAiger( Abc_Frame_t * pAbc, int argc, char ** argv )
348{
349 Abc_Ntk_t * pNtk;
350 char * pFileName;
351 int fCheck;
352 int c;
353
354 fCheck = 1;
355 Extra_UtilGetoptReset();
356 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
357 {
358 switch ( c )
359 {
360 case 'c':
361 fCheck ^= 1;
362 break;
363 case 'h':
364 goto usage;
365 default:
366 goto usage;
367 }
368 }
369 if ( argc != globalUtilOptind + 1 )
370 goto usage;
371 // get the input file name
372 pFileName = argv[globalUtilOptind];
373 // read the file using the corresponding file reader
374 pNtk = Io_Read( pFileName, IO_FILE_AIGER, fCheck, 0 );
375 if ( pNtk == NULL )
376 return 1;
377 // replace the current network
378 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
379 Abc_FrameClearVerifStatus( pAbc );
380 return 0;
381
382usage:
383 fprintf( pAbc->Err, "usage: read_aiger [-ch] <file>\n" );
384 fprintf( pAbc->Err, "\t reads the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
385 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
386 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
387 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
388 return 1;
389}
390
402int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
403{
404 Abc_Ntk_t * pNtk;
405 char * pFileName;
406 int fCheck;
407 int c;
408
409 fCheck = 1;
410 Extra_UtilGetoptReset();
411 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
412 {
413 switch ( c )
414 {
415 case 'c':
416 fCheck ^= 1;
417 break;
418 case 'h':
419 goto usage;
420 default:
421 goto usage;
422 }
423 }
424 if ( argc != globalUtilOptind + 1 )
425 goto usage;
426 // get the input file name
427 pFileName = argv[globalUtilOptind];
428 // read the file using the corresponding file reader
429 pNtk = Io_Read( pFileName, IO_FILE_BAF, fCheck, 0 );
430 if ( pNtk == NULL )
431 return 1;
432 // replace the current network
433 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
434 Abc_FrameClearVerifStatus( pAbc );
435 return 0;
436
437usage:
438 fprintf( pAbc->Err, "usage: read_baf [-ch] <file>\n" );
439 fprintf( pAbc->Err, "\t reads the network in Binary Aig Format (BAF)\n" );
440 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
441 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
442 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
443 return 1;
444}
445
457int IoCommandReadBblif( Abc_Frame_t * pAbc, int argc, char ** argv )
458{
459 Abc_Ntk_t * pNtk;
460 char * pFileName;
461 int fCheck;
462 int c;
463
464 fCheck = 1;
465 Extra_UtilGetoptReset();
466 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
467 {
468 switch ( c )
469 {
470 case 'c':
471 fCheck ^= 1;
472 break;
473 case 'h':
474 goto usage;
475 default:
476 goto usage;
477 }
478 }
479 if ( argc != globalUtilOptind + 1 )
480 goto usage;
481 // get the input file name
482 pFileName = argv[globalUtilOptind];
483 // read the file using the corresponding file reader
484 pNtk = Io_Read( pFileName, IO_FILE_BBLIF, fCheck, 0 );
485 if ( pNtk == NULL )
486 return 1;
487 // replace the current network
488 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
489 Abc_FrameClearVerifStatus( pAbc );
490 return 0;
491
492usage:
493 fprintf( pAbc->Err, "usage: read_bblif [-ch] <file>\n" );
494 fprintf( pAbc->Err, "\t reads the network in a binary BLIF format\n" );
495 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
496 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
497 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
498 return 1;
499}
500
512int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
513{
514 Abc_Ntk_t * pNtk;
515 char * pFileName;
516 int fReadAsAig;
517 int fCheck;
518 int fUseNewParser;
519 int fSaveNames;
520 int c;
521 extern Abc_Ntk_t * Io_ReadBlifAsAig( char * pFileName, int fCheck );
522
523 fCheck = 1;
524 fReadAsAig = 0;
525 fUseNewParser = 1;
526 fSaveNames = 0;
527 Extra_UtilGetoptReset();
528 while ( ( c = Extra_UtilGetopt( argc, argv, "nmach" ) ) != EOF )
529 {
530 switch ( c )
531 {
532 case 'n':
533 fUseNewParser ^= 1;
534 break;
535 case 'm':
536 fSaveNames ^= 1;
537 break;
538 case 'a':
539 fReadAsAig ^= 1;
540 break;
541 case 'c':
542 fCheck ^= 1;
543 break;
544 case 'h':
545 goto usage;
546 default:
547 goto usage;
548 }
549 }
550 if ( argc != globalUtilOptind + 1 )
551 goto usage;
552 // get the input file name
553 pFileName = argv[globalUtilOptind];
554 // read the file using the corresponding file reader
555 if ( fReadAsAig )
556 pNtk = Io_ReadBlifAsAig( pFileName, fCheck );
557 else if ( fUseNewParser )
558 pNtk = Io_Read( pFileName, IO_FILE_BLIF, fCheck, 0 );
559 else
560 {
561 Abc_Ntk_t * pTemp;
562 pNtk = Io_ReadBlif( pFileName, fCheck );
563 if ( pNtk == NULL )
564 return 1;
565 if ( fSaveNames )
566 Abc_NtkStartNameIds( pNtk );
567 pNtk = Abc_NtkToLogic( pTemp = pNtk );
568 if ( fSaveNames )
569 Abc_NtkTransferNameIds( pTemp, pNtk );
570 Abc_NtkDelete( pTemp );
571 }
572
573 if ( pNtk == NULL )
574 return 1;
575 // replace the current network
576 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
577 Abc_FrameClearVerifStatus( pAbc );
578 return 0;
579
580usage:
581 fprintf( pAbc->Err, "usage: read_blif [-nmach] <file>\n" );
582 fprintf( pAbc->Err, "\t reads the network in binary BLIF format\n" );
583 fprintf( pAbc->Err, "\t (if this command does not work, try \"read\")\n" );
584 fprintf( pAbc->Err, "\t-n : toggle using old BLIF parser without hierarchy support [default = %s]\n", !fUseNewParser? "yes":"no" );
585 fprintf( pAbc->Err, "\t-m : toggle saving original circuit names into a file [default = %s]\n", fSaveNames? "yes":"no" );
586 fprintf( pAbc->Err, "\t-a : toggle creating AIG while reading the file [default = %s]\n", fReadAsAig? "yes":"no" );
587 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
588 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
589 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
590 return 1;
591}
592
604int IoCommandReadBlifMv( Abc_Frame_t * pAbc, int argc, char ** argv )
605{
606 Abc_Ntk_t * pNtk;
607 char * pFileName;
608 int fCheck;
609 int c;
610
611 fCheck = 1;
612 Extra_UtilGetoptReset();
613 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
614 {
615 switch ( c )
616 {
617 case 'c':
618 fCheck ^= 1;
619 break;
620 case 'h':
621 goto usage;
622 default:
623 goto usage;
624 }
625 }
626 if ( argc != globalUtilOptind + 1 )
627 goto usage;
628 // get the input file name
629 pFileName = argv[globalUtilOptind];
630 // read the file using the corresponding file reader
631 pNtk = Io_Read( pFileName, IO_FILE_BLIFMV, fCheck, 0 );
632 if ( pNtk == NULL )
633 return 1;
634 // replace the current network
635 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
636 Abc_FrameClearVerifStatus( pAbc );
637 return 0;
638
639usage:
640 fprintf( pAbc->Err, "usage: read_blif_mv [-ch] <file>\n" );
641 fprintf( pAbc->Err, "\t reads the network in BLIF-MV format\n" );
642 fprintf( pAbc->Err, "\t (if this command does not work, try \"read\")\n" );
643 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
644 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
645 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
646 return 1;
647}
648
660int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
661{
662 Abc_Ntk_t * pNtk;
663 char * pFileName;
664 int fCheck;
665 int c;
666
667 fCheck = 1;
668 Extra_UtilGetoptReset();
669 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
670 {
671 switch ( c )
672 {
673 case 'c':
674 fCheck ^= 1;
675 break;
676 case 'h':
677 goto usage;
678 default:
679 goto usage;
680 }
681 }
682 if ( argc != globalUtilOptind + 1 )
683 goto usage;
684 // get the input file name
685 pFileName = argv[globalUtilOptind];
686 // read the file using the corresponding file reader
687 pNtk = Io_Read( pFileName, IO_FILE_BENCH, fCheck, 0 );
688 if ( pNtk == NULL )
689 return 1;
690 // replace the current network
691 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
692 Abc_FrameClearVerifStatus( pAbc );
693 return 0;
694
695usage:
696 fprintf( pAbc->Err, "usage: read_bench [-ch] <file>\n" );
697 fprintf( pAbc->Err, "\t reads the network in BENCH format\n" );
698 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
699 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
700 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
701 return 1;
702}
703
715int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, Abc_Cex_t ** ppCexCare, int * pnFrames, int * fOldFormat, int xMode )
716{
717 FILE * pFile;
718 Abc_Cex_t * pCex;
719 Abc_Cex_t * pCexCare;
720 Vec_Int_t * vNums;
721 int c, nRegs = -1, nFrames = -1;
722 pFile = fopen( pFileName, "r" );
723 if ( pFile == NULL )
724 {
725 printf( "Cannot open log file for reading \"%s\".\n" , pFileName );
726 return -1;
727 }
728
729 vNums = Vec_IntAlloc( 100 );
730 int usedX = 0;
731 *fOldFormat = 0;
732
733 int MaxLine = 1000000;
734 char *Buffer;
735 int BufferLen = 0;
736 int state = 0;
737 int iPo = 0;
738 nFrames = -1;
739 int status = 0;
740 int i;
741 int nRegsNtk = 0;
742 Abc_Obj_t * pObj;
743 Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++;
744
745 Buffer = ABC_ALLOC( char, MaxLine );
746 while ( fgets( Buffer, MaxLine, pFile ) != NULL )
747 {
748 if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' )
749 continue;
750 BufferLen = strlen(Buffer) - 1;
751 Buffer[BufferLen] = '\0';
752 if (state==0 && BufferLen>1) {
753 // old format detected
754 *fOldFormat = 1;
755 state = 2;
756 iPo = 0;
757 status = 1;
758 }
759 if (state==1 && Buffer[0]!='b' && Buffer[0]!='j') {
760 // old format detected, first line was actually register
761 *fOldFormat = 1;
762 state = 3;
763 Vec_IntPush( vNums, status );
764 status = 1;
765 }
766 if (Buffer[0] == '.' )
767 break;
768 switch(state) {
769 case 0 :
770 {
771 char c = Buffer[0];
772 if ( c == '0' || c == '1' || c == '2' ) {
773 status = c - '0' ;
774 state = 1;
775 } else if ( c == 'x' ) {
776 // old format with one x state latch
777 usedX = 1;
778 // set to 2 so we can Abc_LatchSetInitNone
779 // acts like 0 when setting bits
780 Vec_IntPush( vNums, 2 );
781 nRegs = Vec_IntSize(vNums);
782 state = 3;
783 } else {
784 printf( "ERROR: Bad aiger status line.\n" );
785 return -1;
786 }
787 }
788 break;
789 case 1 :
790 iPo = atoi(Buffer+1);
791 state = 2;
792 break;
793 case 2 :
794 for (i=0; i<BufferLen;i++) {
795 char c = Buffer[i];
796 if ( c == '0' || c == '1' )
797 Vec_IntPush( vNums, c - '0' );
798 else if ( c == 'x') {
799 usedX = 1;
800 // set to 2 so we can Abc_LatchSetInitNone
801 // acts like 0 when setting bits
802 Vec_IntPush( vNums, 2 );
803 }
804 }
805 nRegs = Vec_IntSize(vNums);
806 if ( nRegs < nRegsNtk )
807 {
808 printf( "WARNING: Register number is smaller than in Ntk. Appending.\n" );
809 for (i=0; i<nRegsNtk-nRegs;i++) {
810 Vec_IntPush( vNums, 0 );
811 }
812 nRegs = Vec_IntSize(vNums);
813 }
814 else if ( nRegs > nRegsNtk )
815 {
816 printf( "WARNING: Register number is larger than in Ntk. Truncating.\n" );
817 Vec_IntShrink( vNums, nRegsNtk );
818 nRegs = nRegsNtk;
819 }
820 state = 3;
821 break;
822 default:
823 for (i=0; i<BufferLen;i++) {
824 char c = Buffer[i];
825 if ( c == '0' || c == '1' )
826 Vec_IntPush( vNums, c - '0' );
827 else if ( c == 'x') {
828 usedX = 1;
829 Vec_IntPush( vNums, 2 );
830 }
831 }
832 nFrames++;
833 break;
834 }
835 }
836 fclose( pFile );
837
838 if (usedX && !xMode)
839 printf( "Warning: Using 0 instead of x in latches or primary inputs\n" );
840 int iFrameCex = nFrames;
841 if ( nRegs < 0 )
842 {
843 if (status == 0 || *fOldFormat == 0)
844 printf( "Counter-example is not available.\n" );
845 else
846 printf( "ERROR: Cannot read register number.\n" );
847 Vec_IntFree( vNums );
848 return -1;
849 }
850 if ( nRegs != nRegsNtk )
851 {
852 printf( "ERROR: Register number not coresponding to Ntk.\n" );
853 Vec_IntFree( vNums );
854 return -1;
855 }
856 if ( Vec_IntSize(vNums)-nRegs == 0 )
857 {
858 printf( "ERROR: Cannot read counter example.\n" );
859 Vec_IntFree( vNums );
860 return -1;
861 }
862 if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 )
863 {
864 printf( "ERROR: Incorrect number of bits.\n" );
865 Vec_IntFree( vNums );
866 return -1;
867 }
868 int nPi = (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1);
869 if ( nPi != Abc_NtkPiNum(pNtk) )
870 {
871 printf( "ERROR: Number of primary inputs not coresponding to Ntk.\n" );
872 Vec_IntFree( vNums );
873 return -1;
874 }
875 if ( iPo >= Abc_NtkPoNum(pNtk) )
876 {
877 printf( "WARNING: PO that failed verification not coresponding to Ntk, using first PO instead.\n" );
878 iPo = 0;
879 }
880 Abc_NtkForEachLatch( pNtk, pObj, i ) {
881 if ( Vec_IntEntry(vNums, i) == 1 )
882 Abc_LatchSetInit1(pObj);
883 else if ( Vec_IntEntry(vNums, i) == 2 && xMode )
884 Abc_LatchSetInitNone(pObj);
885 else
886 Abc_LatchSetInit0(pObj);
887 }
888
889 pCex = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1 );
890 pCexCare = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1);
891 // the zero-based number of PO, for which verification failed
892 // fails in Bmc_CexVerify if not less than actual number of PO
893 pCex->iPo = iPo;
894 pCexCare->iPo = iPo;
895 // the zero-based number of the time-frame, for which verificaiton failed
896 pCex->iFrame = iFrameCex;
897 pCexCare->iFrame = iFrameCex;
898 assert( Vec_IntSize(vNums) == pCex->nBits );
899 for ( c = 0; c < pCex->nBits; c++ ) {
900 if ( Vec_IntEntry(vNums, c) == 1)
901 {
902 Abc_InfoSetBit( pCex->pData, c );
903 Abc_InfoSetBit( pCexCare->pData, c );
904 }
905 else if ( Vec_IntEntry(vNums, c) == 2 && xMode )
906 {
907 // nothing to set
908 }
909 else
910 Abc_InfoSetBit( pCexCare->pData, c );
911 }
912
913 Vec_IntFree( vNums );
914 Abc_CexFreeP( ppCex );
915 if ( ppCex )
916 *ppCex = pCex;
917 else
918 Abc_CexFree( pCex );
919 Abc_CexFreeP( ppCexCare );
920 if ( ppCexCare )
921 *ppCexCare = pCexCare;
922 else
923 Abc_CexFree( pCexCare );
924
925 if ( pnFrames )
926 *pnFrames = nFrames;
927 return status;
928}
929
941
942
943int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv )
944{
945 Abc_Ntk_t * pNtk;
946 Abc_Cex_t * pCex = NULL;
947 Abc_Cex_t * pCexCare = NULL;
948 char * pFileName;
949 FILE * pFile;
950 int fCheck = 1;
951 int fXMode = 0;
952 int c;
953 int fOldFormat = 0;
954 int verified;
955
956 Extra_UtilGetoptReset();
957 while ( ( c = Extra_UtilGetopt( argc, argv, "cxh" ) ) != EOF )
958 {
959 switch ( c )
960 {
961 case 'c':
962 fCheck ^= 1;
963 break;
964 case 'x':
965 fXMode ^= 1;
966 break;
967 case 'h':
968 goto usage;
969 default:
970 goto usage;
971 }
972 }
973 if ( argc != globalUtilOptind + 1 )
974 goto usage;
975
976 // get the input file name
977 pFileName = argv[globalUtilOptind];
978 if ( (pFile = fopen( pFileName, "r" )) == NULL )
979 {
980 fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
981 return 1;
982 }
983 fclose( pFile );
984
985 pNtk = pAbc->pNtkCur;
986 if ( pNtk == NULL )
987 {
988 fprintf( pAbc->Out, "Empty network.\n" );
989 return 0;
990 }
991 Abc_FrameClearVerifStatus( pAbc );
992 pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pCex, &pCexCare, &pAbc->nFrames, &fOldFormat, fXMode);
993 if ( fOldFormat && !fCheck )
994 printf( "WARNING: Old witness format detected and checking is disabled. Reading might have failed.\n" );
995
996 if ( fCheck && pAbc->Status==1) {
997 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
998 Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
999
1000 verified = Bmc_CexCareVerify( pAig, pCex, pCexCare, false );
1001 if (!verified)
1002 {
1003 printf( "Checking CEX for any PO.\n" );
1004 int verified = Bmc_CexCareVerifyAnyPo( pAig, pCex, pCexCare, false );
1005 Aig_ManStop( pAig );
1006 if (verified < 0)
1007 {
1008 Abc_CexFreeP(&pCex);
1009 Abc_CexFreeP(&pCexCare);
1010 return 1;
1011 }
1012 pAbc->pCex->iPo = verified;
1013 }
1014
1015 Abc_CexFreeP(&pCexCare);
1016 Abc_FrameReplaceCex( pAbc, &pCex );
1017 }
1018 return 0;
1019
1020usage:
1021 fprintf( pAbc->Err, "usage: read_cex [-ch] <file>\n" );
1022 fprintf( pAbc->Err, "\t reads the witness cex\n" );
1023 fprintf( pAbc->Err, "\t-c : toggle check after reading [default = %s]\n", fCheck? "yes":"no" );
1024 fprintf( pAbc->Err, "\t-x : read x bits for verification [default = %s]\n", fXMode? "yes":"no" );
1025 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1026 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1027 return 1;
1028}
1040int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
1041{
1042 Abc_Ntk_t * pNtk;
1043 char * pString;
1044 int fCheck;
1045 int c;
1046 extern Abc_Ntk_t * Io_ReadDsd( char * pFormula );
1047
1048 fCheck = 1;
1049 Extra_UtilGetoptReset();
1050 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
1051 {
1052 switch ( c )
1053 {
1054 case 'c':
1055 fCheck ^= 1;
1056 break;
1057 case 'h':
1058 goto usage;
1059 default:
1060 goto usage;
1061 }
1062 }
1063 if ( argc != globalUtilOptind + 1 )
1064 goto usage;
1065 // get the input file name
1066 pString = argv[globalUtilOptind];
1067 // read the file using the corresponding file reader
1068 pNtk = Io_ReadDsd( pString );
1069 if ( pNtk == NULL )
1070 return 1;
1071 // replace the current network
1072 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1073 Abc_FrameClearVerifStatus( pAbc );
1074 return 0;
1075
1076usage:
1077 fprintf( pAbc->Err, "usage: read_dsd [-h] <formula>\n" );
1078 fprintf( pAbc->Err, "\t parses a formula representing DSD of a function\n" );
1079 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1080 fprintf( pAbc->Err, "\tformula : the formula representing disjoint-support decomposition (DSD)\n" );
1081 fprintf( pAbc->Err, "\t Example of a formula: !(a*(b+CA(!d,e*f,c))*79B3(g,h,i,k))\n" );
1082 fprintf( pAbc->Err, "\t where \'!\' is an INV, \'*\' is an AND, \'+\' is an XOR, \n" );
1083 fprintf( pAbc->Err, "\t CA and 79B3 are hexadecimal representations of truth tables\n" );
1084 fprintf( pAbc->Err, "\t (in this case CA=11001010 is truth table of MUX(Data0,Data1,Ctrl))\n" );
1085 fprintf( pAbc->Err, "\t The lower chars (a,b,c,etc) are reserved for elementary variables.\n" );
1086 fprintf( pAbc->Err, "\t The upper chars (A,B,C,etc) are reserved for hexadecimal digits.\n" );
1087 fprintf( pAbc->Err, "\t No spaces are allowed in formulas. In parentheses, LSB goes first.\n" );
1088 return 1;
1089}
1090
1102int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
1103{
1104 Abc_Ntk_t * pNtk;
1105 char * pFileName;
1106 int fCheck;
1107 int c;
1108
1109 fCheck = 1;
1110 Extra_UtilGetoptReset();
1111 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
1112 {
1113 switch ( c )
1114 {
1115 case 'c':
1116 fCheck ^= 1;
1117 break;
1118 case 'h':
1119 goto usage;
1120 default:
1121 goto usage;
1122 }
1123 }
1124 if ( argc != globalUtilOptind + 1 )
1125 goto usage;
1126 // get the input file name
1127 pFileName = argv[globalUtilOptind];
1128 // read the file using the corresponding file reader
1129 pNtk = Io_Read( pFileName, IO_FILE_EDIF, fCheck, 0 );
1130 if ( pNtk == NULL )
1131 return 1;
1132 // replace the current network
1133 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1134 Abc_FrameClearVerifStatus( pAbc );
1135 return 0;
1136
1137usage:
1138 fprintf( pAbc->Err, "usage: read_edif [-ch] <file>\n" );
1139 fprintf( pAbc->Err, "\t reads the network in EDIF (works only for ISCAS benchmarks)\n" );
1140 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
1141 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1142 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1143 return 1;
1144}
1145
1157int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
1158{
1159 Abc_Ntk_t * pNtk;
1160 char * pFileName;
1161 int fCheck;
1162 int c;
1163
1164 fCheck = 1;
1165 Extra_UtilGetoptReset();
1166 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
1167 {
1168 switch ( c )
1169 {
1170 case 'c':
1171 fCheck ^= 1;
1172 break;
1173 case 'h':
1174 goto usage;
1175 default:
1176 goto usage;
1177 }
1178 }
1179 if ( argc != globalUtilOptind + 1 )
1180 goto usage;
1181 // get the input file name
1182 pFileName = argv[globalUtilOptind];
1183 // read the file using the corresponding file reader
1184 pNtk = Io_Read( pFileName, IO_FILE_EQN, fCheck, 0 );
1185 if ( pNtk == NULL )
1186 return 1;
1187 // replace the current network
1188 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1189 Abc_FrameClearVerifStatus( pAbc );
1190 return 0;
1191
1192usage:
1193 fprintf( pAbc->Err, "usage: read_eqn [-ch] <file>\n" );
1194 fprintf( pAbc->Err, "\t reads the network in equation format\n" );
1195 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
1196 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1197 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1198 return 1;
1199}
1200
1212int IoCommandReadFins( Abc_Frame_t * pAbc, int argc, char ** argv )
1213{
1214 extern Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose );
1215 Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
1216 char * pFileName;
1217 int c, fVerbose = 0;
1218
1219 Extra_UtilGetoptReset();
1220 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1221 {
1222 switch ( c )
1223 {
1224 case 'v':
1225 fVerbose ^= 1;
1226 break;
1227 case 'h':
1228 goto usage;
1229 default:
1230 goto usage;
1231 }
1232 }
1233 if ( argc != globalUtilOptind + 1 )
1234 goto usage;
1235 // get the input file name
1236 pFileName = argv[globalUtilOptind];
1237 // check current network
1238 if ( pNtk == NULL )
1239 {
1240 Abc_Print( -1, "Empty network.\n" );
1241 return 1;
1242 }
1243 // compute information and save it in the network
1244 Vec_IntFreeP( &pNtk->vFins );
1245 pNtk->vFins = Io_ReadFins( pNtk, pFileName, fVerbose );
1246 return 0;
1247
1248usage:
1249 fprintf( pAbc->Err, "usage: read_fins [-vh] <file>\n" );
1250 fprintf( pAbc->Err, "\t reads the network in equation format\n" );
1251 fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
1252 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1253 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1254 return 1;
1255}
1256
1268int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
1269{
1270 FILE * pOut, * pErr;
1271 Abc_Ntk_t * pNtk;
1272 char * pFileName;
1273 int c;
1274
1275 pNtk = Abc_FrameReadNtk(pAbc);
1276 pOut = Abc_FrameReadOut(pAbc);
1277 pErr = Abc_FrameReadErr(pAbc);
1278
1279 Extra_UtilGetoptReset();
1280 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1281 {
1282 switch ( c )
1283 {
1284 case 'h':
1285 goto usage;
1286 default:
1287 goto usage;
1288 }
1289 }
1290 if ( argc != globalUtilOptind && argc != globalUtilOptind + 1 )
1291 goto usage;
1292
1293 if ( pNtk == NULL )
1294 {
1295 fprintf( pErr, "Empty network.\n" );
1296 return 1;
1297 }
1298 // get the input file name
1299 if ( argc == globalUtilOptind + 1 )
1300 pFileName = argv[globalUtilOptind];
1301 else if ( pNtk->pSpec )
1302 pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".init" );
1303 else
1304 {
1305 printf( "File name should be given on the command line.\n" );
1306 return 1;
1307 }
1308
1309 // read the file using the corresponding file reader
1310 pNtk = Abc_NtkDup( pNtk );
1311 Io_ReadBenchInit( pNtk, pFileName );
1312 // replace the current network
1313 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1314 Abc_FrameClearVerifStatus( pAbc );
1315 return 0;
1316
1317usage:
1318 fprintf( pAbc->Err, "usage: read_init [-h] <file>\n" );
1319 fprintf( pAbc->Err, "\t reads initial state of the network in BENCH format\n" );
1320 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1321 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1322 return 1;
1323}
1324
1336int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
1337{
1338 Abc_Ntk_t * pNtk;
1339 char * pFileName;
1340 int c, fZeros = 0, fBoth = 0, fOnDc = 0, fSkipPrepro = 0, fCheck = 1;
1341
1342 Extra_UtilGetoptReset();
1343 while ( ( c = Extra_UtilGetopt( argc, argv, "zbdxch" ) ) != EOF )
1344 {
1345 switch ( c )
1346 {
1347 case 'z':
1348 fZeros ^= 1;
1349 break;
1350 case 'b':
1351 fBoth ^= 1;
1352 break;
1353 case 'd':
1354 fOnDc ^= 1;
1355 break;
1356 case 'x':
1357 fSkipPrepro ^= 1;
1358 break;
1359 case 'c':
1360 fCheck ^= 1;
1361 break;
1362 case 'h':
1363 goto usage;
1364 default:
1365 goto usage;
1366 }
1367 }
1368 if ( argc != globalUtilOptind + 1 )
1369 goto usage;
1370 // get the input file name
1371 pFileName = argv[globalUtilOptind];
1372 // read the file using the corresponding file reader
1373 if ( fZeros || fBoth || fOnDc || fSkipPrepro )
1374 {
1375 Abc_Ntk_t * pTemp;
1376 pNtk = Io_ReadPla( pFileName, fZeros, fBoth, fOnDc, fSkipPrepro, fCheck );
1377 if ( pNtk == NULL )
1378 {
1379 printf( "Reading PLA file has failed.\n" );
1380 return 1;
1381 }
1382 pNtk = Abc_NtkToLogic( pTemp = pNtk );
1383 Abc_NtkDelete( pTemp );
1384 }
1385 else
1386 pNtk = Io_Read( pFileName, IO_FILE_PLA, fCheck, 0 );
1387 if ( pNtk == NULL )
1388 return 1;
1389 // replace the current network
1390 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1391 Abc_FrameClearVerifStatus( pAbc );
1392 return 0;
1393
1394usage:
1395 fprintf( pAbc->Err, "usage: read_pla [-zbdxch] <file>\n" );
1396 fprintf( pAbc->Err, "\t reads the network in PLA\n" );
1397 fprintf( pAbc->Err, "\t-z : toggle reading on-set and off-set [default = %s]\n", fZeros? "off-set":"on-set" );
1398 fprintf( pAbc->Err, "\t-b : toggle reading both on-set and off-set as on-set [default = %s]\n", fBoth? "off-set":"on-set" );
1399 fprintf( pAbc->Err, "\t-d : toggle reading both on-set and dc-set as on-set [default = %s]\n", fOnDc? "off-set":"on-set" );
1400 fprintf( pAbc->Err, "\t-x : toggle reading Exclusive SOP rather than SOP [default = %s]\n", fSkipPrepro? "yes":"no" );
1401 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
1402 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1403 fprintf( pAbc->Err, "\tfile : the name of a file to read\n\n" );
1404 fprintf( pAbc->Err, "\t Please note that the PLA parser is somewhat slow for large SOPs.\n" );
1405 fprintf( pAbc->Err, "\t On the other hand, BLIF parser reads a 3M SOP and converts it into a 7.5K AIG in 1 sec:\n" );
1406 fprintf( pAbc->Err, "\t abc 16> read test.blif; ps; bdd -s; ps; muxes; strash; ps\n" );
1407 fprintf( pAbc->Err, "\t test : i/o = 25/ 1 lat = 0 nd = 1 edge = 25 cube = 2910537 lev = 1\n" );
1408 fprintf( pAbc->Err, "\t test : i/o = 25/ 1 lat = 0 nd = 1 edge = 25 bdd = 2937 lev = 1\n" );
1409 fprintf( pAbc->Err, "\t test : i/o = 25/ 1 lat = 0 and = 7514 lev = 48\n" );
1410 fprintf( pAbc->Err, "\t abc 19> time\n" );
1411 fprintf( pAbc->Err, "\t elapse: 1.05 seconds, total: 1.05 seconds\n" );
1412 return 1;
1413}
1414
1426int IoCommandReadPlaMo( Abc_Frame_t * pAbc, int argc, char ** argv )
1427{
1428 extern Abc_Ntk_t * Mop_ManTest( char * pFileName, int fMerge, int fVerbose );
1429 Abc_Ntk_t * pNtk;
1430 int c, fMerge = 0, fVerbose = 0;
1431 Extra_UtilGetoptReset();
1432 while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
1433 {
1434 switch ( c )
1435 {
1436 case 'm':
1437 fMerge ^= 1;
1438 break;
1439 case 'v':
1440 fVerbose ^= 1;
1441 break;
1442 case 'h':
1443 goto usage;
1444 default:
1445 goto usage;
1446 }
1447 }
1448 if ( argc != globalUtilOptind + 1 )
1449 goto usage;
1450 // get the input file name
1451 pNtk = Mop_ManTest( argv[globalUtilOptind], fMerge, fVerbose );
1452 if ( pNtk == NULL )
1453 return 1;
1454 // replace the current network
1455 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1456 Abc_FrameClearVerifStatus( pAbc );
1457 return 0;
1458
1459usage:
1460 fprintf( pAbc->Err, "usage: read_plamo [-mvh] <file>\n" );
1461 fprintf( pAbc->Err, "\t reads the network in multi-output PLA\n" );
1462 fprintf( pAbc->Err, "\t-m : toggle dist-1 merge for cubes with identical outputs [default = %s]\n", fMerge? "yes":"no" );
1463 fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes":"no" );
1464 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1465 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1466 return 1;
1467}
1468
1480int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
1481{
1482 Abc_Ntk_t * pNtk;
1483 char * pStr = NULL;
1484 Vec_Ptr_t * vSops;
1485 int fHex = 1;
1486 int fFile = 0;
1487 int c;
1488
1489 Extra_UtilGetoptReset();
1490 while ( ( c = Extra_UtilGetopt( argc, argv, "xfh" ) ) != EOF )
1491 {
1492 switch ( c )
1493 {
1494 case 'x':
1495 fHex ^= 1;
1496 break;
1497 case 'f':
1498 fFile ^= 1;
1499 break;
1500 case 'h':
1501 goto usage;
1502 default:
1503 goto usage;
1504 }
1505 }
1506
1507 if ( argc != globalUtilOptind + 1 )
1508 goto usage;
1509
1510 if ( fFile )
1511 {
1512 FILE * pFile = fopen( argv[globalUtilOptind], "rb" );
1513 if ( pFile == NULL )
1514 {
1515 printf( "The file \"%s\" cannot be found.\n", argv[globalUtilOptind] );
1516 return 1;
1517 }
1518 else
1519 fclose( pFile );
1520 pStr = Extra_FileReadContents( argv[globalUtilOptind] );
1521 }
1522 else
1523 pStr = argv[globalUtilOptind];
1524
1525 // convert truth table to SOP
1526 if ( fHex )
1527 vSops = Abc_SopFromTruthsHex(pStr);
1528 else
1529 vSops = Abc_SopFromTruthsBin(pStr);
1530 if ( fFile )
1531 ABC_FREE( pStr );
1532 if ( Vec_PtrSize(vSops) == 0 )
1533 {
1534 Vec_PtrFreeFree( vSops );
1535 fprintf( pAbc->Err, "Reading truth table has failed.\n" );
1536 return 1;
1537 }
1538
1539 pNtk = Abc_NtkCreateWithNodes( vSops );
1540 Vec_PtrFreeFree( vSops );
1541 if ( pNtk == NULL )
1542 {
1543 fprintf( pAbc->Err, "Deriving the network has failed.\n" );
1544 return 1;
1545 }
1546 // replace the current network
1547 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1548 Abc_FrameClearVerifStatus( pAbc );
1549 return 0;
1550
1551usage:
1552 fprintf( pAbc->Err, "usage: read_truth [-xfh] <truth> <file>\n" );
1553 fprintf( pAbc->Err, "\t creates network with node(s) having given truth table(s)\n" );
1554 fprintf( pAbc->Err, "\t-x : toggles between bin and hex notation [default = %s]\n", fHex? "hex":"bin" );
1555 fprintf( pAbc->Err, "\t-f : toggles reading truth table(s) from file [default = %s]\n", fFile? "yes": "no" );
1556 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1557 fprintf( pAbc->Err, "\ttruth : truth table with most significant bit first (e.g. 1000 for AND(a,b))\n" );
1558 fprintf( pAbc->Err, "\tfile : file name with the truth table\n" );
1559 return 1;
1560}
1561
1573int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv )
1574{
1575 extern Vec_Ptr_t * Io_FileReadCnf( char * pFileName, int fMulti );
1576 FILE * pFile;
1577 Abc_Ntk_t * pNtk;
1578 Vec_Ptr_t * vSops;
1579 int fMulti = 0;
1580 int c;
1581
1582 Extra_UtilGetoptReset();
1583 while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
1584 {
1585 switch ( c )
1586 {
1587 case 'm':
1588 fMulti ^= 1;
1589 break;
1590 case 'h':
1591 goto usage;
1592 default:
1593 goto usage;
1594 }
1595 }
1596
1597 if ( argc != globalUtilOptind + 1 )
1598 goto usage;
1599
1600 pFile = fopen( argv[globalUtilOptind], "rb" );
1601 if ( pFile == NULL )
1602 {
1603 printf( "The file \"%s\" cannot be found.\n", argv[globalUtilOptind] );
1604 return 1;
1605 }
1606 else
1607 fclose( pFile );
1608 vSops = Io_FileReadCnf( argv[globalUtilOptind], fMulti );
1609 if ( Vec_PtrSize(vSops) == 0 )
1610 {
1611 Vec_PtrFreeFree( vSops );
1612 fprintf( pAbc->Err, "Reading CNF file has failed.\n" );
1613 return 1;
1614 }
1615 pNtk = Abc_NtkCreateWithNodes( vSops );
1616 Vec_PtrFreeFree( vSops );
1617 if ( pNtk == NULL )
1618 {
1619 fprintf( pAbc->Err, "Deriving the network has failed.\n" );
1620 return 1;
1621 }
1622 // replace the current network
1623 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1624 Abc_FrameClearVerifStatus( pAbc );
1625 return 0;
1626
1627usage:
1628 fprintf( pAbc->Err, "usage: read_cnf [-mh] <file>\n" );
1629 fprintf( pAbc->Err, "\t creates network with one node\n" );
1630 fprintf( pAbc->Err, "\t-m : toggles generating multi-output network [default = %s]\n", fMulti? "yes":"no" );
1631 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1632 fprintf( pAbc->Err, "\tfile : file name with the truth table\n" );
1633 return 1;
1634}
1635
1647int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
1648{
1649 Abc_Ntk_t * pNtk;
1650 char * pFileName;
1651 int fCheck, fBarBufs;
1652 int c;
1653
1654 fCheck = 1;
1655 fBarBufs = 0;
1656 glo_fMapped = 0;
1657 Extra_UtilGetoptReset();
1658 while ( ( c = Extra_UtilGetopt( argc, argv, "mcbh" ) ) != EOF )
1659 {
1660 switch ( c )
1661 {
1662 case 'm':
1663 glo_fMapped ^= 1;
1664 break;
1665 case 'c':
1666 fCheck ^= 1;
1667 break;
1668 case 'b':
1669 fBarBufs ^= 1;
1670 break;
1671 case 'h':
1672 goto usage;
1673 default:
1674 goto usage;
1675 }
1676 }
1677 if ( argc != globalUtilOptind + 1 )
1678 goto usage;
1679 // get the input file name
1680 pFileName = argv[globalUtilOptind];
1681 // read the file using the corresponding file reader
1682 pNtk = Io_Read( pFileName, IO_FILE_VERILOG, fCheck, fBarBufs );
1683 if ( pNtk == NULL )
1684 return 1;
1685 // replace the current network
1686 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1687 Abc_FrameClearVerifStatus( pAbc );
1688 return 0;
1689
1690usage:
1691 fprintf( pAbc->Err, "usage: read_verilog [-mcbh] <file>\n" );
1692 fprintf( pAbc->Err, "\t reads the network in Verilog (IWLS 2002/2005 subset)\n" );
1693 fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
1694 fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
1695 fprintf( pAbc->Err, "\t-b : toggle reading barrier buffers [default = %s]\n", fBarBufs? "yes":"no" );
1696 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1697 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1698 return 1;
1699}
1700
1712int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
1713{
1714 char * pFileName;
1715 FILE * pFile;
1716 int c;
1717 extern int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames );
1718
1719 Extra_UtilGetoptReset();
1720 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1721 {
1722 switch ( c )
1723 {
1724 case 'h':
1725 goto usage;
1726 default:
1727 goto usage;
1728 }
1729 }
1730 if ( argc != globalUtilOptind + 1 )
1731 {
1732 goto usage;
1733 }
1734
1735 // get the input file name
1736 pFileName = argv[globalUtilOptind];
1737 if ( (pFile = fopen( pFileName, "r" )) == NULL )
1738 {
1739 fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
1740 return 1;
1741 }
1742 fclose( pFile );
1743
1744 // set the new network
1745 Abc_FrameClearVerifStatus( pAbc );
1746 pAbc->Status = Abc_NtkReadLogFile( pFileName, &pAbc->pCex, &pAbc->nFrames );
1747 return 0;
1748
1749usage:
1750 fprintf( pAbc->Err, "usage: read_status [-ch] <file>\n" );
1751 fprintf( pAbc->Err, "\t reads verification log file\n" );
1752 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1753 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1754 return 1;
1755}
1756
1768int IoCommandReadGig( Abc_Frame_t * pAbc, int argc, char ** argv )
1769{
1770 extern Gia_Man_t * Gia_ManReadGig( char * pFileName );
1771 Gia_Man_t * pAig;
1772 char * pFileName;
1773 FILE * pFile;
1774 int c;
1775
1776 Extra_UtilGetoptReset();
1777 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1778 {
1779 switch ( c )
1780 {
1781 case 'h':
1782 goto usage;
1783 default:
1784 goto usage;
1785 }
1786 }
1787 if ( argc != globalUtilOptind + 1 )
1788 {
1789 goto usage;
1790 }
1791
1792 // get the input file name
1793 pFileName = argv[globalUtilOptind];
1794 if ( (pFile = fopen( pFileName, "r" )) == NULL )
1795 {
1796 fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
1797 return 1;
1798 }
1799 fclose( pFile );
1800
1801 // set the new network
1802 pAig = Gia_ManReadGig( pFileName );
1803 Abc_FrameUpdateGia( pAbc, pAig );
1804 return 0;
1805
1806usage:
1807 fprintf( pAbc->Err, "usage: &read_gig [-h] <file>\n" );
1808 fprintf( pAbc->Err, "\t reads design in GIG format\n" );
1809 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1810 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1811 return 1;
1812}
1813
1825int IoCommandReadJson( Abc_Frame_t * pAbc, int argc, char ** argv )
1826{
1827 extern Vec_Wec_t * Json_Read( char * pFileName, Abc_Nam_t ** ppStrs );
1828 Vec_Wec_t * vObjs;
1829 Abc_Nam_t * pStrs;
1830 char * pFileName;
1831 FILE * pFile;
1832 int c;
1833
1834 Extra_UtilGetoptReset();
1835 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1836 {
1837 switch ( c )
1838 {
1839 case 'h':
1840 goto usage;
1841 default:
1842 goto usage;
1843 }
1844 }
1845 if ( argc != globalUtilOptind + 1 )
1846 {
1847 goto usage;
1848 }
1849
1850 // get the input file name
1851 pFileName = argv[globalUtilOptind];
1852 if ( (pFile = fopen( pFileName, "r" )) == NULL )
1853 {
1854 fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
1855 return 1;
1856 }
1857 fclose( pFile );
1858
1859 // set the new network
1860 vObjs = Json_Read( pFileName, &pStrs );
1861 if ( vObjs == NULL )
1862 return 0;
1863 Abc_FrameSetJsonStrs( pStrs );
1864 Abc_FrameSetJsonObjs( vObjs );
1865 return 0;
1866
1867usage:
1868 fprintf( pAbc->Err, "usage: read_json [-h] <file>\n" );
1869 fprintf( pAbc->Err, "\t reads file in JSON format\n" );
1870 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1871 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1872 return 1;
1873}
1874
1886int IoCommandReadSF( Abc_Frame_t * pAbc, int argc, char ** argv )
1887{
1888 extern void Io_TransformSF2PLA( char * pNameIn, char * pNameOut );
1889
1890 Abc_Ntk_t * pNtk;
1891 FILE * pFile;
1892 char * pFileName, * pFileTemp = "_temp_sf_.pla";
1893 int c;
1894
1895 Extra_UtilGetoptReset();
1896 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1897 {
1898 switch ( c )
1899 {
1900 case 'h':
1901 goto usage;
1902 default:
1903 goto usage;
1904 }
1905 }
1906 if ( argc != globalUtilOptind + 1 )
1907 {
1908 goto usage;
1909 }
1910
1911 // get the input file name
1912 pFileName = argv[globalUtilOptind];
1913 if ( (pFile = fopen( pFileName, "r" )) == NULL )
1914 {
1915 fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
1916 return 1;
1917 }
1918 fclose( pFile );
1919 Io_TransformSF2PLA( pFileName, pFileTemp );
1920 pNtk = Io_Read( pFileTemp, IO_FILE_PLA, 1, 0 );
1921 unlink( pFileTemp );
1922 if ( pNtk == NULL )
1923 return 1;
1924 ABC_FREE( pNtk->pName );
1925 pNtk->pName = Extra_FileNameGeneric( pFileName );
1926 ABC_FREE( pNtk->pSpec );
1927 pNtk->pSpec = Abc_UtilStrsav( pFileName );
1928 // replace the current network
1929 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1930 Abc_FrameClearVerifStatus( pAbc );
1931
1932 return 0;
1933
1934usage:
1935 fprintf( pAbc->Err, "usage: read_sf [-h] <file>\n" );
1936 fprintf( pAbc->Err, "\t reads file in SF format\n" );
1937 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1938 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1939 return 1;
1940}
1941
1942
1954int IoCommandReadRom( Abc_Frame_t * pAbc, int argc, char ** argv )
1955{
1956 extern void Io_TransformROM2PLA( char * pNameIn, char * pNameOut );
1957
1958 Abc_Ntk_t * pNtk;
1959 FILE * pFile;
1960 char * pFileName, * pFileTemp = "_temp_rom_.pla";
1961 int c;
1962
1963 Extra_UtilGetoptReset();
1964 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1965 {
1966 switch ( c )
1967 {
1968 case 'h':
1969 goto usage;
1970 default:
1971 goto usage;
1972 }
1973 }
1974 if ( argc != globalUtilOptind + 1 )
1975 {
1976 goto usage;
1977 }
1978
1979 // get the input file name
1980 pFileName = argv[globalUtilOptind];
1981 if ( (pFile = fopen( pFileName, "r" )) == NULL )
1982 {
1983 fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
1984 return 1;
1985 }
1986 fclose( pFile );
1987 Io_TransformROM2PLA( pFileName, pFileTemp );
1988 pNtk = Io_Read( pFileTemp, IO_FILE_PLA, 1, 0 );
1989 //unlink( pFileTemp );
1990 if ( pNtk == NULL )
1991 return 1;
1992 ABC_FREE( pNtk->pName );
1993 pNtk->pName = Extra_FileNameGeneric( pFileName );
1994 ABC_FREE( pNtk->pSpec );
1995 pNtk->pSpec = Abc_UtilStrsav( pFileName );
1996 // replace the current network
1997 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1998 Abc_FrameClearVerifStatus( pAbc );
1999
2000 return 0;
2001
2002usage:
2003 fprintf( pAbc->Err, "usage: read_rom [-h] <file>\n" );
2004 fprintf( pAbc->Err, "\t reads ROM file\n" );
2005 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
2006 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
2007 return 1;
2008}
2009
2021int IoCommandReadMM( Abc_Frame_t * pAbc, int argc, char ** argv )
2022{
2023 extern Abc_Ntk_t * Abc_NtkReadFromFile( char * pFileName );
2024 Abc_Ntk_t * pNtk; char * pFileName; int c;
2025
2026 Extra_UtilGetoptReset();
2027 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2028 {
2029 switch ( c )
2030 {
2031 case 'h':
2032 goto usage;
2033 default:
2034 goto usage;
2035 }
2036 }
2037 if ( argc != globalUtilOptind + 1 )
2038 goto usage;
2039 pFileName = argv[globalUtilOptind];
2040 pNtk = Abc_NtkReadFromFile( pFileName );
2041 if ( pNtk == NULL )
2042 return 0;
2043 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
2044 Abc_FrameClearVerifStatus( pAbc );
2045 return 0;
2046
2047usage:
2048 fprintf( pAbc->Err, "usage: read_mm [-h] <file>\n" );
2049 fprintf( pAbc->Err, "\t reads mapped network from file\n" );
2050 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
2051 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
2052 return 1;
2053}
2054
2066int IoCommandReadMMGia( Abc_Frame_t * pAbc, int argc, char ** argv )
2067{
2068 extern Abc_Ntk_t * Abc_NtkReadFromFile( char * pFileName );
2069 Abc_Ntk_t * pNtk; char * pFileName; int c;
2070 Gia_Man_t * pGia = NULL;
2071 Extra_UtilGetoptReset();
2072 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2073 {
2074 switch ( c )
2075 {
2076 case 'h':
2077 goto usage;
2078 default:
2079 goto usage;
2080 }
2081 }
2082 if ( argc != globalUtilOptind + 1 )
2083 goto usage;
2084 pFileName = argv[globalUtilOptind];
2085 pNtk = Abc_NtkReadFromFile( pFileName );
2086 if ( pNtk == NULL )
2087 return 0;
2088 Abc_NtkToAig( pNtk );
2089 pGia = Abc_NtkAigToGia( pNtk, 0 );
2090 Abc_NtkDelete( pNtk );
2091 Abc_FrameUpdateGia( pAbc, pGia );
2092 Abc_FrameClearVerifStatus( pAbc );
2093 return 0;
2094
2095usage:
2096 fprintf( pAbc->Err, "usage: &read_mm [-h] <file>\n" );
2097 fprintf( pAbc->Err, "\t reads mapped network from file\n" );
2098 fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
2099 fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
2100 return 1;
2101}
2102
2114int IoCommandWrite( Abc_Frame_t * pAbc, int argc, char **argv )
2115{
2116 char Command[1000];
2117 char * pFileName;
2118 int c;
2119
2120 Extra_UtilGetoptReset();
2121 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2122 {
2123 switch ( c )
2124 {
2125 case 'h':
2126 goto usage;
2127 default:
2128 goto usage;
2129 }
2130 }
2131 if ( argc != globalUtilOptind + 1 )
2132 goto usage;
2133 // get the output file name
2134 pFileName = argv[globalUtilOptind];
2135 // write libraries
2136 Command[0] = 0;
2137 assert( strlen(pFileName) < 900 );
2138 if ( !strcmp( Extra_FileNameExtension(pFileName), "genlib" ) )
2139 sprintf( Command, "write_genlib %s", pFileName );
2140 else if ( !strcmp( Extra_FileNameExtension(pFileName), "lib" ) )
2141 sprintf( Command, "write_lib %s", pFileName );
2142 else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) )
2143 sprintf( Command, "dsd_save %s", pFileName );
2144 if ( Command[0] )
2145 {
2146 Cmd_CommandExecute( pAbc, Command );
2147 return 0;
2148 }
2149 if ( pAbc->pNtkCur == NULL )
2150 {
2151 fprintf( pAbc->Out, "Empty network.\n" );
2152 return 0;
2153 }
2154 // call the corresponding file writer
2155 Io_Write( pAbc->pNtkCur, pFileName, Io_ReadFileType(pFileName) );
2156 return 0;
2157
2158usage:
2159 fprintf( pAbc->Err, "usage: write [-h] <file>\n" );
2160 fprintf( pAbc->Err, "\t writes the current network into <file> by calling\n" );
2161 fprintf( pAbc->Err, "\t the writer that matches the extension of <file>\n" );
2162 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2163 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2164 return 1;
2165}
2166
2178int IoCommandWriteHie( Abc_Frame_t * pAbc, int argc, char **argv )
2179{
2180 char * pBaseName, * pFileName;
2181 int c;
2182
2183 glo_fMapped = 0;
2184 Extra_UtilGetoptReset();
2185 while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
2186 {
2187 switch ( c )
2188 {
2189 case 'm':
2190 glo_fMapped ^= 1;
2191 break;
2192 case 'h':
2193 goto usage;
2194 default:
2195 goto usage;
2196 }
2197 }
2198 if ( pAbc->pNtkCur == NULL )
2199 {
2200 fprintf( pAbc->Out, "Empty network.\n" );
2201 return 0;
2202 }
2203 if ( argc != globalUtilOptind + 2 )
2204 goto usage;
2205 // get the output file name
2206 pBaseName = argv[globalUtilOptind];
2207 pFileName = argv[globalUtilOptind+1];
2208 // call the corresponding file writer
2209// Io_Write( pAbc->pNtkCur, pFileName, Io_ReadFileType(pFileName) );
2210 Io_WriteHie( pAbc->pNtkCur, pBaseName, pFileName );
2211 return 0;
2212
2213usage:
2214 fprintf( pAbc->Err, "usage: write_hie [-h] <orig> <file>\n" );
2215 fprintf( pAbc->Err, "\t writes the current network into <file> by calling\n" );
2216 fprintf( pAbc->Err, "\t the hierarchical writer that matches the extension of <file>\n" );
2217 fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog for <orig> [default = %s]\n", glo_fMapped? "yes":"no" );
2218 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2219 fprintf( pAbc->Err, "\torig : the name of the original file with the hierarchical design\n" );
2220 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2221 return 1;
2222}
2223
2235int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
2236{
2237 char * pFileName;
2238 int fWriteSymbols;
2239 int fCompact;
2240 int fUnique;
2241 int fVerbose;
2242 int c;
2243
2244 fWriteSymbols = 0;
2245 fCompact = 0;
2246 fUnique = 0;
2247 fVerbose = 0;
2248 Extra_UtilGetoptReset();
2249 while ( ( c = Extra_UtilGetopt( argc, argv, "scuvh" ) ) != EOF )
2250 {
2251 switch ( c )
2252 {
2253 case 's':
2254 fWriteSymbols ^= 1;
2255 break;
2256 case 'c':
2257 fCompact ^= 1;
2258 break;
2259 case 'u':
2260 fUnique ^= 1;
2261 break;
2262 case 'v':
2263 fVerbose ^= 1;
2264 break;
2265 case 'h':
2266 goto usage;
2267 default:
2268 goto usage;
2269 }
2270 }
2271 if ( pAbc->pNtkCur == NULL )
2272 {
2273 fprintf( pAbc->Out, "Empty network.\n" );
2274 return 0;
2275 }
2276 if ( argc != globalUtilOptind + 1 )
2277 goto usage;
2278 // get the output file name
2279 pFileName = argv[globalUtilOptind];
2280 // call the corresponding file writer
2281 if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
2282 {
2283 fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
2284 return 1;
2285 }
2286 if ( fUnique )
2287 {
2288 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
2289 extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
2290 Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
2291 Aig_Man_t * pCan = Saig_ManDupIsoCanonical( pAig, fVerbose );
2292 Abc_Ntk_t * pTemp = Abc_NtkFromAigPhase( pCan );
2293 Aig_ManStop( pCan );
2294 Aig_ManStop( pAig );
2295 Io_WriteAiger( pTemp, pFileName, fWriteSymbols, fCompact, fUnique );
2296 Abc_NtkDelete( pTemp );
2297 }
2298 else
2299 Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact, fUnique );
2300 return 0;
2301
2302usage:
2303 fprintf( pAbc->Err, "usage: write_aiger [-scuvh] <file>\n" );
2304 fprintf( pAbc->Err, "\t writes the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
2305 fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
2306 fprintf( pAbc->Err, "\t-c : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" );
2307 fprintf( pAbc->Err, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
2308 fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
2309 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2310 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aig)\n" );
2311 return 1;
2312}
2313
2325int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv )
2326{
2327 char * pFileName;
2328 int c;
2329 Extra_UtilGetoptReset();
2330 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2331 {
2332 switch ( c )
2333 {
2334 case 'h':
2335 goto usage;
2336 default:
2337 goto usage;
2338 }
2339 }
2340 if ( pAbc->pCex == NULL )
2341 {
2342 fprintf( pAbc->Out, "There is no current CEX.\n" );
2343 return 0;
2344 }
2345 if ( argc != globalUtilOptind + 1 )
2346 goto usage;
2347 // get the output file name
2348 pFileName = argv[globalUtilOptind];
2349 Io_WriteAigerCex( pAbc->pCex, pAbc->pNtkCur, pAbc->pGia, pFileName );
2350 return 0;
2351
2352usage:
2353 fprintf( pAbc->Err, "usage: write_aiger_cex [-h] <file>\n" );
2354 fprintf( pAbc->Err, "\t writes the current CEX in the AIGER format (http://fmv.jku.at/aiger)\n" );
2355 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2356 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2357 return 1;
2358}
2359
2371int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
2372{
2373 char * pFileName;
2374 int c;
2375
2376 Extra_UtilGetoptReset();
2377 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2378 {
2379 switch ( c )
2380 {
2381 case 'h':
2382 goto usage;
2383 default:
2384 goto usage;
2385 }
2386 }
2387 if ( pAbc->pNtkCur == NULL )
2388 {
2389 fprintf( pAbc->Out, "Empty network.\n" );
2390 return 0;
2391 }
2392 if ( argc != globalUtilOptind + 1 )
2393 goto usage;
2394 // get the output file name
2395 pFileName = argv[globalUtilOptind];
2396 // call the corresponding file writer
2397 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BAF );
2398 return 0;
2399
2400usage:
2401 fprintf( pAbc->Err, "usage: write_baf [-h] <file>\n" );
2402 fprintf( pAbc->Err, "\t writes the network into a BLIF file\n" );
2403 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2404 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .baf)\n" );
2405 return 1;
2406}
2407
2419int IoCommandWriteBblif( Abc_Frame_t * pAbc, int argc, char **argv )
2420{
2421 char * pFileName;
2422 int c;
2423
2424 Extra_UtilGetoptReset();
2425 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2426 {
2427 switch ( c )
2428 {
2429 case 'h':
2430 goto usage;
2431 default:
2432 goto usage;
2433 }
2434 }
2435 if ( pAbc->pNtkCur == NULL )
2436 {
2437 fprintf( pAbc->Out, "Empty network.\n" );
2438 return 0;
2439 }
2440 if ( argc != globalUtilOptind + 1 )
2441 goto usage;
2442 // get the output file name
2443 pFileName = argv[globalUtilOptind];
2444 // call the corresponding file writer
2445 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BBLIF );
2446 return 0;
2447
2448usage:
2449 fprintf( pAbc->Err, "usage: write_bblif [-h] <file>\n" );
2450 fprintf( pAbc->Err, "\t writes the network into a binary BLIF file\n" );
2451 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2452 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bblif)\n" );
2453 return 1;
2454}
2455
2467int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
2468{
2469 char * pFileName;
2470 char * pLutStruct = NULL;
2471 int c, fSpecial = 0;
2472 int fUseHie = 0;
2473
2474 Extra_UtilGetoptReset();
2475 while ( ( c = Extra_UtilGetopt( argc, argv, "Sjah" ) ) != EOF )
2476 {
2477 switch ( c )
2478 {
2479 case 'S':
2480 if ( globalUtilOptind >= argc )
2481 {
2482 Abc_Print( -1, "Command line switch \"-S\" should be followed by string.\n" );
2483 goto usage;
2484 }
2485 pLutStruct = argv[globalUtilOptind];
2486 globalUtilOptind++;
2487 if ( strlen(pLutStruct) != 2 && strlen(pLutStruct) != 3 )
2488 {
2489 Abc_Print( -1, "Command line switch \"-S\" should be followed by a 2- or 3-char string (e.g. \"44\" or \"555\").\n" );
2490 goto usage;
2491 }
2492 break;
2493 case 'j':
2494 fSpecial ^= 1;
2495 break;
2496 case 'a':
2497 fUseHie ^= 1;
2498 break;
2499 case 'h':
2500 goto usage;
2501 default:
2502 goto usage;
2503 }
2504 }
2505 if ( pAbc->pNtkCur == NULL )
2506 {
2507 fprintf( pAbc->Out, "Empty network.\n" );
2508 return 0;
2509 }
2510 if ( argc != globalUtilOptind + 1 )
2511 goto usage;
2512 // get the output file name
2513 pFileName = argv[globalUtilOptind];
2514 // call the corresponding file writer
2515 if ( fSpecial || pLutStruct )
2516 Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName, pLutStruct, fUseHie );
2517 else
2518 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
2519 return 0;
2520
2521usage:
2522 fprintf( pAbc->Err, "usage: write_blif [-S str] [-jah] <file>\n" );
2523 fprintf( pAbc->Err, "\t writes the network into a BLIF file\n" );
2524 fprintf( pAbc->Err, "\t-S str : string representing the LUT structure [default = %s]\n", pLutStruct ? pLutStruct : "not used" );
2525 fprintf( pAbc->Err, "\t-j : enables special BLIF writing [default = %s]\n", fSpecial? "yes" : "no" );;
2526 fprintf( pAbc->Err, "\t-a : enables hierarchical BLIF writing for LUT structures [default = %s]\n", fUseHie? "yes" : "no" );;
2527 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2528 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
2529 return 1;
2530}
2531
2543int IoCommandWriteBlifMv( Abc_Frame_t * pAbc, int argc, char **argv )
2544{
2545 char * pFileName;
2546 int c;
2547
2548 Extra_UtilGetoptReset();
2549 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2550 {
2551 switch ( c )
2552 {
2553 case 'h':
2554 goto usage;
2555 default:
2556 goto usage;
2557 }
2558 }
2559 if ( pAbc->pNtkCur == NULL )
2560 {
2561 fprintf( pAbc->Out, "Empty network.\n" );
2562 return 0;
2563 }
2564 if ( argc != globalUtilOptind + 1 )
2565 goto usage;
2566 // get the output file name
2567 pFileName = argv[globalUtilOptind];
2568 // call the corresponding file writer
2569 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIFMV );
2570 return 0;
2571
2572usage:
2573 fprintf( pAbc->Err, "usage: write_blif_mv [-h] <file>\n" );
2574 fprintf( pAbc->Err, "\t writes the network into a BLIF-MV file\n" );
2575 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2576 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .mv)\n" );
2577 return 1;
2578}
2579
2591int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
2592{
2593 char * pFileName;
2594 int fUseLuts;
2595 int c;
2596
2597 fUseLuts = 1;
2598 Extra_UtilGetoptReset();
2599 while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
2600 {
2601 switch ( c )
2602 {
2603 case 'l':
2604 fUseLuts ^= 1;
2605 break;
2606 case 'h':
2607 goto usage;
2608 default:
2609 goto usage;
2610 }
2611 }
2612 if ( pAbc->pNtkCur == NULL )
2613 {
2614 fprintf( pAbc->Out, "Empty network.\n" );
2615 return 0;
2616 }
2617 if ( argc != globalUtilOptind + 1 )
2618 goto usage;
2619 // get the output file name
2620 pFileName = argv[globalUtilOptind];
2621 // call the corresponding file writer
2622 if ( !fUseLuts )
2623 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH );
2624 else if ( pAbc->pNtkCur )
2625 {
2626 Abc_Ntk_t * pNtkTemp;
2627 pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
2628 Abc_NtkToAig( pNtkTemp );
2629 Io_WriteBenchLut( pNtkTemp, pFileName );
2630 Abc_NtkDelete( pNtkTemp );
2631 }
2632 else
2633 printf( "There is no current network.\n" );
2634 return 0;
2635
2636usage:
2637 fprintf( pAbc->Err, "usage: write_bench [-lh] <file>\n" );
2638 fprintf( pAbc->Err, "\t writes the network in BENCH format\n" );
2639 fprintf( pAbc->Err, "\t-l : toggle using LUTs in the output [default = %s]\n", fUseLuts? "yes" : "no" );
2640 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2641 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bench)\n" );
2642 return 1;
2643}
2644
2656int IoCommandWriteBook( Abc_Frame_t * pAbc, int argc, char **argv )
2657{
2658 char * pFileName;
2659 int c;
2660 Extra_UtilGetoptReset();
2661 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2662 {
2663 switch ( c )
2664 {
2665 case 'h':
2666 goto usage;
2667 default:
2668 goto usage;
2669 }
2670 }
2671 if ( argc != globalUtilOptind + 1 )
2672 goto usage;
2673 // get the output file name
2674 pFileName = argv[globalUtilOptind];
2675 // call the corresponding file writer
2676 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BOOK );
2677 return 0;
2678
2679usage:
2680 fprintf( pAbc->Err, "usage: write_book [-h] <file> [-options]\n" );
2681 fprintf( pAbc->Err, "\t-h : prints the help massage\n" );
2682 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aux, .nodes, .nets)\n" );
2683 fprintf( pAbc->Err, "\t\n" );
2684 fprintf( pAbc->Err, "\tThis command is developed by Myungchul Kim (University of Michigan).\n" );
2685 return 1;
2686}
2687
2699int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv )
2700{
2701 Abc_Ntk_t * pNtk;
2702 char * pFileName;
2703 int c;
2704 extern void Io_WriteCellNet( Abc_Ntk_t * pNtk, char * pFileName );
2705
2706 Extra_UtilGetoptReset();
2707 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2708 {
2709 switch ( c )
2710 {
2711 case 'h':
2712 goto usage;
2713 default:
2714 goto usage;
2715 }
2716 }
2717 if ( pAbc->pNtkCur == NULL )
2718 {
2719 fprintf( pAbc->Out, "Empty network.\n" );
2720 return 0;
2721 }
2722 if ( argc != globalUtilOptind + 1 )
2723 goto usage;
2724 pNtk = pAbc->pNtkCur;
2725 // get the output file name
2726 pFileName = argv[globalUtilOptind];
2727 // call the corresponding file writer
2728 if ( !Abc_NtkIsLogic(pNtk) )
2729 {
2730 fprintf( pAbc->Out, "The network should be a logic network (if it an AIG, use command \"logic\")\n" );
2731 return 0;
2732 }
2733 Io_WriteCellNet( pNtk, pFileName );
2734 return 0;
2735
2736usage:
2737 fprintf( pAbc->Err, "usage: write_cellnet [-h] <file>\n" );
2738 fprintf( pAbc->Err, "\t writes the network is the cellnet format\n" );
2739 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2740 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2741 return 1;
2742}
2743
2755int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
2756{
2757 char * pFileName;
2758 int c;
2759 int fNewAlgo;
2760 int fFastAlgo;
2761 int fAllPrimes;
2762 int fChangePol;
2763 int fVerbose;
2764 extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose );
2765
2766 fNewAlgo = 1;
2767 fFastAlgo = 0;
2768 fAllPrimes = 0;
2769 fChangePol = 1;
2770 fVerbose = 0;
2771 Extra_UtilGetoptReset();
2772 while ( ( c = Extra_UtilGetopt( argc, argv, "nfpcvh" ) ) != EOF )
2773 {
2774 switch ( c )
2775 {
2776 case 'n':
2777 fNewAlgo ^= 1;
2778 break;
2779 case 'f':
2780 fFastAlgo ^= 1;
2781 break;
2782 case 'p':
2783 fAllPrimes ^= 1;
2784 break;
2785 case 'c':
2786 fChangePol ^= 1;
2787 break;
2788 case 'v':
2789 fVerbose ^= 1;
2790 break;
2791 case 'h':
2792 goto usage;
2793 default:
2794 goto usage;
2795 }
2796 }
2797 if ( pAbc->pNtkCur == NULL )
2798 {
2799 fprintf( pAbc->Out, "Empty network.\n" );
2800 return 0;
2801 }
2802 if ( argc != globalUtilOptind + 1 )
2803 goto usage;
2804 // get the output file name
2805 pFileName = argv[globalUtilOptind];
2806 // check if the feature will be used
2807 if ( Abc_NtkIsStrash(pAbc->pNtkCur) && fAllPrimes )
2808 {
2809 fAllPrimes = 0;
2810 printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
2811 }
2812 // call the corresponding file writer
2813 if ( fFastAlgo )
2814 Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 1, fChangePol, fVerbose );
2815 else if ( fNewAlgo )
2816 Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 0, fChangePol, fVerbose );
2817 else if ( fAllPrimes )
2818 Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 );
2819 else
2820 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF );
2821 return 0;
2822
2823usage:
2824 fprintf( pAbc->Err, "usage: write_cnf [-nfpcvh] <file>\n" );
2825 fprintf( pAbc->Err, "\t generates CNF for the miter (see also \"&write_cnf\")\n" );
2826 fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
2827 fprintf( pAbc->Err, "\t-f : toggle using fast algorithm [default = %s]\n", fFastAlgo? "yes" : "no" );
2828 fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
2829 fprintf( pAbc->Err, "\t-c : toggle adjasting polarity of internal variables [default = %s]\n", fChangePol? "yes" : "no" );
2830 fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
2831 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2832 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2833 return 1;
2834}
2835
2847int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv )
2848{
2849 extern void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int fVerbose );
2850 extern void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
2851 FILE * pFile;
2852 char * pFileName;
2853 int nLutSize = 8;
2854 int fNewAlgo = 1;
2855 int fCnfObjIds = 0;
2856 int fAddOrCla = 1;
2857 int c, fVerbose = 0;
2858 Extra_UtilGetoptReset();
2859 while ( ( c = Extra_UtilGetopt( argc, argv, "Kaiovh" ) ) != EOF )
2860 {
2861 switch ( c )
2862 {
2863 case 'K':
2864 if ( globalUtilOptind >= argc )
2865 {
2866 Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
2867 goto usage;
2868 }
2869 nLutSize = atoi(argv[globalUtilOptind]);
2870 globalUtilOptind++;
2871 break;
2872 case 'a':
2873 fNewAlgo ^= 1;
2874 break;
2875 case 'i':
2876 fCnfObjIds ^= 1;
2877 break;
2878 case 'o':
2879 fAddOrCla ^= 1;
2880 break;
2881 case 'v':
2882 fVerbose ^= 1;
2883 break;
2884 case 'h':
2885 goto usage;
2886 default:
2887 goto usage;
2888 }
2889 }
2890 if ( pAbc->pGia == NULL )
2891 {
2892 Abc_Print( -1, "IoCommandWriteCnf2(): There is no AIG.\n" );
2893 return 1;
2894 }
2895 if ( Gia_ManRegNum(pAbc->pGia) > 0 )
2896 {
2897 Abc_Print( -1, "IoCommandWriteCnf2(): Works only for combinational miters.\n" );
2898 return 0;
2899 }
2900 if ( nLutSize < 3 || nLutSize > 8 )
2901 {
2902 Abc_Print( -1, "IoCommandWriteCnf2(): Invalid LUT size (%d).\n", nLutSize );
2903 return 0;
2904 }
2905 if ( !fNewAlgo && !Sdm_ManCanRead() )
2906 {
2907 Abc_Print( -1, "IoCommandWriteCnf2(): Cannot input precomputed DSD information.\n" );
2908 return 0;
2909 }
2910 if ( argc != globalUtilOptind + 1 )
2911 goto usage;
2912 // get the input file name
2913 pFileName = argv[globalUtilOptind];
2914 pFile = fopen( pFileName, "wb" );
2915 if ( pFile == NULL )
2916 {
2917 printf( "Cannot open file \"%s\" for writing.\n", pFileName );
2918 return 0;
2919 }
2920 fclose( pFile );
2921 if ( fNewAlgo )
2922 Mf_ManDumpCnf( pAbc->pGia, pFileName, nLutSize, fCnfObjIds, fAddOrCla, fVerbose );
2923 else
2924 Jf_ManDumpCnf( pAbc->pGia, pFileName, fVerbose );
2925 return 0;
2926
2927usage:
2928 fprintf( pAbc->Err, "usage: &write_cnf [-Kaiovh] <file>\n" );
2929 fprintf( pAbc->Err, "\t writes CNF produced by a new generator\n" );
2930 fprintf( pAbc->Err, "\t-K <num> : the LUT size (3 <= num <= 8) [default = %d]\n", nLutSize );
2931 fprintf( pAbc->Err, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
2932 fprintf( pAbc->Err, "\t-i : toggle using AIG object IDs as CNF variables [default = %s]\n", fCnfObjIds? "yes" : "no" );
2933 fprintf( pAbc->Err, "\t-o : toggle adding OR clause for the outputs [default = %s]\n", fAddOrCla? "yes" : "no" );
2934 fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
2935 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2936 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2937 fprintf( pAbc->Err, "\n" );
2938 fprintf( pAbc->Err, "\t CNF variable mapping rules:\n" );
2939 fprintf( pAbc->Err, "\n" );
2940 fprintf( pAbc->Err, "\t Assume CNF has N variables, with variable IDs running from 0 to N-1.\n" );
2941 fprintf( pAbc->Err, "\t Variable number 0 is not used in the CNF.\n" );
2942 fprintf( pAbc->Err, "\t Variables 1, 2, 3,... <nPOs> represent POs in their natural order.\n" );
2943 fprintf( pAbc->Err, "\t Variables N-<nPIs>, N-<nPIs>+1, N-<nPIs>+2, ... N-1, represent PIs in their natural order.\n" );
2944 fprintf( pAbc->Err, "\t The internal variables are ordered in a reverse topological order from outputs to inputs.\n" );
2945 fprintf( pAbc->Err, "\t That is, smaller variable IDs tend to be closer to the outputs, while larger\n" );
2946 fprintf( pAbc->Err, "\t variable IDs tend to be closer to the inputs. It was found that this ordering\n" );
2947 fprintf( pAbc->Err, "\t leads to faster SAT solving for hard UNSAT CEC problems.\n" );
2948 return 1;
2949}
2950
2951
2963int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
2964{
2965 char * pFileName;
2966 int c;
2967
2968 Extra_UtilGetoptReset();
2969 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2970 {
2971 switch ( c )
2972 {
2973 case 'h':
2974 goto usage;
2975 default:
2976 goto usage;
2977 }
2978 }
2979 if ( pAbc->pNtkCur == NULL )
2980 {
2981 fprintf( pAbc->Out, "Empty network.\n" );
2982 return 0;
2983 }
2984 if ( argc != globalUtilOptind + 1 )
2985 goto usage;
2986 // get the output file name
2987 pFileName = argv[globalUtilOptind];
2988 // call the corresponding file writer
2989 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_DOT );
2990 return 0;
2991
2992usage:
2993 fprintf( pAbc->Err, "usage: write_dot [-h] <file>\n" );
2994 fprintf( pAbc->Err, "\t writes the current network into a DOT file\n" );
2995 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2996 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2997 return 1;
2998}
2999
3000ABC_NAMESPACE_IMPL_END
3001
3002#include "proof/fra/fra.h"
3003
3004ABC_NAMESPACE_IMPL_START
3005
3006int Abc_NtkCheckSpecialPi( Abc_Ntk_t * pNtk )
3007{
3008 Abc_Obj_t * pObj; int i;
3009 Abc_NtkForEachPi( pNtk, pObj, i )
3010 if ( !strcmp(Abc_ObjName(pObj), "_abc_190121_abc_") )
3011 return 1;
3012 return 0;
3013}
3014
3026void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
3027{
3028 Abc_Cex_t * pCare = NULL; int i, f; Abc_Obj_t * pObj;
3029 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
3030 Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
3031 //fprintf( pFile, "# FALSIFYING OUTPUTS:");
3032 //fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
3033 pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, 0, 0 );
3034 Aig_ManStop( pAig );
3035 if( pCare == NULL )
3036 {
3037 printf( "Counter-example minimization has failed.\n" );
3038 return;
3039 }
3040 // output flop values (unaffected by the minimization)
3041 Abc_NtkForEachLatch( pNtk, pObj, i )
3042 fprintf( pFile, "CEX: %s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
3043 // output PI values (while skipping the minimized ones)
3044 for ( f = 0; f <= pCex->iFrame; f++ )
3045 Abc_NtkForEachPi( pNtk, pObj, i )
3046 if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
3047 fprintf( pFile, "CEX: %s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
3048 Abc_CexFreeP( &pCare );
3049}
3050
3051
3052extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose );
3053extern Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose );
3054extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose );
3055
3056void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
3057 int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo,
3058 int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended )
3059{
3060 Abc_Cex_t * pCare = NULL;
3061 Abc_Obj_t * pObj;
3062 int i, f;
3063 if ( fPrintFull )
3064 {
3065 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
3066 Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
3067 Abc_Cex_t * pCexFull = Saig_ManExtendCex( pAig, pCex );
3068 Aig_ManStop( pAig );
3069 // output PI values (while skipping the minimized ones)
3070 assert( pCexFull->nBits == Abc_NtkCiNum(pNtk) * (pCex->iFrame + 1) );
3071 for ( f = 0; f <= pCex->iFrame; f++ )
3072 Abc_NtkForEachCi( pNtk, pObj, i )
3073 fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) );
3074 Abc_CexFreeP( &pCexFull );
3075 }
3076 else
3077 {
3078 if ( fNames )
3079 {
3080 fprintf( pFile, "# FALSIFYING OUTPUTS:");
3081 fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
3082 }
3083 if ( fMinimize )
3084 {
3085 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
3086 Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
3087 if ( fUseOldMin )
3088 {
3089 pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
3090 if ( fCheckCex )
3091 Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
3092 }
3093 else if ( fUseSatBased )
3094 {
3095 if ( Abc_NtkPoNum( pNtk ) == 1 )
3096 pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
3097 else
3098 printf( "SAT-based CEX minimization requires having a single PO.\n" );
3099 }
3100 else if ( fCexInfo )
3101 {
3102 Gia_Man_t * p = Gia_ManFromAigSimple( pAig );
3103 Abc_Cex_t * pCexImpl = NULL;
3104 Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
3105 Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
3106 Abc_Cex_t * pCexEss;
3107
3108 if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCexCare ) )
3109 printf( "Counter-example care-set verification has failed.\n" );
3110
3111 pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
3112
3113 // pCare is pCexMin from Bmc_CexTest
3114 pCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
3115
3116 if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCare ) )
3117 printf( "Counter-example min-set verification has failed.\n" );
3118 Abc_CexFreeP( &pCexStates );
3119 Abc_CexFreeP( &pCexImpl );
3120 Abc_CexFreeP( &pCexCare );
3121 Abc_CexFreeP( &pCexEss );
3122 }
3123 else
3124 pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose );
3125 Aig_ManStop( pAig );
3126 if(pCare == NULL)
3127 printf( "Counter-example minimization has failed.\n" );
3128 }
3129 if (fNames)
3130 {
3131 fprintf( pFile, "\n");
3132 fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
3133 }
3134 if ( fNames && fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) )
3135 {
3136 int * pValues;
3137 int nXValues = 0, iFlop = 0, iPivotPi = -1;
3138 Abc_NtkForEachPi( pNtk, pObj, iPivotPi )
3139 if ( !strcmp(Abc_ObjName(pObj), "_abc_190121_abc_") )
3140 break;
3141 if ( iPivotPi == Abc_NtkPiNum(pNtk) )
3142 {
3143 fprintf( stdout, "IoCommandWriteCex(): Cannot find special PI required by switch \"-z\".\n" );
3144 return;
3145 }
3146 // count X-valued flops
3147 for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
3148 if ( Abc_ObjName(Abc_NtkPi(pNtk, i))[0] == 'x' )
3149 nXValues++;
3150 // map X-valued flops into auxiliary PIs
3151 pValues = ABC_FALLOC( int, Abc_NtkPiNum(pNtk) );
3152 for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
3153 if ( Abc_ObjName(Abc_NtkPi(pNtk, i))[0] == 'x' )
3154 pValues[i] = iPivotPi - nXValues + iFlop++;
3155 assert( iFlop == nXValues );
3156 // write flop values
3157 for ( i = iPivotPi+1; i < Abc_NtkPiNum(pNtk); i++ )
3158 if ( pValues[i] == -1 )
3159 fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_NtkPi(pNtk, i))+1, Abc_ObjName(Abc_NtkPi(pNtk, i))[0] );
3160 else if ( Abc_InfoHasBit(pCare->pData, pCare->nRegs + pValues[i]) )
3161 fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_NtkPi(pNtk, i))+1, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs + pValues[i]) );
3162 ABC_FREE( pValues );
3163 // output PI values (while skipping the minimized ones)
3164 for ( f = 0; f <= pCex->iFrame; f++ )
3165 Abc_NtkForEachPi( pNtk, pObj, i )
3166 {
3167 if ( i == iPivotPi - nXValues ) break;
3168 if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
3169 fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
3170 }
3171 }
3172 else
3173 {
3174 if (fExtended && fAiger && !fNames) {
3175 fprintf( pFile, "1\n");
3176 fprintf( pFile, "b%d\n", pCex->iPo);
3177 }
3178 // output flop values (unaffected by the minimization)
3179 Abc_NtkForEachLatch( pNtk, pObj, i )
3180 if ( fNames )
3181 fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
3182 else
3183 fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
3184 if ( !fNames && fAiger)
3185 fprintf( pFile, "\n");
3186 // output PI values (while skipping the minimized ones)
3187 for ( f = 0; f <= pCex->iFrame; f++ ) {
3188 Abc_NtkForEachPi( pNtk, pObj, i )
3189 if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
3190 if ( fNames )
3191 fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
3192 else
3193 fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
3194 else if ( !fNames )
3195 fprintf( pFile, "x");
3196 if ( !fNames && fAiger)
3197 fprintf( pFile, "\n");
3198 }
3199 if (fExtended && fAiger && !fNames)
3200 fprintf( pFile, ".\n");
3201 }
3202 Abc_CexFreeP( &pCare );
3203 }
3204}
3205
3217int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
3218{
3219 Abc_Ntk_t * pNtk;
3220 char * pFileName;
3221 int c, fNames = 0;
3222 int fMinimize = 0;
3223 int fUseSatBased = 0;
3224 int fHighEffort = 0;
3225 int fUseOldMin = 0;
3226 int fCheckCex = 0;
3227 int forceSeq = 0;
3228 int fAiger = 0;
3229 int fPrintFull = 0;
3230 int fUseFfNames = 0;
3231 int fVerbose = 0;
3232 int fCexInfo = 0;
3233 int fExtended = 0;
3234
3235 Extra_UtilGetoptReset();
3236 while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvhxt" ) ) != EOF )
3237 {
3238 switch ( c )
3239 {
3240 case 's':
3241 forceSeq ^= 1;
3242 break;
3243 case 'n':
3244 fNames ^= 1;
3245 break;
3246 case 'm':
3247 fMinimize ^= 1;
3248 break;
3249 case 'u':
3250 fUseSatBased ^= 1;
3251 break;
3252 case 'e':
3253 fHighEffort ^= 1;
3254 break;
3255 case 'o':
3256 fUseOldMin ^= 1;
3257 break;
3258 case 'c':
3259 fCheckCex ^= 1;
3260 break;
3261 case 'a':
3262 fAiger ^= 1;
3263 break;
3264 case 'f':
3265 fPrintFull ^= 1;
3266 break;
3267 case 'z':
3268 fUseFfNames ^= 1;
3269 break;
3270 case 'v':
3271 fVerbose ^= 1;
3272 break;
3273 case 'x':
3274 fCexInfo ^= 1;
3275 break;
3276 case 't':
3277 fExtended ^= 1;
3278 break;
3279 case 'h':
3280 goto usage;
3281 default:
3282 goto usage;
3283 }
3284 }
3285 pNtk = pAbc->pNtkCur;
3286 if ( pNtk == NULL )
3287 {
3288 fprintf( pAbc->Out, "Empty network.\n" );
3289 return 0;
3290 }
3291 if ( pNtk->pModel == NULL && pAbc->pCex == NULL && pAbc->vCexVec == NULL )
3292 {
3293 fprintf( pAbc->Out, "Counter-example is not available.\n" );
3294 return 0;
3295 }
3296 if ( argc != globalUtilOptind + 1 )
3297 {
3298 printf( "File name is missing on the command line.\n" );
3299 goto usage;
3300 }
3301
3302 // get the input file name
3303 pFileName = argv[globalUtilOptind];
3304 // write the counter-example into the file
3305 if ( pAbc->pCex || pAbc->vCexVec )
3306 {
3307 Abc_Cex_t * pCex = pAbc->pCex;
3308 FILE * pFile; int i;
3309 /*
3310 Abc_NtkForEachLatch( pNtk, pObj, i )
3311 if ( !Abc_LatchIsInit0(pObj) )
3312 {
3313 fprintf( stdout, "IoCommandWriteCex(): The init-state should be all-0 for counter-example to work.\n" );
3314 fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
3315 return 1;
3316 }
3317 */
3318 pFile = fopen( pFileName, "w" );
3319 if ( pFile == NULL )
3320 {
3321 fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName );
3322 return 1;
3323 }
3324 if ( pAbc->pCex )
3325 {
3326 Abc_NtkDumpOneCex( pFile, pNtk, pCex,
3327 fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo,
3328 fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended );
3329 }
3330 else if ( pAbc->vCexVec )
3331 {
3332 Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pCex, i )
3333 {
3334 if ( pCex == NULL )
3335 continue;
3336 fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i );
3337 Abc_NtkDumpOneCex( pFile, pNtk, pCex,
3338 fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo,
3339 fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended );
3340 }
3341 }
3342 fprintf( pFile, "# DONE\n" );
3343 fclose( pFile );
3344 }
3345 else
3346 {
3347 Abc_Obj_t * pObj;
3348 FILE * pFile = fopen( pFileName, "w" );
3349 int i;
3350 if ( pFile == NULL )
3351 {
3352 fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName );
3353 return 1;
3354 }
3355 if ( fNames )
3356 {
3357 const char *cycle_ctr = forceSeq?"@0":"";
3358 Abc_NtkForEachPi( pNtk, pObj, i )
3359// fprintf( pFile, "%s=%c\n", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
3360 fprintf( pFile, "%s%s=%c\n", Abc_ObjName(pObj), cycle_ctr, '0'+(pNtk->pModel[i]==1) );
3361 }
3362 else
3363 {
3364 Abc_NtkForEachPi( pNtk, pObj, i )
3365 fprintf( pFile, "%c", '0'+(pNtk->pModel[i]==1) );
3366 }
3367 fprintf( pFile, "\n" );
3368 fclose( pFile );
3369 }
3370
3371 return 0;
3372
3373usage:
3374 fprintf( pAbc->Err, "usage: write_cex [-snmueocfzvh] <file>\n" );
3375 fprintf( pAbc->Err, "\t saves counter-example (CEX) derived by \"sat\", \"iprove\", \"dprove\", etc\n" );
3376 fprintf( pAbc->Err, "\t the output file <file> contains values for each PI in natural order\n" );
3377 fprintf( pAbc->Err, "\t-s : always report a sequential CEX (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
3378 fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
3379 fprintf( pAbc->Err, "\t-m : minimize CEX by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
3380 fprintf( pAbc->Err, "\t-u : use fast SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" );
3381 fprintf( pAbc->Err, "\t-e : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" );
3382 fprintf( pAbc->Err, "\t-o : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
3383 fprintf( pAbc->Err, "\t-x : minimize using algorithm from cexinfo command [default = %s]\n", fCexInfo? "yes": "no" );
3384 fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
3385 fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
3386 fprintf( pAbc->Err, "\t-t : extended header info when cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
3387 fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" );
3388 fprintf( pAbc->Err, "\t-z : toggle using saved flop names [default = %s]\n", fUseFfNames? "yes": "no" );
3389 fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s]\n", fVerbose? "yes": "no" );
3390 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3391 fprintf( pAbc->Err, "\t<file> : the name of the file to write\n" );
3392 return 1;
3393}
3394
3406int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
3407{
3408 char * pFileName;
3409 int c;
3410
3411 Extra_UtilGetoptReset();
3412 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
3413 {
3414 switch ( c )
3415 {
3416 case 'h':
3417 goto usage;
3418 default:
3419 goto usage;
3420 }
3421 }
3422 if ( pAbc->pNtkCur == NULL )
3423 {
3424 fprintf( pAbc->Out, "Empty network.\n" );
3425 return 0;
3426 }
3427 if ( argc != globalUtilOptind + 1 )
3428 goto usage;
3429 // get the output file name
3430 pFileName = argv[globalUtilOptind];
3431 // call the corresponding file writer
3432 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_EQN );
3433 return 0;
3434
3435usage:
3436 fprintf( pAbc->Err, "usage: write_eqn [-h] <file>\n" );
3437 fprintf( pAbc->Err, "\t writes the current network in the equation format\n" );
3438 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3439 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
3440 return 1;
3441}
3442
3454int IoCommandWriteEdgelist( Abc_Frame_t * pAbc, int argc, char **argv )
3455{
3456 char * pFileName;
3457 int c, fSpecial = 0;
3458
3459 Extra_UtilGetoptReset();
3460 while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
3461 {
3462 switch ( c )
3463 {
3464 case 'N':
3465 fSpecial ^= 1;
3466 break;
3467 /*
3468 case 'a':
3469 fUseHie ^= 1;
3470 break;
3471 case 'h':
3472 goto usage;
3473 */
3474 default:
3475 goto usage;
3476 }
3477 }
3478 if ( pAbc->pNtkCur == NULL )
3479 {
3480 fprintf( pAbc->Out, "Empty network.\n" );
3481 return 0;
3482 }
3483 if ( argc != globalUtilOptind + 1 )
3484 goto usage;
3485 // get the output file name
3486 pFileName = argv[globalUtilOptind];
3487 // call the corresponding file writer
3488 if ( fSpecial ) // keep original naming
3489 Io_WriteEdgelist( pAbc->pNtkCur, pFileName, 1, 0, 0, fSpecial); //last option is fName
3490 else
3491 Io_WriteEdgelist( pAbc->pNtkCur, pFileName, 1, 0, 0, fSpecial); //last option is fName
3492 return 0;
3493
3494usage:
3495 fprintf( pAbc->Err, "usage: write_edgelist [-N] <file>\n" );
3496 fprintf( pAbc->Err, "\t writes the network into edgelist file\n" );
3497 fprintf( pAbc->Err, "\t part of Verilog-2-PyG (PyTorch Geometric). more details https://github.com/ycunxi/Verilog-to-PyG \n" );
3498 fprintf( pAbc->Err, "\t-N : toggle keeping original naming of the netlist in edgelist (default=False)\n");
3499 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3500 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .el)\n" );
3501 return 1;
3502}
3503
3504
3516int IoCommandWriteHMetis( Abc_Frame_t * pAbc, int argc, char **argv )
3517{
3518 char * pFileName;
3519 int fVerbose;
3520 int fSkipPo;
3521 int fWeightEdges;
3522 int c;
3523
3524 fSkipPo = 1;
3525 fWeightEdges = 0;
3526 fVerbose = 0;
3527 Extra_UtilGetoptReset();
3528 while ( ( c = Extra_UtilGetopt( argc, argv, "swvh" ) ) != EOF )
3529 {
3530 switch ( c )
3531 {
3532 case 's':
3533 fSkipPo ^= 1;
3534 break;
3535 case 'w':
3536 fWeightEdges ^= 1;
3537 break;
3538 case 'v':
3539 fVerbose ^= 1;
3540 break;
3541 case 'h':
3542 goto usage;
3543 default:
3544 goto usage;
3545 }
3546 }
3547 if ( pAbc->pNtkCur == NULL )
3548 {
3549 fprintf( pAbc->Out, "Empty network.\n" );
3550 return 0;
3551 }
3552 if ( argc != globalUtilOptind + 1 )
3553 goto usage;
3554 // get the output file name
3555 pFileName = argv[globalUtilOptind];
3556 // call the corresponding file writer
3557 if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
3558 {
3559 fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
3560 return 1;
3561 }
3562 Io_WriteHMetis( pAbc->pNtkCur, pFileName, fSkipPo, fWeightEdges, fVerbose );
3563 return 0;
3564
3565usage:
3566 fprintf( pAbc->Err, "usage: write_hmetis <file>\n" );
3567 fprintf( pAbc->Err, "\t writes the network in the hMetis format (https://karypis.github.io/glaros/files/sw/hmetis/manual.pdf)\n" );
3568 fprintf( pAbc->Err, "\t-s : skip PO as sink explictly [default = %s]\n", fSkipPo? "yes" : "no" );
3569 fprintf( pAbc->Err, "\t-w : simulate weight on hyperedges [default = %s]\n", fWeightEdges? "yes" : "no" );
3570 fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
3571 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3572 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
3573 return 1;
3574}
3575
3576
3577
3589int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv )
3590{
3591 char * pFileName;
3592 int c;
3593
3594 Extra_UtilGetoptReset();
3595 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
3596 {
3597 switch ( c )
3598 {
3599 case 'h':
3600 goto usage;
3601 default:
3602 goto usage;
3603 }
3604 }
3605 if ( pAbc->pNtkCur == NULL )
3606 {
3607 fprintf( pAbc->Out, "Empty network.\n" );
3608 return 0;
3609 }
3610 if ( argc != globalUtilOptind + 1 )
3611 goto usage;
3612 // get the output file name
3613 pFileName = argv[globalUtilOptind];
3614 // call the corresponding file writer
3615 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_GML );
3616 return 0;
3617
3618usage:
3619 fprintf( pAbc->Err, "usage: write_gml [-h] <file>\n" );
3620 fprintf( pAbc->Err, "\t writes network using graph representation formal GML\n" );
3621 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3622 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
3623 return 1;
3624}
3625
3637int IoCommandWriteList( Abc_Frame_t * pAbc, int argc, char **argv )
3638{
3639 char * pFileName;
3640 int fUseHost;
3641 int c;
3642
3643 printf( "This command currently does not work.\n" );
3644 return 0;
3645
3646 fUseHost = 1;
3647 Extra_UtilGetoptReset();
3648 while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF )
3649 {
3650 switch ( c )
3651 {
3652 case 'n':
3653 fUseHost ^= 1;
3654 break;
3655 case 'h':
3656 goto usage;
3657 default:
3658 goto usage;
3659 }
3660 }
3661 if ( pAbc->pNtkCur == NULL )
3662 {
3663 fprintf( pAbc->Out, "Empty network.\n" );
3664 return 0;
3665 }
3666 if ( argc != globalUtilOptind + 1 )
3667 goto usage;
3668/*
3669 if ( !Abc_NtkIsSeq(pAbc->pNtkCur) )
3670 {
3671 fprintf( stdout, "IoCommandWriteList(): Can write adjacency list for sequential AIGs only.\n" );
3672 return 0;
3673 }
3674*/
3675 // get the input file name
3676 pFileName = argv[globalUtilOptind];
3677 // write the file
3678 Io_WriteList( pAbc->pNtkCur, pFileName, fUseHost );
3679 return 0;
3680
3681usage:
3682 fprintf( pAbc->Err, "usage: write_list [-nh] <file>\n" );
3683 fprintf( pAbc->Err, "\t writes network using graph representation formal GML\n" );
3684 fprintf( pAbc->Err, "\t-n : toggle writing host node [default = %s]\n", fUseHost? "yes":"no" );
3685 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3686 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
3687 return 1;
3688}
3689
3701int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
3702{
3703 extern int Io_WriteMoPlaM( Abc_Ntk_t * pNtk, char * pFileName, int nMints );
3704 char * pFileName;
3705 int c, fUseMoPla = 0, nMints = 0;
3706
3707 Extra_UtilGetoptReset();
3708 while ( ( c = Extra_UtilGetopt( argc, argv, "Mmh" ) ) != EOF )
3709 {
3710 switch ( c )
3711 {
3712 case 'M':
3713 if ( globalUtilOptind >= argc )
3714 {
3715 Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
3716 goto usage;
3717 }
3718 nMints = atoi(argv[globalUtilOptind]);
3719 globalUtilOptind++;
3720 break;
3721 case 'm':
3722 fUseMoPla ^= 1;
3723 break;
3724 case 'h':
3725 goto usage;
3726 default:
3727 goto usage;
3728 }
3729 }
3730 if ( pAbc->pNtkCur == NULL )
3731 {
3732 fprintf( pAbc->Out, "Empty network.\n" );
3733 return 0;
3734 }
3735 if ( argc != globalUtilOptind + 1 )
3736 goto usage;
3737 // get the output file name
3738 pFileName = argv[globalUtilOptind];
3739 // call the corresponding file writer
3740 if ( nMints )
3741 {
3742 if ( Abc_NtkIsBddLogic(pAbc->pNtkCur) )
3743 Io_WriteMoPlaM( pAbc->pNtkCur, pFileName, nMints );
3744 else
3745 {
3746 Abc_Ntk_t * pStrash = Abc_NtkStrash( pAbc->pNtkCur, 0, 0, 0 );
3747 Io_WriteMoPlaM( pStrash, pFileName, nMints );
3748 Abc_NtkDelete( pStrash );
3749 }
3750 }
3751 else
3752 Io_Write( pAbc->pNtkCur, pFileName, fUseMoPla ? IO_FILE_MOPLA : IO_FILE_PLA );
3753 return 0;
3754
3755usage:
3756 fprintf( pAbc->Err, "usage: write_pla [-M <num>] [-mh] <file>\n" );
3757 fprintf( pAbc->Err, "\t writes the collapsed network into a PLA file\n" );
3758 fprintf( pAbc->Err, "\t-M <num> : the number of on-set minterms to write [default = %d]\n", nMints );
3759 fprintf( pAbc->Err, "\t-m : toggle writing multi-output PLA [default = %s]\n", fUseMoPla? "yes":"no" );
3760 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3761 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
3762 return 1;
3763}
3764
3776int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
3777{
3778 extern void Io_WriteVerilogLut( Abc_Ntk_t * pNtk, char * pFileName, int nLutSize, int fFixed, int fNoModules, int fNewInterface );
3779 char * pFileName;
3780 int c, fFixed = 0, fOnlyAnds = 0, fNoModules = 0, fNewInterface = 0;
3781 int nLutSize = -1;
3782
3783 Extra_UtilGetoptReset();
3784 while ( ( c = Extra_UtilGetopt( argc, argv, "Kfamnh" ) ) != EOF )
3785 {
3786 switch ( c )
3787 {
3788 case 'K':
3789 if ( globalUtilOptind >= argc )
3790 {
3791 Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
3792 goto usage;
3793 }
3794 nLutSize = atoi(argv[globalUtilOptind]);
3795 globalUtilOptind++;
3796 if ( nLutSize < 2 || nLutSize > 6 )
3797 goto usage;
3798 break;
3799 case 'f':
3800 fFixed ^= 1;
3801 break;
3802 case 'a':
3803 fOnlyAnds ^= 1;
3804 break;
3805 case 'm':
3806 fNoModules ^= 1;
3807 break;
3808 case 'n':
3809 fNewInterface ^= 1;
3810 break;
3811 case 'h':
3812 goto usage;
3813 default:
3814 goto usage;
3815 }
3816 }
3817 if ( pAbc->pNtkCur == NULL )
3818 {
3819 fprintf( pAbc->Out, "Empty network.\n" );
3820 return 0;
3821 }
3822 if ( argc != globalUtilOptind + 1 )
3823 goto usage;
3824 if ( fFixed )
3825 nLutSize = 6;
3826 // get the output file name
3827 pFileName = argv[globalUtilOptind];
3828 // call the corresponding file writer
3829 if ( nLutSize >= 2 && nLutSize <= 6 )
3830 Io_WriteVerilogLut( pAbc->pNtkCur, pFileName, nLutSize, fFixed, fNoModules, fNewInterface );
3831 else
3832 {
3833 Abc_Ntk_t * pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
3834 if ( !Abc_NtkHasAig(pNtkTemp) && !Abc_NtkHasMapping(pNtkTemp) )
3835 Abc_NtkToAig( pNtkTemp );
3836 Io_WriteVerilog( pNtkTemp, pFileName, fOnlyAnds, fNewInterface );
3837 Abc_NtkDelete( pNtkTemp );
3838 }
3839 return 0;
3840
3841usage:
3842 fprintf( pAbc->Err, "usage: write_verilog [-K num] [-famnh] <file>\n" );
3843 fprintf( pAbc->Err, "\t writes the current network in Verilog format\n" );
3844 fprintf( pAbc->Err, "\t-K num : write the network using instances of K-LUTs (2 <= K <= 6) [default = not used]\n" );
3845 fprintf( pAbc->Err, "\t-f : toggle using fixed format [default = %s]\n", fFixed? "yes":"no" );
3846 fprintf( pAbc->Err, "\t-a : toggle writing expressions with only ANDs (without XORs and MUXes) [default = %s]\n", fOnlyAnds? "yes":"no" );
3847 fprintf( pAbc->Err, "\t-m : toggle writing additional modules [default = %s]\n", !fNoModules? "yes":"no" );
3848 fprintf( pAbc->Err, "\t-n : toggle writing generic PO names and assign-statements [default = %s]\n", fNewInterface? "yes":"no" );
3849 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3850 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
3851 return 1;
3852}
3853
3865int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv )
3866{
3867 char * pFileName;
3868 int c;
3869 int nVars = 16;
3870 int nQueens = 4;
3871 extern void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens );
3872
3873 Extra_UtilGetoptReset();
3874 while ( ( c = Extra_UtilGetopt( argc, argv, "NQh" ) ) != EOF )
3875 {
3876 switch ( c )
3877 {
3878 case 'N':
3879 if ( globalUtilOptind >= argc )
3880 {
3881 fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
3882 goto usage;
3883 }
3884 nVars = atoi(argv[globalUtilOptind]);
3885 globalUtilOptind++;
3886 if ( nVars <= 0 )
3887 goto usage;
3888 break;
3889 case 'Q':
3890 if ( globalUtilOptind >= argc )
3891 {
3892 fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
3893 goto usage;
3894 }
3895 nQueens = atoi(argv[globalUtilOptind]);
3896 globalUtilOptind++;
3897 if ( nQueens <= 0 )
3898 goto usage;
3899 break;
3900 case 'h':
3901 goto usage;
3902 default:
3903 goto usage;
3904 }
3905 }
3906 if ( argc != globalUtilOptind + 1 )
3907 goto usage;
3908 // get the output file name
3909 pFileName = argv[globalUtilOptind];
3910 Abc_NtkWriteSorterCnf( pFileName, nVars, nQueens );
3911 // call the corresponding file writer
3912 return 0;
3913
3914usage:
3915 fprintf( pAbc->Err, "usage: write_sorter_cnf [-N <num>] [-Q <num>] <file>\n" );
3916 fprintf( pAbc->Err, "\t writes CNF for the sorter\n" );
3917 fprintf( pAbc->Err, "\t-N num : the number of sorter bits [default = %d]\n", nVars );
3918 fprintf( pAbc->Err, "\t-Q num : the number of bits to be asserted to 1 [default = %d]\n", nQueens );
3919 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
3920 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
3921 return 1;
3922}
3923
3935int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
3936{
3937 Vec_Int_t * vTruth;
3938 Abc_Ntk_t * pNtk = pAbc->pNtkCur;
3939 Abc_Obj_t * pNode;
3940 char * pFileName;
3941 FILE * pFile;
3942 unsigned * pTruth;
3943 int fHex = 1;
3944 int fReverse = 0;
3945 int c;
3946
3947 Extra_UtilGetoptReset();
3948 while ( ( c = Extra_UtilGetopt( argc, argv, "xrh" ) ) != EOF )
3949 {
3950 switch ( c )
3951 {
3952 case 'x':
3953 fHex ^= 1;
3954 break;
3955 case 'r':
3956 fReverse ^= 1;
3957 break;
3958 case 'h':
3959 goto usage;
3960 default:
3961 goto usage;
3962 }
3963 }
3964 if ( pAbc->pNtkCur == NULL )
3965 {
3966 printf( "Current network is not available.\n" );
3967 return 0;
3968 }
3969 if ( !Abc_NtkIsLogic(pNtk) )
3970 {
3971 printf( "Current network should not an AIG. Run \"logic\".\n" );
3972 return 0;
3973 }
3974 if ( Abc_NtkPoNum(pNtk) != 1 )
3975 {
3976 printf( "Current network should have exactly one primary output.\n" );
3977 return 0;
3978 }
3979 if ( Abc_NtkNodeNum(pNtk) != 1 )
3980 {
3981 printf( "Current network should have exactly one node.\n" );
3982 return 0;
3983 }
3984 pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
3985 if ( Abc_ObjFaninNum(pNode) == 0 )
3986 {
3987 printf( "Can only write logic function with 0 inputs.\n" );
3988 return 0;
3989 }
3990 if ( Abc_ObjFaninNum(pNode) > 16 )
3991 {
3992 printf( "Can only write logic function with no more than 16 inputs.\n" );
3993 return 0;
3994 }
3995 if ( argc != globalUtilOptind + 1 )
3996 goto usage;
3997 // get the input file name
3998 pFileName = argv[globalUtilOptind];
3999 // convert to logic
4000 Abc_NtkToAig( pNtk );
4001 vTruth = Vec_IntAlloc( 0 );
4002 pTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, (Hop_Obj_t *)pNode->pData, Abc_ObjFaninNum(pNode), vTruth, fReverse );
4003 pFile = fopen( pFileName, "w" );
4004 if ( pFile == NULL )
4005 {
4006 Vec_IntFree( vTruth );
4007 printf( "Cannot open file \"%s\" for writing.\n", pFileName );
4008 return 0;
4009 }
4010 if ( fHex )
4011 Extra_PrintHex2( pFile, pTruth, Abc_ObjFaninNum(pNode) );
4012 else
4013 Extra_PrintBinary( pFile, pTruth, 1<<Abc_ObjFaninNum(pNode) );
4014 fclose( pFile );
4015 Vec_IntFree( vTruth );
4016 return 0;
4017
4018usage:
4019 fprintf( pAbc->Err, "usage: write_truth [-xrh] <file>\n" );
4020 fprintf( pAbc->Err, "\t writes truth table into a file\n" );
4021 fprintf( pAbc->Err, "\t-x : toggles between bin and hex representation [default = %s]\n", fHex? "hex":"bin" );
4022 fprintf( pAbc->Err, "\t-r : toggle reversing bits in the truth table [default = %s]\n", fReverse? "yes":"no" );
4023 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
4024 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
4025 return 1;
4026}
4027
4028
4040int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
4041{
4042 Gia_Obj_t * pObj;
4043 char * pFileName;
4044 FILE * pFile;
4045 word * pTruth;
4046 int nBytes;
4047 int fReverse = 0;
4048 int fHex = 1;
4049 int fBinaryFile = 0;
4050 int c, i;
4051
4052 Extra_UtilGetoptReset();
4053 while ( ( c = Extra_UtilGetopt( argc, argv, "rxbh" ) ) != EOF )
4054 {
4055 switch ( c )
4056 {
4057 case 'r':
4058 fReverse ^= 1;
4059 break;
4060 case 'x':
4061 fHex ^= 1;
4062 break;
4063 case 'b':
4064 fBinaryFile ^= 1;
4065 break;
4066 case 'h':
4067 goto usage;
4068 default:
4069 goto usage;
4070 }
4071 }
4072 if ( pAbc->pGia == NULL )
4073 {
4074 Abc_Print( -1, "IoCommandWriteTruths(): There is no AIG.\n" );
4075 return 1;
4076 }
4077 if ( Gia_ManPiNum(pAbc->pGia) > 16 )
4078 {
4079 Abc_Print( -1, "IoCommandWriteTruths(): Can write truth tables up to 16 inputs.\n" );
4080 return 0;
4081 }
4082 if ( Gia_ManPiNum(pAbc->pGia) < 3 )
4083 {
4084 Abc_Print( -1, "IoCommandWriteTruths(): Can write truth tables for 3 inputs or more.\n" );
4085 return 0;
4086 }
4087 if ( argc != globalUtilOptind + 1 )
4088 goto usage;
4089 // get the input file name
4090 pFileName = argv[globalUtilOptind];
4091 // convert to logic
4092 pFile = fopen( pFileName, "wb" );
4093 if ( pFile == NULL )
4094 {
4095 printf( "Cannot open file \"%s\" for writing.\n", pFileName );
4096 return 0;
4097 }
4098 nBytes = 8 * Abc_Truth6WordNum( Gia_ManPiNum(pAbc->pGia) );
4099 Gia_ManForEachCo( pAbc->pGia, pObj, i )
4100 {
4101 pTruth = Gia_ObjComputeTruthTable( pAbc->pGia, pObj );
4102 if ( fBinaryFile )
4103 fwrite( pTruth, nBytes, 1, pFile );
4104 else if ( fHex )
4105 Extra_PrintHex( pFile, (unsigned *)pTruth, Gia_ManPiNum(pAbc->pGia) ), fprintf( pFile, "\n" );
4106 else
4107 Extra_PrintBinary( pFile, (unsigned *)pTruth, 1 << Gia_ManPiNum(pAbc->pGia) ), fprintf( pFile, "\n" );
4108 }
4109 fclose( pFile );
4110 return 0;
4111
4112usage:
4113 fprintf( pAbc->Err, "usage: &write_truth [-rxbh] <file>\n" );
4114 fprintf( pAbc->Err, "\t writes truth tables of each PO of GIA manager into a file\n" );
4115 fprintf( pAbc->Err, "\t-r : toggle reversing bits in the truth table [default = %s]\n", fReverse? "yes":"no" );
4116 fprintf( pAbc->Err, "\t-x : toggle writing in the hex notation [default = %s]\n", fHex? "yes":"no" );
4117 fprintf( pAbc->Err, "\t-b : toggle using binary file format [default = %s]\n", fBinaryFile? "yes":"no" );
4118 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
4119 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
4120 return 1;
4121}
4122
4123
4135int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv )
4136{
4137 char * pFileName;
4138 int c;
4139 extern void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nFrames, char * pCommand );
4140
4141 Extra_UtilGetoptReset();
4142 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
4143 {
4144 switch ( c )
4145 {
4146 case 'h':
4147 goto usage;
4148 default:
4149 goto usage;
4150 }
4151 }
4152 if ( argc != globalUtilOptind + 1 )
4153 goto usage;
4154 // get the input file name
4155 pFileName = argv[globalUtilOptind];
4156 Abc_NtkWriteLogFile( pFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, NULL );
4157 return 0;
4158
4159usage:
4160 fprintf( pAbc->Err, "usage: write_status [-h] <file>\n" );
4161 fprintf( pAbc->Err, "\t writes verification log file\n" );
4162 fprintf( pAbc->Err, "\t-h : print the help massage\n" );
4163 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
4164 return 1;
4165}
4166
4178int IoCommandWriteSmv( Abc_Frame_t * pAbc, int argc, char **argv )
4179{
4180 char * pFileName;
4181 int c;
4182
4183 Extra_UtilGetoptReset();
4184 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
4185 {
4186 switch ( c )
4187 {
4188 case 'h':
4189 goto usage;
4190 default:
4191 goto usage;
4192 }
4193 }
4194 if ( pAbc->pNtkCur == NULL )
4195 {
4196 fprintf( pAbc->Out, "Empty network.\n" );
4197 return 0;
4198 }
4199 if ( argc != globalUtilOptind + 1 )
4200 goto usage;
4201 // get the output file name
4202 pFileName = argv[globalUtilOptind];
4203 // call the corresponding file writer
4204 Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_SMV );
4205 return 0;
4206
4207usage:
4208 fprintf( pAbc->Err, "usage: write_smv [-h] <file>\n" );
4209 fprintf( pAbc->Err, "\t write the network in SMV format\n" );
4210 fprintf( pAbc->Err, "\t-h : print the help message\n" );
4211 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .smv)\n" );
4212 return 1;
4213}
4214
4226int IoCommandWriteJson( Abc_Frame_t * pAbc, int argc, char **argv )
4227{
4228 extern void Json_Write( char * pFileName, Abc_Nam_t * pStr, Vec_Wec_t * vObjs );
4229 extern void Json_Extract( char * pFileName, Abc_Nam_t * pStr, Vec_Wec_t * vObjs );
4230 int c, fExtract = 0;
4231 char * pFileName;
4232
4233 Extra_UtilGetoptReset();
4234 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
4235 {
4236 switch ( c )
4237 {
4238 case 'c':
4239 fExtract ^= 1;
4240 break;
4241 case 'h':
4242 goto usage;
4243 default:
4244 goto usage;
4245 }
4246 }
4247 if ( Abc_FrameReadJsonStrs(Abc_FrameReadGlobalFrame()) == NULL )
4248 {
4249 fprintf( pAbc->Out, "No JSON info is available.\n" );
4250 return 0;
4251 }
4252 if ( argc != globalUtilOptind + 1 )
4253 goto usage;
4254 pFileName = argv[globalUtilOptind];
4255 if ( fExtract )
4256 Json_Extract( pFileName, Abc_FrameReadJsonStrs(Abc_FrameReadGlobalFrame()), Abc_FrameReadJsonObjs(Abc_FrameReadGlobalFrame()) );
4257 else
4258 Json_Write( pFileName, Abc_FrameReadJsonStrs(Abc_FrameReadGlobalFrame()), Abc_FrameReadJsonObjs(Abc_FrameReadGlobalFrame()) );
4259 return 0;
4260
4261usage:
4262 fprintf( pAbc->Err, "usage: write_json [-ch] <file>\n" );
4263 fprintf( pAbc->Err, "\t write the network in JSON format\n" );
4264 fprintf( pAbc->Err, "\t-c : output extracted version\n" );
4265 fprintf( pAbc->Err, "\t-h : print the help message\n" );
4266 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .json)\n" );
4267 return 1;
4268}
4269
4281int IoCommandWriteResub( Abc_Frame_t * pAbc, int argc, char **argv )
4282{
4283 extern void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName );
4284 char * pFileName;
4285 int c;
4286 Extra_UtilGetoptReset();
4287 while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
4288 {
4289 switch ( c )
4290 {
4291 case 'h':
4292 goto usage;
4293 default:
4294 goto usage;
4295 }
4296 }
4297 if ( argc != globalUtilOptind + 1 )
4298 goto usage;
4299 pFileName = argv[globalUtilOptind];
4300 if ( pAbc->pGia == NULL )
4301 {
4302 Abc_Print( -1, "IoCommandWriteResub(): There is no AIG.\n" );
4303 return 1;
4304 }
4305 if ( Gia_ManCiNum(pAbc->pGia) > 20 )
4306 {
4307 Abc_Print( -1, "IoCommandWriteResub(): The number of inputs is wrong.\n" );
4308 return 1;
4309 }
4310 Gia_ManWriteResub( pAbc->pGia, pFileName );
4311 return 0;
4312
4313usage:
4314 fprintf( pAbc->Err, "usage: &write_resub [-ch] <file>\n" );
4315 fprintf( pAbc->Err, "\t write the network in resub format\n" );
4316 fprintf( pAbc->Err, "\t-h : print the help message\n" );
4317 fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .json)\n" );
4318 return 1;
4319}
4320
4332int IoCommandWriteMM( Abc_Frame_t * pAbc, int argc, char **argv )
4333{
4334 extern int Abc_NtkWriteToFile( char * pFileName, Abc_Ntk_t * pNtk );
4335 Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
4336 char * pFileName = NULL; int c;
4337 Extra_UtilGetoptReset();
4338 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
4339 {
4340 switch ( c )
4341 {
4342 case 'h':
4343 goto usage;
4344 default:
4345 goto usage;
4346 }
4347 }
4348 if ( argc != globalUtilOptind + 1 )
4349 goto usage;
4350 pFileName = argv[globalUtilOptind];
4351 if ( pNtk == NULL )
4352 {
4353 Abc_Print( -1, "IoCommandWriteMM(): There is no current network.\n" );
4354 return 1;
4355 }
4356 if ( !Abc_NtkIsMappedLogic(pNtk) )
4357 {
4358 Abc_Print( -1, "IoCommandWriteMM(): The current network is not mapped.\n" );
4359 return 1;
4360 }
4361 Abc_NtkWriteToFile( pFileName, pNtk );
4362 return 0;
4363
4364usage:
4365 fprintf( pAbc->Err, "usage: write_mm [-h] <file>\n" );
4366 fprintf( pAbc->Err, "\t write mapped network into a file\n" );
4367 fprintf( pAbc->Err, "\t-h : print the help message\n" );
4368 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
4369 return 1;
4370}
4371
4383int IoCommandWriteMMGia( Abc_Frame_t * pAbc, int argc, char **argv )
4384{
4385 extern Abc_Ntk_t * Abc_NtkFromCellMappedGia( Gia_Man_t * p, int fUseBuffs );
4386 extern int Abc_NtkWriteToFile( char * pFileName, Abc_Ntk_t * pNtk );
4387 Abc_Ntk_t * pNtk = NULL;
4388 char * pFileName = NULL; int c;
4389 Extra_UtilGetoptReset();
4390 while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
4391 {
4392 switch ( c )
4393 {
4394 case 'h':
4395 goto usage;
4396 default:
4397 goto usage;
4398 }
4399 }
4400 if ( argc != globalUtilOptind + 1 )
4401 goto usage;
4402 pFileName = argv[globalUtilOptind];
4403 if ( pAbc->pGia == NULL )
4404 {
4405 Abc_Print( -1, "IoCommandWriteMMGia(): There is no current AIG.\n" );
4406 return 1;
4407 }
4408 if ( !Gia_ManHasCellMapping(pAbc->pGia) )
4409 {
4410 Abc_Print( -1, "IoCommandWriteMMGia(): Current AIG is not mapped.\n" );
4411 return 1;
4412 }
4413 pNtk = Abc_NtkFromCellMappedGia( pAbc->pGia, 0 );
4414 Abc_NtkWriteToFile( pFileName, pNtk );
4415 Abc_NtkDelete( pNtk );
4416 return 0;
4417
4418usage:
4419 fprintf( pAbc->Err, "usage: &write_mm [-h] <file>\n" );
4420 fprintf( pAbc->Err, "\t write cell mapped current AIG into a file\n" );
4421 fprintf( pAbc->Err, "\t-h : print the help message\n" );
4422 fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
4423 return 1;
4424}
4425
4429
4430
4431ABC_NAMESPACE_IMPL_END
4432
Abc_NtkFromCellMappedGia
Abc_Ntk_t * Abc_NtkFromCellMappedGia(Gia_Man_t *p, int fUseBuffs)
Definition abcDar.c:967
Abc_NtkDarToCnf
Abc_Ntk_t * Abc_NtkDarToCnf(Abc_Ntk_t *pNtk, char *pFileName, int fFastAlgo, int fChangePol, int fVerbose)
Definition abcDar.c:1847
Io_ReadFins
Vec_Int_t * Io_ReadFins(Abc_Ntk_t *pNtk, char *pFileName, int fVerbose)
Definition abcDetect.c:164
Abc_NtkReadLogFile
int Abc_NtkReadLogFile(char *pFileName, Abc_Cex_t **ppCex, int *pnFrames)
Definition abcLog.c:132
Abc_NtkWriteToFile
int Abc_NtkWriteToFile(char *pFileName, Abc_Ntk_t *pNtk)
Definition abcMap.c:1006
Abc_NtkReadFromFile
Abc_Ntk_t * Abc_NtkReadFromFile(char *pFileName)
Definition abcMap.c:992
Abc_NtkWriteSorterCnf
void Abc_NtkWriteSorterCnf(char *pFileName, int nVars, int nQueens)
Definition abcSat.c:945
Abc_FrameUpdateGia
void Abc_FrameUpdateGia(Abc_Frame_t *pAbc, Gia_Man_t *pNew)
Definition abc.c:824
Abc_FrameReplaceCex
void Abc_FrameReplaceCex(Abc_Frame_t *pAbc, Abc_Cex_t **ppCex)
FUNCTION DEFINITIONS ///.
Definition abc.c:679
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkWriteLogFile
ABC_DLL void Abc_NtkWriteLogFile(char *pFileName, Abc_Cex_t *pSeqCex, int Status, int nFrames, char *pCommand)
DECLARATIONS ///.
Definition abcLog.c:68
Abc_NtkToLogic
ABC_DLL Abc_Ntk_t * Abc_NtkToLogic(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition abcNetlist.c:52
Abc_SopFromTruthsBin
ABC_DLL Vec_Ptr_t * Abc_SopFromTruthsBin(char *pTruth)
Definition abcSop.c:1033
Abc_NtkForEachLatch
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition abc.h:500
Abc_NtkAigToGia
ABC_DLL Gia_Man_t * Abc_NtkAigToGia(Abc_Ntk_t *p, int fGiaSimple)
Definition abcFunc.c:1050
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition abcNames.c:49
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_NtkFlattenHierarchyGia
ABC_DLL Gia_Man_t * Abc_NtkFlattenHierarchyGia(Abc_Ntk_t *pNtk, Vec_Ptr_t **pvBuffers, int fVerbose)
Definition abcHieGia.c:418
Abc_NtkToNetlist
ABC_DLL Abc_Ntk_t * Abc_NtkToNetlist(Abc_Ntk_t *pNtk)
Definition abcNetlist.c:100
Abc_NtkToAig
ABC_DLL int Abc_NtkToAig(Abc_Ntk_t *pNtk)
Definition abcFunc.c:1333
Abc_NtkTransferNameIds
ABC_DLL void Abc_NtkTransferNameIds(Abc_Ntk_t *p, Abc_Ntk_t *pNew)
Definition abcNames.c:761
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition abc.h:516
Abc_NtkStrash
ABC_DLL Abc_Ntk_t * Abc_NtkStrash(Abc_Ntk_t *pNtk, int fAllNodes, int fCleanup, int fRecord)
Definition abcStrash.c:265
Abc_SopFromTruthsHex
ABC_DLL Vec_Ptr_t * Abc_SopFromTruthsHex(char *pTruth)
Definition abcSop.c:1127
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition abc.h:518
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition abcNtk.c:1421
Abc_NtkStartNameIds
ABC_DLL void Abc_NtkStartNameIds(Abc_Ntk_t *p)
Definition abcNames.c:711
Abc_NtkCreateWithNodes
ABC_DLL Abc_Ntk_t * Abc_NtkCreateWithNodes(Vec_Ptr_t *vSops)
Definition abcNtk.c:1374
Abc_NtkDup
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Definition abcNtk.c:472
ABC_FALLOC
#define ABC_FALLOC(type, num)
Definition abc_global.h:266
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Abc_Frame_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition abcapis.h:38
Saig_ManCbaFindCexCareBits
Abc_Cex_t * Saig_ManCbaFindCexCareBits(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
Definition absOldCex.c:718
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Abc_FrameClearVerifStatus
ABC_DLL void Abc_FrameClearVerifStatus(Abc_Frame_t *p)
Definition mainFrame.c:292
Abc_FrameReadJsonStrs
ABC_DLL Abc_Nam_t * Abc_FrameReadJsonStrs(Abc_Frame_t *p)
Definition mainFrame.c:81
Abc_FrameSetJsonObjs
ABC_DLL void Abc_FrameSetJsonObjs(Vec_Wec_t *vObjs)
Definition mainFrame.c:106
Abc_FrameReadGlobalFrame
ABC_DLL Abc_Frame_t * Abc_FrameReadGlobalFrame()
Definition mainFrame.c:666
Abc_FrameReadLibGen
ABC_DLL void * Abc_FrameReadLibGen()
Definition mainFrame.c:59
Abc_FrameSetJsonStrs
ABC_DLL void Abc_FrameSetJsonStrs(Abc_Nam_t *pStrs)
Definition mainFrame.c:105
Abc_FrameReadNtk
ABC_DLL Abc_Ntk_t * Abc_FrameReadNtk(Abc_Frame_t *p)
Definition mainFrame.c:327
Abc_FrameReadErr
ABC_DLL FILE * Abc_FrameReadErr(Abc_Frame_t *p)
Definition mainFrame.c:375
Abc_FrameReplaceCurrentNetwork
ABC_DLL void Abc_FrameReplaceCurrentNetwork(Abc_Frame_t *p, Abc_Ntk_t *pNet)
Definition mainFrame.c:538
Abc_FrameReadOut
ABC_DLL FILE * Abc_FrameReadOut(Abc_Frame_t *p)
Definition mainFrame.c:359
Abc_FrameReadJsonObjs
ABC_DLL Vec_Wec_t * Abc_FrameReadJsonObjs(Abc_Frame_t *p)
Definition mainFrame.c:82
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Bmc_CexCareMinimize
Abc_Cex_t * Bmc_CexCareMinimize(Aig_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int nTryCexes, int fCheck, int fVerbose)
Definition bmcCexCare.c:426
Bmc_CexCareVerifyAnyPo
int Bmc_CexCareVerifyAnyPo(Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
Definition bmcCexCare.c:497
Bmc_CexCareSatBasedMinimize
Abc_Cex_t * Bmc_CexCareSatBasedMinimize(Aig_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int fHighEffort, int fCheck, int fVerbose)
Definition bmcCexCare.c:433
Bmc_CexVerify
int Bmc_CexVerify(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Definition bmcCexTools.c:346
Bmc_CexCareVerify
int Bmc_CexCareVerify(Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
Definition bmcCexCare.c:458
Cmd_CommandAdd
void Cmd_CommandAdd(Abc_Frame_t *pAbc, const char *sGroup, const char *sName, Cmd_CommandFuncType pFunc, int fChanges)
Definition cmdApi.c:63
Cmd_CommandExecute
ABC_DLL int Cmd_CommandExecute(Abc_Frame_t *pAbc, const char *sCommand)
Definition cmdApi.c:193
p
Cube * p
Definition exorList.c:222
globalUtilOptind
int globalUtilOptind
Definition extraUtilUtil.c:45
Sdm_ManCanRead
int Sdm_ManCanRead()
Definition extraUtilDsd.c:1080
Extra_UtilGetopt
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
Definition extraUtilUtil.c:98
Extra_UtilGetoptReset
ABC_DLL void Extra_UtilGetoptReset()
Definition extraUtilUtil.c:80
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition extraUtilFile.c:192
Extra_PrintHex2
void Extra_PrintHex2(FILE *pFile, unsigned *pTruth, int nVars)
Definition extraUtilFile.c:661
Extra_FileReadContents
char * Extra_FileReadContents(char *pFileName)
Definition extraUtilFile.c:407
Extra_FileNameExtension
char * Extra_FileNameExtension(char *FileName)
Definition extraUtilFile.c:132
Extra_FileNameGeneric
char * Extra_FileNameGeneric(char *FileName)
Definition extraUtilFile.c:172
Gia_ManFromAigSimple
Gia_Man_t * Gia_ManFromAigSimple(Aig_Man_t *p)
Definition giaAig.c:212
Gia_ManReadGig
Gia_Man_t * Gia_ManReadGig(char *pFileName)
Definition giaGig.c:470
Jf_ManDumpCnf
void Jf_ManDumpCnf(Gia_Man_t *p, char *pFileName, int fVerbose)
Definition giaJf.c:1767
Mf_ManDumpCnf
void Mf_ManDumpCnf(Gia_Man_t *p, char *pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose)
Definition giaMf.c:1895
Abc_NtkFromAigPhase
ABC_NAMESPACE_IMPL_START Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
DECLARATIONS ///.
Definition abcDar.c:595
Extra_PrintHex
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
Definition extraUtilFile.c:643
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition abcDar.c:237
Gia_ManWriteResub
void Gia_ManWriteResub(Gia_Man_t *p, char *pFileName)
Definition giaUtil.c:3161
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ObjComputeTruthTable
word * Gia_ObjComputeTruthTable(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition giaTruth.c:447
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
Hop_ManConvertAigToTruth
unsigned * Hop_ManConvertAigToTruth(Hop_Man_t *p, Hop_Obj_t *pRoot, int nVars, Vec_Int_t *vTruth, int fMsbFirst)
Definition hopTruth.c:143
Hop_Obj_t
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
Io_WriteBlifSpecial
void Io_WriteBlifSpecial(Abc_Ntk_t *pNtk, char *FileName, char *pLutStruct, int fUseHie)
Definition ioWriteBlif.c:1385
Io_WriteHie
void Io_WriteHie(Abc_Ntk_t *pNtk, char *pBaseName, char *pFileName)
Definition ioUtil.c:486
IO_FILE_SMV
@ IO_FILE_SMV
Definition ioAbc.h:66
IO_FILE_DOT
@ IO_FILE_DOT
Definition ioAbc.h:57
IO_FILE_EQN
@ IO_FILE_EQN
Definition ioAbc.h:59
IO_FILE_VERILOG
@ IO_FILE_VERILOG
Definition ioAbc.h:67
IO_FILE_BBLIF
@ IO_FILE_BBLIF
Definition ioAbc.h:51
IO_FILE_BLIFMV
@ IO_FILE_BLIFMV
Definition ioAbc.h:53
IO_FILE_GML
@ IO_FILE_GML
Definition ioAbc.h:60
IO_FILE_PLA
@ IO_FILE_PLA
Definition ioAbc.h:64
IO_FILE_BENCH
@ IO_FILE_BENCH
Definition ioAbc.h:54
IO_FILE_BLIF
@ IO_FILE_BLIF
Definition ioAbc.h:52
IO_FILE_BOOK
@ IO_FILE_BOOK
Definition ioAbc.h:55
IO_FILE_EDIF
@ IO_FILE_EDIF
Definition ioAbc.h:58
IO_FILE_MOPLA
@ IO_FILE_MOPLA
Definition ioAbc.h:65
IO_FILE_BAF
@ IO_FILE_BAF
Definition ioAbc.h:50
IO_FILE_CNF
@ IO_FILE_CNF
Definition ioAbc.h:56
IO_FILE_AIGER
@ IO_FILE_AIGER
Definition ioAbc.h:49
Io_WriteAigerCex
void Io_WriteAigerCex(Abc_Cex_t *pCex, Abc_Ntk_t *pNtk, void *pG, char *pFileName)
Definition ioWriteAiger.c:880
Io_WriteVerilog
void Io_WriteVerilog(Abc_Ntk_t *pNtk, char *FileName, int fOnlyAnds, int fNewInterface)
FUNCTION DEFINITIONS ///.
Definition ioWriteVerilog.c:58
Io_ReadBlif
Abc_Ntk_t * Io_ReadBlif(char *pFileName, int fCheck)
FUNCTION DEFINITIONS ///.
Definition ioReadBlif.c:113
Io_WriteAiger
void Io_WriteAiger(Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols, int fCompact, int fUnique)
Definition ioWriteAiger.c:635
Io_ReadBenchInit
void Io_ReadBenchInit(Abc_Ntk_t *pNtk, char *pFileName)
Definition ioReadBench.c:336
Io_WriteHMetis
void Io_WriteHMetis(Abc_Ntk_t *pNtk, char *pFileName, int fSkipPo, int fWeightEdges, int fVerbose)
Definition ioWriteHMetis.c:26
Io_WriteBenchLut
int Io_WriteBenchLut(Abc_Ntk_t *pNtk, char *FileName)
Definition ioWriteBench.c:175
Io_ReadNetlist
Abc_Ntk_t * Io_ReadNetlist(char *pFileName, Io_FileType_t FileType, int fCheck)
Definition ioUtil.c:99
Io_ReadFileType
Io_FileType_t Io_ReadFileType(char *pFileName)
DECLARATIONS ///.
Definition ioUtil.c:47
Io_Write
void Io_Write(Abc_Ntk_t *pNtk, char *pFileName, Io_FileType_t FileType)
Definition ioUtil.c:320
Io_WriteList
void Io_WriteList(Abc_Ntk_t *pNtk, char *pFileName, int fUseHost)
FUNCTION DEFINITIONS ///.
Definition ioWriteList.c:102
Io_Read
Abc_Ntk_t * Io_Read(char *pFileName, Io_FileType_t FileType, int fCheck, int fBarBufs)
Definition ioUtil.c:241
Io_WriteEdgelist
void Io_WriteEdgelist(Abc_Ntk_t *pNtk, char *pFileName, int fWriteLatches, int fBb2Wb, int fSeq, int fName)
FUNCTION DEFINITIONS ///.
Definition ioWriteEdgelist.c:59
Io_ReadPla
Abc_Ntk_t * Io_ReadPla(char *pFileName, int fZeros, int fBoth, int fOnDc, int fSkipPrepro, int fCheck)
Definition ioReadPla.c:329
Io_WriteCnf
int Io_WriteCnf(Abc_Ntk_t *pNtk, char *FileName, int fAllPrimes)
FUNCTION DEFINITIONS ///.
Definition ioWriteCnf.c:48
Json_Extract
void Json_Extract(char *pFileName, Abc_Nam_t *pStr, Vec_Wec_t *vObjs)
Definition ioJson.c:151
Json_Write
void Json_Write(char *pFileName, Abc_Nam_t *pStr, Vec_Wec_t *vObjs)
Definition ioJson.c:269
Json_Read
Vec_Wec_t * Json_Read(char *pFileName, Abc_Nam_t **ppStrs)
Definition ioJson.c:307
Io_ReadBlifAsAig
Abc_Ntk_t * Io_ReadBlifAsAig(char *pFileName, int fCheck)
FUNCTION DEFINITIONS ///.
Definition ioReadBlifAig.c:118
Io_ReadDsd
Abc_Ntk_t * Io_ReadDsd(char *pForm)
Definition ioReadDsd.c:232
Mop_ManTest
Abc_Ntk_t * Mop_ManTest(char *pFileName, int fMerge, int fVerbose)
Definition ioReadPlaMo.c:788
Io_TransformSF2PLA
void Io_TransformSF2PLA(char *pNameIn, char *pNameOut)
Definition ioUtil.c:879
Io_FileReadCnf
Vec_Ptr_t * Io_FileReadCnf(char *pFileName, int fMulti)
Definition ioUtil.c:1025
Io_TransformROM2PLA
void Io_TransformROM2PLA(char *pNameIn, char *pNameOut)
Definition ioUtil.c:935
Io_WriteCellNet
void Io_WriteCellNet(Abc_Ntk_t *pNtk, char *pFileName)
Definition ioWriteList.c:221
Io_WriteMoPlaM
int Io_WriteMoPlaM(Abc_Ntk_t *pNtk, char *pFileName, int nMints)
Definition ioWritePla.c:577
Io_WriteVerilogLut
void Io_WriteVerilogLut(Abc_Ntk_t *pNtk, char *pFileName, int nLutSize, int fFixed, int fNoModules, int fNewInterface)
Definition ioWriteVerilog.c:923
Abc_NtkDumpOneCexSpecial
void Abc_NtkDumpOneCexSpecial(FILE *pFile, Abc_Ntk_t *pNtk, Abc_Cex_t *pCex)
Definition io.c:3026
Bmc_CexCareBits
Abc_Cex_t * Bmc_CexCareBits(Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexImpl, Abc_Cex_t *pCexEss, int fFindAll, int fVerbose)
Definition bmcCexTools.c:597
Abc_NtkCheckSpecialPi
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START int Abc_NtkCheckSpecialPi(Abc_Ntk_t *pNtk)
Definition io.c:3006
Abc_FrameCopyLTLDataBase
void Abc_FrameCopyLTLDataBase(Abc_Frame_t *pAbc, Abc_Ntk_t *pNtk)
Definition ltl_parser.c:73
Bmc_CexEssentialBits
Abc_Cex_t * Bmc_CexEssentialBits(Gia_Man_t *p, Abc_Cex_t *pCexState, Abc_Cex_t *pCexCare, int fVerbose)
Definition bmcCexTools.c:802
Io_End
void Io_End(Abc_Frame_t *pAbc)
Definition io.c:192
Abc_NtkDumpOneCex
void Abc_NtkDumpOneCex(FILE *pFile, Abc_Ntk_t *pNtk, Abc_Cex_t *pCex, int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo, int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended)
Definition io.c:3056
Bmc_CexInnerStates
Abc_Cex_t * Bmc_CexInnerStates(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t **ppCexImpl, int fVerbose)
Definition bmcCexTools.c:435
Abc_NtkReadCexFile
int Abc_NtkReadCexFile(char *pFileName, Abc_Ntk_t *pNtk, Abc_Cex_t **ppCex, Abc_Cex_t **ppCexCare, int *pnFrames, int *fOldFormat, int xMode)
Definition io.c:715
Io_Init
void Io_Init(Abc_Frame_t *pAbc)
FUNCTION DEFINITIONS ///.
Definition io.c:117
glo_fMapped
int glo_fMapped
Definition verCore.c:80
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
usage
usage()
Definition main.c:626
Saig_ManExtendCex
Abc_Cex_t * Saig_ManExtendCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition saigDup.c:384
Saig_ManDupIsoCanonical
Aig_Man_t * Saig_ManDupIsoCanonical(Aig_Man_t *pAig, int fVerbose)
Definition saigIso.c:128
Abc_Ntk_t_::pName
char * pName
Definition abc.h:158
Abc_Ntk_t_::vFins
Vec_Int_t * vFins
Definition abc.h:216
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition abc.h:191
Abc_Ntk_t_::pModel
int * pModel
Definition abc.h:198
Abc_Ntk_t_::pSpec
char * pSpec
Definition abc.h:159
Abc_Obj_t_::pData
void * pData
Definition abc.h:145
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition utilCex.c:361
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
Abc_Nam_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Nam_t_ Abc_Nam_t
INCLUDES ///.
Definition utilNam.h:39
assert
#define assert(ex)
Definition util_old.h:213
strlen
int strlen()
strcmp
int strcmp()
sprintf
char * sprintf()
strstr
char * strstr()
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42