[14] | 1 | /**CHeaderFile***************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [grab.h] |
---|
| 4 | |
---|
| 5 | PackageName [grab] |
---|
| 6 | |
---|
| 7 | Synopsis [Abstraction refinement for large scale invariant checking.] |
---|
| 8 | |
---|
| 9 | Description [Abstraction refinement for large scale invariant checking.] |
---|
| 10 | |
---|
| 11 | Author [Chao Wang.] |
---|
| 12 | |
---|
| 13 | Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All |
---|
| 14 | rights reserved. |
---|
| 15 | |
---|
| 16 | Permission is hereby granted, without written agreement and without license |
---|
| 17 | or royalty fees, to use, copy, modify, and distribute this software and its |
---|
| 18 | documentation for any purpose, provided that the above copyright notice and |
---|
| 19 | the following two paragraphs appear in all copies of this software. |
---|
| 20 | ] |
---|
| 21 | |
---|
| 22 | ******************************************************************************/ |
---|
| 23 | |
---|
| 24 | #ifndef _GRAB |
---|
| 25 | #define _GRAB |
---|
| 26 | |
---|
| 27 | /*---------------------------------------------------------------------------*/ |
---|
| 28 | /* Nested includes */ |
---|
| 29 | /*---------------------------------------------------------------------------*/ |
---|
| 30 | #include "vm.h" |
---|
| 31 | #include "ntk.h" |
---|
| 32 | |
---|
| 33 | /*---------------------------------------------------------------------------*/ |
---|
| 34 | /* Constant declarations */ |
---|
| 35 | /*---------------------------------------------------------------------------*/ |
---|
| 36 | |
---|
| 37 | |
---|
| 38 | /*---------------------------------------------------------------------------*/ |
---|
| 39 | /* Structure declarations */ |
---|
| 40 | /*---------------------------------------------------------------------------*/ |
---|
| 41 | |
---|
| 42 | |
---|
| 43 | /*---------------------------------------------------------------------------*/ |
---|
| 44 | /* Type declarations */ |
---|
| 45 | /*---------------------------------------------------------------------------*/ |
---|
| 46 | |
---|
| 47 | |
---|
| 48 | /*---------------------------------------------------------------------------*/ |
---|
| 49 | /* Variable declarations */ |
---|
| 50 | /*---------------------------------------------------------------------------*/ |
---|
| 51 | |
---|
| 52 | |
---|
| 53 | /*---------------------------------------------------------------------------*/ |
---|
| 54 | /* Macro declarations */ |
---|
| 55 | /*---------------------------------------------------------------------------*/ |
---|
| 56 | |
---|
| 57 | |
---|
| 58 | /**AutomaticStart*************************************************************/ |
---|
| 59 | |
---|
| 60 | /*---------------------------------------------------------------------------*/ |
---|
| 61 | /* Function prototypes */ |
---|
| 62 | /*---------------------------------------------------------------------------*/ |
---|
| 63 | |
---|
| 64 | EXTERN void Grab_Init(void); |
---|
| 65 | EXTERN void Grab_End(void); |
---|
| 66 | EXTERN void Grab_NetworkCheckInvariants(Ntk_Network_t *network, array_t *InvariantFormulaArray, char *refineAlgorithm, int fineGrainFlag, int refineMinFlag, int useArdcFlag, int cexType, int verbosity, int dbgLevel, int printInputs, FILE *debugFile, int useMore, char *driverName); |
---|
| 67 | |
---|
| 68 | /**AutomaticEnd***************************************************************/ |
---|
| 69 | |
---|
| 70 | #endif /* _GRAB */ |
---|