abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
io.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [io.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Command processing package.]
8 
9  Synopsis [Command file.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: io.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
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 ABC_NAMESPACE_IMPL_START
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 static int IoCommandRead ( Abc_Frame_t * pAbc, int argc, char **argv );
34 static int IoCommandReadAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
35 static int IoCommandReadBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
36 static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
37 static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
38 static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
39 static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
40 static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv );
41 static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
42 static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
43 static int IoCommandReadInit ( Abc_Frame_t * pAbc, int argc, char **argv );
44 static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv );
45 static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
46 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
47 static int IoCommandReadStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
48 static int IoCommandReadGig ( Abc_Frame_t * pAbc, int argc, char **argv );
49 
50 static int IoCommandWrite ( Abc_Frame_t * pAbc, int argc, char **argv );
51 static int IoCommandWriteHie ( Abc_Frame_t * pAbc, int argc, char **argv );
52 static int IoCommandWriteAiger ( Abc_Frame_t * pAbc, int argc, char **argv );
53 static int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv );
54 static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv );
55 static int IoCommandWriteBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
56 static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
57 static int IoCommandWriteBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
58 static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv );
59 static int IoCommandWriteBook ( Abc_Frame_t * pAbc, int argc, char **argv );
60 static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv );
61 static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv );
62 static int IoCommandWriteCnf2 ( Abc_Frame_t * pAbc, int argc, char **argv );
63 static int IoCommandWriteCex ( Abc_Frame_t * pAbc, int argc, char **argv );
64 static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv );
65 static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
66 static int IoCommandWriteGml ( Abc_Frame_t * pAbc, int argc, char **argv );
67 static int IoCommandWriteList ( Abc_Frame_t * pAbc, int argc, char **argv );
68 static int IoCommandWritePla ( Abc_Frame_t * pAbc, int argc, char **argv );
69 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
70 static int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv );
71 static int IoCommandWriteTruth ( Abc_Frame_t * pAbc, int argc, char **argv );
72 static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv );
73 static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
74 static int IoCommandWriteSmv ( Abc_Frame_t * pAbc, int argc, char **argv );
75 
76 extern void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk );
77 
78 extern int glo_fMapped;
79 
80 ////////////////////////////////////////////////////////////////////////
81 /// FUNCTION DEFINITIONS ///
82 ////////////////////////////////////////////////////////////////////////
83 
84 /**Function*************************************************************
85 
86  Synopsis []
87 
88  Description []
89 
90  SideEffects []
91 
92  SeeAlso []
93 
94 ***********************************************************************/
95 void Io_Init( Abc_Frame_t * pAbc )
96 {
97  Cmd_CommandAdd( pAbc, "I/O", "read", IoCommandRead, 1 );
98  Cmd_CommandAdd( pAbc, "I/O", "read_aiger", IoCommandReadAiger, 1 );
99  Cmd_CommandAdd( pAbc, "I/O", "read_baf", IoCommandReadBaf, 1 );
100  Cmd_CommandAdd( pAbc, "I/O", "read_bblif", IoCommandReadBblif, 1 );
101  Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
102  Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 );
103  Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
104  Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 );
105 // Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
106  Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
107  Cmd_CommandAdd( pAbc, "I/O", "read_init", IoCommandReadInit, 1 );
108  Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 );
109  Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 );
110  Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 );
111  Cmd_CommandAdd( pAbc, "I/O", "read_status", IoCommandReadStatus, 0 );
112  Cmd_CommandAdd( pAbc, "I/O", "&read_gig", IoCommandReadGig, 0 );
113 
114  Cmd_CommandAdd( pAbc, "I/O", "write", IoCommandWrite, 0 );
115  Cmd_CommandAdd( pAbc, "I/O", "write_hie", IoCommandWriteHie, 0 );
116  Cmd_CommandAdd( pAbc, "I/O", "write_aiger", IoCommandWriteAiger, 0 );
117  Cmd_CommandAdd( pAbc, "I/O", "write_aiger_cex", IoCommandWriteAigerCex, 0 );
118  Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 );
119  Cmd_CommandAdd( pAbc, "I/O", "write_bblif", IoCommandWriteBblif, 0 );
120  Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 );
121  Cmd_CommandAdd( pAbc, "I/O", "write_blif_mv", IoCommandWriteBlifMv, 0 );
122  Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 );
123  Cmd_CommandAdd( pAbc, "I/O", "write_book", IoCommandWriteBook, 0 );
124  Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
125  Cmd_CommandAdd( pAbc, "I/O", "write_cex", IoCommandWriteCex, 0 );
126  Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 );
127  Cmd_CommandAdd( pAbc, "I/O", "&write_cnf", IoCommandWriteCnf2, 0 );
128  Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 );
129  Cmd_CommandAdd( pAbc, "I/O", "write_eqn", IoCommandWriteEqn, 0 );
130  Cmd_CommandAdd( pAbc, "I/O", "write_gml", IoCommandWriteGml, 0 );
131 // Cmd_CommandAdd( pAbc, "I/O", "write_list", IoCommandWriteList, 0 );
132  Cmd_CommandAdd( pAbc, "I/O", "write_pla", IoCommandWritePla, 0 );
133  Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
134 // Cmd_CommandAdd( pAbc, "I/O", "write_verlib", IoCommandWriteVerLib, 0 );
135  Cmd_CommandAdd( pAbc, "I/O", "write_sorter_cnf", IoCommandWriteSortCnf, 0 );
136  Cmd_CommandAdd( pAbc, "I/O", "write_truth", IoCommandWriteTruth, 0 );
137  Cmd_CommandAdd( pAbc, "I/O", "&write_truths", IoCommandWriteTruths, 0 );
138  Cmd_CommandAdd( pAbc, "I/O", "write_status", IoCommandWriteStatus, 0 );
139  Cmd_CommandAdd( pAbc, "I/O", "write_smv", IoCommandWriteSmv, 0 );
140 }
141 
142 /**Function*************************************************************
143 
144  Synopsis []
145 
146  Description []
147 
148  SideEffects []
149 
150  SeeAlso []
151 
152 ***********************************************************************/
153 void Io_End( Abc_Frame_t * pAbc )
154 {
155 }
156 
157 /**Function*************************************************************
158 
159  Synopsis []
160 
161  Description []
162 
163  SideEffects []
164 
165  SeeAlso []
166 
167 ***********************************************************************/
168 int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
169 {
170  char Command[1000];
171  Abc_Ntk_t * pNtk;
172  char * pFileName, * pTemp;
173  int c, fCheck, fBarBufs, fReadGia;
174 
175  fCheck = 1;
176  fBarBufs = 0;
177  fReadGia = 0;
178  glo_fMapped = 0;
179  Extra_UtilGetoptReset();
180  while ( ( c = Extra_UtilGetopt( argc, argv, "mcbgh" ) ) != EOF )
181  {
182  switch ( c )
183  {
184  case 'm':
185  glo_fMapped ^= 1;
186  break;
187  case 'c':
188  fCheck ^= 1;
189  break;
190  case 'b':
191  fBarBufs ^= 1;
192  break;
193  case 'g':
194  fReadGia ^= 1;
195  break;
196  case 'h':
197  goto usage;
198  default:
199  goto usage;
200  }
201  }
202  if ( argc != globalUtilOptind + 1 )
203  goto usage;
204  // get the input file name
205  pFileName = argv[globalUtilOptind];
206  // fix the wrong symbol
207  for ( pTemp = pFileName; *pTemp; pTemp++ )
208  if ( *pTemp == '>' || *pTemp == '\\' )
209  *pTemp = '/';
210  // read libraries
211  Command[0] = 0;
212  assert( strlen(pFileName) < 900 );
213  if ( !strcmp( Extra_FileNameExtension(pFileName), "genlib" ) )
214  sprintf( Command, "read_genlib %s", pFileName );
215  else if ( !strcmp( Extra_FileNameExtension(pFileName), "lib" ) )
216  sprintf( Command, "read_lib %s", pFileName );
217  else if ( !strcmp( Extra_FileNameExtension(pFileName), "scl" ) )
218  sprintf( Command, "read_scl %s", pFileName );
219  else if ( !strcmp( Extra_FileNameExtension(pFileName), "super" ) )
220  sprintf( Command, "read_super %s", pFileName );
221  else if ( !strcmp( Extra_FileNameExtension(pFileName), "constr" ) )
222  sprintf( Command, "read_constr %s", pFileName );
223  else if ( !strcmp( Extra_FileNameExtension(pFileName), "c" ) )
224  sprintf( Command, "so %s", pFileName );
225  else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) )
226  sprintf( Command, "dsd_load %s", pFileName );
227  if ( Command[0] )
228  {
229  Cmd_CommandExecute( pAbc, Command );
230  return 0;
231  }
232  if ( fReadGia )
233  {
234  Abc_Ntk_t * pNtk = Io_ReadNetlist( pFileName, Io_ReadFileType(pFileName), fCheck );
235  if ( pNtk )
236  {
237  Gia_Man_t * pGia = Abc_NtkFlattenHierarchyGia( pNtk, NULL, 0 );
238  Abc_NtkDelete( pNtk );
239  if ( pGia == NULL )
240  {
241  Abc_Print( 1, "Abc_CommandBlast(): Bit-blasting has failed.\n" );
242  return 0;
243  }
244  Abc_FrameUpdateGia( pAbc, pGia );
245  }
246  return 0;
247  }
248  // check if the library is available
249  if ( glo_fMapped && Abc_FrameReadLibGen() == NULL )
250  {
251  Abc_Print( 1, "Cannot read mapped design when the library is not given.\n" );
252  return 0;
253  }
254  // read the file using the corresponding file reader
255  pNtk = Io_Read( pFileName, Io_ReadFileType(pFileName), fCheck, fBarBufs );
256  if ( pNtk == NULL )
257  return 0;
258  if ( Abc_NtkPiNum(pNtk) == 0 )
259  {
260  Abc_Print( 0, "The new network has no primary inputs. It is recommended\n" );
261  Abc_Print( 1, "to add a dummy PI to make sure all commands work correctly.\n" );
262  }
263  // replace the current network
264  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
265  Abc_FrameCopyLTLDataBase( pAbc, pNtk );
266  Abc_FrameClearVerifStatus( pAbc );
267  return 0;
268 
269 usage:
270  fprintf( pAbc->Err, "usage: read [-mcbgh] <file>\n" );
271  fprintf( pAbc->Err, "\t replaces the current network by the network read from <file>\n" );
272  fprintf( pAbc->Err, "\t by calling the parser that matches the extension of <file>\n" );
273  fprintf( pAbc->Err, "\t (to read a hierarchical design, use \"read_hie\")\n" );
274  fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
275  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
276  fprintf( pAbc->Err, "\t-b : toggle reading barrier buffers [default = %s]\n", fBarBufs? "yes":"no" );
277  fprintf( pAbc->Err, "\t-g : toggle reading and flattening into &-space [default = %s]\n", fBarBufs? "yes":"no" );
278  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
279  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
280  return 1;
281 }
282 
283 /**Function*************************************************************
284 
285  Synopsis []
286 
287  Description []
288 
289  SideEffects []
290 
291  SeeAlso []
292 
293 ***********************************************************************/
294 int IoCommandReadAiger( Abc_Frame_t * pAbc, int argc, char ** argv )
295 {
296  Abc_Ntk_t * pNtk;
297  char * pFileName;
298  int fCheck;
299  int c;
300 
301  fCheck = 1;
302  Extra_UtilGetoptReset();
303  while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
304  {
305  switch ( c )
306  {
307  case 'c':
308  fCheck ^= 1;
309  break;
310  case 'h':
311  goto usage;
312  default:
313  goto usage;
314  }
315  }
316  if ( argc != globalUtilOptind + 1 )
317  goto usage;
318  // get the input file name
319  pFileName = argv[globalUtilOptind];
320  // read the file using the corresponding file reader
321  pNtk = Io_Read( pFileName, IO_FILE_AIGER, fCheck, 0 );
322  if ( pNtk == NULL )
323  return 1;
324  // replace the current network
325  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
326  Abc_FrameClearVerifStatus( pAbc );
327  return 0;
328 
329 usage:
330  fprintf( pAbc->Err, "usage: read_aiger [-ch] <file>\n" );
331  fprintf( pAbc->Err, "\t reads the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
332  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
333  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
334  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
335  return 1;
336 }
337 
338 /**Function*************************************************************
339 
340  Synopsis []
341 
342  Description []
343 
344  SideEffects []
345 
346  SeeAlso []
347 
348 ***********************************************************************/
349 int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv )
350 {
351  Abc_Ntk_t * pNtk;
352  char * pFileName;
353  int fCheck;
354  int c;
355 
356  fCheck = 1;
357  Extra_UtilGetoptReset();
358  while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
359  {
360  switch ( c )
361  {
362  case 'c':
363  fCheck ^= 1;
364  break;
365  case 'h':
366  goto usage;
367  default:
368  goto usage;
369  }
370  }
371  if ( argc != globalUtilOptind + 1 )
372  goto usage;
373  // get the input file name
374  pFileName = argv[globalUtilOptind];
375  // read the file using the corresponding file reader
376  pNtk = Io_Read( pFileName, IO_FILE_BAF, fCheck, 0 );
377  if ( pNtk == NULL )
378  return 1;
379  // replace the current network
380  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
381  Abc_FrameClearVerifStatus( pAbc );
382  return 0;
383 
384 usage:
385  fprintf( pAbc->Err, "usage: read_baf [-ch] <file>\n" );
386  fprintf( pAbc->Err, "\t reads the network in Binary Aig Format (BAF)\n" );
387  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
388  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
389  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
390  return 1;
391 }
392 
393 /**Function*************************************************************
394 
395  Synopsis []
396 
397  Description []
398 
399  SideEffects []
400 
401  SeeAlso []
402 
403 ***********************************************************************/
404 int IoCommandReadBblif( Abc_Frame_t * pAbc, int argc, char ** argv )
405 {
406  Abc_Ntk_t * pNtk;
407  char * pFileName;
408  int fCheck;
409  int c;
410 
411  fCheck = 1;
412  Extra_UtilGetoptReset();
413  while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
414  {
415  switch ( c )
416  {
417  case 'c':
418  fCheck ^= 1;
419  break;
420  case 'h':
421  goto usage;
422  default:
423  goto usage;
424  }
425  }
426  if ( argc != globalUtilOptind + 1 )
427  goto usage;
428  // get the input file name
429  pFileName = argv[globalUtilOptind];
430  // read the file using the corresponding file reader
431  pNtk = Io_Read( pFileName, IO_FILE_BBLIF, fCheck, 0 );
432  if ( pNtk == NULL )
433  return 1;
434  // replace the current network
435  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
436  Abc_FrameClearVerifStatus( pAbc );
437  return 0;
438 
439 usage:
440  fprintf( pAbc->Err, "usage: read_bblif [-ch] <file>\n" );
441  fprintf( pAbc->Err, "\t reads the network in a binary BLIF format\n" );
442  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
443  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
444  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
445  return 1;
446 }
447 
448 /**Function*************************************************************
449 
450  Synopsis []
451 
452  Description []
453 
454  SideEffects []
455 
456  SeeAlso []
457 
458 ***********************************************************************/
459 int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv )
460 {
461  Abc_Ntk_t * pNtk;
462  char * pFileName;
463  int fReadAsAig;
464  int fCheck;
465  int fUseNewParser;
466  int fSaveNames;
467  int c;
468  extern Abc_Ntk_t * Io_ReadBlifAsAig( char * pFileName, int fCheck );
469 
470  fCheck = 1;
471  fReadAsAig = 0;
472  fUseNewParser = 1;
473  fSaveNames = 0;
474  Extra_UtilGetoptReset();
475  while ( ( c = Extra_UtilGetopt( argc, argv, "nmach" ) ) != EOF )
476  {
477  switch ( c )
478  {
479  case 'n':
480  fUseNewParser ^= 1;
481  break;
482  case 'm':
483  fSaveNames ^= 1;
484  break;
485  case 'a':
486  fReadAsAig ^= 1;
487  break;
488  case 'c':
489  fCheck ^= 1;
490  break;
491  case 'h':
492  goto usage;
493  default:
494  goto usage;
495  }
496  }
497  if ( argc != globalUtilOptind + 1 )
498  goto usage;
499  // get the input file name
500  pFileName = argv[globalUtilOptind];
501  // read the file using the corresponding file reader
502  if ( fReadAsAig )
503  pNtk = Io_ReadBlifAsAig( pFileName, fCheck );
504  else if ( fUseNewParser )
505  pNtk = Io_Read( pFileName, IO_FILE_BLIF, fCheck, 0 );
506  else
507  {
508  Abc_Ntk_t * pTemp;
509  pNtk = Io_ReadBlif( pFileName, fCheck );
510  if ( pNtk == NULL )
511  return 1;
512  if ( fSaveNames )
513  Abc_NtkStartNameIds( pNtk );
514  pNtk = Abc_NtkToLogic( pTemp = pNtk );
515  if ( fSaveNames )
516  Abc_NtkTransferNameIds( pTemp, pNtk );
517  Abc_NtkDelete( pTemp );
518  }
519 
520  if ( pNtk == NULL )
521  return 1;
522  // replace the current network
523  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
524  Abc_FrameClearVerifStatus( pAbc );
525  return 0;
526 
527 usage:
528  fprintf( pAbc->Err, "usage: read_blif [-nmach] <file>\n" );
529  fprintf( pAbc->Err, "\t reads the network in binary BLIF format\n" );
530  fprintf( pAbc->Err, "\t (if this command does not work, try \"read\")\n" );
531  fprintf( pAbc->Err, "\t-n : toggle using old BLIF parser without hierarchy support [default = %s]\n", !fUseNewParser? "yes":"no" );
532  fprintf( pAbc->Err, "\t-m : toggle saving original circuit names into a file [default = %s]\n", fSaveNames? "yes":"no" );
533  fprintf( pAbc->Err, "\t-a : toggle creating AIG while reading the file [default = %s]\n", fReadAsAig? "yes":"no" );
534  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
535  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
536  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
537  return 1;
538 }
539 
540 /**Function*************************************************************
541 
542  Synopsis []
543 
544  Description []
545 
546  SideEffects []
547 
548  SeeAlso []
549 
550 ***********************************************************************/
551 int IoCommandReadBlifMv( Abc_Frame_t * pAbc, int argc, char ** argv )
552 {
553  Abc_Ntk_t * pNtk;
554  char * pFileName;
555  int fCheck;
556  int c;
557 
558  fCheck = 1;
559  Extra_UtilGetoptReset();
560  while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
561  {
562  switch ( c )
563  {
564  case 'c':
565  fCheck ^= 1;
566  break;
567  case 'h':
568  goto usage;
569  default:
570  goto usage;
571  }
572  }
573  if ( argc != globalUtilOptind + 1 )
574  goto usage;
575  // get the input file name
576  pFileName = argv[globalUtilOptind];
577  // read the file using the corresponding file reader
578  pNtk = Io_Read( pFileName, IO_FILE_BLIFMV, fCheck, 0 );
579  if ( pNtk == NULL )
580  return 1;
581  // replace the current network
582  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
583  Abc_FrameClearVerifStatus( pAbc );
584  return 0;
585 
586 usage:
587  fprintf( pAbc->Err, "usage: read_blif_mv [-ch] <file>\n" );
588  fprintf( pAbc->Err, "\t reads the network in BLIF-MV format\n" );
589  fprintf( pAbc->Err, "\t (if this command does not work, try \"read\")\n" );
590  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
591  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
592  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
593  return 1;
594 }
595 
596 /**Function*************************************************************
597 
598  Synopsis []
599 
600  Description []
601 
602  SideEffects []
603 
604  SeeAlso []
605 
606 ***********************************************************************/
607 int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv )
608 {
609  Abc_Ntk_t * pNtk;
610  char * pFileName;
611  int fCheck;
612  int c;
613 
614  fCheck = 1;
615  Extra_UtilGetoptReset();
616  while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
617  {
618  switch ( c )
619  {
620  case 'c':
621  fCheck ^= 1;
622  break;
623  case 'h':
624  goto usage;
625  default:
626  goto usage;
627  }
628  }
629  if ( argc != globalUtilOptind + 1 )
630  goto usage;
631  // get the input file name
632  pFileName = argv[globalUtilOptind];
633  // read the file using the corresponding file reader
634  pNtk = Io_Read( pFileName, IO_FILE_BENCH, fCheck, 0 );
635  if ( pNtk == NULL )
636  return 1;
637  // replace the current network
638  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
639  Abc_FrameClearVerifStatus( pAbc );
640  return 0;
641 
642 usage:
643  fprintf( pAbc->Err, "usage: read_bench [-ch] <file>\n" );
644  fprintf( pAbc->Err, "\t reads the network in BENCH format\n" );
645  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
646  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
647  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
648  return 1;
649 }
650 
651 /**Function*************************************************************
652 
653  Synopsis []
654 
655  Description []
656 
657  SideEffects []
658 
659  SeeAlso []
660 
661 ***********************************************************************/
662 int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
663 {
664  Abc_Ntk_t * pNtk;
665  char * pString;
666  int fCheck;
667  int c;
668  extern Abc_Ntk_t * Io_ReadDsd( char * pFormula );
669 
670  fCheck = 1;
671  Extra_UtilGetoptReset();
672  while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
673  {
674  switch ( c )
675  {
676  case 'c':
677  fCheck ^= 1;
678  break;
679  case 'h':
680  goto usage;
681  default:
682  goto usage;
683  }
684  }
685  if ( argc != globalUtilOptind + 1 )
686  goto usage;
687  // get the input file name
688  pString = argv[globalUtilOptind];
689  // read the file using the corresponding file reader
690  pNtk = Io_ReadDsd( pString );
691  if ( pNtk == NULL )
692  return 1;
693  // replace the current network
694  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
695  Abc_FrameClearVerifStatus( pAbc );
696  return 0;
697 
698 usage:
699  fprintf( pAbc->Err, "usage: read_dsd [-h] <formula>\n" );
700  fprintf( pAbc->Err, "\t parses a formula representing DSD of a function\n" );
701  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
702  fprintf( pAbc->Err, "\tformula : the formula representing disjoint-support decomposition (DSD)\n" );
703  fprintf( pAbc->Err, "\t Example of a formula: !(a*(b+CA(!d,e*f,c))*79B3(g,h,i,k))\n" );
704  fprintf( pAbc->Err, "\t where \'!\' is an INV, \'*\' is an AND, \'+\' is an XOR, \n" );
705  fprintf( pAbc->Err, "\t CA and 79B3 are hexadecimal representations of truth tables\n" );
706  fprintf( pAbc->Err, "\t (in this case CA=11001010 is truth table of MUX(Data0,Data1,Ctrl))\n" );
707  fprintf( pAbc->Err, "\t The lower chars (a,b,c,etc) are reserved for elementary variables.\n" );
708  fprintf( pAbc->Err, "\t The upper chars (A,B,C,etc) are reserved for hexadecimal digits.\n" );
709  fprintf( pAbc->Err, "\t No spaces are allowed in formulas. In parantheses, LSB goes first.\n" );
710  return 1;
711 }
712 
713 /**Function*************************************************************
714 
715  Synopsis []
716 
717  Description []
718 
719  SideEffects []
720 
721  SeeAlso []
722 
723 ***********************************************************************/
724 int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv )
725 {
726  Abc_Ntk_t * pNtk;
727  char * pFileName;
728  int fCheck;
729  int c;
730 
731  fCheck = 1;
732  Extra_UtilGetoptReset();
733  while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
734  {
735  switch ( c )
736  {
737  case 'c':
738  fCheck ^= 1;
739  break;
740  case 'h':
741  goto usage;
742  default:
743  goto usage;
744  }
745  }
746  if ( argc != globalUtilOptind + 1 )
747  goto usage;
748  // get the input file name
749  pFileName = argv[globalUtilOptind];
750  // read the file using the corresponding file reader
751  pNtk = Io_Read( pFileName, IO_FILE_EDIF, fCheck, 0 );
752  if ( pNtk == NULL )
753  return 1;
754  // replace the current network
755  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
756  Abc_FrameClearVerifStatus( pAbc );
757  return 0;
758 
759 usage:
760  fprintf( pAbc->Err, "usage: read_edif [-ch] <file>\n" );
761  fprintf( pAbc->Err, "\t reads the network in EDIF (works only for ISCAS benchmarks)\n" );
762  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
763  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
764  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
765  return 1;
766 }
767 
768 /**Function*************************************************************
769 
770  Synopsis []
771 
772  Description []
773 
774  SideEffects []
775 
776  SeeAlso []
777 
778 ***********************************************************************/
779 int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv )
780 {
781  Abc_Ntk_t * pNtk;
782  char * pFileName;
783  int fCheck;
784  int c;
785 
786  fCheck = 1;
787  Extra_UtilGetoptReset();
788  while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
789  {
790  switch ( c )
791  {
792  case 'c':
793  fCheck ^= 1;
794  break;
795  case 'h':
796  goto usage;
797  default:
798  goto usage;
799  }
800  }
801  if ( argc != globalUtilOptind + 1 )
802  goto usage;
803  // get the input file name
804  pFileName = argv[globalUtilOptind];
805  // read the file using the corresponding file reader
806  pNtk = Io_Read( pFileName, IO_FILE_EQN, fCheck, 0 );
807  if ( pNtk == NULL )
808  return 1;
809  // replace the current network
810  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
811  Abc_FrameClearVerifStatus( pAbc );
812  return 0;
813 
814 usage:
815  fprintf( pAbc->Err, "usage: read_eqn [-ch] <file>\n" );
816  fprintf( pAbc->Err, "\t reads the network in equation format\n" );
817  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
818  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
819  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
820  return 1;
821 }
822 
823 /**Function*************************************************************
824 
825  Synopsis []
826 
827  Description []
828 
829  SideEffects []
830 
831  SeeAlso []
832 
833 ***********************************************************************/
834 int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv )
835 {
836  FILE * pOut, * pErr;
837  Abc_Ntk_t * pNtk;
838  char * pFileName;
839  int c;
840 
841  pNtk = Abc_FrameReadNtk(pAbc);
842  pOut = Abc_FrameReadOut(pAbc);
843  pErr = Abc_FrameReadErr(pAbc);
844 
845  Extra_UtilGetoptReset();
846  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
847  {
848  switch ( c )
849  {
850  case 'h':
851  goto usage;
852  default:
853  goto usage;
854  }
855  }
856  if ( argc != globalUtilOptind && argc != globalUtilOptind + 1 )
857  goto usage;
858 
859  if ( pNtk == NULL )
860  {
861  fprintf( pErr, "Empty network.\n" );
862  return 1;
863  }
864  // get the input file name
865  if ( argc == globalUtilOptind + 1 )
866  pFileName = argv[globalUtilOptind];
867  else if ( pNtk->pSpec )
868  pFileName = Extra_FileNameGenericAppend( pNtk->pSpec, ".init" );
869  else
870  {
871  printf( "File name should be given on the command line.\n" );
872  return 1;
873  }
874 
875  // read the file using the corresponding file reader
876  pNtk = Abc_NtkDup( pNtk );
877  Io_ReadBenchInit( pNtk, pFileName );
878  // replace the current network
879  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
880  Abc_FrameClearVerifStatus( pAbc );
881  return 0;
882 
883 usage:
884  fprintf( pAbc->Err, "usage: read_init [-h] <file>\n" );
885  fprintf( pAbc->Err, "\t reads initial state of the network in BENCH format\n" );
886  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
887  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
888  return 1;
889 }
890 
891 /**Function*************************************************************
892 
893  Synopsis []
894 
895  Description []
896 
897  SideEffects []
898 
899  SeeAlso []
900 
901 ***********************************************************************/
902 int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
903 {
904  Abc_Ntk_t * pNtk;
905  char * pFileName;
906  int fCheck;
907  int fZeros;
908  int c;
909 
910  fZeros = 0;
911  fCheck = 1;
912  Extra_UtilGetoptReset();
913  while ( ( c = Extra_UtilGetopt( argc, argv, "zch" ) ) != EOF )
914  {
915  switch ( c )
916  {
917  case 'z':
918  fZeros ^= 1;
919  break;
920  case 'c':
921  fCheck ^= 1;
922  break;
923  case 'h':
924  goto usage;
925  default:
926  goto usage;
927  }
928  }
929  if ( argc != globalUtilOptind + 1 )
930  goto usage;
931  // get the input file name
932  pFileName = argv[globalUtilOptind];
933  // read the file using the corresponding file reader
934  if ( fZeros )
935  {
936  Abc_Ntk_t * pTemp;
937  pNtk = Io_ReadPla( pFileName, fZeros, fCheck );
938  if ( pNtk == NULL )
939  {
940  printf( "Reading PLA file has failed.\n" );
941  return 1;
942  }
943  pNtk = Abc_NtkToLogic( pTemp = pNtk );
944  Abc_NtkDelete( pTemp );
945  }
946  else
947  pNtk = Io_Read( pFileName, IO_FILE_PLA, fCheck, 0 );
948  if ( pNtk == NULL )
949  return 1;
950  // replace the current network
951  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
952  Abc_FrameClearVerifStatus( pAbc );
953  return 0;
954 
955 usage:
956  fprintf( pAbc->Err, "usage: read_pla [-zch] <file>\n" );
957  fprintf( pAbc->Err, "\t reads the network in PLA\n" );
958  fprintf( pAbc->Err, "\t-z : toggle reading on-set and off-set [default = %s]\n", fZeros? "off-set":"on-set" );
959  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
960  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
961  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
962  return 1;
963 }
964 
965 /**Function*************************************************************
966 
967  Synopsis []
968 
969  Description []
970 
971  SideEffects []
972 
973  SeeAlso []
974 
975 ***********************************************************************/
976 int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
977 {
978  Abc_Ntk_t * pNtk;
979  char * pSopCover;
980  int fHex;
981  int c;
982 
983  fHex = 1;
984  Extra_UtilGetoptReset();
985  while ( ( c = Extra_UtilGetopt( argc, argv, "xh" ) ) != EOF )
986  {
987  switch ( c )
988  {
989  case 'x':
990  fHex ^= 1;
991  break;
992  case 'h':
993  goto usage;
994  default:
995  goto usage;
996  }
997  }
998 
999  if ( argc != globalUtilOptind + 1 )
1000  {
1001  goto usage;
1002  }
1003 
1004  // convert truth table to SOP
1005  if ( fHex )
1006  pSopCover = Abc_SopFromTruthHex(argv[globalUtilOptind]);
1007  else
1008  pSopCover = Abc_SopFromTruthBin(argv[globalUtilOptind]);
1009  if ( pSopCover == NULL || pSopCover[0] == 0 )
1010  {
1011  ABC_FREE( pSopCover );
1012  fprintf( pAbc->Err, "Reading truth table has failed.\n" );
1013  return 1;
1014  }
1015 
1016  pNtk = Abc_NtkCreateWithNode( pSopCover );
1017  ABC_FREE( pSopCover );
1018  if ( pNtk == NULL )
1019  {
1020  fprintf( pAbc->Err, "Deriving the network has failed.\n" );
1021  return 1;
1022  }
1023  // replace the current network
1024  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1025  Abc_FrameClearVerifStatus( pAbc );
1026  return 0;
1027 
1028 usage:
1029  fprintf( pAbc->Err, "usage: read_truth [-xh] <truth>\n" );
1030  fprintf( pAbc->Err, "\t creates network with node having given truth table\n" );
1031  fprintf( pAbc->Err, "\t-x : toggles between bin and hex representation [default = %s]\n", fHex? "hex":"bin" );
1032  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1033  fprintf( pAbc->Err, "\ttruth : truth table with most signficant bit first (e.g. 1000 for AND(a,b))\n" );
1034  return 1;
1035 }
1036 
1037 /**Function*************************************************************
1038 
1039  Synopsis []
1040 
1041  Description []
1042 
1043  SideEffects []
1044 
1045  SeeAlso []
1046 
1047 ***********************************************************************/
1048 int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv )
1049 {
1050  Abc_Ntk_t * pNtk;
1051  char * pFileName;
1052  int fCheck, fBarBufs;
1053  int c;
1054 
1055  fCheck = 1;
1056  fBarBufs = 0;
1057  glo_fMapped = 0;
1058  Extra_UtilGetoptReset();
1059  while ( ( c = Extra_UtilGetopt( argc, argv, "mcbh" ) ) != EOF )
1060  {
1061  switch ( c )
1062  {
1063  case 'm':
1064  glo_fMapped ^= 1;
1065  break;
1066  case 'c':
1067  fCheck ^= 1;
1068  break;
1069  case 'b':
1070  fBarBufs ^= 1;
1071  break;
1072  case 'h':
1073  goto usage;
1074  default:
1075  goto usage;
1076  }
1077  }
1078  if ( argc != globalUtilOptind + 1 )
1079  goto usage;
1080  // get the input file name
1081  pFileName = argv[globalUtilOptind];
1082  // read the file using the corresponding file reader
1083  pNtk = Io_Read( pFileName, IO_FILE_VERILOG, fCheck, fBarBufs );
1084  if ( pNtk == NULL )
1085  return 1;
1086  // replace the current network
1087  Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
1088  Abc_FrameClearVerifStatus( pAbc );
1089  return 0;
1090 
1091 usage:
1092  fprintf( pAbc->Err, "usage: read_verilog [-mcbh] <file>\n" );
1093  fprintf( pAbc->Err, "\t reads the network in Verilog (IWLS 2002/2005 subset)\n" );
1094  fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog [default = %s]\n", glo_fMapped? "yes":"no" );
1095  fprintf( pAbc->Err, "\t-c : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
1096  fprintf( pAbc->Err, "\t-b : toggle reading barrier buffers [default = %s]\n", fBarBufs? "yes":"no" );
1097  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1098  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1099  return 1;
1100 }
1101 
1102 /**Function*************************************************************
1103 
1104  Synopsis []
1105 
1106  Description []
1107 
1108  SideEffects []
1109 
1110  SeeAlso []
1111 
1112 ***********************************************************************/
1113 int IoCommandReadStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
1114 {
1115  char * pFileName;
1116  FILE * pFile;
1117  int c;
1118  extern int Abc_NtkReadLogFile( char * pFileName, Abc_Cex_t ** ppCex, int * pnFrames );
1119 
1120  Extra_UtilGetoptReset();
1121  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1122  {
1123  switch ( c )
1124  {
1125  case 'h':
1126  goto usage;
1127  default:
1128  goto usage;
1129  }
1130  }
1131  if ( argc != globalUtilOptind + 1 )
1132  {
1133  goto usage;
1134  }
1135 
1136  // get the input file name
1137  pFileName = argv[globalUtilOptind];
1138  if ( (pFile = fopen( pFileName, "r" )) == NULL )
1139  {
1140  fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
1141  return 1;
1142  }
1143  fclose( pFile );
1144 
1145  // set the new network
1146  Abc_FrameClearVerifStatus( pAbc );
1147  pAbc->Status = Abc_NtkReadLogFile( pFileName, &pAbc->pCex, &pAbc->nFrames );
1148  return 0;
1149 
1150 usage:
1151  fprintf( pAbc->Err, "usage: read_status [-ch] <file>\n" );
1152  fprintf( pAbc->Err, "\t reads verification log file\n" );
1153  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1154  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1155  return 1;
1156 }
1157 
1158 /**Function*************************************************************
1159 
1160  Synopsis []
1161 
1162  Description []
1163 
1164  SideEffects []
1165 
1166  SeeAlso []
1167 
1168 ***********************************************************************/
1169 int IoCommandReadGig( Abc_Frame_t * pAbc, int argc, char ** argv )
1170 {
1171  extern Gia_Man_t * Gia_ManReadGig( char * pFileName );
1172  Gia_Man_t * pAig;
1173  char * pFileName;
1174  FILE * pFile;
1175  int c;
1176 
1177  Extra_UtilGetoptReset();
1178  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1179  {
1180  switch ( c )
1181  {
1182  case 'h':
1183  goto usage;
1184  default:
1185  goto usage;
1186  }
1187  }
1188  if ( argc != globalUtilOptind + 1 )
1189  {
1190  goto usage;
1191  }
1192 
1193  // get the input file name
1194  pFileName = argv[globalUtilOptind];
1195  if ( (pFile = fopen( pFileName, "r" )) == NULL )
1196  {
1197  fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
1198  return 1;
1199  }
1200  fclose( pFile );
1201 
1202  // set the new network
1203  pAig = Gia_ManReadGig( pFileName );
1204  //Abc_FrameUpdateGia( pAbc, pAig );
1205  return 0;
1206 
1207 usage:
1208  fprintf( pAbc->Err, "usage: &read_gig [-h] <file>\n" );
1209  fprintf( pAbc->Err, "\t reads design in GIG format\n" );
1210  fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
1211  fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
1212  return 1;
1213 }
1214 
1215 
1216 /**Function*************************************************************
1217 
1218  Synopsis []
1219 
1220  Description []
1221 
1222  SideEffects []
1223 
1224  SeeAlso []
1225 
1226 ***********************************************************************/
1227 int IoCommandWrite( Abc_Frame_t * pAbc, int argc, char **argv )
1228 {
1229  char Command[1000];
1230  char * pFileName;
1231  int c;
1232 
1233  Extra_UtilGetoptReset();
1234  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1235  {
1236  switch ( c )
1237  {
1238  case 'h':
1239  goto usage;
1240  default:
1241  goto usage;
1242  }
1243  }
1244  if ( argc != globalUtilOptind + 1 )
1245  goto usage;
1246  // get the output file name
1247  pFileName = argv[globalUtilOptind];
1248  // write libraries
1249  Command[0] = 0;
1250  assert( strlen(pFileName) < 900 );
1251  if ( !strcmp( Extra_FileNameExtension(pFileName), "genlib" ) )
1252  sprintf( Command, "write_genlib %s", pFileName );
1253  else if ( !strcmp( Extra_FileNameExtension(pFileName), "lib" ) )
1254  sprintf( Command, "write_liberty %s", pFileName );
1255  else if ( !strcmp( Extra_FileNameExtension(pFileName), "dsd" ) )
1256  sprintf( Command, "dsd_save %s", pFileName );
1257  if ( Command[0] )
1258  {
1259  Cmd_CommandExecute( pAbc, Command );
1260  return 0;
1261  }
1262  if ( pAbc->pNtkCur == NULL )
1263  {
1264  fprintf( pAbc->Out, "Empty network.\n" );
1265  return 0;
1266  }
1267  // call the corresponding file writer
1268  Io_Write( pAbc->pNtkCur, pFileName, Io_ReadFileType(pFileName) );
1269  return 0;
1270 
1271 usage:
1272  fprintf( pAbc->Err, "usage: write [-h] <file>\n" );
1273  fprintf( pAbc->Err, "\t writes the current network into <file> by calling\n" );
1274  fprintf( pAbc->Err, "\t the writer that matches the extension of <file>\n" );
1275  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1276  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
1277  return 1;
1278 }
1279 
1280 /**Function*************************************************************
1281 
1282  Synopsis []
1283 
1284  Description []
1285 
1286  SideEffects []
1287 
1288  SeeAlso []
1289 
1290 ***********************************************************************/
1291 int IoCommandWriteHie( Abc_Frame_t * pAbc, int argc, char **argv )
1292 {
1293  char * pBaseName, * pFileName;
1294  int c;
1295 
1296  glo_fMapped = 0;
1297  Extra_UtilGetoptReset();
1298  while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
1299  {
1300  switch ( c )
1301  {
1302  case 'm':
1303  glo_fMapped ^= 1;
1304  break;
1305  case 'h':
1306  goto usage;
1307  default:
1308  goto usage;
1309  }
1310  }
1311  if ( pAbc->pNtkCur == NULL )
1312  {
1313  fprintf( pAbc->Out, "Empty network.\n" );
1314  return 0;
1315  }
1316  if ( argc != globalUtilOptind + 2 )
1317  goto usage;
1318  // get the output file name
1319  pBaseName = argv[globalUtilOptind];
1320  pFileName = argv[globalUtilOptind+1];
1321  // call the corresponding file writer
1322 // Io_Write( pAbc->pNtkCur, pFileName, Io_ReadFileType(pFileName) );
1323  Io_WriteHie( pAbc->pNtkCur, pBaseName, pFileName );
1324  return 0;
1325 
1326 usage:
1327  fprintf( pAbc->Err, "usage: write_hie [-h] <orig> <file>\n" );
1328  fprintf( pAbc->Err, "\t writes the current network into <file> by calling\n" );
1329  fprintf( pAbc->Err, "\t the hierarchical writer that matches the extension of <file>\n" );
1330  fprintf( pAbc->Err, "\t-m : toggle reading mapped Verilog for <orig> [default = %s]\n", glo_fMapped? "yes":"no" );
1331  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1332  fprintf( pAbc->Err, "\torig : the name of the original file with the hierarchical design\n" );
1333  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
1334  return 1;
1335 }
1336 
1337 /**Function*************************************************************
1338 
1339  Synopsis []
1340 
1341  Description []
1342 
1343  SideEffects []
1344 
1345  SeeAlso []
1346 
1347 ***********************************************************************/
1348 int IoCommandWriteAiger( Abc_Frame_t * pAbc, int argc, char **argv )
1349 {
1350  char * pFileName;
1351  int fWriteSymbols;
1352  int fCompact;
1353  int fUnique;
1354  int fVerbose;
1355  int c;
1356 
1357  fWriteSymbols = 0;
1358  fCompact = 0;
1359  fUnique = 0;
1360  fVerbose = 0;
1361  Extra_UtilGetoptReset();
1362  while ( ( c = Extra_UtilGetopt( argc, argv, "scuvh" ) ) != EOF )
1363  {
1364  switch ( c )
1365  {
1366  case 's':
1367  fWriteSymbols ^= 1;
1368  break;
1369  case 'c':
1370  fCompact ^= 1;
1371  break;
1372  case 'u':
1373  fUnique ^= 1;
1374  break;
1375  case 'v':
1376  fVerbose ^= 1;
1377  break;
1378  case 'h':
1379  goto usage;
1380  default:
1381  goto usage;
1382  }
1383  }
1384  if ( pAbc->pNtkCur == NULL )
1385  {
1386  fprintf( pAbc->Out, "Empty network.\n" );
1387  return 0;
1388  }
1389  if ( argc != globalUtilOptind + 1 )
1390  goto usage;
1391  // get the output file name
1392  pFileName = argv[globalUtilOptind];
1393  // call the corresponding file writer
1394  if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
1395  {
1396  fprintf( stdout, "Writing this format is only possible for structurally hashed AIGs.\n" );
1397  return 1;
1398  }
1399  if ( fUnique )
1400  {
1401  extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
1402  extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
1403  Aig_Man_t * pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
1404  Aig_Man_t * pCan = Saig_ManDupIsoCanonical( pAig, fVerbose );
1405  Abc_Ntk_t * pTemp = Abc_NtkFromAigPhase( pCan );
1406  Aig_ManStop( pCan );
1407  Aig_ManStop( pAig );
1408  Io_WriteAiger( pTemp, pFileName, fWriteSymbols, fCompact, fUnique );
1409  Abc_NtkDelete( pTemp );
1410  }
1411  else
1412  Io_WriteAiger( pAbc->pNtkCur, pFileName, fWriteSymbols, fCompact, fUnique );
1413  return 0;
1414 
1415 usage:
1416  fprintf( pAbc->Err, "usage: write_aiger [-scuvh] <file>\n" );
1417  fprintf( pAbc->Err, "\t writes the network in the AIGER format (http://fmv.jku.at/aiger)\n" );
1418  fprintf( pAbc->Err, "\t-s : toggle saving I/O names [default = %s]\n", fWriteSymbols? "yes" : "no" );
1419  fprintf( pAbc->Err, "\t-c : toggle writing more compactly [default = %s]\n", fCompact? "yes" : "no" );
1420  fprintf( pAbc->Err, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
1421  fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
1422  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1423  fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aig)\n" );
1424  return 1;
1425 }
1426 
1427 /**Function*************************************************************
1428 
1429  Synopsis []
1430 
1431  Description []
1432 
1433  SideEffects []
1434 
1435  SeeAlso []
1436 
1437 ***********************************************************************/
1438 int IoCommandWriteAigerCex( Abc_Frame_t * pAbc, int argc, char **argv )
1439 {
1440  char * pFileName;
1441  int c;
1442  Extra_UtilGetoptReset();
1443  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1444  {
1445  switch ( c )
1446  {
1447  case 'h':
1448  goto usage;
1449  default:
1450  goto usage;
1451  }
1452  }
1453  if ( pAbc->pCex == NULL )
1454  {
1455  fprintf( pAbc->Out, "There is no current CEX.\n" );
1456  return 0;
1457  }
1458  if ( argc != globalUtilOptind + 1 )
1459  goto usage;
1460  // get the output file name
1461  pFileName = argv[globalUtilOptind];
1462  Io_WriteAigerCex( pAbc->pCex, pAbc->pNtkCur, pAbc->pGia, pFileName );
1463  return 0;
1464 
1465 usage:
1466  fprintf( pAbc->Err, "usage: write_aiger_cex [-h] <file>\n" );
1467  fprintf( pAbc->Err, "\t writes the current CEX in the AIGER format (http://fmv.jku.at/aiger)\n" );
1468  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1469  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
1470  return 1;
1471 }
1472 
1473 /**Function*************************************************************
1474 
1475  Synopsis []
1476 
1477  Description []
1478 
1479  SideEffects []
1480 
1481  SeeAlso []
1482 
1483 ***********************************************************************/
1484 int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv )
1485 {
1486  char * pFileName;
1487  int c;
1488 
1489  Extra_UtilGetoptReset();
1490  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1491  {
1492  switch ( c )
1493  {
1494  case 'h':
1495  goto usage;
1496  default:
1497  goto usage;
1498  }
1499  }
1500  if ( pAbc->pNtkCur == NULL )
1501  {
1502  fprintf( pAbc->Out, "Empty network.\n" );
1503  return 0;
1504  }
1505  if ( argc != globalUtilOptind + 1 )
1506  goto usage;
1507  // get the output file name
1508  pFileName = argv[globalUtilOptind];
1509  // call the corresponding file writer
1510  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BAF );
1511  return 0;
1512 
1513 usage:
1514  fprintf( pAbc->Err, "usage: write_baf [-h] <file>\n" );
1515  fprintf( pAbc->Err, "\t writes the network into a BLIF file\n" );
1516  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1517  fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .baf)\n" );
1518  return 1;
1519 }
1520 
1521 /**Function*************************************************************
1522 
1523  Synopsis []
1524 
1525  Description []
1526 
1527  SideEffects []
1528 
1529  SeeAlso []
1530 
1531 ***********************************************************************/
1532 int IoCommandWriteBblif( Abc_Frame_t * pAbc, int argc, char **argv )
1533 {
1534  char * pFileName;
1535  int c;
1536 
1537  Extra_UtilGetoptReset();
1538  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1539  {
1540  switch ( c )
1541  {
1542  case 'h':
1543  goto usage;
1544  default:
1545  goto usage;
1546  }
1547  }
1548  if ( pAbc->pNtkCur == NULL )
1549  {
1550  fprintf( pAbc->Out, "Empty network.\n" );
1551  return 0;
1552  }
1553  if ( argc != globalUtilOptind + 1 )
1554  goto usage;
1555  // get the output file name
1556  pFileName = argv[globalUtilOptind];
1557  // call the corresponding file writer
1558  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BBLIF );
1559  return 0;
1560 
1561 usage:
1562  fprintf( pAbc->Err, "usage: write_bblif [-h] <file>\n" );
1563  fprintf( pAbc->Err, "\t writes the network into a binary BLIF file\n" );
1564  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1565  fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bblif)\n" );
1566  return 1;
1567 }
1568 
1569 /**Function*************************************************************
1570 
1571  Synopsis []
1572 
1573  Description []
1574 
1575  SideEffects []
1576 
1577  SeeAlso []
1578 
1579 ***********************************************************************/
1580 int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
1581 {
1582  char * pFileName;
1583  char * pLutStruct = NULL;
1584  int c, fSpecial = 0;
1585  int fUseHie = 0;
1586 
1587  Extra_UtilGetoptReset();
1588  while ( ( c = Extra_UtilGetopt( argc, argv, "Sjah" ) ) != EOF )
1589  {
1590  switch ( c )
1591  {
1592  case 'S':
1593  if ( globalUtilOptind >= argc )
1594  {
1595  Abc_Print( -1, "Command line switch \"-S\" should be followed by string.\n" );
1596  goto usage;
1597  }
1598  pLutStruct = argv[globalUtilOptind];
1599  globalUtilOptind++;
1600  if ( strlen(pLutStruct) != 2 && strlen(pLutStruct) != 3 )
1601  {
1602  Abc_Print( -1, "Command line switch \"-S\" should be followed by a 2- or 3-char string (e.g. \"44\" or \"555\").\n" );
1603  goto usage;
1604  }
1605  break;
1606  case 'j':
1607  fSpecial ^= 1;
1608  break;
1609  case 'a':
1610  fUseHie ^= 1;
1611  break;
1612  case 'h':
1613  goto usage;
1614  default:
1615  goto usage;
1616  }
1617  }
1618  if ( pAbc->pNtkCur == NULL )
1619  {
1620  fprintf( pAbc->Out, "Empty network.\n" );
1621  return 0;
1622  }
1623  if ( argc != globalUtilOptind + 1 )
1624  goto usage;
1625  // get the output file name
1626  pFileName = argv[globalUtilOptind];
1627  // call the corresponding file writer
1628  if ( fSpecial || pLutStruct )
1629  Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName, pLutStruct, fUseHie );
1630  else
1631  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
1632  return 0;
1633 
1634 usage:
1635  fprintf( pAbc->Err, "usage: write_blif [-S str] [-jah] <file>\n" );
1636  fprintf( pAbc->Err, "\t writes the network into a BLIF file\n" );
1637  fprintf( pAbc->Err, "\t-S str : string representing the LUT structure [default = %s]\n", pLutStruct ? pLutStruct : "not used" );
1638  fprintf( pAbc->Err, "\t-j : enables special BLIF writing [default = %s]\n", fSpecial? "yes" : "no" );;
1639  fprintf( pAbc->Err, "\t-a : enables hierarchical BLIF writing for LUT structures [default = %s]\n", fUseHie? "yes" : "no" );;
1640  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1641  fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
1642  return 1;
1643 }
1644 
1645 /**Function*************************************************************
1646 
1647  Synopsis []
1648 
1649  Description []
1650 
1651  SideEffects []
1652 
1653  SeeAlso []
1654 
1655 ***********************************************************************/
1656 int IoCommandWriteBlifMv( Abc_Frame_t * pAbc, int argc, char **argv )
1657 {
1658  char * pFileName;
1659  int c;
1660 
1661  Extra_UtilGetoptReset();
1662  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1663  {
1664  switch ( c )
1665  {
1666  case 'h':
1667  goto usage;
1668  default:
1669  goto usage;
1670  }
1671  }
1672  if ( pAbc->pNtkCur == NULL )
1673  {
1674  fprintf( pAbc->Out, "Empty network.\n" );
1675  return 0;
1676  }
1677  if ( argc != globalUtilOptind + 1 )
1678  goto usage;
1679  // get the output file name
1680  pFileName = argv[globalUtilOptind];
1681  // call the corresponding file writer
1682  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIFMV );
1683  return 0;
1684 
1685 usage:
1686  fprintf( pAbc->Err, "usage: write_blif_mv [-h] <file>\n" );
1687  fprintf( pAbc->Err, "\t writes the network into a BLIF-MV file\n" );
1688  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1689  fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .mv)\n" );
1690  return 1;
1691 }
1692 
1693 /**Function*************************************************************
1694 
1695  Synopsis []
1696 
1697  Description []
1698 
1699  SideEffects []
1700 
1701  SeeAlso []
1702 
1703 ***********************************************************************/
1704 int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv )
1705 {
1706  char * pFileName;
1707  int fUseLuts;
1708  int c;
1709 
1710  fUseLuts = 1;
1711  Extra_UtilGetoptReset();
1712  while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF )
1713  {
1714  switch ( c )
1715  {
1716  case 'l':
1717  fUseLuts ^= 1;
1718  break;
1719  case 'h':
1720  goto usage;
1721  default:
1722  goto usage;
1723  }
1724  }
1725  if ( pAbc->pNtkCur == NULL )
1726  {
1727  fprintf( pAbc->Out, "Empty network.\n" );
1728  return 0;
1729  }
1730  if ( argc != globalUtilOptind + 1 )
1731  goto usage;
1732  // get the output file name
1733  pFileName = argv[globalUtilOptind];
1734  // call the corresponding file writer
1735  if ( !fUseLuts )
1736  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BENCH );
1737  else if ( pAbc->pNtkCur )
1738  {
1739  Abc_Ntk_t * pNtkTemp;
1740  pNtkTemp = Abc_NtkToNetlist( pAbc->pNtkCur );
1741  Abc_NtkToAig( pNtkTemp );
1742  Io_WriteBenchLut( pNtkTemp, pFileName );
1743  Abc_NtkDelete( pNtkTemp );
1744  }
1745  else
1746  printf( "There is no current network.\n" );
1747  return 0;
1748 
1749 usage:
1750  fprintf( pAbc->Err, "usage: write_bench [-lh] <file>\n" );
1751  fprintf( pAbc->Err, "\t writes the network in BENCH format\n" );
1752  fprintf( pAbc->Err, "\t-l : toggle using LUTs in the output [default = %s]\n", fUseLuts? "yes" : "no" );
1753  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1754  fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .bench)\n" );
1755  return 1;
1756 }
1757 
1758 /**Function*************************************************************
1759 
1760  Synopsis []
1761 
1762  Description []
1763 
1764  SideEffects []
1765 
1766  SeeAlso []
1767 
1768 ***********************************************************************/
1769 int IoCommandWriteBook( Abc_Frame_t * pAbc, int argc, char **argv )
1770 {
1771  char * pFileName;
1772  int c;
1773  Extra_UtilGetoptReset();
1774  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1775  {
1776  switch ( c )
1777  {
1778  case 'h':
1779  goto usage;
1780  default:
1781  goto usage;
1782  }
1783  }
1784  if ( argc != globalUtilOptind + 1 )
1785  goto usage;
1786  // get the output file name
1787  pFileName = argv[globalUtilOptind];
1788  // call the corresponding file writer
1789  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BOOK );
1790  return 0;
1791 
1792 usage:
1793  fprintf( pAbc->Err, "usage: write_book [-h] <file> [-options]\n" );
1794  fprintf( pAbc->Err, "\t-h : prints the help massage\n" );
1795  fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .aux, .nodes, .nets)\n" );
1796  fprintf( pAbc->Err, "\t\n" );
1797  fprintf( pAbc->Err, "\tThis command is developed by Myungchul Kim (University of Michigan).\n" );
1798  return 1;
1799 }
1800 
1801 /**Function*************************************************************
1802 
1803  Synopsis []
1804 
1805  Description []
1806 
1807  SideEffects []
1808 
1809  SeeAlso []
1810 
1811 ***********************************************************************/
1812 int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv )
1813 {
1814  Abc_Ntk_t * pNtk;
1815  char * pFileName;
1816  int c;
1817  extern void Io_WriteCellNet( Abc_Ntk_t * pNtk, char * pFileName );
1818 
1819  Extra_UtilGetoptReset();
1820  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
1821  {
1822  switch ( c )
1823  {
1824  case 'h':
1825  goto usage;
1826  default:
1827  goto usage;
1828  }
1829  }
1830  if ( pAbc->pNtkCur == NULL )
1831  {
1832  fprintf( pAbc->Out, "Empty network.\n" );
1833  return 0;
1834  }
1835  if ( argc != globalUtilOptind + 1 )
1836  goto usage;
1837  pNtk = pAbc->pNtkCur;
1838  // get the output file name
1839  pFileName = argv[globalUtilOptind];
1840  // call the corresponding file writer
1841  if ( !Abc_NtkIsLogic(pNtk) )
1842  {
1843  fprintf( pAbc->Out, "The network should be a logic network (if it an AIG, use command \"logic\")\n" );
1844  return 0;
1845  }
1846  Io_WriteCellNet( pNtk, pFileName );
1847  return 0;
1848 
1849 usage:
1850  fprintf( pAbc->Err, "usage: write_cellnet [-h] <file>\n" );
1851  fprintf( pAbc->Err, "\t writes the network is the cellnet format\n" );
1852  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1853  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
1854  return 1;
1855 }
1856 
1857 /**Function*************************************************************
1858 
1859  Synopsis []
1860 
1861  Description []
1862 
1863  SideEffects []
1864 
1865  SeeAlso []
1866 
1867 ***********************************************************************/
1868 int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv )
1869 {
1870  char * pFileName;
1871  int c;
1872  int fNewAlgo;
1873  int fFastAlgo;
1874  int fAllPrimes;
1875  int fChangePol;
1876  int fVerbose;
1877  extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo, int fChangePol, int fVerbose );
1878 
1879  fNewAlgo = 1;
1880  fFastAlgo = 0;
1881  fAllPrimes = 0;
1882  fChangePol = 1;
1883  fVerbose = 0;
1884  Extra_UtilGetoptReset();
1885  while ( ( c = Extra_UtilGetopt( argc, argv, "nfpcvh" ) ) != EOF )
1886  {
1887  switch ( c )
1888  {
1889  case 'n':
1890  fNewAlgo ^= 1;
1891  break;
1892  case 'f':
1893  fFastAlgo ^= 1;
1894  break;
1895  case 'p':
1896  fAllPrimes ^= 1;
1897  break;
1898  case 'c':
1899  fChangePol ^= 1;
1900  break;
1901  case 'v':
1902  fVerbose ^= 1;
1903  break;
1904  case 'h':
1905  goto usage;
1906  default:
1907  goto usage;
1908  }
1909  }
1910  if ( pAbc->pNtkCur == NULL )
1911  {
1912  fprintf( pAbc->Out, "Empty network.\n" );
1913  return 0;
1914  }
1915  if ( argc != globalUtilOptind + 1 )
1916  goto usage;
1917  // get the output file name
1918  pFileName = argv[globalUtilOptind];
1919  // check if the feature will be used
1920  if ( Abc_NtkIsStrash(pAbc->pNtkCur) && fAllPrimes )
1921  {
1922  fAllPrimes = 0;
1923  printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" );
1924  }
1925  // call the corresponding file writer
1926  if ( fFastAlgo )
1927  Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 1, fChangePol, fVerbose );
1928  else if ( fNewAlgo )
1929  Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName, 0, fChangePol, fVerbose );
1930  else if ( fAllPrimes )
1931  Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 );
1932  else
1933  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF );
1934  return 0;
1935 
1936 usage:
1937  fprintf( pAbc->Err, "usage: write_cnf [-nfpcvh] <file>\n" );
1938  fprintf( pAbc->Err, "\t generates CNF for the miter (see also \"&write_cnf\")\n" );
1939  fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
1940  fprintf( pAbc->Err, "\t-f : toggle using fast algorithm [default = %s]\n", fFastAlgo? "yes" : "no" );
1941  fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" );
1942  fprintf( pAbc->Err, "\t-c : toggle adjasting polarity of internal variables [default = %s]\n", fChangePol? "yes" : "no" );
1943  fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
1944  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
1945  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
1946  return 1;
1947 }
1948 
1949 /**Function*************************************************************
1950 
1951  Synopsis []
1952 
1953  Description []
1954 
1955  SideEffects []
1956 
1957  SeeAlso []
1958 
1959 ***********************************************************************/
1960 int IoCommandWriteCnf2( Abc_Frame_t * pAbc, int argc, char **argv )
1961 {
1962  extern void Jf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int fVerbose );
1963  extern void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
1964  FILE * pFile;
1965  char * pFileName;
1966  int nLutSize = 6;
1967  int fNewAlgo = 1;
1968  int fCnfObjIds = 0;
1969  int fAddOrCla = 1;
1970  int c, fVerbose = 0;
1971  Extra_UtilGetoptReset();
1972  while ( ( c = Extra_UtilGetopt( argc, argv, "Kaiovh" ) ) != EOF )
1973  {
1974  switch ( c )
1975  {
1976  case 'K':
1977  if ( globalUtilOptind >= argc )
1978  {
1979  Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
1980  goto usage;
1981  }
1982  nLutSize = atoi(argv[globalUtilOptind]);
1983  globalUtilOptind++;
1984  break;
1985  case 'a':
1986  fNewAlgo ^= 1;
1987  break;
1988  case 'i':
1989  fCnfObjIds ^= 1;
1990  break;
1991  case 'o':
1992  fAddOrCla ^= 1;
1993  break;
1994  case 'v':
1995  fVerbose ^= 1;
1996  break;
1997  case 'h':
1998  goto usage;
1999  default:
2000  goto usage;
2001  }
2002  }
2003  if ( pAbc->pGia == NULL )
2004  {
2005  Abc_Print( -1, "IoCommandWriteCnf2(): There is no AIG.\n" );
2006  return 1;
2007  }
2008  if ( Gia_ManRegNum(pAbc->pGia) > 0 )
2009  {
2010  Abc_Print( -1, "IoCommandWriteCnf2(): Works only for combinational miters.\n" );
2011  return 0;
2012  }
2013  if ( nLutSize < 3 || nLutSize > 8 )
2014  {
2015  Abc_Print( -1, "IoCommandWriteCnf2(): Invalid LUT size (%d).\n", nLutSize );
2016  return 0;
2017  }
2018  if ( !fNewAlgo && !Sdm_ManCanRead() )
2019  {
2020  Abc_Print( -1, "IoCommandWriteCnf2(): Cannot input precomputed DSD information.\n" );
2021  return 0;
2022  }
2023  if ( argc != globalUtilOptind + 1 )
2024  goto usage;
2025  // get the input file name
2026  pFileName = argv[globalUtilOptind];
2027  pFile = fopen( pFileName, "wb" );
2028  if ( pFile == NULL )
2029  {
2030  printf( "Cannot open file \"%s\" for writing.\n", pFileName );
2031  return 0;
2032  }
2033  fclose( pFile );
2034  if ( fNewAlgo )
2035  Mf_ManDumpCnf( pAbc->pGia, pFileName, nLutSize, fCnfObjIds, fAddOrCla, fVerbose );
2036  else
2037  Jf_ManDumpCnf( pAbc->pGia, pFileName, fVerbose );
2038  return 0;
2039 
2040 usage:
2041  fprintf( pAbc->Err, "usage: &write_cnf [-Kaiovh] <file>\n" );
2042  fprintf( pAbc->Err, "\t writes CNF produced by a new generator\n" );
2043  fprintf( pAbc->Err, "\t-K <num> : the LUT size (3 <= num <= 8) [default = %d]\n", nLutSize );
2044  fprintf( pAbc->Err, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" );
2045  fprintf( pAbc->Err, "\t-i : toggle using AIG object IDs as CNF variables [default = %s]\n", fCnfObjIds? "yes" : "no" );
2046  fprintf( pAbc->Err, "\t-o : toggle adding OR clause for the outputs [default = %s]\n", fAddOrCla? "yes" : "no" );
2047  fprintf( pAbc->Err, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes" : "no" );
2048  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2049  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2050  return 1;
2051 }
2052 
2053 
2054 /**Function*************************************************************
2055 
2056  Synopsis []
2057 
2058  Description []
2059 
2060  SideEffects []
2061 
2062  SeeAlso []
2063 
2064 ***********************************************************************/
2065 int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv )
2066 {
2067  char * pFileName;
2068  int c;
2069 
2070  Extra_UtilGetoptReset();
2071  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2072  {
2073  switch ( c )
2074  {
2075  case 'h':
2076  goto usage;
2077  default:
2078  goto usage;
2079  }
2080  }
2081  if ( pAbc->pNtkCur == NULL )
2082  {
2083  fprintf( pAbc->Out, "Empty network.\n" );
2084  return 0;
2085  }
2086  if ( argc != globalUtilOptind + 1 )
2087  goto usage;
2088  // get the output file name
2089  pFileName = argv[globalUtilOptind];
2090  // call the corresponding file writer
2091  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_DOT );
2092  return 0;
2093 
2094 usage:
2095  fprintf( pAbc->Err, "usage: write_dot [-h] <file>\n" );
2096  fprintf( pAbc->Err, "\t writes the current network into a DOT file\n" );
2097  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2098  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2099  return 1;
2100 }
2101 
2102 ABC_NAMESPACE_IMPL_END
2103 
2104 #include "proof/fra/fra.h"
2105 
2106 ABC_NAMESPACE_IMPL_START
2107 
2108 
2109 /**Function*************************************************************
2110 
2111  Synopsis []
2112 
2113  Description []
2114 
2115  SideEffects []
2116 
2117  SeeAlso []
2118 
2119 ***********************************************************************/
2120 int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
2121 {
2122  Abc_Ntk_t * pNtk;
2123  char * pFileName;
2124  int c, fNames = 0;
2125  int fMinimize = 0;
2126  int fUseOldMin = 0;
2127  int fCheckCex = 0;
2128  int forceSeq = 0;
2129  int fAiger = 0;
2130  int fPrintFull = 0;
2131  int fVerbose = 0;
2132 
2133  Extra_UtilGetoptReset();
2134  while ( ( c = Extra_UtilGetopt( argc, argv, "snmocafvh" ) ) != EOF )
2135  {
2136  switch ( c )
2137  {
2138  case 's':
2139  forceSeq ^= 1;
2140  break;
2141  case 'n':
2142  fNames ^= 1;
2143  break;
2144  case 'm':
2145  fMinimize ^= 1;
2146  break;
2147  case 'o':
2148  fUseOldMin ^= 1;
2149  break;
2150  case 'c':
2151  fCheckCex ^= 1;
2152  break;
2153  case 'a':
2154  fAiger ^= 1;
2155  break;
2156  case 'f':
2157  fPrintFull ^= 1;
2158  break;
2159  case 'v':
2160  fVerbose ^= 1;
2161  break;
2162  case 'h':
2163  goto usage;
2164  default:
2165  goto usage;
2166  }
2167  }
2168  pNtk = pAbc->pNtkCur;
2169  if ( pNtk == NULL )
2170  {
2171  fprintf( pAbc->Out, "Empty network.\n" );
2172  return 0;
2173  }
2174  if ( pNtk->pModel == NULL && pAbc->pCex == NULL )
2175  {
2176  fprintf( pAbc->Out, "Counter-example is not available.\n" );
2177  return 0;
2178  }
2179  if ( argc != globalUtilOptind + 1 )
2180  {
2181  printf( "File name is missing on the command line.\n" );
2182  goto usage;
2183  }
2184 
2185  // get the input file name
2186  pFileName = argv[globalUtilOptind];
2187  // write the counter-example into the file
2188  if ( pAbc->pCex )
2189  {
2190  Abc_Cex_t * pCex = pAbc->pCex;
2191  Abc_Obj_t * pObj;
2192  FILE * pFile;
2193  int i, f;
2194  Abc_NtkForEachLatch( pNtk, pObj, i )
2195  if ( !Abc_LatchIsInit0(pObj) )
2196  {
2197  fprintf( stdout, "IoCommandWriteCex(): The init-state should be all-0 for counter-example to work.\n" );
2198  fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
2199  return 1;
2200  }
2201 
2202  pFile = fopen( pFileName, "w" );
2203  if ( pFile == NULL )
2204  {
2205  fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName );
2206  return 1;
2207  }
2208  if ( fPrintFull )
2209  {
2210  extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
2211  Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
2212  Abc_Cex_t * pCexFull = Saig_ManExtendCex( pAig, pCex );
2213  Aig_ManStop( pAig );
2214  // output PI values (while skipping the minimized ones)
2215  assert( pCexFull->nBits == Abc_NtkCiNum(pNtk) * (pCex->iFrame + 1) );
2216  for ( f = 0; f <= pCex->iFrame; f++ )
2217  Abc_NtkForEachCi( pNtk, pObj, i )
2218  fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) );
2219  Abc_CexFreeP( &pCexFull );
2220  }
2221  else if ( fNames )
2222  {
2223  Abc_Cex_t * pCare = NULL;
2224  if ( fMinimize )
2225  {
2226  extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
2227  Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
2228  if ( fUseOldMin )
2229  {
2230  pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
2231  if ( fCheckCex )
2232  Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
2233  }
2234  else
2235  pCare = Bmc_CexCareMinimize( pAig, pCex, fCheckCex, fVerbose );
2236  Aig_ManStop( pAig );
2237  }
2238  // output flop values (unaffected by the minimization)
2239  Abc_NtkForEachLatch( pNtk, pObj, i )
2240  fprintf( pFile, "%s@0=%c ", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
2241  // output PI values (while skipping the minimized ones)
2242  for ( f = 0; f <= pCex->iFrame; f++ )
2243  Abc_NtkForEachPi( pNtk, pObj, i )
2244  if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
2245  fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
2246  Abc_CexFreeP( &pCare );
2247  }
2248  else
2249  {
2250  Abc_NtkForEachLatch( pNtk, pObj, i )
2251  fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
2252 
2253  for ( i = pCex->nRegs; i < pCex->nBits; i++ )
2254  {
2255  if ( fAiger && (i-pCex->nRegs)%pCex->nPis == 0)
2256  fprintf( pFile, "\n");
2257  fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) );
2258  }
2259  }
2260  fprintf( pFile, "\n" );
2261  fclose( pFile );
2262  }
2263  else
2264  {
2265  Abc_Obj_t * pObj;
2266  FILE * pFile = fopen( pFileName, "w" );
2267  int i;
2268  if ( pFile == NULL )
2269  {
2270  fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName );
2271  return 1;
2272  }
2273  if ( fNames )
2274  {
2275  const char *cycle_ctr = forceSeq?"@0":"";
2276  Abc_NtkForEachPi( pNtk, pObj, i )
2277 // fprintf( pFile, "%s=%c\n", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
2278  fprintf( pFile, "%s%s=%c\n", Abc_ObjName(pObj), cycle_ctr, '0'+(pNtk->pModel[i]==1) );
2279  }
2280  else
2281  {
2282  Abc_NtkForEachPi( pNtk, pObj, i )
2283  fprintf( pFile, "%c", '0'+(pNtk->pModel[i]==1) );
2284  }
2285  fprintf( pFile, "\n" );
2286  fclose( pFile );
2287  }
2288 
2289  return 0;
2290 
2291 usage:
2292  fprintf( pAbc->Err, "usage: write_cex [-snmocfvh] <file>\n" );
2293  fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
2294  fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" );
2295  fprintf( pAbc->Err, "\t-s : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
2296  fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
2297  fprintf( pAbc->Err, "\t-m : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
2298  fprintf( pAbc->Err, "\t-o : use old counter-example minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
2299  fprintf( pAbc->Err, "\t-c : check generated counter-example using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
2300  fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s].\n", fAiger? "yes": "no" );
2301  fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "yes": "no" );
2302  fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
2303  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2304  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2305  return 1;
2306 }
2307 
2308 /**Function*************************************************************
2309 
2310  Synopsis []
2311 
2312  Description []
2313 
2314  SideEffects []
2315 
2316  SeeAlso []
2317 
2318 ***********************************************************************/
2319 int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
2320 {
2321  char * pFileName;
2322  int c;
2323 
2324  Extra_UtilGetoptReset();
2325  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2326  {
2327  switch ( c )
2328  {
2329  case 'h':
2330  goto usage;
2331  default:
2332  goto usage;
2333  }
2334  }
2335  if ( pAbc->pNtkCur == NULL )
2336  {
2337  fprintf( pAbc->Out, "Empty network.\n" );
2338  return 0;
2339  }
2340  if ( argc != globalUtilOptind + 1 )
2341  goto usage;
2342  // get the output file name
2343  pFileName = argv[globalUtilOptind];
2344  // call the corresponding file writer
2345  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_EQN );
2346  return 0;
2347 
2348 usage:
2349  fprintf( pAbc->Err, "usage: write_eqn [-h] <file>\n" );
2350  fprintf( pAbc->Err, "\t writes the current network in the equation format\n" );
2351  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2352  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2353  return 1;
2354 }
2355 
2356 /**Function*************************************************************
2357 
2358  Synopsis []
2359 
2360  Description []
2361 
2362  SideEffects []
2363 
2364  SeeAlso []
2365 
2366 ***********************************************************************/
2367 int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv )
2368 {
2369  char * pFileName;
2370  int c;
2371 
2372  Extra_UtilGetoptReset();
2373  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2374  {
2375  switch ( c )
2376  {
2377  case 'h':
2378  goto usage;
2379  default:
2380  goto usage;
2381  }
2382  }
2383  if ( pAbc->pNtkCur == NULL )
2384  {
2385  fprintf( pAbc->Out, "Empty network.\n" );
2386  return 0;
2387  }
2388  if ( argc != globalUtilOptind + 1 )
2389  goto usage;
2390  // get the output file name
2391  pFileName = argv[globalUtilOptind];
2392  // call the corresponding file writer
2393  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_GML );
2394  return 0;
2395 
2396 usage:
2397  fprintf( pAbc->Err, "usage: write_gml [-h] <file>\n" );
2398  fprintf( pAbc->Err, "\t writes network using graph representation formal GML\n" );
2399  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2400  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2401  return 1;
2402 }
2403 
2404 /**Function*************************************************************
2405 
2406  Synopsis []
2407 
2408  Description []
2409 
2410  SideEffects []
2411 
2412  SeeAlso []
2413 
2414 ***********************************************************************/
2415 int IoCommandWriteList( Abc_Frame_t * pAbc, int argc, char **argv )
2416 {
2417  char * pFileName;
2418  int fUseHost;
2419  int c;
2420 
2421  printf( "This command currently does not work.\n" );
2422  return 0;
2423 
2424  fUseHost = 1;
2425  Extra_UtilGetoptReset();
2426  while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF )
2427  {
2428  switch ( c )
2429  {
2430  case 'n':
2431  fUseHost ^= 1;
2432  break;
2433  case 'h':
2434  goto usage;
2435  default:
2436  goto usage;
2437  }
2438  }
2439  if ( pAbc->pNtkCur == NULL )
2440  {
2441  fprintf( pAbc->Out, "Empty network.\n" );
2442  return 0;
2443  }
2444  if ( argc != globalUtilOptind + 1 )
2445  goto usage;
2446 /*
2447  if ( !Abc_NtkIsSeq(pAbc->pNtkCur) )
2448  {
2449  fprintf( stdout, "IoCommandWriteList(): Can write adjacency list for sequential AIGs only.\n" );
2450  return 0;
2451  }
2452 */
2453  // get the input file name
2454  pFileName = argv[globalUtilOptind];
2455  // write the file
2456  Io_WriteList( pAbc->pNtkCur, pFileName, fUseHost );
2457  return 0;
2458 
2459 usage:
2460  fprintf( pAbc->Err, "usage: write_list [-nh] <file>\n" );
2461  fprintf( pAbc->Err, "\t writes network using graph representation formal GML\n" );
2462  fprintf( pAbc->Err, "\t-n : toggle writing host node [default = %s]\n", fUseHost? "yes":"no" );
2463  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2464  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2465  return 1;
2466 }
2467 
2468 /**Function*************************************************************
2469 
2470  Synopsis []
2471 
2472  Description []
2473 
2474  SideEffects []
2475 
2476  SeeAlso []
2477 
2478 ***********************************************************************/
2479 int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
2480 {
2481  char * pFileName;
2482  int c;
2483 
2484  Extra_UtilGetoptReset();
2485  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2486  {
2487  switch ( c )
2488  {
2489  case 'h':
2490  goto usage;
2491  default:
2492  goto usage;
2493  }
2494  }
2495  if ( pAbc->pNtkCur == NULL )
2496  {
2497  fprintf( pAbc->Out, "Empty network.\n" );
2498  return 0;
2499  }
2500  if ( argc != globalUtilOptind + 1 )
2501  goto usage;
2502  // get the output file name
2503  pFileName = argv[globalUtilOptind];
2504  // call the corresponding file writer
2505  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_PLA );
2506  return 0;
2507 
2508 usage:
2509  fprintf( pAbc->Err, "usage: write_pla [-h] <file>\n" );
2510  fprintf( pAbc->Err, "\t writes the collapsed network into a PLA file\n" );
2511  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2512  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2513  return 1;
2514 }
2515 
2516 /**Function*************************************************************
2517 
2518  Synopsis []
2519 
2520  Description []
2521 
2522  SideEffects []
2523 
2524  SeeAlso []
2525 
2526 ***********************************************************************/
2527 int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
2528 {
2529  char * pFileName;
2530  int c;
2531 
2532  Extra_UtilGetoptReset();
2533  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2534  {
2535  switch ( c )
2536  {
2537  case 'h':
2538  goto usage;
2539  default:
2540  goto usage;
2541  }
2542  }
2543  if ( pAbc->pNtkCur == NULL )
2544  {
2545  fprintf( pAbc->Out, "Empty network.\n" );
2546  return 0;
2547  }
2548  if ( argc != globalUtilOptind + 1 )
2549  goto usage;
2550  // get the output file name
2551  pFileName = argv[globalUtilOptind];
2552  // call the corresponding file writer
2553  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_VERILOG );
2554  return 0;
2555 
2556 usage:
2557  fprintf( pAbc->Err, "usage: write_verilog [-h] <file>\n" );
2558  fprintf( pAbc->Err, "\t writes the current network in Verilog format\n" );
2559  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2560  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2561  return 1;
2562 }
2563 
2564 /**Function*************************************************************
2565 
2566  Synopsis []
2567 
2568  Description []
2569 
2570  SideEffects []
2571 
2572  SeeAlso []
2573 
2574 ***********************************************************************/
2575 int IoCommandWriteSortCnf( Abc_Frame_t * pAbc, int argc, char **argv )
2576 {
2577  char * pFileName;
2578  int c;
2579  int nVars = 16;
2580  int nQueens = 4;
2581  extern void Abc_NtkWriteSorterCnf( char * pFileName, int nVars, int nQueens );
2582 
2583  Extra_UtilGetoptReset();
2584  while ( ( c = Extra_UtilGetopt( argc, argv, "NQh" ) ) != EOF )
2585  {
2586  switch ( c )
2587  {
2588  case 'N':
2589  if ( globalUtilOptind >= argc )
2590  {
2591  fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
2592  goto usage;
2593  }
2594  nVars = atoi(argv[globalUtilOptind]);
2595  globalUtilOptind++;
2596  if ( nVars <= 0 )
2597  goto usage;
2598  break;
2599  case 'Q':
2600  if ( globalUtilOptind >= argc )
2601  {
2602  fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
2603  goto usage;
2604  }
2605  nQueens = atoi(argv[globalUtilOptind]);
2606  globalUtilOptind++;
2607  if ( nQueens <= 0 )
2608  goto usage;
2609  break;
2610  case 'h':
2611  goto usage;
2612  default:
2613  goto usage;
2614  }
2615  }
2616  if ( argc != globalUtilOptind + 1 )
2617  goto usage;
2618  // get the output file name
2619  pFileName = argv[globalUtilOptind];
2620  Abc_NtkWriteSorterCnf( pFileName, nVars, nQueens );
2621  // call the corresponding file writer
2622  return 0;
2623 
2624 usage:
2625  fprintf( pAbc->Err, "usage: write_sorter_cnf [-N <num>] [-Q <num>] <file>\n" );
2626  fprintf( pAbc->Err, "\t writes CNF for the sorter\n" );
2627  fprintf( pAbc->Err, "\t-N num : the number of sorter bits [default = %d]\n", nVars );
2628  fprintf( pAbc->Err, "\t-Q num : the number of bits to be asserted to 1 [default = %d]\n", nQueens );
2629  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2630  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2631  return 1;
2632 }
2633 
2634 /**Function*************************************************************
2635 
2636  Synopsis []
2637 
2638  Description []
2639 
2640  SideEffects []
2641 
2642  SeeAlso []
2643 
2644 ***********************************************************************/
2645 int IoCommandWriteTruth( Abc_Frame_t * pAbc, int argc, char **argv )
2646 {
2647  Vec_Int_t * vTruth;
2648  Abc_Ntk_t * pNtk = pAbc->pNtkCur;
2649  Abc_Obj_t * pNode;
2650  char * pFileName;
2651  FILE * pFile;
2652  unsigned * pTruth;
2653  int fReverse = 0;
2654  int c;
2655 
2656  Extra_UtilGetoptReset();
2657  while ( ( c = Extra_UtilGetopt( argc, argv, "rh" ) ) != EOF )
2658  {
2659  switch ( c )
2660  {
2661  case 'r':
2662  fReverse ^= 1;
2663  break;
2664  case 'h':
2665  goto usage;
2666  default:
2667  goto usage;
2668  }
2669  }
2670  if ( pAbc->pNtkCur == NULL )
2671  {
2672  printf( "Current network is not available.\n" );
2673  return 0;
2674  }
2675  if ( !Abc_NtkIsLogic(pNtk) )
2676  {
2677  printf( "Current network should not an AIG. Run \"logic\".\n" );
2678  return 0;
2679  }
2680  if ( Abc_NtkPoNum(pNtk) != 1 )
2681  {
2682  printf( "Current network should have exactly one primary output.\n" );
2683  return 0;
2684  }
2685  if ( Abc_NtkNodeNum(pNtk) != 1 )
2686  {
2687  printf( "Current network should have exactly one node.\n" );
2688  return 0;
2689  }
2690  pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
2691  if ( Abc_ObjFaninNum(pNode) == 0 )
2692  {
2693  printf( "Can only write logic function with 0 inputs.\n" );
2694  return 0;
2695  }
2696  if ( Abc_ObjFaninNum(pNode) > 16 )
2697  {
2698  printf( "Can only write logic function with no more than 16 inputs.\n" );
2699  return 0;
2700  }
2701  if ( argc != globalUtilOptind + 1 )
2702  goto usage;
2703  // get the input file name
2704  pFileName = argv[globalUtilOptind];
2705  // convert to logic
2706  Abc_NtkToAig( pNtk );
2707  vTruth = Vec_IntAlloc( 0 );
2708  pTruth = Hop_ManConvertAigToTruth( (Hop_Man_t *)pNtk->pManFunc, (Hop_Obj_t *)pNode->pData, Abc_ObjFaninNum(pNode), vTruth, fReverse );
2709  pFile = fopen( pFileName, "w" );
2710  if ( pFile == NULL )
2711  {
2712  Vec_IntFree( vTruth );
2713  printf( "Cannot open file \"%s\" for writing.\n", pFileName );
2714  return 0;
2715  }
2716  Extra_PrintBinary( pFile, pTruth, 1<<Abc_ObjFaninNum(pNode) );
2717  fclose( pFile );
2718  Vec_IntFree( vTruth );
2719  return 0;
2720 
2721 usage:
2722  fprintf( pAbc->Err, "usage: write_truth [-rh] <file>\n" );
2723  fprintf( pAbc->Err, "\t writes truth table into a file\n" );
2724  fprintf( pAbc->Err, "\t-r : toggle reversing bits in the truth table [default = %s]\n", fReverse? "yes":"no" );
2725  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2726  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2727  return 1;
2728 }
2729 
2730 
2731 /**Function*************************************************************
2732 
2733  Synopsis []
2734 
2735  Description []
2736 
2737  SideEffects []
2738 
2739  SeeAlso []
2740 
2741 ***********************************************************************/
2742 int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
2743 {
2744  Gia_Obj_t * pObj;
2745  char * pFileName;
2746  FILE * pFile;
2747  word * pTruth;
2748  int nBytes;
2749  int fReverse = 0;
2750  int fBinary = 0;
2751  int c, i;
2752 
2753  Extra_UtilGetoptReset();
2754  while ( ( c = Extra_UtilGetopt( argc, argv, "rbh" ) ) != EOF )
2755  {
2756  switch ( c )
2757  {
2758  case 'r':
2759  fReverse ^= 1;
2760  break;
2761  case 'b':
2762  fBinary ^= 1;
2763  break;
2764  case 'h':
2765  goto usage;
2766  default:
2767  goto usage;
2768  }
2769  }
2770  if ( pAbc->pGia == NULL )
2771  {
2772  Abc_Print( -1, "IoCommandWriteTruths(): There is no AIG.\n" );
2773  return 1;
2774  }
2775  if ( Gia_ManPiNum(pAbc->pGia) > 16 )
2776  {
2777  Abc_Print( -1, "IoCommandWriteTruths(): Can write truth tables up to 16 inputs.\n" );
2778  return 0;
2779  }
2780  if ( Gia_ManPiNum(pAbc->pGia) < 3 )
2781  {
2782  Abc_Print( -1, "IoCommandWriteTruths(): Can write truth tables for 3 inputs or more.\n" );
2783  return 0;
2784  }
2785  if ( argc != globalUtilOptind + 1 )
2786  goto usage;
2787  // get the input file name
2788  pFileName = argv[globalUtilOptind];
2789  // convert to logic
2790  pFile = fopen( pFileName, "wb" );
2791  if ( pFile == NULL )
2792  {
2793  printf( "Cannot open file \"%s\" for writing.\n", pFileName );
2794  return 0;
2795  }
2796  nBytes = 8 * Abc_Truth6WordNum( Gia_ManPiNum(pAbc->pGia) );
2797  Gia_ManForEachCo( pAbc->pGia, pObj, i )
2798  {
2799  pTruth = Gia_ObjComputeTruthTable( pAbc->pGia, pObj );
2800  if ( fBinary )
2801  fwrite( pTruth, nBytes, 1, pFile );
2802  else
2803  Extra_PrintHex( pFile, (unsigned *)pTruth, Gia_ManPiNum(pAbc->pGia) ), fprintf( pFile, "\n" );
2804  }
2805  fclose( pFile );
2806  return 0;
2807 
2808 usage:
2809  fprintf( pAbc->Err, "usage: &write_truths [-rbh] <file>\n" );
2810  fprintf( pAbc->Err, "\t writes truth tables of each PO of GIA manager into a file\n" );
2811  fprintf( pAbc->Err, "\t-r : toggle reversing bits in the truth table [default = %s]\n", fReverse? "yes":"no" );
2812  fprintf( pAbc->Err, "\t-b : toggle using binary format [default = %s]\n", fBinary? "yes":"no" );
2813  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2814  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2815  return 1;
2816 }
2817 
2818 
2819 /**Function*************************************************************
2820 
2821  Synopsis []
2822 
2823  Description []
2824 
2825  SideEffects []
2826 
2827  SeeAlso []
2828 
2829 ***********************************************************************/
2830 int IoCommandWriteStatus( Abc_Frame_t * pAbc, int argc, char **argv )
2831 {
2832  char * pFileName;
2833  int c;
2834  extern void Abc_NtkWriteLogFile( char * pFileName, Abc_Cex_t * pCex, int Status, int nFrames, char * pCommand );
2835 
2836  Extra_UtilGetoptReset();
2837  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2838  {
2839  switch ( c )
2840  {
2841  case 'h':
2842  goto usage;
2843  default:
2844  goto usage;
2845  }
2846  }
2847  if ( argc != globalUtilOptind + 1 )
2848  goto usage;
2849  // get the input file name
2850  pFileName = argv[globalUtilOptind];
2851  Abc_NtkWriteLogFile( pFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, NULL );
2852  return 0;
2853 
2854 usage:
2855  fprintf( pAbc->Err, "usage: write_status [-h] <file>\n" );
2856  fprintf( pAbc->Err, "\t writes verification log file\n" );
2857  fprintf( pAbc->Err, "\t-h : print the help massage\n" );
2858  fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
2859  return 1;
2860 }
2861 
2862 /**Function*************************************************************
2863 
2864  Synopsis []
2865 
2866  Description []
2867 
2868  SideEffects []
2869 
2870  SeeAlso []
2871 
2872 ***********************************************************************/
2873 int IoCommandWriteSmv( Abc_Frame_t * pAbc, int argc, char **argv )
2874 {
2875  char * pFileName;
2876  int fUseLuts;
2877  int c;
2878 
2879  fUseLuts = 0;
2880  Extra_UtilGetoptReset();
2881  while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
2882  {
2883  switch ( c )
2884  {
2885  case 'h':
2886  goto usage;
2887  default:
2888  goto usage;
2889  }
2890  }
2891  if ( pAbc->pNtkCur == NULL )
2892  {
2893  fprintf( pAbc->Out, "Empty network.\n" );
2894  return 0;
2895  }
2896  if ( argc != globalUtilOptind + 1 )
2897  goto usage;
2898  // get the output file name
2899  pFileName = argv[globalUtilOptind];
2900  // call the corresponding file writer
2901  Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_SMV );
2902  return 0;
2903 
2904 usage:
2905  fprintf( pAbc->Err, "usage: write_smv [-h] <file>\n" );
2906  fprintf( pAbc->Err, "\t write the network in SMV format\n" );
2907  fprintf( pAbc->Err, "\t-h : print the help message\n" );
2908  fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .smv)\n" );
2909  return 1;
2910 }
2911 ////////////////////////////////////////////////////////////////////////
2912 /// END OF FILE ///
2913 ////////////////////////////////////////////////////////////////////////
2914 
2915 
2916 ABC_NAMESPACE_IMPL_END
2917 
IoCommandReadEdif
static int IoCommandReadEdif(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:724
Abc_NtkStartNameIds
ABC_DLL void Abc_NtkStartNameIds(Abc_Ntk_t *p)
Definition: abcNames.c:538
IoCommandReadTruth
static int IoCommandReadTruth(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:976
Io_Init
void Io_Init(Abc_Frame_t *pAbc)
FUNCTION DEFINITIONS ///.
Definition: io.c:95
Abc_FrameReplaceCurrentNetwork
ABC_DLL void Abc_FrameReplaceCurrentNetwork(Abc_Frame_t *p, Abc_Ntk_t *pNet)
Definition: mainFrame.c:493
Abc_NtkIsStrash
static int Abc_NtkIsStrash(Abc_Ntk_t *pNtk)
Definition: abc.h:251
glo_fMapped
int glo_fMapped
Definition: verCore.c:80
Abc_NtkIsLogic
static int Abc_NtkIsLogic(Abc_Ntk_t *pNtk)
Definition: abc.h:250
Abc_FrameReadLibGen
ABC_DLL void * Abc_FrameReadLibGen()
Definition: mainFrame.c:56
Io_WriteHie
void Io_WriteHie(Abc_Ntk_t *pNtk, char *pBaseName, char *pFileName)
Definition: ioUtil.c:477
IoCommandWriteDot
static int IoCommandWriteDot(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2065
Abc_FrameCopyLTLDataBase
void Abc_FrameCopyLTLDataBase(Abc_Frame_t *pAbc, Abc_Ntk_t *pNtk)
Definition: ltl_parser.c:73
Io_ReadBlif
Abc_Ntk_t * Io_ReadBlif(char *pFileName, int fCheck)
FUNCTION DEFINITIONS ///.
Definition: ioReadBlif.c:92
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
IoCommandReadBblif
static int IoCommandReadBblif(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:404
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
IoCommandWriteVerilog
static int IoCommandWriteVerilog(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2527
Cmd_CommandExecute
int Cmd_CommandExecute(void *pAbc, char *pCommandLine)
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
IoCommandWriteAigerCex
static int IoCommandWriteAigerCex(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1438
IoCommandWriteBblif
static int IoCommandWriteBblif(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1532
IoCommandWriteEqn
static int IoCommandWriteEqn(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2319
Abc_Truth6WordNum
static int Abc_Truth6WordNum(int nVars)
Definition: abc_global.h:257
Abc_Ntk_t_
Definition: abc.h:153
Abc_NtkReadLogFile
int Abc_NtkReadLogFile(char *pFileName, Abc_Cex_t **ppCex, int *pnFrames)
Definition: abcLog.c:132
IoCommandReadBlifMv
static int IoCommandReadBlifMv(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:551
Io_ReadNetlist
Abc_Ntk_t * Io_ReadNetlist(char *pFileName, Io_FileType_t FileType, int fCheck)
Definition: ioUtil.c:98
IoCommandReadEqn
static int IoCommandReadEqn(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:779
Abc_ObjFaninNum
static int Abc_ObjFaninNum(Abc_Obj_t *pObj)
Definition: abc.h:364
IoCommandReadGig
static int IoCommandReadGig(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1169
IoCommandWritePla
static int IoCommandWritePla(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2479
IoCommandReadInit
static int IoCommandReadInit(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:834
IoCommandWriteGml
static int IoCommandWriteGml(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2367
Abc_NtkDup
ABC_DLL Abc_Ntk_t * Abc_NtkDup(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:419
Io_WriteCellNet
void Io_WriteCellNet(Abc_Ntk_t *pNtk, char *pFileName)
Definition: ioWriteList.c:221
Cmd_CommandAdd
void Cmd_CommandAdd(Abc_Frame_t *pAbc, const char *sGroup, const char *sName, Cmd_CommandFuncType pFunc, int fChanges)
Definition: cmdApi.c:63
Abc_NtkCiNum
static int Abc_NtkCiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:287
IoCommandReadBlif
static int IoCommandReadBlif(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:459
IoCommandWrite
static int IoCommandWrite(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1227
Abc_LatchIsInit0
static int Abc_LatchIsInit0(Abc_Obj_t *pLatch)
Definition: abc.h:422
Abc_NtkToNetlist
ABC_DLL Abc_Ntk_t * Abc_NtkToNetlist(Abc_Ntk_t *pNtk)
Definition: abcNetlist.c:97
IoCommandWriteBlifMv
static int IoCommandWriteBlifMv(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1656
Abc_NtkWriteSorterCnf
void Abc_NtkWriteSorterCnf(char *pFileName, int nVars, int nQueens)
Definition: abcSat.c:905
Mf_ManDumpCnf
void Mf_ManDumpCnf(Gia_Man_t *p, char *pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose)
Definition: giaMf.c:1646
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
IoCommandWriteBlif
static int IoCommandWriteBlif(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1580
Abc_SopFromTruthHex
ABC_DLL char * Abc_SopFromTruthHex(char *pTruth)
Definition: abcSop.c:948
Hop_Obj_t_
Definition: hop.h:65
Gia_Obj_t_
Definition: gia.h:75
Abc_NtkDelete
ABC_DLL void Abc_NtkDelete(Abc_Ntk_t *pNtk)
Definition: abcNtk.c:1233
Io_Read
Abc_Ntk_t * Io_Read(char *pFileName, Io_FileType_t FileType, int fCheck, int fBarBufs)
Definition: ioUtil.c:238
Gia_ObjComputeTruthTable
word * Gia_ObjComputeTruthTable(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: giaTruth.c:177
Abc_Ntk_t_::pModel
int * pModel
Definition: abc.h:198
strcmp
int strcmp()
Abc_Obj_t_
Definition: abc.h:128
Abc_NtkToLogic
ABC_DLL Abc_Ntk_t * Abc_NtkToLogic(Abc_Ntk_t *pNtk)
FUNCTION DEFINITIONS ///.
Definition: abcNetlist.c:52
Abc_FrameClearVerifStatus
ABC_DLL void Abc_FrameClearVerifStatus(Abc_Frame_t *p)
Definition: mainFrame.c:247
Io_Write
void Io_Write(Abc_Ntk_t *pNtk, char *pFileName, Io_FileType_t FileType)
Definition: ioUtil.c:317
Io_ReadFileType
Io_FileType_t Io_ReadFileType(char *pFileName)
DECLARATIONS ///.
Definition: ioUtil.c:46
Abc_Ntk_t_::pManFunc
void * pManFunc
Definition: abc.h:191
Abc_NtkNodeNum
static int Abc_NtkNodeNum(Abc_Ntk_t *pNtk)
Definition: abc.h:293
Extra_PrintHex
void Extra_PrintHex(FILE *pFile, unsigned *pTruth, int nVars)
Definition: extraUtilFile.c:620
Abc_Frame_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition: base/main/main.h:39
Extra_UtilGetoptReset
ABC_DLL void Extra_UtilGetoptReset()
Definition: extraUtilUtil.c:80
IoCommandWriteCnf
static int IoCommandWriteCnf(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1868
Io_WriteAigerCex
void Io_WriteAigerCex(Abc_Cex_t *pCex, Abc_Ntk_t *pNtk, void *pG, char *pFileName)
Definition: ioWriteAiger.c:880
Io_WriteList
void Io_WriteList(Abc_Ntk_t *pNtk, char *pFileName, int fUseHost)
FUNCTION DEFINITIONS ///.
Definition: ioWriteList.c:102
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
IoCommandReadStatus
static int IoCommandReadStatus(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1113
IoCommandWriteBaf
static int IoCommandWriteBaf(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1484
Abc_NtkToDar
Aig_Man_t * Abc_NtkToDar(Abc_Ntk_t *pNtk, int fExors, int fRegisters)
Definition: abcDar.c:233
Saig_ManCbaFindCexCareBits
Abc_Cex_t * Saig_ManCbaFindCexCareBits(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
Definition: absOldCex.c:718
IoCommandWriteSortCnf
static int IoCommandWriteSortCnf(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2575
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Abc_SopFromTruthBin
ABC_DLL char * Abc_SopFromTruthBin(char *pTruth)
Definition: abcSop.c:879
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition: utilCex.c:350
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Jf_ManDumpCnf
void Jf_ManDumpCnf(Gia_Man_t *p, char *pFileName, int fVerbose)
Definition: giaJf.c:1764
IoCommandReadAiger
static int IoCommandReadAiger(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:294
globalUtilOptind
int globalUtilOptind
Definition: extraUtilUtil.c:45
Io_WriteBlifSpecial
void Io_WriteBlifSpecial(Abc_Ntk_t *pNtk, char *FileName, char *pLutStruct, int fUseHie)
Definition: ioWriteBlif.c:1378
Abc_NtkDarToCnf
Abc_Ntk_t * Abc_NtkDarToCnf(Abc_Ntk_t *pNtk, char *pFileName, int fFastAlgo, int fChangePol, int fVerbose)
Definition: abcDar.c:1736
Io_WriteBenchLut
int Io_WriteBenchLut(Abc_Ntk_t *pNtk, char *FileName)
Definition: ioWriteBench.c:175
IoCommandWriteList
static int IoCommandWriteList(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2415
sprintf
char * sprintf()
Abc_NtkForEachLatch
#define Abc_NtkForEachLatch(pNtk, pObj, i)
Definition: abc.h:497
IoCommandWriteBench
static int IoCommandWriteBench(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1704
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_NtkFlattenHierarchyGia
ABC_DLL Gia_Man_t * Abc_NtkFlattenHierarchyGia(Abc_Ntk_t *pNtk, Vec_Ptr_t **pvBuffers, int fVerbose)
Definition: abcHieGia.c:277
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
IoCommandReadDsd
static int IoCommandReadDsd(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:662
Abc_NtkFromAigPhase
Abc_Ntk_t * Abc_NtkFromAigPhase(Aig_Man_t *pMan)
Definition: abcDar.c:590
Bmc_CexCareVerify
void Bmc_CexCareVerify(Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
Definition: bmcCexCare.c:274
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Io_ReadPla
Abc_Ntk_t * Io_ReadPla(char *pFileName, int fZeros, int fCheck)
FUNCTION DEFINITIONS ///.
Definition: ioReadPla.c:47
Abc_FrameReadNtk
ABC_DLL Abc_Ntk_t * Abc_FrameReadNtk(Abc_Frame_t *p)
Definition: mainFrame.c:282
Abc_Ntk_t_::pSpec
char * pSpec
Definition: abc.h:159
Sdm_ManCanRead
int Sdm_ManCanRead()
Definition: extraUtilDsd.c:1080
Abc_NtkCreateWithNode
ABC_DLL Abc_Ntk_t * Abc_NtkCreateWithNode(char *pSop)
Definition: abcNtk.c:1192
Abc_NtkPo
static Abc_Obj_t * Abc_NtkPo(Abc_Ntk_t *pNtk, int i)
Definition: abc.h:316
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition: extraUtilFile.c:497
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition: abc.h:515
Abc_NtkPoNum
static int Abc_NtkPoNum(Abc_Ntk_t *pNtk)
Definition: abc.h:286
IoCommandWriteCellNet
static int IoCommandWriteCellNet(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1812
IoCommandReadBench
static int IoCommandReadBench(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:607
IoCommandWriteBook
static int IoCommandWriteBook(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1769
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Man_t_
Definition: gia.h:95
Abc_NtkPiNum
static int Abc_NtkPiNum(Abc_Ntk_t *pNtk)
Definition: abc.h:285
Abc_ObjName
ABC_DLL char * Abc_ObjName(Abc_Obj_t *pNode)
DECLARATIONS ///.
Definition: abcNames.c:48
Extra_UtilGetopt
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
Definition: extraUtilUtil.c:98
Io_ReadBlifAsAig
Abc_Ntk_t * Io_ReadBlifAsAig(char *pFileName, int fCheck)
FUNCTION DEFINITIONS ///.
Definition: ioReadBlifAig.c:118
IoCommandWriteTruths
static int IoCommandWriteTruths(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2742
Gia_ManReadGig
Gia_Man_t * Gia_ManReadGig(char *pFileName)
Definition: giaGig.c:204
Inter_Check_t_::nVars
int nVars
Definition: intCheck.c:34
Abc_FrameUpdateGia
void Abc_FrameUpdateGia(Abc_Frame_t *pAbc, Gia_Man_t *pNew)
Definition: abc.c:616
Io_ReadDsd
Abc_Ntk_t * Io_ReadDsd(char *pForm)
Definition: ioReadDsd.c:232
Abc_NtkToAig
ABC_DLL int Abc_NtkToAig(Abc_Ntk_t *pNtk)
Definition: abcFunc.c:1192
Saig_ManExtendCex
Abc_Cex_t * Saig_ManExtendCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:382
IoCommandWriteCnf2
static int IoCommandWriteCnf2(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1960
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
IoCommandReadVerilog
static int IoCommandReadVerilog(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1048
Abc_NtkTransferNameIds
ABC_DLL void Abc_NtkTransferNameIds(Abc_Ntk_t *p, Abc_Ntk_t *pNew)
Definition: abcNames.c:588
Abc_FrameReadErr
ABC_DLL FILE * Abc_FrameReadErr(Abc_Frame_t *p)
Definition: mainFrame.c:330
assert
#define assert(ex)
Definition: util_old.h:213
Extra_FileNameGenericAppend
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
Definition: extraUtilFile.c:185
strlen
int strlen()
Saig_ManDupIsoCanonical
Aig_Man_t * Saig_ManDupIsoCanonical(Aig_Man_t *pAig, int fVerbose)
Definition: saigIso.c:128
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Bmc_CexCareMinimize
Abc_Cex_t * Bmc_CexCareMinimize(Aig_Man_t *p, Abc_Cex_t *pCex, int fCheck, int fVerbose)
Definition: bmcCexCare.c:255
IoCommandWriteStatus
static int IoCommandWriteStatus(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2830
Io_ReadBenchInit
void Io_ReadBenchInit(Abc_Ntk_t *pNtk, char *pFileName)
Definition: ioReadBench.c:311
Extra_FileNameExtension
char * Extra_FileNameExtension(char *FileName)
Definition: extraUtilFile.c:125
Abc_Obj_t_::pData
void * pData
Definition: abc.h:145
Io_WriteCnf
int Io_WriteCnf(Abc_Ntk_t *pNtk, char *FileName, int fAllPrimes)
FUNCTION DEFINITIONS ///.
Definition: ioWriteCnf.c:48
Abc_FrameReadOut
ABC_DLL FILE * Abc_FrameReadOut(Abc_Frame_t *p)
Definition: mainFrame.c:314
IoCommandWriteSmv
static int IoCommandWriteSmv(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2873
IoCommandWriteTruth
static int IoCommandWriteTruth(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2645
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
IoCommandWriteAiger
static int IoCommandWriteAiger(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1348
Hop_Man_t
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition: hop.h:49
Io_WriteAiger
void Io_WriteAiger(Abc_Ntk_t *pNtk, char *pFileName, int fWriteSymbols, int fCompact, int fUnique)
Definition: ioWriteAiger.c:635
IoCommandReadPla
static int IoCommandReadPla(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:902
Abc_ObjFanout0
static Abc_Obj_t * Abc_ObjFanout0(Abc_Obj_t *pObj)
Definition: abc.h:371
IoCommandWriteHie
static int IoCommandWriteHie(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:1291
Abc_NtkForEachPi
#define Abc_NtkForEachPi(pNtk, pPi, i)
Definition: abc.h:513
IoCommandReadBaf
static int IoCommandReadBaf(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:349
IoCommandWriteCex
static int IoCommandWriteCex(Abc_Frame_t *pAbc, int argc, char **argv)
Definition: io.c:2120
IoCommandRead
static ABC_NAMESPACE_IMPL_START int IoCommandRead(Abc_Frame_t *pAbc, int argc, char **argv)
DECLARATIONS ///.
Definition: io.c:168
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Io_End
void Io_End(Abc_Frame_t *pAbc)
Definition: io.c:153