[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); |
---|
[41] | 67 | static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv); |
---|
[27] | 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 | */ |
---|
[35] | 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); |
---|
[41] | 97 | Cmd_CommandAdd("print_network_cnf", CommandGenerateNetworkCNF, 0); |
---|
[27] | 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 | |
---|
[35] | 130 | |
---|
[36] | 131 | static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int argc, char ** argv) |
---|
[35] | 132 | { |
---|
| 133 | Ntk_Network_t * ntk; |
---|
[36] | 134 | int c,verbose; |
---|
| 135 | Dbg_Abnormal_t * abnormal; |
---|
[35] | 136 | ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 137 | if (ntk == NIL(Ntk_Network_t)) { |
---|
| 138 | (void) fprintf(vis_stdout, "** abn error: No network\n"); |
---|
| 139 | return 1; |
---|
| 140 | } |
---|
[36] | 141 | while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) { |
---|
| 142 | switch(c) { |
---|
| 143 | case 'v': |
---|
| 144 | verbose = 1; |
---|
| 145 | break; |
---|
[35] | 146 | } |
---|
[36] | 147 | } |
---|
| 148 | abnormal = Dbg_DebugAbnormalAlloc(ntk); |
---|
| 149 | abnormal->verbose = verbose; |
---|
| 150 | Dbg_AddAbnormalPredicatetoNetwork(abnormal); |
---|
[35] | 151 | } |
---|
[27] | 152 | /**Function******************************************************************** |
---|
| 153 | |
---|
[35] | 154 | Synopsis [Implements the _sat_debug command.] |
---|
| 155 | |
---|
| 156 | CommandName [_sat_debug] |
---|
| 157 | |
---|
| 158 | CommandSynopsis [locate faulty candidates] |
---|
| 159 | |
---|
| 160 | CommandArguments [\[-h\] \[-v\]] |
---|
| 161 | |
---|
| 162 | CommandDescription [This command compute the fault candidates of a given |
---|
| 163 | properties.<p> |
---|
| 164 | |
---|
| 165 | Command options:<p> |
---|
| 166 | |
---|
| 167 | <dl> |
---|
| 168 | <dt> -h |
---|
| 169 | <dd> Print the command usage. |
---|
| 170 | </dl> |
---|
| 171 | |
---|
| 172 | <dt> -v |
---|
| 173 | <dd> Verbose mode. |
---|
| 174 | </dl> |
---|
| 175 | ] |
---|
| 176 | |
---|
| 177 | SideEffects [] |
---|
| 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 */ |
---|
[41] | 187 | BmcOption_t * options = BmcOptionAlloc(); |
---|
| 188 | Ntk_Network_t * network; |
---|
| 189 | bAig_Manager_t * manager; |
---|
| 190 | array_t * formulaArray; |
---|
| 191 | array_t * LTLformulaArray; |
---|
| 192 | char * ltlFileName = NIL(char); |
---|
[42] | 193 | array_t * faultNodes = array_alloc(Ntk_Node_t*,0); |
---|
[35] | 194 | |
---|
| 195 | /* |
---|
| 196 | * Parse command line options. |
---|
| 197 | */ |
---|
[41] | 198 | if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) { |
---|
| 199 | return 1; |
---|
| 200 | } |
---|
[35] | 201 | |
---|
[41] | 202 | |
---|
[38] | 203 | printf("MAX K %d", options->maxK); |
---|
[35] | 204 | |
---|
| 205 | if (verbose) { |
---|
| 206 | (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n"); |
---|
| 207 | } |
---|
[41] | 208 | /* |
---|
| 209 | * Read the network |
---|
| 210 | */ |
---|
| 211 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 212 | if (network == NIL(Ntk_Network_t)) { |
---|
| 213 | (void) fprintf(vis_stdout, "** _sat_debug error: No network\n"); |
---|
| 214 | BmcOptionFree(options); |
---|
| 215 | return 1; |
---|
[35] | 216 | } |
---|
[41] | 217 | manager = Ntk_NetworkReadMAigManager(network); |
---|
| 218 | if (manager == NIL(mAig_Manager_t)) { |
---|
| 219 | (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n"); |
---|
[35] | 220 | BmcOptionFree(options); |
---|
| 221 | return 1; |
---|
| 222 | } |
---|
| 223 | |
---|
[40] | 224 | Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network); |
---|
[41] | 225 | if(abn == NIL(Dbg_Abnormal_t)){ |
---|
| 226 | (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n"); |
---|
| 227 | return 1; |
---|
| 228 | } |
---|
| 229 | if(verbose) |
---|
| 230 | printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn))); |
---|
[38] | 231 | |
---|
| 232 | |
---|
[41] | 233 | formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile); |
---|
| 234 | if (formulaArray == NIL(array_t)) { |
---|
| 235 | (void) fprintf(vis_stderr, |
---|
| 236 | "** bmc error: error in parsing CTL* Fromula from file\n"); |
---|
| 237 | BmcOptionFree(options); |
---|
| 238 | return 1; |
---|
| 239 | } |
---|
| 240 | if (array_n(formulaArray) == 0) { |
---|
| 241 | (void) fprintf(vis_stderr, "** bmc error: No formula in file\n"); |
---|
| 242 | BmcOptionFree(options); |
---|
[38] | 243 | Ctlsp_FormulaArrayFree(formulaArray); |
---|
[41] | 244 | return 1; |
---|
| 245 | } |
---|
| 246 | LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray); |
---|
| 247 | Ctlsp_FormulaArrayFree(formulaArray); |
---|
| 248 | if (LTLformulaArray == NIL(array_t)){ |
---|
| 249 | (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n"); |
---|
| 250 | BmcOptionFree(options); |
---|
| 251 | return 1; |
---|
| 252 | } |
---|
| 253 | Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0); |
---|
[38] | 254 | |
---|
| 255 | |
---|
| 256 | |
---|
[35] | 257 | /* |
---|
| 258 | Compute the cone of influence |
---|
[38] | 259 | here : a list of state variables (latches) |
---|
[41] | 260 | TODO refine to COI of the property |
---|
[35] | 261 | */ |
---|
| 262 | st_table *CoiTable = generateAllLatches(network); |
---|
| 263 | /* |
---|
| 264 | Generate clauses for each time frame. This is the old way of generating |
---|
| 265 | clauses in BMC. |
---|
| 266 | */ |
---|
[41] | 267 | if(verbose) |
---|
[35] | 268 | { |
---|
| 269 | (void) fprintf(vis_stdout, "------ COI ----\n"); |
---|
| 270 | printLatch(CoiTable); |
---|
| 271 | (void) fprintf(vis_stdout, "--------------------------\n"); |
---|
| 272 | } |
---|
[41] | 273 | BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable); |
---|
[38] | 274 | |
---|
[41] | 275 | |
---|
[38] | 276 | //Generate ltl CNF |
---|
| 277 | // BmcGenerateCnfForLtl Génére la formule borné et retourne un index |
---|
| 278 | // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ... |
---|
| 279 | // cf. BmcLtlVerifyGeneralLtl |
---|
[41] | 280 | Ctlsp_FormulaPrint(vis_stdout, ltlFormula); |
---|
| 281 | fprintf(vis_stdout, "\n"); |
---|
[38] | 282 | int k = options->maxK; |
---|
| 283 | int l; |
---|
| 284 | // return the clause number |
---|
[40] | 285 | int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); |
---|
[38] | 286 | |
---|
[41] | 287 | |
---|
[42] | 288 | array_t *objClause = NIL(array_t); |
---|
[40] | 289 | objClause = array_alloc(int, 0); |
---|
| 290 | array_insert_last(int, objClause, noLoopIndex); |
---|
| 291 | BmcCnfInsertClause(cnfClauses, objClause); |
---|
| 292 | array_free(objClause); |
---|
[38] | 293 | |
---|
[41] | 294 | //Add Abnormal |
---|
| 295 | st_table * nodeToMvfAigTable = NIL(st_table); |
---|
| 296 | nodeToMvfAigTable = |
---|
[42] | 297 | (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); |
---|
| 298 | assert(nodeToMvfAigTable != NIL(st_table)); |
---|
[38] | 299 | |
---|
[41] | 300 | Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses); |
---|
[38] | 301 | |
---|
[42] | 302 | //loop abnormal |
---|
[41] | 303 | int aIndex; |
---|
| 304 | Ntk_Node_t * abnNode; |
---|
[42] | 305 | Dbg_ForEachAbnormal(abn,aIndex,abnNode){ |
---|
| 306 | char * nodeName = Ntk_NodeReadName(abnNode); |
---|
| 307 | //set abnormal |
---|
[41] | 308 | int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex); |
---|
| 309 | bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex); |
---|
| 310 | int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses); |
---|
| 311 | array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex); |
---|
| 312 | FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); |
---|
| 313 | BmcWriteClauses(manager, cnfFile, cnfClauses, options); |
---|
| 314 | fclose(cnfFile); |
---|
[42] | 315 | |
---|
[41] | 316 | //SAT procedure |
---|
[42] | 317 | //assig assig input from cex |
---|
| 318 | //TODO build cex correctly |
---|
| 319 | int res = Dbg_SatCheck("assig",options->cnfFileName,options->verbosityLevel); |
---|
| 320 | // Build set of FaultCandidates |
---|
| 321 | if (res == SAT_SAT) |
---|
| 322 | { |
---|
| 323 | char * realNodeName = util_strsav(nodeName); |
---|
| 324 | realNodeName[strlen(nodeName)-4] = '\0'; |
---|
| 325 | Ntk_Node_t * realNode = Ntk_NetworkFindNodeByName(network,realNodeName); |
---|
| 326 | array_insert_last(Ntk_Node_t*,faultNodes,realNode); |
---|
| 327 | } |
---|
[38] | 328 | |
---|
[41] | 329 | |
---|
[42] | 330 | array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex); |
---|
| 331 | } |
---|
| 332 | |
---|
[35] | 333 | if(verbose) |
---|
| 334 | (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\ |
---|
[42] | 335 | latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable)); |
---|
| 336 | |
---|
| 337 | (void) fprintf(vis_stdout,"Number of Fault candidates %d\n", |
---|
| 338 | array_n(faultNodes)); |
---|
| 339 | (void) fprintf(vis_stdout,"gates : \n"); |
---|
| 340 | printNodeArray(faultNodes); |
---|
| 341 | |
---|
| 342 | |
---|
[41] | 343 | Ctlsp_FormulaArrayFree(LTLformulaArray); |
---|
[35] | 344 | BmcCnfClausesFree(cnfClauses); |
---|
| 345 | BmcOptionFree(options); |
---|
[42] | 346 | array_free(faultNodes); |
---|
[35] | 347 | return 0; |
---|
[41] | 348 | |
---|
| 349 | } |
---|
| 350 | /**Function******************************************************************** |
---|
| 351 | |
---|
| 352 | Synopsis [Implements the generate_network_cnf.] |
---|
| 353 | |
---|
| 354 | CommandName [generate_network_cnf] |
---|
| 355 | |
---|
| 356 | CommandSynopsis [generate a CNF view of the network] |
---|
| 357 | |
---|
| 358 | CommandArguments [\[-h\] \[-v\] \[-k\] [fileName] ] |
---|
| 359 | |
---|
| 360 | CommandDescription [This command geerate a CNF of the network in DMACS form. |
---|
| 361 | The network may be unroll within k steps. |
---|
| 362 | <p> |
---|
| 363 | |
---|
| 364 | Command options:<p> |
---|
| 365 | |
---|
| 366 | <dl> |
---|
| 367 | <dt> -h |
---|
| 368 | <dd> Print the command usage. |
---|
| 369 | </dl> |
---|
| 370 | |
---|
| 371 | <dt> -v |
---|
| 372 | <dd> Verbose mode. |
---|
| 373 | </dl> |
---|
| 374 | |
---|
| 375 | <dt> -k |
---|
| 376 | <dd> number of steps (default 1). |
---|
| 377 | </dl> |
---|
| 378 | ] |
---|
| 379 | |
---|
| 380 | SideEffects [] |
---|
| 381 | |
---|
| 382 | ******************************************************************************/ |
---|
| 383 | |
---|
| 384 | static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int argc, char ** argv) |
---|
| 385 | { |
---|
| 386 | BmcOption_t *options = BmcOptionAlloc(); |
---|
| 387 | int c; |
---|
| 388 | unsigned int i; |
---|
| 389 | Ntk_Network_t * network; |
---|
| 390 | bAig_Manager_t * manager; |
---|
| 391 | char * outName = NIL(char); |
---|
| 392 | FILE *cnfFile; |
---|
| 393 | if (!options){ |
---|
| 394 | return 1; |
---|
| 395 | } |
---|
| 396 | options->dbgOut = 0; |
---|
| 397 | /* |
---|
| 398 | * Parse command line options. |
---|
| 399 | */ |
---|
| 400 | util_getopt_reset(); |
---|
| 401 | while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) { |
---|
| 402 | switch(c) { |
---|
| 403 | case 'h': |
---|
| 404 | goto usage; |
---|
| 405 | case 'k': |
---|
| 406 | options->maxK = atoi(util_optarg); |
---|
| 407 | break; |
---|
| 408 | case 'v': |
---|
| 409 | for (i = 0; i < strlen(util_optarg); i++) { |
---|
| 410 | if (!isdigit((int)util_optarg[i])) { |
---|
| 411 | goto usage; |
---|
| 412 | } |
---|
| 413 | } |
---|
| 414 | options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg); |
---|
| 415 | break; |
---|
| 416 | default: |
---|
| 417 | goto usage; |
---|
| 418 | } |
---|
| 419 | } |
---|
| 420 | if (argc - util_optind != 0) |
---|
| 421 | { |
---|
| 422 | outName = util_strsav(argv[util_optind]); |
---|
| 423 | /* create SAT Solver input file */ |
---|
| 424 | options->cnfFileName= outName; |
---|
| 425 | options->satInFile = options->cnfFileName; |
---|
| 426 | cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); |
---|
| 427 | } |
---|
| 428 | |
---|
| 429 | |
---|
| 430 | /* |
---|
| 431 | * Read the network |
---|
| 432 | */ |
---|
| 433 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 434 | if (network == NIL(Ntk_Network_t)) { |
---|
| 435 | (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n"); |
---|
| 436 | BmcOptionFree(options); |
---|
| 437 | return 1; |
---|
| 438 | } |
---|
| 439 | manager = Ntk_NetworkReadMAigManager(network); |
---|
| 440 | if (manager == NIL(mAig_Manager_t)) { |
---|
| 441 | (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n"); |
---|
| 442 | BmcOptionFree(options); |
---|
| 443 | return 1; |
---|
| 444 | } |
---|
| 445 | |
---|
| 446 | /* |
---|
| 447 | Compute the cone of influence |
---|
| 448 | here : a list of state variables (latches) |
---|
| 449 | */ |
---|
| 450 | st_table *CoiTable = generateAllLatches(network); |
---|
| 451 | |
---|
| 452 | if(options->verbosityLevel) |
---|
| 453 | { |
---|
| 454 | (void) fprintf(vis_stdout, "------ COI ----\n"); |
---|
| 455 | printLatch(CoiTable); |
---|
| 456 | (void) fprintf(vis_stdout, "--------------------------\n"); |
---|
| 457 | } |
---|
| 458 | BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable); |
---|
| 459 | if(outName != NIL(char)) |
---|
| 460 | { |
---|
| 461 | BmcWriteClauses(manager, cnfFile, cnfClauses, options); |
---|
| 462 | fclose(cnfFile); |
---|
| 463 | } |
---|
| 464 | else |
---|
| 465 | BmcWriteClauses(manager, vis_stdout, cnfClauses, options); |
---|
| 466 | |
---|
| 467 | if(options->verbosityLevel) |
---|
| 468 | { |
---|
| 469 | (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK); |
---|
| 470 | (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses, |
---|
| 471 | st_count(CoiTable)); |
---|
| 472 | } |
---|
| 473 | |
---|
| 474 | BmcOptionFree(options); |
---|
| 475 | return 0; |
---|
| 476 | usage: |
---|
| 477 | (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n"); |
---|
| 478 | (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); |
---|
[35] | 479 | (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n"); |
---|
[41] | 480 | (void) fprintf(vis_stderr, " -v <verbosity_level>\n"); |
---|
| 481 | (void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n"); |
---|
| 482 | (void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n"); |
---|
| 483 | (void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n"); |
---|
| 484 | (void) fprintf(vis_stderr, " <cnf_file> The output file containing CNF of the network.\n"); |
---|
[35] | 485 | |
---|
[41] | 486 | BmcOptionFree(options); |
---|
| 487 | return 1; |
---|
[35] | 488 | } |
---|
[41] | 489 | |
---|
[35] | 490 | /**Function******************************************************************** |
---|
| 491 | |
---|
[27] | 492 | Synopsis [Implements the _Debug_test command.] |
---|
| 493 | |
---|
| 494 | CommandName [_Debug_test] |
---|
| 495 | |
---|
| 496 | CommandSynopsis [template for implementing commands] |
---|
| 497 | |
---|
| 498 | CommandArguments [\[-h\] \[-v\]] |
---|
| 499 | |
---|
| 500 | CommandDescription [This command does nothing useful. It merely serves as a |
---|
| 501 | template for the implementation of new commands.<p> |
---|
| 502 | |
---|
| 503 | Command options:<p> |
---|
| 504 | |
---|
| 505 | <dl> |
---|
| 506 | <dt> -h |
---|
| 507 | <dd> Print the command usage. |
---|
| 508 | </dl> |
---|
| 509 | |
---|
| 510 | <dt> -v |
---|
| 511 | <dd> Verbose mode. |
---|
| 512 | </dl> |
---|
| 513 | ] |
---|
| 514 | |
---|
| 515 | SideEffects [] |
---|
| 516 | |
---|
| 517 | ******************************************************************************/ |
---|
| 518 | static int |
---|
| 519 | CommandDebug( |
---|
| 520 | Hrc_Manager_t ** hmgr, |
---|
| 521 | int argc, |
---|
| 522 | char ** argv) |
---|
| 523 | { |
---|
| 524 | int c; |
---|
| 525 | int verbose = 0; /* default value */ |
---|
| 526 | |
---|
| 527 | /* |
---|
| 528 | * Parse command line options. |
---|
| 529 | */ |
---|
| 530 | util_getopt_reset(); |
---|
| 531 | while ((c = util_getopt(argc, argv, "vh")) != EOF) { |
---|
| 532 | switch(c) { |
---|
| 533 | case 'v': |
---|
| 534 | verbose = 1; |
---|
| 535 | break; |
---|
| 536 | case 'h': |
---|
| 537 | goto usage; |
---|
| 538 | default: |
---|
| 539 | goto usage; |
---|
| 540 | } |
---|
| 541 | } |
---|
| 542 | |
---|
| 543 | if (verbose) { |
---|
| 544 | (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n"); |
---|
| 545 | } |
---|
| 546 | |
---|
| 547 | Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); |
---|
| 548 | mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm); |
---|
| 549 | printf("** DEBUG MODE **\n"); |
---|
| 550 | Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr); |
---|
| 551 | printf("model : %s\n", Hrc_NodeReadModelName(n)); |
---|
| 552 | |
---|
| 553 | mdd_t * safe = getSafe(fsm); |
---|
| 554 | mdd_t * forbid = getForbidden(fsm); |
---|
| 555 | mdd_t * reach = getReach(fsm); |
---|
| 556 | |
---|
| 557 | if(safe == NIL(mdd_t)) |
---|
| 558 | { |
---|
| 559 | printf("call command set_safe before\n"); |
---|
| 560 | return 1; |
---|
| 561 | } |
---|
| 562 | if(forbid == NIL(mdd_t)) |
---|
| 563 | { |
---|
| 564 | printf("call command set_forbidden before\n"); |
---|
| 565 | return 1; |
---|
| 566 | } |
---|
| 567 | |
---|
| 568 | FILE* oFile; |
---|
| 569 | oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0); |
---|
| 570 | // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile); |
---|
| 571 | // mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile); |
---|
| 572 | |
---|
| 573 | mdd_t * EFState = mdd_and(reach,safe,1,1); |
---|
| 574 | // mdd_t * errorState = mdd_and(reach,forbid,1,1); |
---|
| 575 | |
---|
| 576 | mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm)); |
---|
| 577 | array_t *careStatesArray = array_alloc(mdd_t *, 0); |
---|
| 578 | array_insert(mdd_t *, careStatesArray, 0,mddOne); |
---|
| 579 | |
---|
| 580 | mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
| 581 | EFState, |
---|
| 582 | fsm->fairnessInfo.states, |
---|
| 583 | careStatesArray, |
---|
| 584 | 0, |
---|
| 585 | McDcLevelNone_c); |
---|
| 586 | |
---|
| 587 | mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1); |
---|
| 588 | mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile); |
---|
| 589 | |
---|
| 590 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
| 591 | EXEFState, |
---|
| 592 | fsm->fairnessInfo.states, |
---|
| 593 | careStatesArray, |
---|
| 594 | 0, |
---|
| 595 | McDcLevelNone_c); |
---|
| 596 | mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
| 597 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
| 598 | mdd_t * andState = mdd_xor(EXEFState2,EXEFState); |
---|
| 599 | mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile); |
---|
| 600 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
| 601 | andState, |
---|
| 602 | fsm->fairnessInfo.states, |
---|
| 603 | careStatesArray, |
---|
| 604 | 0, |
---|
| 605 | McDcLevelNone_c); |
---|
| 606 | EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
| 607 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
| 608 | andState = mdd_xor(EXEFState2,andState); |
---|
| 609 | mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile); |
---|
| 610 | tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm, |
---|
| 611 | andState, |
---|
| 612 | fsm->fairnessInfo.states, |
---|
| 613 | careStatesArray, |
---|
| 614 | 0, |
---|
| 615 | McDcLevelNone_c); |
---|
| 616 | EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1); |
---|
| 617 | mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile); |
---|
| 618 | andState = mdd_xor(EXEFState2,andState); |
---|
| 619 | mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile); |
---|
| 620 | |
---|
| 621 | |
---|
| 622 | |
---|
| 623 | //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile); |
---|
| 624 | //mdd_GetState_Values(mddManager , EFState, stdout); |
---|
| 625 | fclose(oFile); |
---|
| 626 | |
---|
| 627 | |
---|
| 628 | |
---|
| 629 | |
---|
| 630 | |
---|
| 631 | return 0; /* normal exit */ |
---|
| 632 | |
---|
| 633 | usage: |
---|
| 634 | (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n"); |
---|
| 635 | (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); |
---|
| 636 | (void) fprintf(vis_stderr, " -v\t\tverbose\n"); |
---|
| 637 | return 1; /* error exit */ |
---|
| 638 | } |
---|
| 639 | |
---|
[30] | 640 | /******************************************/ |
---|
| 641 | /* function that build a bdd for the */ |
---|
| 642 | /* simple example : */ |
---|
| 643 | /* (state = 0) -> !(state = 1) */ |
---|
| 644 | /******************************************/ |
---|
| 645 | mdd_t * buildDummyBdd(mdd_manager *mddManager) |
---|
[27] | 646 | { |
---|
[30] | 647 | /** state0 = 0 **/ |
---|
| 648 | mdd_t * s0 = mdd_eq_c(mddManager,0, 0); |
---|
| 649 | mdd_t * s1 = mdd_eq_c(mddManager,2, 0); |
---|
| 650 | mdd_t * state0 = mdd_one(mddManager); |
---|
| 651 | state0 = mdd_and(s0,s1,1,1); |
---|
| 652 | /** state1 = 1 **/ |
---|
| 653 | mdd_t * ns0 = mdd_eq_c(mddManager,1, 1); |
---|
| 654 | mdd_t * ns1 = mdd_eq_c(mddManager,3, 0); |
---|
| 655 | mdd_t * state1 = mdd_one(mddManager); |
---|
| 656 | state1 = mdd_and(ns0,ns1,1,1); |
---|
| 657 | /** state = 0) -> !(state = 1) **/ |
---|
| 658 | mdd_t * rel = mdd_one(mddManager); |
---|
| 659 | rel = mdd_or(state0,state1,0,0); |
---|
| 660 | |
---|
| 661 | return rel; |
---|
| 662 | } |
---|
[27] | 663 | |
---|
| 664 | |
---|
| 665 | /**Function******************************************************************** |
---|
| 666 | |
---|
[30] | 667 | Synopsis [Implements the transtion command.] |
---|
[27] | 668 | |
---|
[30] | 669 | CommandName [_transition] |
---|
[27] | 670 | |
---|
[30] | 671 | CommandSynopsis [compute new transition relation] |
---|
[27] | 672 | |
---|
[30] | 673 | CommandArguments [\[-h\] \[-v\]] |
---|
| 674 | |
---|
| 675 | CommandDescription [This command create a new transition relation that is a |
---|
| 676 | and of the Bdd of the old one and an other bdd. |
---|
| 677 | <p> |
---|
[27] | 678 | |
---|
[30] | 679 | Command options:<p> |
---|
[27] | 680 | |
---|
[30] | 681 | <dl> |
---|
| 682 | <dt> -h |
---|
| 683 | <dd> Print the command usage. |
---|
| 684 | </dl> |
---|
[27] | 685 | |
---|
[30] | 686 | <dt> -v |
---|
| 687 | <dd> Verbose mode. |
---|
| 688 | </dl> |
---|
| 689 | ] |
---|
[27] | 690 | |
---|
[30] | 691 | SideEffects [Change the fsm] |
---|
[27] | 692 | |
---|
| 693 | ******************************************************************************/ |
---|
| 694 | |
---|
| 695 | static int |
---|
[30] | 696 | CommandTransition (Hrc_Manager_t ** hmgr, |
---|
[27] | 697 | int argc, char ** argv){ |
---|
[30] | 698 | int c; |
---|
| 699 | int verbose = 0; /* default value */ |
---|
[27] | 700 | |
---|
[30] | 701 | /* |
---|
| 702 | * Parse command line options. |
---|
| 703 | */ |
---|
| 704 | util_getopt_reset(); |
---|
| 705 | while ((c = util_getopt(argc, argv, "vh")) != EOF) { |
---|
| 706 | switch(c) { |
---|
| 707 | case 'v': |
---|
| 708 | verbose = 1; |
---|
| 709 | break; |
---|
| 710 | case 'h': |
---|
| 711 | goto usage; |
---|
| 712 | default: |
---|
| 713 | goto usage; |
---|
[27] | 714 | } |
---|
[30] | 715 | } |
---|
[27] | 716 | |
---|
[30] | 717 | if (verbose) { |
---|
| 718 | (void) fprintf(vis_stdout, "The _transition is under construction.\n"); |
---|
| 719 | } |
---|
[27] | 720 | |
---|
[30] | 721 | Fsm_Fsm_t *fsm = NIL(Fsm_Fsm_t); |
---|
| 722 | Ntk_Network_t *network = NIL(Ntk_Network_t); |
---|
| 723 | mdd_manager *mddManager; |
---|
| 724 | mdd_t *rel = NIL(mdd_t); |
---|
| 725 | graph_t *partition; |
---|
| 726 | int i; |
---|
| 727 | /******************/ |
---|
| 728 | network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
| 729 | if(network == NIL(Ntk_Network_t)) |
---|
| 730 | return 1; |
---|
| 731 | fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); |
---|
| 732 | if(fsm == NIL(Fsm_Fsm_t)) |
---|
| 733 | return 1; |
---|
| 734 | mddManager = Fsm_FsmReadMddManager(fsm); |
---|
[27] | 735 | |
---|
| 736 | |
---|
| 737 | |
---|
[30] | 738 | /********** Build cex ***********/ |
---|
| 739 | /* Here add the function */ |
---|
| 740 | /* that build the Bdd to and */ |
---|
| 741 | /* with the transtion relation */ |
---|
| 742 | /***********************************/ |
---|
| 743 | rel = buildDummyBdd(mddManager); |
---|
| 744 | if(rel == NIL(mdd_t)) |
---|
| 745 | { |
---|
| 746 | fprintf(vis_stdout,"Problem when building the new relation bdd"); |
---|
| 747 | return 1; |
---|
[27] | 748 | } |
---|
[37] | 749 | if (verbose) |
---|
| 750 | mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout); |
---|
[27] | 751 | |
---|
[37] | 752 | |
---|
[30] | 753 | /** Get image_info **/ |
---|
| 754 | Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0); |
---|
| 755 | partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm)); |
---|
| 756 | /**** The complete transtion relation ****/ |
---|
| 757 | // array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0); |
---|
| 758 | /*****************************************/ |
---|
| 759 | /*** For each latch rebuild the transition function ***/ |
---|
| 760 | /*** mvf table is composed of mdd for each possible ***/ |
---|
| 761 | /*** value of the latch ***/ |
---|
| 762 | ImgFunctionData_t * functionData = &(imageInfo->functionData); |
---|
| 763 | array_t *roots = functionData->roots; |
---|
| 764 | array_t *rangeVarMddIdArray = functionData->rangeVars; |
---|
| 765 | char * nodeName; |
---|
| 766 | arrayForEachItem(char *, roots, i, nodeName) { |
---|
| 767 | /* The new relation */ |
---|
| 768 | vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName); |
---|
| 769 | Mvf_Function_t *mvf = Part_VertexReadFunction(vertex); |
---|
| 770 | int mddId = array_fetch(int, rangeVarMddIdArray, i); |
---|
| 771 | mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId); |
---|
| 772 | mdd_t * n_relation = mdd_and(relation,rel,1,1); |
---|
| 773 | /* Build for each possible value */ |
---|
| 774 | int nbValue = Mvf_FunctionReadNumComponents(mvf) ; |
---|
| 775 | int v ; |
---|
| 776 | Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue); |
---|
| 777 | for(v = 0; v<nbValue;v++) |
---|
| 778 | { |
---|
| 779 | mdd_t * n_s1 = mdd_eq_c(mddManager,mddId, v); |
---|
| 780 | mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1); |
---|
| 781 | mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1); |
---|
| 782 | Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1); |
---|
[27] | 783 | |
---|
[30] | 784 | } |
---|
| 785 | /* Replace the function for the latch */ |
---|
| 786 | Part_VertexSetFunction(vertex, newMvf); |
---|
| 787 | // printf("vertex %s changed % d\n",PartVertexReadName(vertex)); |
---|
[27] | 788 | } |
---|
| 789 | |
---|
[37] | 790 | /** Change the fsm and the network with a new partition and the new fsm **/ |
---|
| 791 | Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY, |
---|
| 792 | (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, |
---|
| 793 | (void *) partition); |
---|
| 794 | fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t)); |
---|
[30] | 795 | mdd_t * init = Fsm_FsmComputeInitialStates(fsm); |
---|
[37] | 796 | mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose, |
---|
[30] | 797 | 0,0, 0, |
---|
| 798 | 0, 0, Fsm_Rch_Default_c, |
---|
| 799 | 0,1, NIL(array_t), |
---|
| 800 | (verbose > 0), NIL(array_t)); |
---|
[37] | 801 | fsm->reachabilityInfo.initialStates = init; |
---|
| 802 | fsm->reachabilityInfo.reachableStates = reach; |
---|
[30] | 803 | if(verbose) |
---|
| 804 | Fsm_FsmReachabilityPrintResults(fsm,3, 0); |
---|
[27] | 805 | |
---|
[37] | 806 | Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY, |
---|
| 807 | (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, |
---|
| 808 | (void *) fsm); |
---|
[27] | 809 | |
---|
[30] | 810 | return 0; /* normal exit */ |
---|
[27] | 811 | |
---|
[30] | 812 | usage: |
---|
| 813 | (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n"); |
---|
| 814 | (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n"); |
---|
| 815 | (void) fprintf(vis_stderr, " -v\t\tverbose\n"); |
---|
| 816 | return 1; /* error exit */ |
---|
[27] | 817 | |
---|
| 818 | } |
---|
| 819 | |
---|
| 820 | |
---|