abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
mainMC.c File Reference
#include "mainInt.h"
#include "aig/aig/aig.h"
#include "aig/saig/saig.h"
#include "aig/fra/fra.h"
#include "aig/ioa/ioa.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int main (int argc, char *argv[])
 DECLARATIONS ///. More...
 

Function Documentation

ABC_NAMESPACE_IMPL_START int main ( int  argc,
char *  argv[] 
)

DECLARATIONS ///.

GLOBAL VARIABLES ///.

CFile****************************************************************

FileName [mainMC.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The main package.]

Synopsis [The main file for the model checker.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
main.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [The main() procedure.]

Description []

SideEffects []

SeeAlso []

Definition at line 49 of file mainMC.c.

50 {
51  int fEnableBmcOnly = 0; // enable to make it BMC-only
52 
53  int fEnableCounter = 1; // should be 1 in the final version
54  int fEnableComment = 0; // should be 0 in the final version
55 
56  Fra_Sec_t SecPar, * pSecPar = &SecPar;
57  FILE * pFile;
58  Aig_Man_t * pAig;
59  int RetValue = -1;
60  int Depth = -1;
61  // BMC parameters
62  int nFrames = 50;
63  int nSizeMax = 500000;
64  int nBTLimit = 10000;
65  int fRewrite = 0;
66  int fNewAlgo = 1;
67  int fVerbose = 0;
68  clock_t clkTotal = clock();
69 
70  if ( argc != 2 )
71  {
72  printf( " Expecting one command-line argument (an input file in AIGER format).\n" );
73  printf( " usage: %s <file.aig>\n", argv[0] );
74  return 0;
75  }
76  pFile = fopen( argv[1], "r" );
77  if ( pFile == NULL )
78  {
79  printf( " Cannot open input AIGER file \"%s\".\n", argv[1] );
80  printf( " usage: %s <file.aig>\n", argv[0] );
81  return 0;
82  }
83  fclose( pFile );
84  pAig = Ioa_ReadAiger( argv[1], 1 );
85  if ( pAig == NULL )
86  {
87  printf( " Parsing the AIGER file \"%s\" has failed.\n", argv[1] );
88  printf( " usage: %s <file.aig>\n", argv[0] );
89  return 0;
90  }
91 
92  Aig_ManSetRegNum( pAig, pAig->nRegs );
93  if ( !fEnableBmcOnly )
94  {
95  // perform BMC
96  if ( pAig->nRegs != 0 )
97  RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL, 0 );
98 
99  // perform full-blown SEC
100  if ( RetValue != 0 )
101  {
102  extern void Dar_LibStart();
103  extern void Dar_LibStop();
104  extern void Cnf_ManFree();
105 
106  Fra_SecSetDefaultParams( pSecPar );
107  pSecPar->TimeLimit = 600;
108  pSecPar->nFramesMax = 4; // the max number of frames used for induction
109  pSecPar->fPhaseAbstract = 0; // disable phase-abstraction
110  pSecPar->fSilent = 1; // disable phase-abstraction
111 
112  Dar_LibStart();
113  RetValue = Fra_FraigSec( pAig, pSecPar, NULL );
114  Dar_LibStop();
115  Cnf_ManFree();
116  }
117  }
118 
119  // perform BMC again
120  if ( RetValue == -1 && pAig->nRegs != 0 )
121  {
122  int nFrames = 200;
123  int nSizeMax = 500000;
124  int nBTLimit = 10000000;
125  int fRewrite = 0;
126  RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth, 0 );
127  if ( RetValue != 0 )
128  RetValue = -1;
129  }
130 
131  // decide how to report the output
132  pFile = stdout;
133 
134  // report the result
135  if ( RetValue == 0 )
136  {
137 // fprintf(stdout, "s SATIFIABLE\n");
138  fprintf( pFile, "1" );
139  if ( fEnableCounter )
140  {
141  printf( "\n" );
142  if ( pAig->pSeqModel )
143  Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel );
144  }
145 
146  if ( fEnableComment )
147  {
148  printf( " # File %10s. ", argv[1] );
149  PRT( "Time", clock() - clkTotal );
150  }
151 
152  if ( pFile != stdout )
153  fclose(pFile);
154  Aig_ManStop( pAig );
155  exit(10);
156  }
157  else if ( RetValue == 1 )
158  {
159 // fprintf(stdout, "s UNSATISFIABLE\n");
160  fprintf( pFile, "0" );
161 
162  if ( fEnableComment )
163  {
164  printf( " # File %10s. ", argv[1] );
165  PRT( "Time", clock() - clkTotal );
166  }
167  printf( "\n" );
168 
169  if ( pFile != stdout )
170  fclose(pFile);
171  Aig_ManStop( pAig );
172  exit(20);
173  }
174  else // if ( RetValue == -1 )
175  {
176 // fprintf(stdout, "s UNKNOWN\n");
177  fprintf( pFile, "2" );
178 
179  if ( fEnableComment )
180  {
181  printf( " # File %10s. ", argv[1] );
182  PRT( "Time", clock() - clkTotal );
183  }
184  printf( "\n" );
185 
186  if ( pFile != stdout )
187  fclose(pFile);
188  Aig_ManStop( pAig );
189  exit(0);
190  }
191  return 0;
192 }
VOID_HACK exit()
int TimeLimit
Definition: fra.h:141
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
int nFramesMax
Definition: fra.h:118
int Saig_ManBmcSimple(Aig_Man_t *pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int *piFrame, int nCofFanLit)
Definition: bmcBmc.c:186
void Fra_SecSetDefaultParams(Fra_Sec_t *p)
DECLARATIONS ///.
Definition: fraSec.c:51
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
void Cnf_ManFree()
Definition: cnfCore.c:58
void Dar_LibStop()
Definition: darLib.c:615
int fPhaseAbstract
Definition: fra.h:126
int Fra_FraigSec(Aig_Man_t *p, Fra_Sec_t *pParSec, Aig_Man_t **ppResult)
Definition: fraSec.c:95
Aig_Man_t * Ioa_ReadAiger(char *pFileName, int fCheck)
Definition: ioaReadAig.c:431
void Dar_LibStart()
MACRO DEFINITIONS ///.
Definition: darLib.c:593
int fSilent
Definition: fra.h:138
static int Depth
Definition: dsdProc.c:56