source: vis_dev/vis-2.3/src/puresat/puresat.c @ 14

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

vis2.3
File size: 8.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresat.c]
4
5  PackageName [puresat]
6
7  Synopsis    [Abstraction refinement for large scale invariant checking.]
8
9  Description [This file contains the functions to check invariant properties
10  by the PureSAT abstraction refinement algorithm, which is entirely based on
11  SAT solver, the input of which could be either CNF or AIG. It has several
12  parts:
13
14  * Localization-reduction base Abstraction
15  * K-induction or interpolation to prove the truth of a property
16  * Bounded Model Checking to find bugs
17  * Incremental concretization based methods to verify abstract bugs
18  * Incremental SAT solver to improve efficiency
19  * UNSAT proof based method to obtain refinement
20  * AROSAT to bring in only necessary latches into unsat proofs
21  * Bridge abstraction to get compact coarse refinement
22  * Refinement minization to guarrantee minimal refinements
23  * Unsat proof-based refinement minimization to eliminate multiple candidate
24    by on SAT test
25  * Refinement prediction to decrease the number of refinement iterations
26  * Dynamic switching to redistribute computional resources to improve
27    efficiency
28 
29  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
30  paper of Li et al., "A satisfiability-based appraoch to abstraction
31  refinement in model checking", " Abstraction in symbolic model checking
32  using satisfiability as the only decision procedure", "Efficient computation
33  of small abstraction refinements", and "Efficient abstraction refinement in
34  interpolation-based unbounded model checking"]
35 
36  Author      [Bing Li]
37
38  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
39  All rights reserved.
40
41  Permission is hereby granted, without written agreement and without
42  license or royalty fees, to use, copy, modify, and distribute this
43  software and its documentation for any purpose, provided that the
44  above copyright notice and the following two paragraphs appear in
45  all copies of this software.]
46
47******************************************************************************/
48
49#include "puresatInt.h"
50
51/*---------------------------------------------------------------------------*/
52/* Constant declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Structure declarations                                                    */
57/*---------------------------------------------------------------------------*/
58
59/*---------------------------------------------------------------------------*/
60/* Type declarations                                                         */
61/*---------------------------------------------------------------------------*/
62
63/*---------------------------------------------------------------------------*/
64/* Variable declarations                                                     */
65/*---------------------------------------------------------------------------*/
66
67static jmp_buf timeOutEnv;
68
69/*---------------------------------------------------------------------------*/
70/* Macro declarations                                                        */
71/*---------------------------------------------------------------------------*/
72
73/**AutomaticStart*************************************************************/
74
75/*---------------------------------------------------------------------------*/
76/* Static function prototypes                                                */
77/*---------------------------------------------------------------------------*/
78static int CommandPureSatAbRf( Hrc_Manager_t ** hmgr,int  argc, char ** argv);
79static void TimeOutHandle(void);
80/**AutomaticEnd***************************************************************/
81
82/*---------------------------------------------------------------------------*/
83/* Definition of exported functions                                          */
84/*---------------------------------------------------------------------------*/
85
86/**Function********************************************************************
87
88  Synopsis    [Initializes the puresat package. The added command is for
89  testing purpose only; the same algorithm can be activated by the
90  check_invariant command.]
91
92  Description [Initializes the puresat package. The added command is for
93  testing purpose only; the same algorithm can be activated by the
94  check_invariant command.]
95
96  SideEffects []
97
98  SeeAlso     [PureSat_End]
99
100******************************************************************************/
101void
102PureSat_Init(void)
103{
104  /*
105   * Add a command to the global command table.  By using the leading
106   * underscore, the command will be listed under "help -a" but not "help".
107   */
108  Cmd_CommandAdd("_puresat_test", CommandPureSatAbRf,  0);
109}
110
111
112/**Function********************************************************************
113
114  Synopsis    [Ends the puresat package.]
115
116  Description [Ends the puresat package.]
117   
118  SideEffects []
119
120  SeeAlso     [PureSat_Init]
121
122******************************************************************************/
123void
124PureSat_End(void)
125{
126
127}
128
129/*---------------------------------------------------------------------------*/
130/* Definition of internal functions                                          */
131/*---------------------------------------------------------------------------*/
132
133
134/*---------------------------------------------------------------------------*/
135/* Definition of static functions                                            */
136/*---------------------------------------------------------------------------*/
137
138
139/**Function********************************************************************
140
141  Synopsis    [time out function]
142
143  Description [time out function]
144
145  SideEffects []
146
147  SeeAlso     []
148
149******************************************************************************/
150
151
152static void
153TimeOutHandle()
154{
155  longjmp(timeOutEnv, 1);
156}
157
158/**Function********************************************************************
159
160  Synopsis    [Check invariant formulae with abstraction refinement method
161  PureSat.]
162
163  Description [Check invariant formulae with abstraction refinement method
164  PureSat.]
165
166  SideEffects []
167
168  SeeAlso     []
169
170******************************************************************************/ 
171static int
172CommandPureSatAbRf(
173  Hrc_Manager_t ** hmgr,
174  int  argc,
175  char ** argv)
176{
177  Ntk_Network_t * network;
178 
179  FILE * ltlFile;
180  array_t * formulaArray;
181  boolean re;
182  int i;
183
184  PureSat_Manager_t *pm;
185  int timeOutPeriod;
186
187  pm = PureSatManagerAlloc();
188  timeOutPeriod = pm->timeOutPeriod;
189  PureSatCmdParse(argc, argv,pm);
190  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
191  fprintf(vis_stdout, "Num of latches is %d\n",Ntk_NetworkReadNumLatches(network));
192  if (network == NIL(Ntk_Network_t)) {
193      fprintf(vis_stderr,
194              "No network, please read in the circuit, and init_verify\n");
195      return 1;
196  }
197 
198  ltlFile = Cmd_FileOpen(pm->ltlFileName, "r", NIL(char *), 0);
199  if (ltlFile == NIL(FILE)) {
200    fprintf(vis_stdout,"Cannot open LTL file %s\n", pm->ltlFileName);
201    exit(1);
202  }
203 
204  formulaArray = Ctlsp_FileParseFormulaArray(ltlFile);
205  if(!array_n(formulaArray))
206    {fprintf(vis_stderr,"ltlfile doesn't contain any formula \n");
207    exit (1);}
208
209  /*timeout*/
210  if (timeOutPeriod > 0) {
211    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
212    fprintf(vis_stdout, "signal\n");
213    (void) alarm(timeOutPeriod);
214    if (setjmp(timeOutEnv) > 0) {
215      (void) fprintf(vis_stdout,
216                     "# PURESAT: timeout occurred after %d seconds.\n", timeOutPeriod);
217      (void) fprintf(vis_stdout, "# PURESAT: data may be corrupted.\n");
218      alarm(0);
219      return 1;
220    }
221  }
222
223  for (i = 0; i < array_n(formulaArray); i++) {
224    Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
225    re = PureSatCheckInv_SSS(network,ltlFormula,pm);
226    if(re)
227      fprintf(vis_stdout,"formula #%d is true\n",i);
228    else
229      fprintf(vis_stdout,"formula #%d is False\n",i);
230  }
231  return 0;
232}
233
234
Note: See TracBrowser for help on using the repository browser.