1 | /**CFile*********************************************************************** |
---|
2 | |
---|
3 | FileName [debug.c] |
---|
4 | |
---|
5 | PackageName [debug] |
---|
6 | |
---|
7 | Synopsis [Debug package initialization, ending, and the command debug] |
---|
8 | |
---|
9 | Author [Cecile B.] |
---|
10 | |
---|
11 | Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. |
---|
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 | IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR |
---|
20 | DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT |
---|
21 | OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF |
---|
22 | CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. |
---|
23 | |
---|
24 | THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, |
---|
25 | INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND |
---|
26 | FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN |
---|
27 | "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE |
---|
28 | MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.] |
---|
29 | |
---|
30 | ******************************************************************************/ |
---|
31 | |
---|
32 | #include "debugInt.h" |
---|
33 | #include "imgInt.h" |
---|
34 | #include "partInt.h" |
---|
35 | static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12 braun Exp $"; |
---|
36 | |
---|
37 | /*---------------------------------------------------------------------------*/ |
---|
38 | /* Constant declarations */ |
---|
39 | /*---------------------------------------------------------------------------*/ |
---|
40 | |
---|
41 | /*---------------------------------------------------------------------------*/ |
---|
42 | /* Structure declarations */ |
---|
43 | /*---------------------------------------------------------------------------*/ |
---|
44 | |
---|
45 | /*---------------------------------------------------------------------------*/ |
---|
46 | /* Type declarations */ |
---|
47 | /*---------------------------------------------------------------------------*/ |
---|
48 | |
---|
49 | /*---------------------------------------------------------------------------*/ |
---|
50 | /* Variable declarations */ |
---|
51 | /*---------------------------------------------------------------------------*/ |
---|
52 | |
---|
53 | /*---------------------------------------------------------------------------*/ |
---|
54 | /* Macro declarations */ |
---|
55 | /*---------------------------------------------------------------------------*/ |
---|
56 | |
---|
57 | /**AutomaticStart*************************************************************/ |
---|
58 | |
---|
59 | /*---------------------------------------------------------------------------*/ |
---|
60 | /* Static function prototypes */ |
---|
61 | /*---------------------------------------------------------------------------*/ |
---|
62 | |
---|
63 | static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv); |
---|
64 | static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv); |
---|
65 | static int CommandTransition(Hrc_Manager_t ** hmgr,int argc, char ** argv); |
---|
66 | static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv); |
---|
67 | static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv); |
---|
68 | |
---|
69 | |
---|
70 | /**AutomaticEnd***************************************************************/ |
---|
71 | |
---|
72 | |
---|
73 | /*---------------------------------------------------------------------------*/ |
---|
74 | /* Definition of exported functions */ |
---|
75 | /*---------------------------------------------------------------------------*/ |
---|
76 | |
---|
77 | /**Function******************************************************************** |
---|
78 | |
---|
79 | Synopsis [Initializes the test package.] |
---|
80 | |
---|
81 | SideEffects [] |
---|
82 | |
---|
83 | SeeAlso [Debug_End] |
---|
84 | |
---|
85 | ******************************************************************************/ |
---|
86 | void |
---|
87 | Debug_Init(void) |
---|
88 | { |
---|
89 | /* |
---|
90 | * Add a command to the global command table. By using the leading |
---|
91 | * underscore, the command will be listed under "help -a" but not "help". |
---|
92 | */ |
---|
93 | Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0); |
---|
94 | Cmd_CommandAdd("_transition", CommandTransition, 1); |
---|
95 | Cmd_CommandAdd("_sat_debug", CommandSatDebug, 0); |
---|
96 | Cmd_CommandAdd("_createAbn", CommandCreateAbnormal, 1); |
---|
97 | Cmd_CommandAdd("print_network_cnf", CommandGenerateNetworkCNF, 0); |
---|
98 | |
---|
99 | } |
---|
100 | |
---|
101 | |
---|
102 | /**Function******************************************************************** |
---|
103 | |
---|
104 | Synopsis [Ends the test package.] |
---|
105 | |
---|
106 | SideEffects [] |
---|
107 | |
---|
108 | SeeAlso [Debug_Init] |
---|
109 | |
---|
110 | ******************************************************************************/ |
---|
111 | void |
---|
112 | Debug_End(void) |
---|
113 | { |
---|
114 | /* |
---|
115 | * For example, free any global memory (if any) which the test package is |
---|
116 | * responsible for. |
---|
117 | */ |
---|
118 | } |
---|
119 | |
---|
120 | |
---|
121 | /*---------------------------------------------------------------------------*/ |
---|
122 | /* Definition of internal functions */ |
---|
123 | /*---------------------------------------------------------------------------*/ |
---|
124 | |
---|
125 | |
---|
126 | /*---------------------------------------------------------------------------*/ |
---|
127 | /* Definition of static functions */ |
---|
128 | /*---------------------------------------------------------------------------*/ |
---|
129 | |
---|
130 | |
---|
131 | static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int argc, char ** argv) |
---|
132 | { |
---|
133 | Ntk_Network_t * ntk; |
---|
134 | int c,verbose = 0; |
---|
135 | array_t * excludes = NIL(array_t); |
---|
136 | Dbg_Abnormal_t * abnormal; |
---|
137 | ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
138 | char * subs; |
---|
139 | if (ntk == NIL(Ntk_Network_t)) { |
---|
140 | (void) fprintf(vis_stdout, "** abn error: No network\n"); |
---|
141 | return 1; |
---|
142 | } |
---|
143 | while ((c = util_getopt(argc, argv, "vhs:")) != EOF) { |
---|
144 | switch(c) { |
---|
145 | case 'h': |
---|
146 | goto usage; |
---|
147 | case 'v': |
---|
148 | verbose = 1; |
---|
149 | break; |
---|
150 | case 's': |
---|
151 | subs = util_strsav(util_optarg); |
---|
152 | excludes = array_alloc(char*,0); |
---|
153 | array_insert_last(char*,excludes,subs); |
---|
154 | break; |
---|
155 | default : |
---|
156 | goto usage; |
---|
157 | } |
---|
158 | } |
---|
159 | abnormal = Dbg_DebugAbnormalAlloc(ntk); |
---|
160 | abnormal->verbose = verbose; |
---|
161 | printf("SUBS %s \n",subs); |
---|
162 | Dbg_AddAbnormalPredicatetoNetwork(abnormal,excludes); |
---|
163 | printf("\t # Abnormal predicate created %d\n", array_n(abnormal->abnormal)); |
---|
164 | return 0; |
---|
165 | usage : |
---|
166 | (void) fprintf(vis_stderr, "usage: _createAbn [-h] [-v verboseLevel] [-s substystem excludes\n"); |
---|
167 | (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); |
---|
168 | (void) fprintf(vis_stderr, " -v \t verbosity\n"); |
---|
169 | (void) fprintf(vis_stderr, " -s <subsystemName> \texclude the abnormal predicate\ |
---|
170 | for this subssytem\n"); |
---|
171 | return 1; |
---|
172 | } |
---|
173 | |
---|
174 | /**Function******************************************************************** |
---|
175 | |
---|
176 | Synopsis [Implements the _sat_debug command.] |
---|
177 | |
---|
178 | CommandName [_sat_debug] |
---|
179 | |
---|
180 | CommandSynopsis [locate faulty candidates] |
---|
181 | |
---|
182 | CommandArguments [\[-h\] \[-v\]] |
---|
183 | |
---|
184 | CommandDescription [This command compute the fault candidates of a given |
---|
185 | properties.<p> |
---|
186 | |
---|
187 | Command options:<p> |
---|
188 | |
---|
189 | <dl> |
---|
190 | <dt> -h |
---|
191 | <dd> Print the command usage. |
---|
192 | </dl> |
---|
193 | |
---|
194 | <dt> -v |
---|
195 | <dd> Verbose mode. |
---|
196 | </dl> |
---|
197 | ] |
---|
198 | |
---|
199 | SideEffects [] |
---|
200 | |
---|
201 | ******************************************************************************/ |
---|
202 | static int |
---|
203 | CommandSatDebug( |
---|
204 | Hrc_Manager_t ** hmgr, |
---|
205 | int argc, |
---|
206 | char ** argv){ |
---|
207 | int c,i; |
---|
208 | int verbose = 0; /* default value */ |
---|
209 | BmcOption_t * options = BmcOptionAlloc(); |
---|
210 | Ntk_Network_t * network; |
---|
211 | bAig_Manager_t * manager; |
---|
212 | array_t * formulaArray; |
---|
213 | array_t * LTLformulaArray; |
---|
214 | array_t * faultNodes = array_alloc(Ntk_Node_t*,0); |
---|
215 | |
---|
216 | /* |
---|
217 | * Parse command line options. |
---|
218 | */ |
---|
219 | if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) { |
---|
220 | return 1; |
---|
221 | } |
---|
222 | |
---|
223 | |
---|
224 | |
---|
225 | if (verbose) { |
---|
226 | (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n"); |
---|
227 | } |
---|
228 | /* |
---|
229 | * Read the network |
---|
230 | */ |
---|
231 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
232 | if (network == NIL(Ntk_Network_t)) { |
---|
233 | (void) fprintf(vis_stdout, "** _sat_debug error: No network\n"); |
---|
234 | BmcOptionFree(options); |
---|
235 | return 1; |
---|
236 | } |
---|
237 | manager = Ntk_NetworkReadMAigManager(network); |
---|
238 | if (manager == NIL(mAig_Manager_t)) { |
---|
239 | (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n"); |
---|
240 | BmcOptionFree(options); |
---|
241 | return 1; |
---|
242 | } |
---|
243 | |
---|
244 | Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network); |
---|
245 | if(abn == NIL(Dbg_Abnormal_t)){ |
---|
246 | (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n"); |
---|
247 | return 1; |
---|
248 | } |
---|
249 | if(verbose) |
---|
250 | printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn))); |
---|
251 | |
---|
252 | |
---|
253 | formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile); |
---|
254 | if (formulaArray == NIL(array_t)) { |
---|
255 | (void) fprintf(vis_stderr, |
---|
256 | "** bmc error: error in parsing CTL* Fromula from file\n"); |
---|
257 | BmcOptionFree(options); |
---|
258 | return 1; |
---|
259 | } |
---|
260 | if (array_n(formulaArray) == 0) { |
---|
261 | (void) fprintf(vis_stderr, "** bmc error: No formula in file\n"); |
---|
262 | BmcOptionFree(options); |
---|
263 | Ctlsp_FormulaArrayFree(formulaArray); |
---|
264 | return 1; |
---|
265 | } |
---|
266 | LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray); |
---|
267 | Ctlsp_FormulaArrayFree(formulaArray); |
---|
268 | if (LTLformulaArray == NIL(array_t)){ |
---|
269 | (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n"); |
---|
270 | BmcOptionFree(options); |
---|
271 | return 1; |
---|
272 | } |
---|
273 | Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0); |
---|
274 | |
---|
275 | |
---|
276 | /* |
---|
277 | Compute the cone of influence |
---|
278 | here : a list of state variables (latches) |
---|
279 | TODO refine to COI of the property |
---|
280 | */ |
---|
281 | st_table *CoiTable = generateAllLatches(network); |
---|
282 | /* |
---|
283 | Generate clauses for each time frame. This is the old way of generating |
---|
284 | clauses in BMC. |
---|
285 | */ |
---|
286 | if(verbose) |
---|
287 | { |
---|
288 | (void) fprintf(vis_stdout, "------ COI ----\n"); |
---|
289 | printLatch(CoiTable); |
---|
290 | (void) fprintf(vis_stdout, "--------------------------\n"); |
---|
291 | } |
---|
292 | BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable); |
---|
293 | |
---|
294 | |
---|
295 | //Generate ltl CNF |
---|
296 | // BmcGenerateCnfForLtl Génére la formule borné et retourne un index |
---|
297 | // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ... |
---|
298 | // cf. BmcLtlVerifyGeneralLtl |
---|
299 | Ctlsp_FormulaPrint(vis_stdout, ltlFormula); |
---|
300 | fprintf(vis_stdout, "\n"); |
---|
301 | int k = options->maxK; |
---|
302 | int l; |
---|
303 | // return the clause number |
---|
304 | int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); printf("LTL %d \n",noLoopIndex); |
---|
305 | |
---|
306 | |
---|
307 | array_t *objClause = NIL(array_t); |
---|
308 | objClause = array_alloc(int, 0); |
---|
309 | array_insert_last(int, objClause, noLoopIndex); |
---|
310 | BmcCnfInsertClause(cnfClauses, objClause); |
---|
311 | array_free(objClause); |
---|
312 | |
---|
313 | //Add Abnormal |
---|
314 | st_table * nodeToMvfAigTable = NIL(st_table); |
---|
315 | nodeToMvfAigTable = |
---|
316 | (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); |
---|
317 | assert(nodeToMvfAigTable != NIL(st_table)); |
---|
318 | |
---|
319 | Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses); |
---|
320 | |
---|
321 | //loop abnormal |
---|
322 | int aIndex; |
---|
323 | Ntk_Node_t * abnNode; |
---|
324 | Dbg_ForEachAbnormal(abn,aIndex,abnNode){ |
---|
325 | char * nodeName = Ntk_NodeReadName(abnNode); |
---|
326 | //set abnormal for each step |
---|
327 | array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex); |
---|
328 | int cnfIndex; |
---|
329 | int step; |
---|
330 | bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex); |
---|
331 | array_t * cnfVal = array_alloc(int,0); |
---|
332 | arrayForEachItem(int, cnfIndexArray, step, cnfIndex){ |
---|
333 | int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],step,cnfClauses); |
---|
334 | array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex); |
---|
335 | array_insert_last(int,cnfVal,abnIndex); |
---|
336 | FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); |
---|
337 | BmcWriteClauses(manager, cnfFile, cnfClauses, options); |
---|
338 | fclose(cnfFile); |
---|
339 | printf("AINDEX %d\n",aIndex); |
---|
340 | if(aIndex == 0) |
---|
341 | { |
---|
342 | FILE *cnfFile = Cmd_FileOpen("test_aks.cnf", "w", NIL(char *), 0); |
---|
343 | BmcWriteClauses(manager, cnfFile, cnfClauses, options); |
---|
344 | fclose(cnfFile); |
---|
345 | |
---|
346 | } |
---|
347 | }//end for each step |
---|
348 | |
---|
349 | //SAT procedure |
---|
350 | //assig assig input from cex |
---|
351 | //TODO build cex correctly |
---|
352 | int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel); |
---|
353 | // Build set of FaultCandidates |
---|
354 | if (res == SAT_SAT) |
---|
355 | { |
---|
356 | char * realNodeName = util_strsav(nodeName); |
---|
357 | realNodeName[strlen(nodeName)-3] = '\0'; |
---|
358 | printf("Real = %s\n", realNodeName); |
---|
359 | Ntk_Node_t * realNode = Ntk_NetworkFindNodeByName(network,realNodeName); |
---|
360 | array_insert_last(Ntk_Node_t*,faultNodes,realNode); |
---|
361 | } |
---|
362 | |
---|
363 | arrayForEachItem(int, cnfIndexArray, step, cnfIndex){ |
---|
364 | int abnIndex = array_fetch(int,cnfVal,step); |
---|
365 | array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex); |
---|
366 | } |
---|
367 | } |
---|
368 | |
---|
369 | if(verbose) |
---|
370 | (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\ |
---|
371 | latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable)); |
---|
372 | |
---|
373 | |
---|
374 | (void) fprintf(vis_stdout,"Number of Fault candidates %d\n", |
---|
375 | array_n(faultNodes)); |
---|
376 | (void) fprintf(vis_stdout,"gates : \n"); |
---|
377 | |
---|
378 | |
---|
379 | printNodeArray(faultNodes); |
---|
380 | |
---|
381 | |
---|
382 | Ctlsp_FormulaArrayFree(LTLformulaArray); |
---|
383 | BmcCnfClausesFree(cnfClauses); |
---|
384 | BmcOptionFree(options); |
---|
385 | array_free(faultNodes); |
---|
386 | return 0; |
---|
387 | } |
---|
388 | |
---|
389 | /**Function******************************************************************** |
---|
390 | |
---|
391 | Synopsis [Implements the generate_network_cnf.] |
---|
392 | |
---|
393 | CommandName [generate_network_cnf] |
---|
394 | |
---|
395 | CommandSynopsis [generate a CNF view of the network] |
---|
396 | |
---|
397 | CommandArguments [\[-h\] \[-v\] \[-k\] [fileName] ] |
---|
398 | |
---|
399 | CommandDescription [This command geerate a CNF of the network in DMACS form. |
---|
400 | The network may be unroll within k steps. |
---|
401 | <p> |
---|
402 | |
---|
403 | Command options:<p> |
---|
404 | |
---|
405 | <dl> |
---|
406 | <dt> -h |
---|
407 | <dd> Print the command usage. |
---|
408 | </dl> |
---|
409 | |
---|
410 | <dt> -v |
---|
411 | <dd> Verbose mode. |
---|
412 | </dl> |
---|
413 | |
---|
414 | <dt> -k |
---|
415 | <dd> number of steps (default 1). |
---|
416 | </dl> |
---|
417 | ] |
---|
418 | |
---|
419 | SideEffects [] |
---|
420 | |
---|
421 | ******************************************************************************/ |
---|
422 | |
---|
423 | static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv) |
---|
424 | { |
---|
425 | BmcOption_t *options = BmcOptionAlloc(); |
---|
426 | int c; |
---|
427 | unsigned int i; |
---|
428 | Ntk_Network_t * network; |
---|
429 | bAig_Manager_t * manager; |
---|
430 | char * outName = NIL(char); |
---|
431 | FILE *cnfFile; |
---|
432 | if (!options){ |
---|
433 | return 1; |
---|
434 | } |
---|
435 | options->dbgOut = 0; |
---|
436 | /* |
---|
437 | * Parse command line options. |
---|
438 | */ |
---|
439 | util_getopt_reset(); |
---|
440 | while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) { |
---|
441 | switch(c) { |
---|
442 | case 'h': |
---|
443 | goto usage; |
---|
444 | case 'k': |
---|
445 | options->maxK = atoi(util_optarg); |
---|
446 | break; |
---|
447 | case 'v': |
---|
448 | for (i = 0; i < strlen(util_optarg); i++) { |
---|
449 | if (!isdigit((int)util_optarg[i])) { |
---|
450 | goto usage; |
---|
451 | } |
---|
452 | } |
---|
453 | options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg); |
---|
454 | break; |
---|
455 | default: |
---|
456 | goto usage; |
---|
457 | } |
---|
458 | } |
---|
459 | if (argc - util_optind != 0) |
---|
460 | { |
---|
461 | outName = util_strsav(argv[util_optind]); |
---|
462 | /* create SAT Solver input file */ |
---|
463 | options->cnfFileName= outName; |
---|
464 | options->satInFile = options->cnfFileName; |
---|
465 | cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); |
---|
466 | } |
---|
467 | |
---|
468 | |
---|
469 | /* |
---|
470 | * Read the network |
---|
471 | */ |
---|
472 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
473 | if (network == NIL(Ntk_Network_t)) { |
---|
474 | (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n"); |
---|
475 | BmcOptionFree(options); |
---|
476 | return 1; |
---|
477 | } |
---|
478 | manager = Ntk_NetworkReadMAigManager(network); |
---|
479 | if (manager == NIL(mAig_Manager_t)) { |
---|
480 | (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n"); |
---|
481 | BmcOptionFree(options); |
---|
482 | return 1; |
---|
483 | } |
---|
484 | |
---|
485 | /* |
---|
486 | Compute the cone of influence |
---|
487 | here : a list of state variables (latches) |
---|
488 | */ |
---|
489 | st_table *CoiTable = generateAllLatches(network); |
---|
490 | |
---|
491 | if(options->verbosityLevel) |
---|
492 | { |
---|
493 | (void) fprintf(vis_stdout, "------ COI ----\n"); |
---|
494 | printLatch(CoiTable); |
---|
495 | (void) fprintf(vis_stdout, "--------------------------\n"); |
---|
496 | } |
---|
497 | BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable); |
---|
498 | if(outName != NIL(char)) |
---|
499 | { |
---|
500 | BmcWriteClauses(manager, cnfFile, cnfClauses, options); |
---|
501 | fclose(cnfFile); |
---|
502 | } |
---|
503 | else |
---|
504 | BmcWriteClauses(manager, vis_stdout, cnfClauses, options); |
---|
505 | |
---|
506 | if(options->verbosityLevel) |
---|
507 | { |
---|
508 | (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK); |
---|
509 | (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses, |
---|
510 | st_count(CoiTable)); |
---|
511 | } |
---|
512 | |
---|
513 | BmcOptionFree(options); |
---|
514 | return 0; |
---|
515 | usage: |
---|
516 | (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n"); |
---|
517 | (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); |
---|
518 | (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n"); |
---|
519 | (void) fprintf(vis_stderr, " -v <verbosity_level>\n"); |
---|
520 | (void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n"); |
---|
521 | (void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n"); |
---|
522 | (void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n"); |
---|
523 | (void) fprintf(vis_stderr, " <cnf_file> The output file containing CNF of the network.\n"); |
---|
524 | |
---|
525 | BmcOptionFree(options); |
---|
526 | return 1; |
---|
527 | } |
---|
528 | |
---|
529 | /**Function******************************************************************** |
---|
530 | |
---|
531 | Synopsis [Implements the _Debug_test command.] |
---|
532 | |
---|
533 | CommandName [_Debug_test] |
---|
534 | |
---|
535 | CommandSynopsis [template for implementing commands] |
---|
536 | |
---|
537 | CommandArguments [\[-h\] \[-v\]] |
---|
538 | |
---|
539 | CommandDescription [This command does nothing useful. It merely serves as a |
---|
540 | template for the implementation of new commands.<p> |
---|
541 | |
---|
542 | Command options:<p> |
---|
543 | |
---|
544 | <dl> |
---|
545 | <dt> -h |
---|
546 | <dd> Print the command usage. |
---|
547 | </dl> |
---|
548 | |
---|
549 | <dt> -v |
---|
550 | <dd> Verbose mode. |
---|
551 | </dl> |
---|
552 | ] |
---|
553 | |
---|
554 | SideEffects [] |
---|
555 | |
---|
556 | ******************************************************************************/ |
---|
557 | static int |
---|
558 | CommandDebug( |
---|
559 | Hrc_Manager_t ** hmgr, |
---|
560 | int argc, |
---|
561 | char ** argv) |
---|
562 | { |
---|
563 | int c; |
---|
564 | int verbose = 0; /* default value */ |
---|
565 | |
---|
566 | /* |
---|
567 | * Parse command line options. |
---|
568 | */ |
---|
569 | util_getopt_reset(); |
---|
570 | while ((c = util_getopt(argc, argv, "vh")) != EOF) { |
---|
571 | switch(c) { |
---|
572 | case 'v': |
---|
573 | verbose = 1; |
---|
574 | break; |
---|
575 | case 'h': |
---|
576 | goto usage; |
---|
577 | default: |
---|
578 | goto usage; |
---|
579 | } |
---|
580 | } |
---|
581 | |
---|
582 | if (verbose) { |
---|
583 | (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n"); |
---|
584 | } |
---|
585 | |
---|
586 | Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); |
---|
587 | mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); |
---|
588 | printf("** DEBUG MODE **\n"); |
---|
589 | Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr); |
---|
590 | printf("model : %s\n", Hrc_NodeReadModelName(n)); |
---|
591 | |
---|
592 | mdd_t * safe = getSafe(fsm); |
---|
593 | mdd_t * forbid = getForbidden(fsm); |
---|
594 | mdd_t * reach = getReach(fsm); |
---|
595 | |
---|
596 | if(safe == NIL(mdd_t)) |
---|
597 | { |
---|
598 | printf("call command set_safe before\n"); |
---|
599 | return 1; |
---|
600 | } |
---|
601 | if(forbid == NIL(mdd_t)) |
---|
602 | { |
---|
603 | printf("call command set_forbidden before\n"); |
---|
604 | return 1; |
---|
605 | } |
---|
606 | |
---|
607 | FILE* oFile; |
---|
608 | oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0); |
---|
609 | // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile); |
---|
610 | // mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile); |
---|
611 | |
---|
612 | mdd_t * EFState = mdd_and(reach,safe,1,1); |
---|
613 | // mdd_t * errorState = mdd_and(reach,forbid,1,1); |
---|
614 | |
---|
615 | mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); |
---|
616 | array_t *careStatesArray = array_alloc(mdd_t *, 0); |
---|
617 | array_insert(mdd_t *, careStatesArray, 0,mddOne); |
---|
618 | |
---|
619 | mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
620 | EFState, |
---|
621 | fsm->fairnessInfo.states, |
---|
622 | careStatesArray, |
---|
623 | 0, |
---|
624 | McDcLevelNone_c); |
---|
625 | |
---|
626 | mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1); |
---|
627 | mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile); |
---|
628 | |
---|
629 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
630 | EXEFState, |
---|
631 | fsm->fairnessInfo.states, |
---|
632 | careStatesArray, |
---|
633 | 0, |
---|
634 | McDcLevelNone_c); |
---|
635 | mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
636 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
637 | mdd_t * andState = mdd_xor(EXEFState2,EXEFState); |
---|
638 | mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile); |
---|
639 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
640 | andState, |
---|
641 | fsm->fairnessInfo.states, |
---|
642 | careStatesArray, |
---|
643 | 0, |
---|
644 | McDcLevelNone_c); |
---|
645 | EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
646 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
647 | andState = mdd_xor(EXEFState2,andState); |
---|
648 | mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile); |
---|
649 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
650 | andState, |
---|
651 | fsm->fairnessInfo.states, |
---|
652 | careStatesArray, |
---|
653 | 0, |
---|
654 | McDcLevelNone_c); |
---|
655 | EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
656 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
657 | andState = mdd_xor(EXEFState2,andState); |
---|
658 | mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile); |
---|
659 | |
---|
660 | |
---|
661 | |
---|
662 | //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile); |
---|
663 | //mdd_GetState_Values(mddManager , EFState, stdout); |
---|
664 | fclose(oFile); |
---|
665 | |
---|
666 | |
---|
667 | |
---|
668 | |
---|
669 | |
---|
670 | return 0; /* normal exit */ |
---|
671 | |
---|
672 | usage: |
---|
673 | (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n"); |
---|
674 | (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); |
---|
675 | (void) fprintf(vis_stderr, " -v\t\tverbose\n"); |
---|
676 | return 1; /* error exit */ |
---|
677 | } |
---|
678 | |
---|
679 | /******************************************/ |
---|
680 | /* function that build a bdd for the */ |
---|
681 | /* simple example : */ |
---|
682 | /* (state = 0) -> !(state = 1) */ |
---|
683 | /******************************************/ |
---|
684 | mdd_t * buildDummyBdd(mdd_manager *mddManager) |
---|
685 | { |
---|
686 | /** state0 = 0 **/ |
---|
687 | mdd_t * s0 = mdd_eq_c(mddManager,0, 0); |
---|
688 | mdd_t * s1 = mdd_eq_c(mddManager,2, 0); |
---|
689 | mdd_t * state0 = mdd_one(mddManager); |
---|
690 | state0 = mdd_and(s0,s1,1,1); |
---|
691 | /** state1 = 1 **/ |
---|
692 | mdd_t * ns0 = mdd_eq_c(mddManager,1, 1); |
---|
693 | mdd_t * ns1 = mdd_eq_c(mddManager,3, 0); |
---|
694 | mdd_t * state1 = mdd_one(mddManager); |
---|
695 | state1 = mdd_and(ns0,ns1,1,1); |
---|
696 | /** state = 0) -> !(state = 1) **/ |
---|
697 | mdd_t * rel = mdd_one(mddManager); |
---|
698 | rel = mdd_or(state0,state1,0,0); |
---|
699 | |
---|
700 | return rel; |
---|
701 | } |
---|
702 | |
---|
703 | |
---|
704 | /**Function******************************************************************** |
---|
705 | |
---|
706 | Synopsis [Implements the transtion command.] |
---|
707 | |
---|
708 | CommandName [_transition] |
---|
709 | |
---|
710 | CommandSynopsis [compute new transition relation] |
---|
711 | |
---|
712 | CommandArguments [\[-h\] \[-v\]] |
---|
713 | |
---|
714 | CommandDescription [This command create a new transition relation that is a |
---|
715 | and of the Bdd of the old one and an other bdd. |
---|
716 | <p> |
---|
717 | |
---|
718 | Command options:<p> |
---|
719 | |
---|
720 | <dl> |
---|
721 | <dt> -h |
---|
722 | <dd> Print the command usage. |
---|
723 | </dl> |
---|
724 | |
---|
725 | <dt> -v |
---|
726 | <dd> Verbose mode. |
---|
727 | </dl> |
---|
728 | ] |
---|
729 | |
---|
730 | SideEffects [Change the fsm] |
---|
731 | |
---|
732 | ******************************************************************************/ |
---|
733 | |
---|
734 | static int |
---|
735 | CommandTransition (Hrc_Manager_t ** hmgr, |
---|
736 | int argc, char ** argv){ |
---|
737 | int c; |
---|
738 | int verbose = 0; /* default value */ |
---|
739 | |
---|
740 | /* |
---|
741 | * Parse command line options. |
---|
742 | */ |
---|
743 | util_getopt_reset(); |
---|
744 | while ((c = util_getopt(argc, argv, "vh")) != EOF) { |
---|
745 | switch(c) { |
---|
746 | case 'v': |
---|
747 | verbose = 1; |
---|
748 | break; |
---|
749 | case 'h': |
---|
750 | goto usage; |
---|
751 | default: |
---|
752 | goto usage; |
---|
753 | } |
---|
754 | } |
---|
755 | |
---|
756 | if (verbose) { |
---|
757 | (void) fprintf(vis_stdout, "The _transition is under construction.\n"); |
---|
758 | } |
---|
759 | |
---|
760 | Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t); |
---|
761 | Ntk_Network_t *network = NIL(Ntk_Network_t); |
---|
762 | mdd_manager *mddManager; |
---|
763 | mdd_t *rel = NIL(mdd_t); |
---|
764 | graph_t *partition; |
---|
765 | int i; |
---|
766 | /******************/ |
---|
767 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
768 | if(network == NIL(Ntk_Network_t)) |
---|
769 | return 1; |
---|
770 | fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); |
---|
771 | if(fsm == NIL(Fsm_Fsm_t)) |
---|
772 | return 1; |
---|
773 | mddManager = Fsm_FsmReadMddManager(fsm); |
---|
774 | |
---|
775 | |
---|
776 | |
---|
777 | /********** Build cex ***********/ |
---|
778 | /* Here add the function */ |
---|
779 | /* that build the Bdd to and */ |
---|
780 | /* with the transtion relation */ |
---|
781 | /***********************************/ |
---|
782 | rel = buildDummyBdd(mddManager); |
---|
783 | if(rel == NIL(mdd_t)) |
---|
784 | { |
---|
785 | fprintf(vis_stdout,"Problem when building the new relation bdd"); |
---|
786 | return 1; |
---|
787 | } |
---|
788 | if (verbose) |
---|
789 | mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout); |
---|
790 | |
---|
791 | |
---|
792 | /** Get image_info **/ |
---|
793 | Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0); |
---|
794 | partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm)); |
---|
795 | /**** The complete transtion relation ****/ |
---|
796 | // array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0); |
---|
797 | /*****************************************/ |
---|
798 | /*** For each latch rebuild the transition function ***/ |
---|
799 | /*** mvf table is composed of mdd for each possible ***/ |
---|
800 | /*** value of the latch ***/ |
---|
801 | ImgFunctionData_t * functionData = &(imageInfo->functionData); |
---|
802 | array_t *roots = functionData->roots; |
---|
803 | array_t *rangeVarMddIdArray = functionData->rangeVars; |
---|
804 | char * nodeName; |
---|
805 | arrayForEachItem(char *, roots, i, nodeName) { |
---|
806 | /* The new relation */ |
---|
807 | vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName); |
---|
808 | Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); |
---|
809 | int mddId = array_fetch(int, rangeVarMddIdArray, i); |
---|
810 | mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId); |
---|
811 | mdd_t * n_relation = mdd_and(relation,rel,1,1); |
---|
812 | /* Build for each possible value */ |
---|
813 | int nbValue = Mvf_FunctionReadNumComponents(mvf) ; |
---|
814 | int v ; |
---|
815 | Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue); |
---|
816 | for(v = 0; v<nbValue;v++) |
---|
817 | { |
---|
818 | mdd_t * n_s1 = mdd_eq_c(mddManager,mddId, v); |
---|
819 | mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1); |
---|
820 | mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1); |
---|
821 | Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1); |
---|
822 | |
---|
823 | } |
---|
824 | /* Replace the function for the latch */ |
---|
825 | Part_VertexSetFunction(vertex, newMvf); |
---|
826 | // printf("vertex %s changed % d\n",PartVertexReadName(vertex)); |
---|
827 | } |
---|
828 | |
---|
829 | /** Change the fsm and the network with a new partition and the new fsm **/ |
---|
830 | Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY, |
---|
831 | (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, |
---|
832 | (void *) partition); |
---|
833 | fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t)); |
---|
834 | mdd_t * init = Fsm_FsmComputeInitialStates(fsm); |
---|
835 | mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose, |
---|
836 | 0,0, 0, |
---|
837 | 0, 0, Fsm_Rch_Default_c, |
---|
838 | 0,1, NIL(array_t), |
---|
839 | (verbose > 0), NIL(array_t)); |
---|
840 | fsm->reachabilityInfo.initialStates = init; |
---|
841 | fsm->reachabilityInfo.reachableStates = reach; |
---|
842 | if(verbose) |
---|
843 | Fsm_FsmReachabilityPrintResults(fsm,3, 0); |
---|
844 | |
---|
845 | Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY, |
---|
846 | (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, |
---|
847 | (void *) fsm); |
---|
848 | |
---|
849 | return 0; /* normal exit */ |
---|
850 | |
---|
851 | usage: |
---|
852 | (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n"); |
---|
853 | (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); |
---|
854 | (void) fprintf(vis_stderr, " -v\t\tverbose\n"); |
---|
855 | return 1; /* error exit */ |
---|
856 | |
---|
857 | } |
---|
858 | |
---|
859 | |
---|