source: vis_dev/vis-2.3/src/bmc/bmc.h @ 25

Last change on this file since 25 was 21, checked in by cecile, 13 years ago

un delete de trop
File size: 2.6 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [bmc.h]
4
5  PackageName [bmc]
6
7  Synopsis    [bounded model checking (BMC) header file.]
8
9  Description []
10
11  Author      [Mohammad Awedh]
12
13  Copyright   [This file was created at the University of Colorado at Boulder.
14  The University of Colorado at Boulder makes no warranty about the suitability
15  of this software for any purpose.  It is presented on an AS IS basis.]
16
17  Revision    [$Id: bmc.h,v 1.26 2010/04/09 23:50:57 fabio Exp $]
18
19******************************************************************************/
20
21#ifndef _BMC
22#define _BMC
23
24/*---------------------------------------------------------------------------*/
25/* Nested includes                                                           */
26/*---------------------------------------------------------------------------*/
27#include "ntk.h"
28#include "ntmaig.h"
29#include "ctlspInt.h"
30#include "mcInt.h"
31#include "fsm.h"
32/*---------------------------------------------------------------------------*/
33/* Constant declarations                                                     */
34/*---------------------------------------------------------------------------*/
35
36#define BMC_INITIAL_STATES 1
37#define BMC_NO_INITIAL_STATES 0
38
39#define CirCUs 0
40#define cusp 1
41
42
43/*---------------------------------------------------------------------------*/
44/* Type declarations                                                         */
45/*---------------------------------------------------------------------------*/
46
47typedef struct BmcOption     BmcOption_t;
48typedef struct BmcCnfClauses BmcCnfClauses_t;
49typedef struct BmcCnfStates  BmcCnfStates_t; 
50typedef struct BmcCheckForTermination BmcCheckForTermination_t;
51/**AutomaticStart*************************************************************/
52
53/*---------------------------------------------------------------------------*/
54/* Function prototypes                                                       */
55/*---------------------------------------------------------------------------*/
56
57EXTERN boolean Bmc_AbstractCheckAbstractPath(Ntk_Network_t *network, McPath_t *abstractPath, array_t *supportList, Ctlsp_Formula_t *formula);
58EXTERN void Bmc_Init(void);
59EXTERN void Bmc_End(void);
60EXTERN mdd_t * Bmc_ComputeCloseCube(mdd_t *states, mdd_t *target, int *dist, Fsm_Fsm_t *modelFsm);
61EXTERN MvfAig_Function_t * Bmc_NodeBuildMVF(Ntk_Network_t *network, Ntk_Node_t *node);
62EXTERN MvfAig_Function_t * Bmc_ReadMvfAig(Ntk_Node_t * node, st_table * nodeToMvfAigTable);
63 BmcOption_t * ParseBmcOptions(int argc, char **argv);
64/**AutomaticEnd***************************************************************/
65
66#endif /* _BMC */
Note: See TracBrowser for help on using the repository browser.