[27] | 1 | /**CFile*********************************************************************** |
---|
| 2 | |
---|
| 3 | FileName [debug.c] |
---|
| 4 | |
---|
| 5 | PackageName [debug] |
---|
| 6 | |
---|
[30] | 7 | Synopsis [Debug package initialization, ending, and the command debug] |
---|
[27] | 8 | |
---|
[35] | 9 | Author [Cecile B.] |
---|
[27] | 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" |
---|
[30] | 33 | #include "imgInt.h" |
---|
| 34 | #include "partInt.h" |
---|
[27] | 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 | |
---|
[35] | 63 | static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv); |
---|
[27] | 64 | static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv); |
---|
[30] | 65 | static int CommandTransition(Hrc_Manager_t ** hmgr,int argc, char ** argv); |
---|
[35] | 66 | static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv); |
---|
[27] | 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 | ******************************************************************************/ |
---|
| 85 | void |
---|
| 86 | Debug_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 | */ |
---|
[35] | 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); |
---|
[27] | 96 | |
---|
| 97 | } |
---|
| 98 | |
---|
| 99 | |
---|
| 100 | /**Function******************************************************************** |
---|
| 101 | |
---|
| 102 | Synopsis [Ends the test package.] |
---|
| 103 | |
---|
| 104 | SideEffects [] |
---|
| 105 | |
---|
| 106 | SeeAlso [Debug_Init] |
---|
| 107 | |
---|
| 108 | ******************************************************************************/ |
---|
| 109 | void |
---|
| 110 | Debug_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 | |
---|
[35] | 128 | |
---|
[36] | 129 | static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int argc, char ** argv) |
---|
[35] | 130 | { |
---|
| 131 | Ntk_Network_t * ntk; |
---|
[36] | 132 | int c,verbose; |
---|
| 133 | Dbg_Abnormal_t * abnormal; |
---|
[35] | 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 | } |
---|
[36] | 139 | while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) { |
---|
| 140 | switch(c) { |
---|
| 141 | case 'v': |
---|
| 142 | verbose = 1; |
---|
| 143 | break; |
---|
[35] | 144 | } |
---|
[36] | 145 | } |
---|
| 146 | abnormal = Dbg_DebugAbnormalAlloc(ntk); |
---|
| 147 | abnormal->verbose = verbose; |
---|
| 148 | Dbg_AddAbnormalPredicatetoNetwork(abnormal); |
---|
[35] | 149 | } |
---|
[27] | 150 | /**Function******************************************************************** |
---|
| 151 | |
---|
[35] | 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 | |
---|
| 180 | static int |
---|
| 181 | CommandSatDebug( |
---|
| 182 | Hrc_Manager_t ** hmgr, |
---|
| 183 | int argc, |
---|
| 184 | char ** argv){ |
---|
| 185 | int c,i; |
---|
| 186 | int verbose = 0; /* default value */ |
---|
| 187 | BmcOption_t *options = BmcOptionAlloc(); |
---|
| 188 | Ntk_Network_t * network; |
---|
| 189 | bAig_Manager_t *manager; |
---|
| 190 | |
---|
| 191 | |
---|
| 192 | /* |
---|
| 193 | * Parse command line options. |
---|
| 194 | */ |
---|
| 195 | util_getopt_reset(); |
---|
| 196 | while ((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 | |
---|
| 233 | if (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 */ |
---|
| 245 | options->satOutFile = BmcCreateTmpFile(); |
---|
| 246 | if (options->satOutFile == NIL(char)){ |
---|
| 247 | BmcOptionFree(options); |
---|
| 248 | (void) fprintf(vis_stdout, "The _sat_debug problem.\n"); |
---|
| 249 | return 1; |
---|
| 250 | } |
---|
| 251 | |
---|
| 252 | options->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); |
---|
| 326 | fclose(cnfFile); |
---|
| 327 | BmcCnfClausesFree(cnfClauses); |
---|
| 328 | BmcOptionFree(options); |
---|
| 329 | return 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 | |
---|
[27] | 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 | ******************************************************************************/ |
---|
| 369 | static int |
---|
| 370 | CommandDebug( |
---|
| 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 | |
---|
[30] | 491 | /******************************************/ |
---|
| 492 | /* function that build a bdd for the */ |
---|
| 493 | /* simple example : */ |
---|
| 494 | /* (state = 0) -> !(state = 1) */ |
---|
| 495 | /******************************************/ |
---|
| 496 | mdd_t * buildDummyBdd(mdd_manager *mddManager) |
---|
[27] | 497 | { |
---|
[30] | 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 | } |
---|
[27] | 514 | |
---|
| 515 | |
---|
| 516 | /**Function******************************************************************** |
---|
| 517 | |
---|
[30] | 518 | Synopsis [Implements the transtion command.] |
---|
[27] | 519 | |
---|
[30] | 520 | CommandName [_transition] |
---|
[27] | 521 | |
---|
[30] | 522 | CommandSynopsis [compute new transition relation] |
---|
[27] | 523 | |
---|
[30] | 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> |
---|
[27] | 529 | |
---|
[30] | 530 | Command options:<p> |
---|
[27] | 531 | |
---|
[30] | 532 | <dl> |
---|
| 533 | <dt> -h |
---|
| 534 | <dd> Print the command usage. |
---|
| 535 | </dl> |
---|
[27] | 536 | |
---|
[30] | 537 | <dt> -v |
---|
| 538 | <dd> Verbose mode. |
---|
| 539 | </dl> |
---|
| 540 | ] |
---|
[27] | 541 | |
---|
[30] | 542 | SideEffects [Change the fsm] |
---|
[27] | 543 | |
---|
| 544 | ******************************************************************************/ |
---|
| 545 | |
---|
| 546 | static int |
---|
[30] | 547 | CommandTransition (Hrc_Manager_t ** hmgr, |
---|
[27] | 548 | int argc, char ** argv){ |
---|
[30] | 549 | int c; |
---|
| 550 | int verbose = 0; /* default value */ |
---|
[27] | 551 | |
---|
[30] | 552 | /* |
---|
| 553 | * Parse command line options. |
---|
| 554 | */ |
---|
| 555 | util_getopt_reset(); |
---|
| 556 | while ((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; |
---|
[27] | 565 | } |
---|
[30] | 566 | } |
---|
[27] | 567 | |
---|
[30] | 568 | if (verbose) { |
---|
| 569 | (void) fprintf(vis_stdout, "The _transition is under construction.\n"); |
---|
| 570 | } |
---|
[27] | 571 | |
---|
[30] | 572 | Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t); |
---|
| 573 | Ntk_Network_t *network = NIL(Ntk_Network_t); |
---|
| 574 | mdd_manager *mddManager; |
---|
| 575 | mdd_t *rel = NIL(mdd_t); |
---|
| 576 | graph_t *partition; |
---|
| 577 | int i; |
---|
| 578 | /******************/ |
---|
| 579 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 580 | if(network == NIL(Ntk_Network_t)) |
---|
| 581 | return 1; |
---|
| 582 | fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); |
---|
| 583 | if(fsm == NIL(Fsm_Fsm_t)) |
---|
| 584 | return 1; |
---|
| 585 | mddManager = Fsm_FsmReadMddManager(fsm); |
---|
[27] | 586 | |
---|
| 587 | |
---|
| 588 | |
---|
[30] | 589 | /********** Build cex ***********/ |
---|
| 590 | /* Here add the function */ |
---|
| 591 | /* that build the Bdd to and */ |
---|
| 592 | /* with the transtion relation */ |
---|
| 593 | /***********************************/ |
---|
| 594 | rel = buildDummyBdd(mddManager); |
---|
| 595 | if(rel == NIL(mdd_t)) |
---|
| 596 | { |
---|
| 597 | fprintf(vis_stdout,"Problem when building the new relation bdd"); |
---|
| 598 | return 1; |
---|
[27] | 599 | } |
---|
| 600 | |
---|
[30] | 601 | /** Get image_info **/ |
---|
| 602 | Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0); |
---|
| 603 | partition = 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 ***/ |
---|
| 610 | ImgFunctionData_t * functionData = &(imageInfo->functionData); |
---|
| 611 | array_t *roots = functionData->roots; |
---|
| 612 | array_t *rangeVarMddIdArray = functionData->rangeVars; |
---|
| 613 | char * nodeName; |
---|
| 614 | arrayForEachItem(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); |
---|
[27] | 631 | |
---|
[30] | 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); |
---|
[27] | 637 | } |
---|
| 638 | |
---|
[30] | 639 | /** Change the fsm **/ |
---|
| 640 | fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition); |
---|
| 641 | mdd_t * init = Fsm_FsmComputeInitialStates(fsm); |
---|
| 642 | Fsm_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)); |
---|
| 647 | if(verbose) |
---|
| 648 | Fsm_FsmReachabilityPrintResults(fsm,3, 0); |
---|
| 649 | /** Change Image Info **/ |
---|
| 650 | Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY, |
---|
| 651 | (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, |
---|
| 652 | (void *) partition); |
---|
[27] | 653 | |
---|
| 654 | |
---|
[30] | 655 | return 0; /* normal exit */ |
---|
[27] | 656 | |
---|
[30] | 657 | usage: |
---|
| 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"); |
---|
| 661 | return 1; /* error exit */ |
---|
[27] | 662 | |
---|
| 663 | } |
---|
| 664 | |
---|
| 665 | |
---|