[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; |
---|
[44] | 134 | int c,verbose = 0; |
---|
| 135 | array_t * excludes = NIL(array_t); |
---|
[36] | 136 | Dbg_Abnormal_t * abnormal; |
---|
[35] | 137 | ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr); |
---|
[44] | 138 | char * subs; |
---|
[35] | 139 | if (ntk == NIL(Ntk_Network_t)) { |
---|
| 140 | (void) fprintf(vis_stdout, "** abn error: No network\n"); |
---|
| 141 | return 1; |
---|
| 142 | } |
---|
[44] | 143 | while ((c = util_getopt(argc, argv, "vhs:")) != EOF) { |
---|
[36] | 144 | switch(c) { |
---|
[44] | 145 | case 'h': |
---|
| 146 | goto usage; |
---|
[36] | 147 | case 'v': |
---|
| 148 | verbose = 1; |
---|
| 149 | break; |
---|
[44] | 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; |
---|
[35] | 157 | } |
---|
[36] | 158 | } |
---|
| 159 | abnormal = Dbg_DebugAbnormalAlloc(ntk); |
---|
| 160 | abnormal->verbose = verbose; |
---|
[44] | 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; |
---|
[35] | 172 | } |
---|
[44] | 173 | |
---|
[27] | 174 | /**Function******************************************************************** |
---|
| 175 | |
---|
[35] | 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 */ |
---|
[41] | 209 | BmcOption_t * options = BmcOptionAlloc(); |
---|
| 210 | Ntk_Network_t * network; |
---|
| 211 | bAig_Manager_t * manager; |
---|
| 212 | array_t * formulaArray; |
---|
| 213 | array_t * LTLformulaArray; |
---|
[42] | 214 | array_t * faultNodes = array_alloc(Ntk_Node_t*,0); |
---|
[35] | 215 | |
---|
| 216 | /* |
---|
| 217 | * Parse command line options. |
---|
| 218 | */ |
---|
[41] | 219 | if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) { |
---|
| 220 | return 1; |
---|
| 221 | } |
---|
[35] | 222 | |
---|
[41] | 223 | |
---|
[35] | 224 | |
---|
| 225 | if (verbose) { |
---|
| 226 | (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n"); |
---|
| 227 | } |
---|
[41] | 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; |
---|
[35] | 236 | } |
---|
[41] | 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"); |
---|
[35] | 240 | BmcOptionFree(options); |
---|
| 241 | return 1; |
---|
| 242 | } |
---|
| 243 | |
---|
[40] | 244 | Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network); |
---|
[41] | 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))); |
---|
[38] | 251 | |
---|
| 252 | |
---|
[41] | 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); |
---|
[38] | 263 | Ctlsp_FormulaArrayFree(formulaArray); |
---|
[41] | 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); |
---|
[38] | 274 | |
---|
| 275 | |
---|
[35] | 276 | /* |
---|
| 277 | Compute the cone of influence |
---|
[38] | 278 | here : a list of state variables (latches) |
---|
[41] | 279 | TODO refine to COI of the property |
---|
[35] | 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 | */ |
---|
[41] | 286 | if(verbose) |
---|
[35] | 287 | { |
---|
| 288 | (void) fprintf(vis_stdout, "------ COI ----\n"); |
---|
| 289 | printLatch(CoiTable); |
---|
| 290 | (void) fprintf(vis_stdout, "--------------------------\n"); |
---|
| 291 | } |
---|
[41] | 292 | BmcCnfClauses_t* cnfClauses = Dbg_GenerateCNF(network,options,CoiTable); |
---|
[38] | 293 | |
---|
[41] | 294 | |
---|
[38] | 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 |
---|
[41] | 299 | Ctlsp_FormulaPrint(vis_stdout, ltlFormula); |
---|
| 300 | fprintf(vis_stdout, "\n"); |
---|
[38] | 301 | int k = options->maxK; |
---|
| 302 | int l; |
---|
| 303 | // return the clause number |
---|
[44] | 304 | int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses); printf("LTL %d \n",noLoopIndex); |
---|
[38] | 305 | |
---|
[41] | 306 | |
---|
[42] | 307 | array_t *objClause = NIL(array_t); |
---|
[40] | 308 | objClause = array_alloc(int, 0); |
---|
| 309 | array_insert_last(int, objClause, noLoopIndex); |
---|
| 310 | BmcCnfInsertClause(cnfClauses, objClause); |
---|
| 311 | array_free(objClause); |
---|
[38] | 312 | |
---|
[41] | 313 | //Add Abnormal |
---|
| 314 | st_table * nodeToMvfAigTable = NIL(st_table); |
---|
| 315 | nodeToMvfAigTable = |
---|
[42] | 316 | (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); |
---|
| 317 | assert(nodeToMvfAigTable != NIL(st_table)); |
---|
[38] | 318 | |
---|
[44] | 319 | Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses); |
---|
[38] | 320 | |
---|
[42] | 321 | //loop abnormal |
---|
[41] | 322 | int aIndex; |
---|
| 323 | Ntk_Node_t * abnNode; |
---|
[42] | 324 | Dbg_ForEachAbnormal(abn,aIndex,abnNode){ |
---|
| 325 | char * nodeName = Ntk_NodeReadName(abnNode); |
---|
[44] | 326 | //set abnormal for each step |
---|
| 327 | array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex); |
---|
| 328 | int cnfIndex; |
---|
| 329 | int step; |
---|
[41] | 330 | bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex); |
---|
[44] | 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 | |
---|
[41] | 349 | //SAT procedure |
---|
[42] | 350 | //assig assig input from cex |
---|
| 351 | //TODO build cex correctly |
---|
[44] | 352 | int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel); |
---|
[42] | 353 | // Build set of FaultCandidates |
---|
| 354 | if (res == SAT_SAT) |
---|
| 355 | { |
---|
| 356 | char * realNodeName = util_strsav(nodeName); |
---|
[44] | 357 | realNodeName[strlen(nodeName)-3] = '\0'; |
---|
| 358 | printf("Real = %s\n", realNodeName); |
---|
[42] | 359 | Ntk_Node_t * realNode = Ntk_NetworkFindNodeByName(network,realNodeName); |
---|
| 360 | array_insert_last(Ntk_Node_t*,faultNodes,realNode); |
---|
| 361 | } |
---|
[38] | 362 | |
---|
[44] | 363 | arrayForEachItem(int, cnfIndexArray, step, cnfIndex){ |
---|
| 364 | int abnIndex = array_fetch(int,cnfVal,step); |
---|
| 365 | array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex); |
---|
| 366 | } |
---|
[42] | 367 | } |
---|
| 368 | |
---|
[35] | 369 | if(verbose) |
---|
| 370 | (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\ |
---|
[42] | 371 | latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable)); |
---|
| 372 | |
---|
[44] | 373 | |
---|
[42] | 374 | (void) fprintf(vis_stdout,"Number of Fault candidates %d\n", |
---|
| 375 | array_n(faultNodes)); |
---|
| 376 | (void) fprintf(vis_stdout,"gates : \n"); |
---|
[44] | 377 | |
---|
| 378 | |
---|
[42] | 379 | printNodeArray(faultNodes); |
---|
| 380 | |
---|
| 381 | |
---|
[41] | 382 | Ctlsp_FormulaArrayFree(LTLformulaArray); |
---|
[35] | 383 | BmcCnfClausesFree(cnfClauses); |
---|
| 384 | BmcOptionFree(options); |
---|
[42] | 385 | array_free(faultNodes); |
---|
[35] | 386 | return 0; |
---|
[41] | 387 | } |
---|
[44] | 388 | |
---|
[41] | 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 | { |
---|
[44] | 461 | outName = util_strsav(argv[util_optind]); |
---|
| 462 | /* create SAT Solver input file */ |
---|
[41] | 463 | options->cnfFileName= outName; |
---|
[44] | 464 | options->satInFile = options->cnfFileName; |
---|
| 465 | cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); |
---|
[41] | 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"); |
---|
[35] | 518 | (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n"); |
---|
[41] | 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"); |
---|
[35] | 524 | |
---|
[41] | 525 | BmcOptionFree(options); |
---|
| 526 | return 1; |
---|
[35] | 527 | } |
---|
[41] | 528 | |
---|
[35] | 529 | /**Function******************************************************************** |
---|
| 530 | |
---|
[27] | 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 | |
---|
[30] | 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) |
---|
[27] | 685 | { |
---|
[30] | 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 | } |
---|
[27] | 702 | |
---|
| 703 | |
---|
| 704 | /**Function******************************************************************** |
---|
| 705 | |
---|
[30] | 706 | Synopsis [Implements the transtion command.] |
---|
[27] | 707 | |
---|
[30] | 708 | CommandName [_transition] |
---|
[27] | 709 | |
---|
[30] | 710 | CommandSynopsis [compute new transition relation] |
---|
[27] | 711 | |
---|
[30] | 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> |
---|
[27] | 717 | |
---|
[30] | 718 | Command options:<p> |
---|
[27] | 719 | |
---|
[30] | 720 | <dl> |
---|
| 721 | <dt> -h |
---|
| 722 | <dd> Print the command usage. |
---|
| 723 | </dl> |
---|
[27] | 724 | |
---|
[30] | 725 | <dt> -v |
---|
| 726 | <dd> Verbose mode. |
---|
| 727 | </dl> |
---|
| 728 | ] |
---|
[27] | 729 | |
---|
[30] | 730 | SideEffects [Change the fsm] |
---|
[27] | 731 | |
---|
| 732 | ******************************************************************************/ |
---|
| 733 | |
---|
| 734 | static int |
---|
[30] | 735 | CommandTransition (Hrc_Manager_t ** hmgr, |
---|
[27] | 736 | int argc, char ** argv){ |
---|
[30] | 737 | int c; |
---|
| 738 | int verbose = 0; /* default value */ |
---|
[27] | 739 | |
---|
[30] | 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; |
---|
[27] | 753 | } |
---|
[30] | 754 | } |
---|
[27] | 755 | |
---|
[30] | 756 | if (verbose) { |
---|
| 757 | (void) fprintf(vis_stdout, "The _transition is under construction.\n"); |
---|
| 758 | } |
---|
[27] | 759 | |
---|
[30] | 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); |
---|
[27] | 774 | |
---|
| 775 | |
---|
| 776 | |
---|
[30] | 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; |
---|
[27] | 787 | } |
---|
[37] | 788 | if (verbose) |
---|
| 789 | mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout); |
---|
[27] | 790 | |
---|
[37] | 791 | |
---|
[30] | 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); |
---|
[27] | 822 | |
---|
[30] | 823 | } |
---|
| 824 | /* Replace the function for the latch */ |
---|
| 825 | Part_VertexSetFunction(vertex, newMvf); |
---|
| 826 | // printf("vertex %s changed % d\n",PartVertexReadName(vertex)); |
---|
[27] | 827 | } |
---|
| 828 | |
---|
[37] | 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)); |
---|
[30] | 834 | mdd_t * init = Fsm_FsmComputeInitialStates(fsm); |
---|
[37] | 835 | mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose, |
---|
[30] | 836 | 0,0, 0, |
---|
| 837 | 0, 0, Fsm_Rch_Default_c, |
---|
| 838 | 0,1, NIL(array_t), |
---|
| 839 | (verbose > 0), NIL(array_t)); |
---|
[37] | 840 | fsm->reachabilityInfo.initialStates = init; |
---|
| 841 | fsm->reachabilityInfo.reachableStates = reach; |
---|
[30] | 842 | if(verbose) |
---|
| 843 | Fsm_FsmReachabilityPrintResults(fsm,3, 0); |
---|
[27] | 844 | |
---|
[37] | 845 | Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY, |
---|
| 846 | (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, |
---|
| 847 | (void *) fsm); |
---|
[27] | 848 | |
---|
[30] | 849 | return 0; /* normal exit */ |
---|
[27] | 850 | |
---|
[30] | 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 */ |
---|
[27] | 856 | |
---|
| 857 | } |
---|
| 858 | |
---|
| 859 | |
---|