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

Last change on this file since 17 was 14, checked in by cecile, 14 years ago

vis2.3
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
64/**AutomaticEnd***************************************************************/
65
66#endif /* _BMC */
Note: See TracBrowser for help on using the repository browser.