Index: /vis_dev/vis-2.3/src/debug/debug.c
===================================================================
--- /vis_dev/vis-2.3/src/debug/debug.c (revision 34)
+++ /vis_dev/vis-2.3/src/debug/debug.c (revision 35)
@@ -7,5 +7,5 @@
Synopsis [Debug package initialization, ending, and the command debug]
- Author [Originated from SIS.]
+ Author [Cecile B.]
Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California.
@@ -61,6 +61,8 @@
/*---------------------------------------------------------------------------*/
+static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandTransition(Hrc_Manager_t ** hmgr,int argc, char ** argv);
+static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv);
@@ -88,6 +90,8 @@
* underscore, the command will be listed under "help -a" but not "help".
*/
- Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
- Cmd_CommandAdd("_transition", CommandTransition, 0);
+ Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
+ Cmd_CommandAdd("_transition", CommandTransition, 1);
+ Cmd_CommandAdd("_sat_debug", CommandSatDebug, 0);
+ Cmd_CommandAdd("_createAbn", CommandCreateAbnormal, 1);
}
@@ -122,4 +126,279 @@
/*---------------------------------------------------------------------------*/
+
+static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int argc, char ** argv)
+{
+ Ntk_Network_t * ntk;
+ ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+ if (ntk == NIL(Ntk_Network_t)) {
+ (void) fprintf(vis_stdout, "** abn error: No network\n");
+ return 1;
+ }
+ lsGen gen;
+ Ntk_Node_t* node;
+
+ (void) fprintf(vis_stdout, "** NODE **\n");
+ Ntk_NetworkForEachNode(ntk,gen,node){
+ if(Ntk_NodeTestIsCombinational(node)){
+ if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0)
+ {
+ if(strcmp(Ntk_NodeReadName(node),"_n2")==0)
+ {
+ char * nodeName = util_strsav(Ntk_NodeReadName(node));
+ printf("%s \n", nodeName);
+ (void) fprintf(vis_stdout, "** read table\n");
+ Tbl_Table_t *table = Ntk_NodeReadTable(node);
+
+ Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
+ // Build new variables abnormal and input
+ //abn
+ char * abnName = (char *) malloc(strlen(nodeName) + 5);
+ sprintf(abnName,"abn_%s",Ntk_NodeReadName(node));
+ Var_Variable_t * abn = Var_VariableAlloc(NIL(Hrc_Node_t),abnName);
+ Ntk_Node_t * newNode = Ntk_NodeCreateInNetwork(ntk, abnName,abn);
+ Ntk_NodeDeclareAsPrimaryInput(newNode);
+ //new free inputs
+ char * iName = (char *) malloc(strlen(nodeName) + 3);
+ sprintf(iName,"i_%s",Ntk_NodeReadName(node));
+ Var_Variable_t * i = Var_VariableAlloc(NIL(Hrc_Node_t),iName);
+ Ntk_Node_t * newNode2 = Ntk_NodeCreateInNetwork(ntk, iName, i);
+ Ntk_NodeDeclareAsPrimaryInput(newNode2);
+ //Add in the table
+ Tbl_TableAddColumn(table,abn,0);
+ int abnIndex = Tbl_TableReadVarIndex(table, abn, 0);
+ Tbl_TableAddColumn(table,i,0);
+ int iIndex = Tbl_TableReadVarIndex(table, i, 0);
+
+ //For each row already there in the table
+ int rowNum;
+ for(rowNum = 0; rowNum < Tbl_TableReadNumRows(table);rowNum++){
+ Tbl_Entry_t *abnEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+ Tbl_EntrySetValue(abnEntry,0,0);
+ Tbl_TableSetEntry(table, abnEntry, rowNum, abnIndex, 0);
+ Tbl_Entry_t *iEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+ Tbl_EntrySetValue(iEntry,0,1);
+ Tbl_TableSetEntry(table, iEntry, rowNum, iIndex, 0);
+ }
+ //the new row
+ int r = Tbl_TableAddRow(table);
+
+ int colNum;
+ for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) {
+ Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+ printf("entry : colNum %d \n",colNum);
+ if(colNum == abnIndex || colNum == iIndex)
+ Tbl_EntrySetValue(entry,1,1);
+ else
+ Tbl_EntrySetValue(entry,0,1);
+ Tbl_TableSetEntry(table, entry, r, colNum, 0);
+ }
+ for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){
+ Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
+ Tbl_EntrySetValue(entry,1,1);
+ Tbl_TableSetEntry(table, entry, r, colNum, 1);
+ }
+ printf("---------------\n");
+ Tbl_TablePrintStats(table, vis_stdout);
+ Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
+ free(abnName);
+ free(iName);
+ }
+ }
+ }
+ }
+ // TODO
+ //Remplacer l'ancien network par le nouveau
+}
+/**Function********************************************************************
+
+ Synopsis [Implements the _sat_debug command.]
+
+ CommandName [_sat_debug]
+
+ CommandSynopsis [locate faulty candidates]
+
+ CommandArguments [\[-h\] \[-v\]]
+
+ CommandDescription [This command compute the fault candidates of a given
+ properties.
+
+ Command options:
+
+
+ - -h
+
- Print the command usage.
+
+
+ -v
+ Verbose mode.
+
+ ]
+
+ SideEffects []
+
+******************************************************************************/
+
+
+static int
+CommandSatDebug(
+Hrc_Manager_t ** hmgr,
+int argc,
+char ** argv){
+int c,i;
+int verbose = 0; /* default value */
+BmcOption_t *options = BmcOptionAlloc();
+Ntk_Network_t * network;
+bAig_Manager_t *manager;
+
+
+/*
+ * Parse command line options.
+ */
+util_getopt_reset();
+while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
+ switch(c) {
+ case 'v':
+ verbose = 1;
+ options->verbosityLevel = verbose;
+ break;
+ case 'h':
+ goto usage;
+ case 'm':
+ for (i = 0; i < strlen(util_optarg); i++) {
+ if (!isdigit((int)util_optarg[i])) {
+ goto usage;
+ }
+ }
+ options->minK = atoi(util_optarg);
+ break;
+ case 'k':
+ for (i = 0; i < strlen(util_optarg); i++) {
+ if (!isdigit((int)util_optarg[i])) {
+ goto usage;
+ }
+ }
+ options->maxK = atoi(util_optarg);
+ break;
+ case 'o':
+ options->cnfFileName = util_strsav(util_optarg);
+ break;
+
+ default:
+ goto usage;
+ }
+}
+ if (options->minK > options->maxK){
+ (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");
+ goto usage;
+ }
+
+if (verbose) {
+ (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
+}
+ /* create SAT Solver input file */
+ if (options->cnfFileName == NIL(char)) {
+ options->satInFile = BmcCreateTmpFile();
+}
+ else {
+ options->satInFile = options->cnfFileName;
+ }
+
+/* create SAT Solver output file */
+options->satOutFile = BmcCreateTmpFile();
+if (options->satOutFile == NIL(char)){
+ BmcOptionFree(options);
+ (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
+ return 1;
+}
+
+options->verbosityLevel = 1;
+//options->satSolver
+//options->clauses
+
+ /*
+ * Read the network
+ */
+ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+ if (network == NIL(Ntk_Network_t)) {
+ (void) fprintf(vis_stdout, "** bmc error: No network\n");
+ BmcOptionFree(options);
+ return 1;
+ }
+ manager = Ntk_NetworkReadMAigManager(network);
+ if (manager == NIL(mAig_Manager_t)) {
+ (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
+ BmcOptionFree(options);
+ return 1;
+ }
+ /*
+ We need the bdd when building the transition relation of the automaton
+ */
+ if(options->inductiveStep !=0){
+ Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
+
+ designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
+ if (designFsm == NIL(Fsm_Fsm_t)) {
+ (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
+ return 1;
+ }
+ }
+
+ /*
+ Compute the cone of influence
+ here a list of state variables (latches)
+ */
+ st_table *CoiTable = generateAllLatches(network);
+ /*
+ Generate clauses for each time frame. This is the old way of generating
+ clauses in BMC.
+ */
+ st_table *nodeToMvfAigTable = NIL(st_table); /* node to mvfAig */
+ BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
+ FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
+ /*
+ nodeToMvfAigTable maps each node to its multi-function And/Inv graph
+ */
+ nodeToMvfAigTable =
+ (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
+ assert(nodeToMvfAigTable != NIL(st_table));
+
+ if(verbose)
+ {
+ (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
+ printLatch(nodeToMvfAigTable);
+ (void) fprintf(vis_stdout, "------ COI ----\n");
+ printLatch(CoiTable);
+ (void) fprintf(vis_stdout, "--------------------------\n");
+ }
+ /*
+ Create a clause database
+ */
+ cnfClauses = BmcCnfClausesAlloc();
+ /*
+ Generate clauses for an initialized path of length k
+ */
+ BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
+ cnfClauses, nodeToMvfAigTable, CoiTable);
+ if(verbose)
+ (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
+ latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
+
+
+ BmcWriteClauses(manager, cnfFile, cnfClauses, options);
+fclose(cnfFile);
+BmcCnfClausesFree(cnfClauses);
+BmcOptionFree(options);
+return 0;
+ usage:
+ (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
+ minimum length] [-o cnf_file]\n");
+ (void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
+ (void) fprintf(vis_stderr, " -v\t\tverbose\n");
+ (void) fprintf(vis_stderr, " -m \tminimum length of counterexample to be checked (default is 0)\n");
+ (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n");
+ (void) fprintf(vis_stderr, " -o contains CNF of the counterexample\n");
+ return 1; /* error exit */
+
+}
/**Function********************************************************************
Index: /vis_dev/vis-2.3/src/debug/debug.h
===================================================================
--- /vis_dev/vis-2.3/src/debug/debug.h (revision 34)
+++ /vis_dev/vis-2.3/src/debug/debug.h (revision 35)
@@ -83,5 +83,6 @@
/*---------------------------------------------------------------------------*/
-
+void printLatch(st_table* CoiTable);
+st_table * generateAllLatches(Ntk_Network_t * ntk);
void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f);
EXTERN void Debug_Init(void);
Index: /vis_dev/vis-2.3/src/debug/debug.make
===================================================================
--- /vis_dev/vis-2.3/src/debug/debug.make (revision 34)
+++ /vis_dev/vis-2.3/src/debug/debug.make (revision 35)
@@ -1,3 +1,3 @@
-CSRC += debug.c
+CSRC += debug.c debugUtilities.c
HEADERS += debug.h debugInt.h
Index: /vis_dev/vis-2.3/src/debug/debugUtilities.c
===================================================================
--- /vis_dev/vis-2.3/src/debug/debugUtilities.c (revision 34)
+++ /vis_dev/vis-2.3/src/debug/debugUtilities.c (revision 35)
@@ -1,3 +1,30 @@
-#include "Debug.h"
+#include "debug.h"
+void printLatch(st_table* CoiTable)
+{
+// COI contents
+ printf("*** COI ***\n");
+ st_generator *stGen;
+ Ntk_Node_t * latch;
+ st_foreach_item(CoiTable, stGen, &latch, NULL) {
+ printf("%s\n",Ntk_NodeReadName(latch));
+ }
+}
+
+
+st_table * generateAllLatches(Ntk_Network_t * ntk)
+{
+ st_table *CoiTable = st_init_table(st_ptrcmp, st_ptrhash);
+ lsGen gen ;
+ Ntk_Node_t *node;
+
+ Ntk_NetworkForEachNode(ntk,gen, node){
+ if (Ntk_NodeTestIsLatch(node)){
+ st_insert(CoiTable, (char *) node, Ntk_NodeReadName(node));
+ }
+ }
+ return CoiTable;
+
+}
+
void mdd_GetState_Values(