source: vis_dev/vis-2.3/src/grab/grabInt.h @ 36

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

vis2.3
File size: 7.2 KB
RevLine 
[14]1/**CHeaderFile*****************************************************************
2
3  FileName    [grabInt.h]
4
5  PackageName [grab]
6
7  Synopsis    [Internal declarations.]
8
9  Author      [Chao Wang.]
10
11  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18  ]
19 
20******************************************************************************/
21
22#ifndef _GRABINT
23#define _GRABINT
24
25/*---------------------------------------------------------------------------*/
26/* Nested includes                                                           */
27/*---------------------------------------------------------------------------*/
28#include "grab.h"
29#include "cmd.h"
30#include "ctlp.h"
31#include "ctlsp.h"
32#include "mc.h"
33#include "img.h"
34#include "ntk.h"
35#include "ntm.h"
36#include "part.h"
37#include "mvf.h"
38#include <string.h>
39#include "bmc.h"
40#include "mdd.h"
41#include "epd.h"
42#include "fsm.h"
43#include "partInt.h"
44#include "fsmInt.h"
45
46
47
48/*---------------------------------------------------------------------------*/
49/* Constant declarations                                                     */
50/*---------------------------------------------------------------------------*/
51#define GRAB_PARTITION_NOCHANGE    0
52#define GRAB_PARTITION_BUILD       1
53#define GRAB_PARTITION_UPDATE      2
54
55#define GRAB_CEX_MINTERM             0
56#define GRAB_CEX_CUBE                1
57#define GRAB_CEX_SOR                 2
58
59/*---------------------------------------------------------------------------*/
60/* Structure declarations                                                    */
61/*---------------------------------------------------------------------------*/
62struct mAigManagerStateStruct{
63  mAig_Manager_t   *manager;
64  st_table         *nodeToMvfAigTable;
65  st_table         *nodeToMAigIdTable;
66};
67
68/*---------------------------------------------------------------------------*/
69/* Type declarations                                                         */
70/*---------------------------------------------------------------------------*/
71typedef struct mAigManagerStateStruct mAigManagerState_t;
72
73/*---------------------------------------------------------------------------*/
74/* Variable declarations                                                     */
75/*---------------------------------------------------------------------------*/
76
77/*---------------------------------------------------------------------------*/
78/* Macro declarations                                                        */
79/*---------------------------------------------------------------------------*/
80
81#define DBGMSG1(msg)         fprintf(vis_stdout, "\n<<%s>>\n", msg)
82#define DBGMSG2(msg,msg2)         fprintf(vis_stdout, msg, msg2)
83
84#define CHKPRINT(flag, msg)   if(flag) fprintf(vis_stdout, msg)
85#define CHKPRINT1(flag, msg)   if(flag) fprintf(vis_stdout, msg)
86#define CHKPRINT2(flag, msg, msg2)   if(flag) fprintf(vis_stdout, msg, msg2)
87#define CHKPRINT3(flag, msg, msg2, msg3)   if(flag) fprintf(vis_stdout,msg,msg2,msg3)
88#define CHKPRINT4(flag, msg, msg2, msg3, msg4)   if(flag) fprintf(vis_stdout,msg,msg2,msg3,msg4)
89#define CHKPRINT5(flag, msg, msg2, msg3, msg4, msg5)   if(flag) fprintf(vis_stdout,msg,msg2,msg3,msg4,msg5)
90
91#if 0
92
93#define DBGMSG(msg)         fprintf(vis_stdout, "\n<<%s>>\n", msg)
94#define CHKCPUTIME(flag, startTime, msg) \
95        if (flag) { \
96            long thisTime = util_cpu_ctime();\
97            fprintf(vis_stdout, "\n-- elapsed time %5g  (%s)\n",\
98                    (double)(thisTime - startTime)/1000.0, msg); \
99            fflush(vis_stdout);\
100        }
101
102#else
103
104#define DBGMSG(msg)         
105#define CHKCPUTIME(flag,startTime,msg) 
106
107#endif
108
109/**AutomaticStart*************************************************************/
110
111/*---------------------------------------------------------------------------*/
112/* Function prototypes                                                       */
113/*---------------------------------------------------------------------------*/
114
115EXTERN boolean Bmc_AbstractCheckAbstractTraces(Ntk_Network_t *network, array_t *synOnionRings, st_table *absLatches, int verbose, int dbgLevel, int printInputs);
116EXTERN boolean Bmc_AbstractCheckAbstractTracesWithFineGrain(Ntk_Network_t *network, st_table *coiBnvTable, array_t *synOnionRings, st_table *absLatches, st_table *absBnvs);
117EXTERN void GrabRefineAbstractionByGrab(Fsm_Fsm_t *absFsm, array_t *SORs, st_table *absVarTable, st_table *BnvTable, array_t *addedVars, array_t *addedBnvs, int refine_direction, st_table *nodeToFaninNumberTable, int verbose);
118EXTERN int GrabNodeComputeFaninNumberTableItem(Ntk_Network_t *network, st_table *nodeToFaninNumberTable, Ntk_Node_t *node);
119EXTERN st_table * GrabComputeCOIAbstraction(Ntk_Network_t *network, Ctlp_Formula_t *invFormula);
120EXTERN st_table * GrabComputeInitialAbstraction(Ntk_Network_t *network, Ctlp_Formula_t *invFormula);
121EXTERN void GrabUpdateAbstractPartition(Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table *absBnvTable, int partitionFlag);
122EXTERN Fsm_Fsm_t * GrabCreateAbstractFsm(Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table *absBnvTable, int partitionFlag, int independentFlag);
123EXTERN mdd_t * GrabComputeInitialStates(Ntk_Network_t *network, array_t *psVars);
124EXTERN mdd_t * GrabFsmComputeReachableStates(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *invStatesArray, int verbose);
125EXTERN mdd_t * GrabFsmComputeConstrainedReachableStates(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *SORs, int verbose);
126EXTERN array_t * GrabFsmComputeSynchronousOnionRings(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *oldRings, mdd_t *inv_states, int cexType, int verbose);
127EXTERN array_t * GrabGetVisibleVarMddIds(Fsm_Fsm_t *absFsm, st_table *absVarTable);
128EXTERN array_t * GrabGetInvisibleVarMddIds(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable);
129EXTERN int GrabTestRefinementSetSufficient(Ntk_Network_t *network, array_t *SORs, st_table *absVarTable, int verbose);
130EXTERN int GrabTestRefinementBnvSetSufficient(Ntk_Network_t *network, st_table *coiBnvTable, array_t *SORs, st_table *absVarTable, st_table *absBnvTable, int verbose);
131EXTERN void GrabMinimizeLatchRefinementSet(Ntk_Network_t *network, st_table **absVarTable, st_table **absBnvTable, array_t *newlyAddedLatches, array_t **newlyAddedBnvs, array_t *SORs, int verbose);
132EXTERN void GrabMinimizeBnvRefinementSet(Ntk_Network_t *network, st_table *coiBnvTable, st_table *absVarTable, st_table **absBnvTable, array_t *newlyAddedBnvs, array_t *SORs, int verbose);
133EXTERN void GrabNtkClearAllMddIds(Ntk_Network_t *network);
134EXTERN void GrabPrintNodeArray(char *caption, array_t *theArray);
135EXTERN void GrabPrintMddIdArray(Ntk_Network_t *network, char *caption, array_t *mddIdArray);
136EXTERN void GrabPrintNodeList(char *caption, lsList theList);
137EXTERN void GrabPrintNodeHashTable(char *caption, st_table *theTable);
138
139/**AutomaticEnd***************************************************************/
140
141#endif /* _GRABINT */
142
143
Note: See TracBrowser for help on using the repository browser.