source: vis_dev/vis-2.3/src/debug/debug.c@ 36

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

Add Abnormal predicate structures
File size: 19.7 KB
Line 
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"
35static 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
63static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
64static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
65static int CommandTransition(Hrc_Manager_t ** hmgr,int argc, char ** argv);
66static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv);
67
68
69/**AutomaticEnd***************************************************************/
70
71
72/*---------------------------------------------------------------------------*/
73/* Definition of exported functions */
74/*---------------------------------------------------------------------------*/
75
76/**Function********************************************************************
77
78 Synopsis [Initializes the test package.]
79
80 SideEffects []
81
82 SeeAlso [Debug_End]
83
84******************************************************************************/
85void
86Debug_Init(void)
87{
88 /*
89 * Add a command to the global command table. By using the leading
90 * underscore, the command will be listed under "help -a" but not "help".
91 */
92 Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
93 Cmd_CommandAdd("_transition", CommandTransition, 1);
94 Cmd_CommandAdd("_sat_debug", CommandSatDebug, 0);
95 Cmd_CommandAdd("_createAbn", CommandCreateAbnormal, 1);
96
97}
98
99
100/**Function********************************************************************
101
102 Synopsis [Ends the test package.]
103
104 SideEffects []
105
106 SeeAlso [Debug_Init]
107
108******************************************************************************/
109void
110Debug_End(void)
111{
112 /*
113 * For example, free any global memory (if any) which the test package is
114 * responsible for.
115 */
116}
117
118
119/*---------------------------------------------------------------------------*/
120/* Definition of internal functions */
121/*---------------------------------------------------------------------------*/
122
123
124/*---------------------------------------------------------------------------*/
125/* Definition of static functions */
126/*---------------------------------------------------------------------------*/
127
128
129static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int argc, char ** argv)
130{
131 Ntk_Network_t * ntk;
132 int c,verbose;
133 Dbg_Abnormal_t * abnormal;
134 ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
135 if (ntk == NIL(Ntk_Network_t)) {
136 (void) fprintf(vis_stdout, "** abn error: No network\n");
137 return 1;
138 }
139 while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
140 switch(c) {
141 case 'v':
142 verbose = 1;
143 break;
144 }
145 }
146 abnormal = Dbg_DebugAbnormalAlloc(ntk);
147 abnormal->verbose = verbose;
148 Dbg_AddAbnormalPredicatetoNetwork(abnormal);
149}
150/**Function********************************************************************
151
152 Synopsis [Implements the _sat_debug command.]
153
154 CommandName [_sat_debug]
155
156 CommandSynopsis [locate faulty candidates]
157
158 CommandArguments [\[-h\] \[-v\]]
159
160 CommandDescription [This command compute the fault candidates of a given
161 properties.<p>
162
163 Command options:<p>
164
165 <dl>
166 <dt> -h
167 <dd> Print the command usage.
168 </dl>
169
170 <dt> -v
171 <dd> Verbose mode.
172 </dl>
173 ]
174
175 SideEffects []
176
177******************************************************************************/
178
179
180static int
181CommandSatDebug(
182Hrc_Manager_t ** hmgr,
183int argc,
184char ** argv){
185int c,i;
186int verbose = 0; /* default value */
187BmcOption_t *options = BmcOptionAlloc();
188Ntk_Network_t * network;
189bAig_Manager_t *manager;
190
191
192/*
193 * Parse command line options.
194 */
195util_getopt_reset();
196while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
197 switch(c) {
198 case 'v':
199 verbose = 1;
200 options->verbosityLevel = verbose;
201 break;
202 case 'h':
203 goto usage;
204 case 'm':
205 for (i = 0; i < strlen(util_optarg); i++) {
206 if (!isdigit((int)util_optarg[i])) {
207 goto usage;
208 }
209 }
210 options->minK = atoi(util_optarg);
211 break;
212 case 'k':
213 for (i = 0; i < strlen(util_optarg); i++) {
214 if (!isdigit((int)util_optarg[i])) {
215 goto usage;
216 }
217 }
218 options->maxK = atoi(util_optarg);
219 break;
220 case 'o':
221 options->cnfFileName = util_strsav(util_optarg);
222 break;
223
224 default:
225 goto usage;
226 }
227}
228 if (options->minK > options->maxK){
229 (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");
230 goto usage;
231 }
232
233if (verbose) {
234 (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
235}
236 /* create SAT Solver input file */
237 if (options->cnfFileName == NIL(char)) {
238 options->satInFile = BmcCreateTmpFile();
239}
240 else {
241 options->satInFile = options->cnfFileName;
242 }
243
244/* create SAT Solver output file */
245options->satOutFile = BmcCreateTmpFile();
246if (options->satOutFile == NIL(char)){
247 BmcOptionFree(options);
248 (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
249 return 1;
250}
251
252options->verbosityLevel = 1;
253//options->satSolver
254//options->clauses
255
256 /*
257 * Read the network
258 */
259 network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
260 if (network == NIL(Ntk_Network_t)) {
261 (void) fprintf(vis_stdout, "** bmc error: No network\n");
262 BmcOptionFree(options);
263 return 1;
264 }
265 manager = Ntk_NetworkReadMAigManager(network);
266 if (manager == NIL(mAig_Manager_t)) {
267 (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
268 BmcOptionFree(options);
269 return 1;
270 }
271 /*
272 We need the bdd when building the transition relation of the automaton
273 */
274 if(options->inductiveStep !=0){
275 Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
276
277 designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
278 if (designFsm == NIL(Fsm_Fsm_t)) {
279 (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
280 return 1;
281 }
282 }
283
284 /*
285 Compute the cone of influence
286 here a list of state variables (latches)
287 */
288 st_table *CoiTable = generateAllLatches(network);
289 /*
290 Generate clauses for each time frame. This is the old way of generating
291 clauses in BMC.
292 */
293 st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
294 BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
295 FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
296 /*
297 nodeToMvfAigTable maps each node to its multi-function And/Inv graph
298 */
299 nodeToMvfAigTable =
300 (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
301 assert(nodeToMvfAigTable != NIL(st_table));
302
303 if(verbose)
304 {
305 (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
306 printLatch(nodeToMvfAigTable);
307 (void) fprintf(vis_stdout, "------ COI ----\n");
308 printLatch(CoiTable);
309 (void) fprintf(vis_stdout, "--------------------------\n");
310 }
311 /*
312 Create a clause database
313 */
314 cnfClauses = BmcCnfClausesAlloc();
315 /*
316 Generate clauses for an initialized path of length k
317 */
318 BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
319 cnfClauses, nodeToMvfAigTable, CoiTable);
320 if(verbose)
321 (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
322 latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
323
324
325 BmcWriteClauses(manager, cnfFile, cnfClauses, options);
326fclose(cnfFile);
327BmcCnfClausesFree(cnfClauses);
328BmcOptionFree(options);
329return 0;
330 usage:
331 (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
332 minimum length] [-o cnf_file]\n");
333 (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
334 (void) fprintf(vis_stderr, " -v\t\tverbose\n");
335 (void) fprintf(vis_stderr, " -m \tminimum length of counterexample to be checked (default is 0)\n");
336 (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n");
337 (void) fprintf(vis_stderr, " -o <cnf_file> contains CNF of the counterexample\n");
338 return 1; /* error exit */
339
340}
341/**Function********************************************************************
342
343 Synopsis [Implements the _Debug_test command.]
344
345 CommandName [_Debug_test]
346
347 CommandSynopsis [template for implementing commands]
348
349 CommandArguments [\[-h\] \[-v\]]
350
351 CommandDescription [This command does nothing useful. It merely serves as a
352 template for the implementation of new commands.<p>
353
354 Command options:<p>
355
356 <dl>
357 <dt> -h
358 <dd> Print the command usage.
359 </dl>
360
361 <dt> -v
362 <dd> Verbose mode.
363 </dl>
364 ]
365
366 SideEffects []
367
368******************************************************************************/
369static int
370CommandDebug(
371 Hrc_Manager_t ** hmgr,
372 int argc,
373 char ** argv)
374{
375 int c;
376 int verbose = 0; /* default value */
377
378 /*
379 * Parse command line options.
380 */
381 util_getopt_reset();
382 while ((c = util_getopt(argc, argv, "vh")) != EOF) {
383 switch(c) {
384 case 'v':
385 verbose = 1;
386 break;
387 case 'h':
388 goto usage;
389 default:
390 goto usage;
391 }
392 }
393
394 if (verbose) {
395 (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
396 }
397
398 Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
399 mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
400 printf("** DEBUG MODE **\n");
401 Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
402 printf("model : %s\n", Hrc_NodeReadModelName(n));
403
404 mdd_t * safe = getSafe(fsm);
405 mdd_t * forbid = getForbidden(fsm);
406 mdd_t * reach = getReach(fsm);
407
408 if(safe == NIL(mdd_t))
409 {
410 printf("call command set_safe before\n");
411 return 1;
412 }
413 if(forbid == NIL(mdd_t))
414 {
415 printf("call command set_forbidden before\n");
416 return 1;
417 }
418
419 FILE* oFile;
420 oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
421 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
422// mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
423
424 mdd_t * EFState = mdd_and(reach,safe,1,1);
425// mdd_t * errorState = mdd_and(reach,forbid,1,1);
426
427 mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
428 array_t *careStatesArray = array_alloc(mdd_t *, 0);
429 array_insert(mdd_t *, careStatesArray, 0,mddOne);
430
431 mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
432 EFState,
433 fsm->fairnessInfo.states,
434 careStatesArray,
435 0,
436 McDcLevelNone_c);
437
438 mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
439 mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
440
441 tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
442 EXEFState,
443 fsm->fairnessInfo.states,
444 careStatesArray,
445 0,
446 McDcLevelNone_c);
447 mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
448 mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
449 mdd_t * andState = mdd_xor(EXEFState2,EXEFState);
450 mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
451 tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
452 andState,
453 fsm->fairnessInfo.states,
454 careStatesArray,
455 0,
456 McDcLevelNone_c);
457 EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
458 mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
459 andState = mdd_xor(EXEFState2,andState);
460 mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
461 tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
462 andState,
463 fsm->fairnessInfo.states,
464 careStatesArray,
465 0,
466 McDcLevelNone_c);
467 EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
468 mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
469 andState = mdd_xor(EXEFState2,andState);
470 mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
471
472
473
474 //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
475 //mdd_GetState_Values(mddManager , EFState, stdout);
476 fclose(oFile);
477
478
479
480
481
482 return 0; /* normal exit */
483
484 usage:
485 (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
486 (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
487 (void) fprintf(vis_stderr, " -v\t\tverbose\n");
488 return 1; /* error exit */
489}
490
491/******************************************/
492/* function that build a bdd for the */
493/* simple example : */
494/* (state = 0) -> !(state = 1) */
495/******************************************/
496mdd_t * buildDummyBdd(mdd_manager *mddManager)
497{
498/** state0 = 0 **/
499 mdd_t * s0 = mdd_eq_c(mddManager,0, 0);
500 mdd_t * s1 = mdd_eq_c(mddManager,2, 0);
501 mdd_t * state0 = mdd_one(mddManager);
502 state0 = mdd_and(s0,s1,1,1);
503/** state1 = 1 **/
504 mdd_t * ns0 = mdd_eq_c(mddManager,1, 1);
505 mdd_t * ns1 = mdd_eq_c(mddManager,3, 0);
506 mdd_t * state1 = mdd_one(mddManager);
507 state1 = mdd_and(ns0,ns1,1,1);
508/** state = 0) -> !(state = 1) **/
509 mdd_t * rel = mdd_one(mddManager);
510 rel = mdd_or(state0,state1,0,0);
511
512 return rel;
513}
514
515
516/**Function********************************************************************
517
518 Synopsis [Implements the transtion command.]
519
520 CommandName [_transition]
521
522 CommandSynopsis [compute new transition relation]
523
524 CommandArguments [\[-h\] \[-v\]]
525
526 CommandDescription [This command create a new transition relation that is a
527 and of the Bdd of the old one and an other bdd.
528 <p>
529
530 Command options:<p>
531
532 <dl>
533 <dt> -h
534 <dd> Print the command usage.
535 </dl>
536
537 <dt> -v
538 <dd> Verbose mode.
539 </dl>
540 ]
541
542 SideEffects [Change the fsm]
543
544******************************************************************************/
545
546static int
547CommandTransition (Hrc_Manager_t ** hmgr,
548 int argc, char ** argv){
549int c;
550int verbose = 0; /* default value */
551
552/*
553 * Parse command line options.
554 */
555util_getopt_reset();
556while ((c = util_getopt(argc, argv, "vh")) != EOF) {
557 switch(c) {
558 case 'v':
559 verbose = 1;
560 break;
561 case 'h':
562 goto usage;
563 default:
564 goto usage;
565 }
566}
567
568if (verbose) {
569 (void) fprintf(vis_stdout, "The _transition is under construction.\n");
570}
571
572Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t);
573Ntk_Network_t *network = NIL(Ntk_Network_t);
574mdd_manager *mddManager;
575mdd_t *rel = NIL(mdd_t);
576graph_t *partition;
577int i;
578/******************/
579network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
580if(network == NIL(Ntk_Network_t))
581 return 1;
582fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
583if(fsm == NIL(Fsm_Fsm_t))
584 return 1;
585mddManager = Fsm_FsmReadMddManager(fsm);
586
587
588
589/********** Build cex ***********/
590/* Here add the function */
591/* that build the Bdd to and */
592/* with the transtion relation */
593/***********************************/
594rel = buildDummyBdd(mddManager);
595if(rel == NIL(mdd_t))
596{
597 fprintf(vis_stdout,"Problem when building the new relation bdd");
598 return 1;
599}
600
601/** Get image_info **/
602Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
603partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
604/**** The complete transtion relation ****/
605// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
606/*****************************************/
607/*** For each latch rebuild the transition function ***/
608/*** mvf table is composed of mdd for each possible ***/
609/*** value of the latch ***/
610ImgFunctionData_t * functionData = &(imageInfo->functionData);
611array_t *roots = functionData->roots;
612array_t *rangeVarMddIdArray = functionData->rangeVars;
613char * nodeName;
614arrayForEachItem(char *, roots, i, nodeName) {
615 /* The new relation */
616 vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
617 Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
618 int mddId = array_fetch(int, rangeVarMddIdArray, i);
619 mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
620 mdd_t * n_relation = mdd_and(relation,rel,1,1);
621 /* Build for each possible value */
622 int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
623 int v ;
624 Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
625 for(v = 0; v<nbValue;v++)
626 {
627 mdd_t * n_s1 = mdd_eq_c(mddManager,mddId, v);
628 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
629 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
630 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
631
632 }
633 /* Replace the function for the latch */
634 Part_VertexSetFunction(vertex, newMvf);
635// printf("vertex %s changed % d\n",PartVertexReadName(vertex));
636 Mvf_FunctionFree(mvf);
637}
638
639/** Change the fsm **/
640fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition);
641mdd_t * init = Fsm_FsmComputeInitialStates(fsm);
642Fsm_FsmComputeReachableStates(fsm,0,verbose,
643 0,0, 0,
644 0, 0, Fsm_Rch_Default_c,
645 0,1, NIL(array_t),
646 (verbose > 0), NIL(array_t));
647if(verbose)
648 Fsm_FsmReachabilityPrintResults(fsm,3, 0);
649/** Change Image Info **/
650Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
651 (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
652 (void *) partition);
653
654
655return 0; /* normal exit */
656
657usage:
658(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
659(void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
660(void) fprintf(vis_stderr, " -v\t\tverbose\n");
661return 1; /* error exit */
662
663}
664
665
Note: See TracBrowser for help on using the repository browser.