#include "bmcInt.h"#include "sat.h"#include "baig.h"
Include dependency graph for bmcUtil.c:
Go to the source code of this file.
Defines | |
| #define | MAX_LENGTH 320 |
Functions | |
| static int | StringCheckIsInteger (char *string, int *value) |
| static int | nameCompare (const void *name1, const void *name2) |
| static void | printValue (mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue) |
| static void | printValueAiger (mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue) |
| static void | printValueAigerInputs (mAig_Manager_t *manager, Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *varNames, st_table *resultTable, int state, int *prevValue) |
| mdd_t * | Bmc_ComputeCloseCube (mdd_t *states, mdd_t *target, int *dist, Fsm_Fsm_t *modelFsm) |
| MvfAig_Function_t * | Bmc_NodeBuildMVF (Ntk_Network_t *network, Ntk_Node_t *node) |
| MvfAig_Function_t * | Bmc_ReadMvfAig (Ntk_Node_t *node, st_table *nodeToMvfAigTable) |
| mdd_t * | BmcFsmEvaluateX (Fsm_Fsm_t *modelFsm, mdd_t *targetMdd) |
| mdd_t * | BmcComputeCloseCube (mdd_t *aSet, mdd_t *target, int *dist, array_t *Support, mdd_manager *mddMgr) |
| mAigEdge_t | BmcCreateMaigOfInitialStates (Ntk_Network_t *network, st_table *nodeToMvfAigTable, st_table *CoiTable) |
| mAigEdge_t | BmcCreateMaigOfPropFormula (Ntk_Network_t *network, mAig_Manager_t *manager, Ctlsp_Formula_t *formula) |
| mdd_t * | BmcCreateMddOfSafetyProperty (Fsm_Fsm_t *fsm, Ctlsp_Formula_t *formula) |
| int | BmcGenerateCnfFormulaForAigFunction (bAig_Manager_t *manager, bAigEdge_t node, int k, BmcCnfClauses_t *cnfClauses) |
| int | BmcGenerateCnfFormulaForBdd (bdd_t *bddFunction, int k, BmcCnfClauses_t *cnfClauses) |
| int | BmcGenerateCnfFormulaForBddOffSet (bdd_t *bddFunction, int k, BmcCnfClauses_t *cnfClauses) |
| void | BmcGenerateClausesFromStateTostate (bAig_Manager_t *manager, bAigEdge_t *fromAigArray, bAigEdge_t *toAigArray, int mvfSize, int fromState, int toState, BmcCnfClauses_t *cnfClauses, int outIndex) |
| void | BmcWriteClauses (mAig_Manager_t *maigManager, FILE *cnfFile, BmcCnfClauses_t *cnfClauses, BmcOption_t *options) |
| array_t * | BmcCheckSAT (BmcOption_t *options) |
| array_t * | BmcCallCirCUs (BmcOption_t *options) |
| array_t * | BmcCallCusp (BmcOption_t *options) |
| void | BmcPrintCounterExample (Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause) |
| void | BmcPrintCounterExampleAiger (Ntk_Network_t *network, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause) |
| void | BmcAutPrintCounterExample (Ntk_Network_t *network, Ltl_Automaton_t *automaton, st_table *nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses, array_t *result, int length, st_table *CoiTable, BmcOption_t *options, array_t *loopClause) |
| void | BmcCnfGenerateClausesForPath (Ntk_Network_t *network, int from, int to, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) |
| void | BmcCnfGenerateClausesForLoopFreePath (Ntk_Network_t *network, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) |
| void | BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates (Ntk_Network_t *network, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) |
| void | BmcCnfGenerateClausesForLoopToAnyPreviouseStates (Ntk_Network_t *network, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) |
| void | BmcCnfGenerateClausesFromStateToState (Ntk_Network_t *network, int from, int to, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable, int loop) |
| void | BmcCnfGenerateClausesForAND (int a, int b, int c, BmcCnfClauses_t *cnfClauses) |
| void | BmcCnfGenerateClausesForOR (int a, int b, int c, BmcCnfClauses_t *cnfClauses) |
| BmcCnfClauses_t * | BmcCnfClausesAlloc (void) |
| void | BmcCnfClausesFree (BmcCnfClauses_t *cnfClauses) |
| BmcCnfStates_t * | BmcCnfClausesFreeze (BmcCnfClauses_t *cnfClauses) |
| void | BmcCnfClausesUnFreeze (BmcCnfClauses_t *cnfClauses, BmcCnfStates_t *state) |
| void | BmcCnfClausesRestore (BmcCnfClauses_t *cnfClauses, BmcCnfStates_t *state) |
| void | BmcCnfInsertClause (BmcCnfClauses_t *cnfClauses, array_t *clause) |
| void | BmcAddEmptyClause (BmcCnfClauses_t *cnfClauses) |
| int | BmcCnfReadOrInsertNode (BmcCnfClauses_t *cnfClauses, nameType_t *nodeName, int state, int *nodeIndex) |
| void | BmcGetCoiForLtlFormula (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable) |
| void | BmcGetCoiForLtlFormulaRecursive (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited) |
| void | BmcGetCoiForNtkNode (Ntk_Node_t *node, st_table *CoiTable, st_table *visited) |
| mdd_t * | BmcModelCheckAtomicFormula (Fsm_Fsm_t *modelFsm, Ctlsp_Formula_t *ctlFormula) |
| array_t * | BmcReadFairnessConstraints (FILE *fp) |
| int | BmcGetCnfVarIndexForBddNode (bdd_manager *bddManager, bdd_node *node, int state, BmcCnfClauses_t *cnfClauses) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: bmcUtil.c,v 1.82 2010/04/10 04:07:06 fabio Exp $" |
Define Documentation
Function Documentation
| mdd_t* Bmc_ComputeCloseCube | ( | mdd_t * | states, |
| mdd_t * | target, | ||
| int * | dist, | ||
| Fsm_Fsm_t * | modelFsm | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Compute cube that is close to target states.]
SideEffects []
Definition at line 71 of file bmcUtil.c.
{
array_t *PSVars = Fsm_FsmReadPresentStateVars( modelFsm );
mdd_manager *mddMgr = Ntk_NetworkReadMddManager( Fsm_FsmReadNetwork( modelFsm ) );
mdd_t *result = BmcComputeCloseCube( states, target, dist, PSVars, mddMgr );
return result;
}
Here is the call graph for this function:
| MvfAig_Function_t* Bmc_NodeBuildMVF | ( | Ntk_Network_t * | network, |
| Ntk_Node_t * | node | ||
| ) |
Function********************************************************************
Synopsis [Build multi-valued function for a given node.]
SideEffects [The mvf of this node is a function of combinational input nodes.]
Definition at line 93 of file bmcUtil.c.
{
MvfAig_Function_t * MvfAig;
lsGen tmpGen;
Ntk_Node_t *tmpNode;
array_t *mvfArray;
array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0);
st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
array_insert_last(Ntk_Node_t *, tmpRoots, node);
Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
st_insert(tmpLeaves, (char *) tmpNode, (char *) ntmaig_UNUSED);
}
mvfArray = ntmaig_NetworkBuildMvfAigs(network, tmpRoots, tmpLeaves);
MvfAig = array_fetch(MvfAig_Function_t *, mvfArray, 0);
array_free(tmpRoots);
st_free_table(tmpLeaves);
array_free(mvfArray);
return MvfAig;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| MvfAig_Function_t* Bmc_ReadMvfAig | ( | Ntk_Node_t * | node, |
| st_table * | nodeToMvfAigTable | ||
| ) |
Function********************************************************************
Synopsis [Returns MvfAig corresponding to a node; returns NIL if node not in table.]
SideEffects [None]
Definition at line 127 of file bmcUtil.c.
{
MvfAig_Function_t *result;
if (st_lookup(nodeToMvfAigTable, node, &result)){
return result;
}
return NIL(MvfAig_Function_t);
}
Here is the caller graph for this function:
| void BmcAddEmptyClause | ( | BmcCnfClauses_t * | cnfClauses | ) |
| void BmcAutPrintCounterExample | ( | Ntk_Network_t * | network, |
| Ltl_Automaton_t * | automaton, | ||
| st_table * | nodeToMvfAigTable, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| array_t * | result, | ||
| int | length, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options, | ||
| array_t * | loopClause | ||
| ) |
Function********************************************************************
Synopsis [Print CounterExample.]
SideEffects [Print a counterexample that was returned from the SAT solver in term of an array of integer "result". The counterexample starts from state 0 and of lenght eqaual to "length". If loopClause is not empty, this function print a loopback from the last state to a state in loopClause that exist in "result".]
Definition at line 1650 of file bmcUtil.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
lsGen gen;
st_generator *stGen;
Ntk_Node_t *node;
int k;
array_t *latches = array_alloc(int, 0);
int *prevValueLatches;
array_t *inputs = array_alloc(int, 0);
int *prevValueInputs;
int tmp;
int loop;
st_table *resultTable = st_init_table(st_numcmp, st_numhash);
/*
Initialize resultTable from the result to speed up the search in the result array.
*/
for(k=0; k< array_n(result); k++){
st_insert(resultTable, (char *) (long) array_fetch(int, result, k), (char *) 0);
}
/* sort latches by name */
st_foreach_item(CoiTable, stGen, &node, NULL) {
array_insert_last(char*, latches, Ntk_NodeReadName(node));
}
array_sort(latches, nameCompare);
/*
Use to store the last value of each latch. If the current value of a latch
differs from its corresponding value in this array, we will print the new values.
*/
prevValueLatches = ALLOC(int, array_n(latches));
prevValueInputs = 0;
if(options->printInputs == TRUE){
/* sort inputs by name */
Ntk_NetworkForEachInput(network, gen, node){
array_insert_last(char*, inputs, Ntk_NodeReadName(node));
}
array_sort(inputs, nameCompare);
prevValueInputs = ALLOC(int, array_n(inputs));
}
loop = -1; /* no loop back */
if(loopClause != NIL(array_t)){
for(k=0; k < array_n(loopClause); k++){
/* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
loop = k;
break;
}
}
}
/*
Ntk_NetworkForEachPrimaryOutput(network, gen, node){
array_insert_last(char*, outputs, Ntk_NodeReadName(node));
}
array_sort(outputs, nameCompare);
*/
for (k=0; k<= length; k++){
if (k == 0){
(void) fprintf(vis_stdout, "\n--State %d:\n", k);
} else {
(void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
}
/*
Print the current values of the latches if they are different form their
previous values.
*/
printValue(manager, network, nodeToMvfAigTable, cnfClauses,
latches, resultTable, k, prevValueLatches);
{
lsGen lsGen;
vertex_t *vtx;
Ltl_AutomatonNode_t *state;
int stateIndex;
bdd_node *node;
int is_complemented;
foreach_vertex(automaton->G, lsGen, vtx) {
state = (Ltl_AutomatonNode_t *) vtx->user_data;
node = bdd_get_node(state->Encode, &is_complemented);
stateIndex = state->cnfIndex[k];
if (st_lookup_int(resultTable, (char *)(long)stateIndex, &tmp)){
(void) fprintf(vis_stdout,"n%d \n", state->index);
}
}
}
#if 0
(void) fprintf(vis_stdout, "--Primary output:\n");
printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
#endif
if((options->printInputs == TRUE) && (k !=0)) {
(void) fprintf(vis_stdout, "--On input:\n");
printValue(manager, network, nodeToMvfAigTable, cnfClauses,
inputs, resultTable, k-1, prevValueInputs);
}
} /* for k loop */
if(loop != -1){
(void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
printValue(manager, network, nodeToMvfAigTable, cnfClauses,
latches, resultTable, loop, prevValueLatches);
if((options->printInputs == TRUE)) {
(void) fprintf(vis_stdout, "--On input:\n");
printValue(manager, network, nodeToMvfAigTable, cnfClauses,
inputs, resultTable, length, prevValueInputs);
}
}
array_free(latches);
FREE(prevValueLatches);
if(options->printInputs == TRUE){
array_free(inputs);
FREE(prevValueInputs);
}
st_free_table(resultTable);
return;
} /* BmcPrintCounterExample() */
Here is the call graph for this function:
| array_t* BmcCallCirCUs | ( | BmcOption_t * | options | ) |
Function********************************************************************
Synopsis [Check the satisfiability of CNF formula written in file]
Description [Run CirCUs on input file]
SideEffects []
Definition at line 1158 of file bmcUtil.c.
{
satOption_t *satOption;
array_t *result = NIL(array_t);
satManager_t *cm;
int maxSize;
satOption = sat_InitOption();
satOption->verbose = options->verbosityLevel;
satOption->verbose = 0;
cm = sat_InitManager(0);
cm->comment = ALLOC(char, 2);
cm->comment[0] = ' ';
cm->comment[1] = '\0';
cm->stdOut = stdout;
cm->stdErr = stderr;
cm->option = satOption;
cm->each = sat_InitStatistics();
cm->unitLits = sat_ArrayAlloc(16);
cm->pureLits = sat_ArrayAlloc(16);
maxSize = 10000 << (bAigNodeSize-4);
cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
cm->maxNodesArraySize = maxSize;
cm->nodesArraySize = bAigNodeSize;
sat_AllocLiteralsDB(cm);
sat_ReadCNF(cm, options->satInFile);
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void)fprintf(vis_stdout,"Calling SAT solver (CirCUs) ...");
(void) fflush(vis_stdout);
}
sat_Main(cm);
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout," done ");
(void) fprintf(vis_stdout, "(%g s)\n", cm->each->satTime);
}
if(cm->status == SAT_UNSAT) {
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
}
fflush(cm->stdOut);
} else if(cm->status == SAT_SAT) {
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
}
if (options->verbosityLevel == BmcVerbosityMax_c){
sat_ReportStatistics(cm, cm->each);
}
fflush(cm->stdOut);
result = array_alloc(int, 0);
{
int i, size, value;
size = cm->initNumVariables * bAigNodeSize;
for(i=bAigNodeSize; i<=size; i+=bAigNodeSize) {
value = SATvalue(i);
if(value == 1) {
array_insert_last(int, result, SATnodeID(i));
}
else if(value == 0) {
array_insert_last(int, result, -(SATnodeID(i)));
}
}
}
}
//Bing: To avoid SEVERE memory leakage
FREE(cm->nodesArray);
sat_FreeManager(cm);
return result;
} /* BmcCallCirCUs */
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* BmcCallCusp | ( | BmcOption_t * | options | ) |
Function********************************************************************
Synopsis [Check the satisfiability of CNF formula written in file]
Description [Run external solver on input file]
SideEffects []
Definition at line 1249 of file bmcUtil.c.
{
FILE *fp;
static char parseBuffer[1024];
int satStatus;
char line[MAX_LENGTH];
int num = 0;
array_t *result = NIL(array_t);
char *tmpStr, *tmpStr1, *tmpStr2;
long solverStart;
int satTimeOutPeriod = 0;
strcpy(parseBuffer,"cusp -distill -velim -cnf ");
options->satSolverError = FALSE; /* assume no error*/
if (options->timeOutPeriod > 0) {
/* Compute the residual CPU time and subtract a little time to
give vis a chance to clean up before its own time out expires.
*/
satTimeOutPeriod = options->timeOutPeriod - 1 -
(util_cpu_ctime() - options->startTime) / 1000;
if (satTimeOutPeriod <= 0){ /* no time left to run SAT solver*/
options->satSolverError=TRUE;
return NIL(array_t);
}
tmpStr2 = util_inttostr(satTimeOutPeriod);
tmpStr1 = util_strcat3(options->satInFile," -t ", tmpStr2);
tmpStr = util_strcat3(tmpStr1, " >", options->satOutFile);
FREE(tmpStr1);
FREE(tmpStr2);
} else {
tmpStr = util_strcat3(options->satInFile, " >", options->satOutFile);
}
strcat(parseBuffer, tmpStr);
FREE(tmpStr);
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void)fprintf(vis_stdout,"Calling SAT solver (cusp) ...");
(void) fflush(vis_stdout);
solverStart = util_cpu_ctime();
} else { /* to remove uninitialized variables warning */
solverStart = 0;
}
/* Call Sat Solver*/
satStatus = system(parseBuffer);
if (satStatus != 0){
(void) fprintf(vis_stderr, "Can't run cusp. It may not be in your path. Status = %d\n", satStatus);
options->satSolverError = TRUE;
return NIL(array_t);
}
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout," done ");
(void) fprintf(vis_stdout, "(%g s)\n",
(double) (util_cpu_ctime() - solverStart)/1000.0);
}
fp = Cmd_FileOpen(options->satOutFile, "r", NIL(char *), 0);
if (fp == NIL(FILE)) {
(void) fprintf(vis_stderr, "** bmc error: Cannot open the file %s\n",
options->satOutFile);
options->satSolverError = TRUE;
return NIL(array_t);
}
/* Skip the lines until the result */
while(1) {
if (fgets(line, MAX_LENGTH - 1, fp) == NULL) break;
if(strstr(line,"UNSATISFIABLE") ||
strstr(line,"SATISFIABLE") ||
strstr(line,"MEMOUT") ||
strstr(line,"TIMEOUT"))
break;
}
if(strstr(line,"UNSATISFIABLE") != NIL(char)) {
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "# SAT: Counterexample not found\n");
}
} else if(strstr(line,"SATISFIABLE") != NIL(char)) {
if (options->verbosityLevel != BmcVerbosityNone_c){
(void) fprintf(vis_stdout, "# SAT: Counterexample found\n");
}
/* Skip the initial v of the result line */
result = array_alloc(int, 0);
while (fgets(line, MAX_LENGTH - 1, fp) != NULL) {
char *word;
if (line[0] != 'v') {
(void) fprintf(vis_stderr,
"** bmc error: Cannot find assignment in file %s\n",
options->satOutFile);
options->satSolverError = TRUE;
return NIL(array_t);
}
word = strtok(&(line[1])," \n");
while (word != NIL(char)) {
num = atoi(word);
if (num == 0) break;
array_insert_last(int, result, num);
word = strtok(NIL(char)," \n");
}
if (num == 0) break;
}
} else if(strstr(line,"MEMOUT") != NIL(char)) {
(void) fprintf(vis_stdout,"# SAT: SAT Solver Memory out\n");
options->satSolverError = TRUE;
} else if(strstr(line,"TIMEOUT") != NIL(char)) {
(void) fprintf(vis_stdout,
"# SAT: SAT Solver Time out occurred after %d seconds.\n",
satTimeOutPeriod);
options->satSolverError = TRUE;
} else {
(void) fprintf(vis_stdout, "# SAT: SAT Solver failed, try again\n");
options->satSolverError = TRUE;
}
(void) fflush(vis_stdout);
(void) fclose(fp);
return result;
} /* BmcCallCusp */
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* BmcCheckSAT | ( | BmcOption_t * | options | ) |
Function********************************************************************
Synopsis [Check the satisfiability of CNF formula written in file]
Description [Run SAT solver on input file]
SideEffects []
Definition at line 1115 of file bmcUtil.c.
{
array_t *result = NIL(array_t);
if(options->satSolver == cusp){
result = BmcCallCusp(options);
}
if(options->satSolver == CirCUs){
result = BmcCallCirCUs(options);
}
/* Adjust alarm if timeout in effect. This is necessary because the
* alarm may have gone off while the SAT solver is running. Since
* the CPU time of a child process is charged to the parent only when
* the child terminates, the SIGALRM handler assumes that more time
* is left than it is in reality. We could do this adjustment right
* after calling the SAT solver, but we prefer to give ourselves the
* extra time to report the result even if this means using more time
* than we are allotted.
*/
if (options->timeOutPeriod > 0) {
int residualTime = options->timeOutPeriod -
(util_cpu_ctime() - options->startTime) / 1000;
/* Make sure we do not cancel the alarm if no time is left. */
if (residualTime <= 0) {
residualTime = 1;
}
(void) alarm(residualTime);
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| BmcCnfClauses_t* BmcCnfClausesAlloc | ( | void | ) |
Function********************************************************************
Synopsis [Alloc Memory for BmcCnfClauses_t]
SideEffects []
SeeAlso []
Definition at line 2267 of file bmcUtil.c.
{
BmcCnfClauses_t *result = ALLOC(BmcCnfClauses_t, 1);
if (!result){
return result;
}
result->clauseArray = array_alloc(int, 0);
result->cnfIndexTable = st_init_table(strcmp, st_strhash);
result->freezedKeys = array_alloc(nameType_t *, 0);
result->nextIndex = 0;
result->noOfClauses = 0;
result->cnfGlobalIndex = 1;
result->emptyClause = FALSE;
result->freezed = FALSE;
return result;
} /*BmcCnfClausesAlloc()*/
Here is the caller graph for this function:
| void BmcCnfClausesFree | ( | BmcCnfClauses_t * | cnfClauses | ) |
Function********************************************************************
Synopsis [Free Memory for BmcCnfClauses_t]
SideEffects []
SeeAlso []
Definition at line 2296 of file bmcUtil.c.
{
st_generator *stGen;
char *name;
int cnfIndex;
array_free(cnfClauses->clauseArray);
array_free(cnfClauses->freezedKeys);
if (cnfClauses->cnfIndexTable != NIL(st_table)){
st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, (char **) &name, &cnfIndex) {
FREE(name);
}
st_free_table(cnfClauses->cnfIndexTable);
}
FREE(cnfClauses);
cnfClauses = NIL(BmcCnfClauses_t);
} /* BmcCnfClausesFree() */
Here is the caller graph for this function:
| BmcCnfStates_t* BmcCnfClausesFreeze | ( | BmcCnfClauses_t * | cnfClauses | ) |
Function********************************************************************
Synopsis [Freeze the current state of CNF]
Description [The current state of CNF is stored in the structure BmcCnfStates_t. This information may use later to store CNF to this state by calling BmcCnfClausesRestore().]
SideEffects []
SeeAlso [BmcCnfClausesRestore() BmcCnfClausesUnFreeze() ]
Definition at line 2329 of file bmcUtil.c.
{
BmcCnfStates_t *state = ALLOC(BmcCnfStates_t, 1);
state->nextIndex = cnfClauses->nextIndex;
state->noOfClauses = cnfClauses->noOfClauses;
state->cnfGlobalIndex = cnfClauses->cnfGlobalIndex;
/* This variable is used when deleting any new entries in cnfClauses->freezedKeys
that will be added after CNF is freezed.*/
state->freezedKeySize = array_n(cnfClauses->freezedKeys);
state->emptyClause = cnfClauses->emptyClause;
state->freezed = cnfClauses->freezed;
cnfClauses->freezed = TRUE;
return state;
} /* mcCnfClausesFreeze() */
Here is the caller graph for this function:
| void BmcCnfClausesRestore | ( | BmcCnfClauses_t * | cnfClauses, |
| BmcCnfStates_t * | state | ||
| ) |
Function********************************************************************
Synopsis [Restore the CNF to its previouse state]
Description [Restore the CNF to its previouse state that CNF was when BmcCnfClausesFreeze() was last called]
SideEffects []
SeeAlso []
Definition at line 2387 of file bmcUtil.c.
{
int i, index;
nameType_t *key;
cnfClauses->nextIndex = state->nextIndex;
cnfClauses->noOfClauses = state->noOfClauses;
cnfClauses->cnfGlobalIndex = state->cnfGlobalIndex;
cnfClauses->emptyClause = state->emptyClause;
cnfClauses->freezed = state->freezed;
if (array_n(cnfClauses->freezedKeys) != 0){
int freezedKeySize = array_n(cnfClauses->freezedKeys);
for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){
key = array_fetch_last(nameType_t *, cnfClauses->freezedKeys);
if (st_delete_int(cnfClauses->cnfIndexTable, &key, &index)){
FREE(key);
}
(cnfClauses->freezedKeys)->num--;
}
}
} /* BmcCnfClausesRestore() */
Here is the caller graph for this function:
| void BmcCnfClausesUnFreeze | ( | BmcCnfClauses_t * | cnfClauses, |
| BmcCnfStates_t * | state | ||
| ) |
Function********************************************************************
Synopsis [Unfreeze CNF]
Description [Keeps the current state of CNF]
SideEffects []
SeeAlso []
Definition at line 2359 of file bmcUtil.c.
{
int i;
cnfClauses->freezed = FALSE;
if (array_n(cnfClauses->freezedKeys) != 0){
int freezedKeySize = array_n(cnfClauses->freezedKeys);
for (i=0; i< (freezedKeySize-state->freezedKeySize); i++){
(cnfClauses->freezedKeys)->num--;
}
}
} /* BmcCnfClausesUnFreeze() */
Here is the caller graph for this function:
| void BmcCnfGenerateClausesForAND | ( | int | a, |
| int | b, | ||
| int | c, | ||
| BmcCnfClauses_t * | cnfClauses | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF clauses for the AND gate]
Description []
SideEffects []
SeeAlso []
Definition at line 2191 of file bmcUtil.c.
{
array_t *tmpClause;
tmpClause = array_alloc(int, 3);
array_insert(int, tmpClause, 0, -a);
array_insert(int, tmpClause, 1, -b);
array_insert(int, tmpClause, 2, c);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_free(tmpClause);
tmpClause = array_alloc(int, 2);
array_insert(int, tmpClause, 0, a);
array_insert(int, tmpClause, 1, -c);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_insert(int, tmpClause, 0, b);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_free(tmpClause);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCnfGenerateClausesForLoopFreePath | ( | Ntk_Network_t * | network, |
| int | fromState, | ||
| int | toState, | ||
| int | initialState, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF formula for a loop-free path]
Description [This function generates CNF formula for a loop-free path from state fromState to state toState. A loop free path is a path from a state S0 to state Sn such that every state in the path is distinct. i.e for all states in the path Si != Sj for 0<= i < j <= n.
The initialState value may be either BMC_INITIAL_STATES to generate the clause for the intial states. BMC_NO_INITIAL_STATES otherwise. ]
SideEffects []
SeeAlso []
Definition at line 1908 of file bmcUtil.c.
{
int state;
/*
Generate clauses for a path from fromState to toState.
*/
BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable);
/*
Restrict the above path to be loop-free path.
*/
/*
for(state=0; state< toState; state++){
*/
/*
Don't include the last state because we know it is not equal any of the previous states.
The property fails at this state, and true at all other states.
*/
/*
for(state=1; state < toState; state++){
*/
for(state= fromState + 1; state <= toState; state++){
BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates(network, fromState, state, cnfClauses, nodeToMvfAigTable, CoiTable);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCnfGenerateClausesForLoopToAnyPreviouseStates | ( | Ntk_Network_t * | network, |
| int | fromState, | ||
| int | toState, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Generate Clauses for last state equal to any of the previouse states]
Description [ Change it! Generate Clauses for no loop from last state (toState) to any of the previous states starting from fromState. It generates the CNF clauses such that the last state of the path is not equal to any of the path previous states. ]
SideEffects []
SeeAlso []
Definition at line 2042 of file bmcUtil.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_generator *stGen;
Ntk_Node_t *latch;
MvfAig_Function_t *latchMvfAig;
bAigEdge_t *latchBAig;
array_t *orClause;
int lastIndex, prevIndex, andIndex1, andIndex2;
int i, k, mvfSize;
/*
Generates the clauses to check if the toState is not equal to any previouse states starting
from fromState.
Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses
for the formula ( ai != aj + bi != bj).
*/
for(k=fromState; k < toState; k++){
orClause = array_alloc(int,0);
st_foreach_item(CoiTable, stGen, &latch, NULL) {
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(latchMvfAig);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
}
for (i=0; i< mvfSize; i++){
prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k ,cnfClauses);
lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);
andIndex1 = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesForAND(prevIndex, lastIndex, andIndex1, cnfClauses);
andIndex2 = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesForAND(-prevIndex, -lastIndex, andIndex2, cnfClauses);
array_insert_last(int, orClause, andIndex1);
array_insert_last(int, orClause, andIndex2);
}
FREE(latchBAig);
}/* For each latch loop*/
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
} /* foreach k*/
return;
}
Here is the call graph for this function:
| void BmcCnfGenerateClausesForNoLoopToAnyPreviouseStates | ( | Ntk_Network_t * | network, |
| int | fromState, | ||
| int | toState, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Generate Clauses for no loop from last state to any of the previouse states]
Description [Generate Clauses for no loop from last state (toState) to any of the previous states starting from fromState. It generates the CNF clauses such that the last state of the path is not equal to any of the path previous states. ]
SideEffects []
SeeAlso []
Definition at line 1961 of file bmcUtil.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_generator *stGen;
Ntk_Node_t *latch;
MvfAig_Function_t *latchMvfAig;
bAigEdge_t *latchBAig;
array_t *orClause;
int lastIndex, prevIndex, andIndex1, andIndex2;
int i, k, mvfSize;
/*
Generates the clauses to check if the toState is not equal to any previouse states starting
from fromState.
Assume there are two state varaibles a and b. To check if Si != Sj, we must generate clauses
for the formula ( ai != aj + bi != bj).
*/
for(k=fromState; k < toState; k++){
orClause = array_alloc(int,0);
st_foreach_item(CoiTable, stGen, &latch, NULL) {
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(latchMvfAig);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
}
for (i=0; i< mvfSize; i++){
prevIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k ,cnfClauses);
lastIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);
andIndex1 = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesForAND(prevIndex, -lastIndex, andIndex1, cnfClauses);
andIndex2 = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesForAND(-prevIndex, lastIndex, andIndex2, cnfClauses);
array_insert_last(int, orClause, andIndex1);
array_insert_last(int, orClause, andIndex2);
}
FREE(latchBAig);
}/* For each latch loop*/
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
} /* foreach k*/
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCnfGenerateClausesForOR | ( | int | a, |
| int | b, | ||
| int | c, | ||
| BmcCnfClauses_t * | cnfClauses | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF clauses for the OR gate]
Description []
SideEffects []
SeeAlso []
Definition at line 2231 of file bmcUtil.c.
{
array_t *tmpClause;
tmpClause = array_alloc(int, 3);
array_insert(int, tmpClause, 0, a);
array_insert(int, tmpClause, 1, b);
array_insert(int, tmpClause, 2, -c);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_free(tmpClause);
tmpClause = array_alloc(int, 2);
array_insert(int, tmpClause, 0, -a);
array_insert(int, tmpClause, 1, c);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_insert(int, tmpClause, 0, -b);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_free(tmpClause);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCnfGenerateClausesForPath | ( | Ntk_Network_t * | network, |
| int | from, | ||
| int | to, | ||
| int | initialState, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF formula for a path from state 'from' to state 'to']
Description [Unfold the transition relation 'k' states (k = to-from +1), and generate clauses for each state.
For a multi-valued latch of 4 vlaues. Two binary variables are used to rpresent X, x1 and x0. For this latch, there exist three multi-valued functions. One for the binary reoresentation of the variable. For example the second entry of the mvf = 1, iff ~x1 and x0. The second mfv is for the data input of the latch. If the And/Inv graph attached to an entry of this mvf equal to 1, X equal to the binary representation corresponding to this entry. For example, if the And/ INV graph attached to the first entry =1, then X = ~x1 & ~x0. To generate the CNF to the transition relation, first generate CNF to next state varaible using mvf of the latch. Then, generate CNF for latch data input using current state variavles. Finaly, generate CNF for the AND of these two MVF. This for every entry of the MVF. Then OR the results. The third MVF is for the initial value of the latch. It is treat the same as the latch data input except if the initial value is constant.
The initialState value may be either BMC_INITIAL_STATES to generate the clause for the intial states. BMC_NO_INITIAL_STATES otherwise. ]
SideEffects []
SeeAlso []
Definition at line 1817 of file bmcUtil.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_generator *stGen;
Ntk_Node_t *latch, *latchData, *latchInit;
MvfAig_Function_t *initMvfAig, *dataMvfAig, *latchMvfAig;
bAigEdge_t *initBAig, *latchBAig, *dataBAig;
int i, k, mvfSize;
st_foreach_item(CoiTable, stGen, &latch, NULL) {
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
/* Get the multi-valued function for each node*/
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
if (initMvfAig == NIL(MvfAig_Function_t)){
(void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
return;
}
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
if (dataMvfAig == NIL(MvfAig_Function_t)){
(void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData));
return;
}
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig, i));
}
/*
if (from == 0){
*/
if (initialState == BMC_INITIAL_STATES){
/* Generate the CNF for the initial state of the latch */
BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
}
/* Generate the CNF for the transition functions */
for (k=from; k < to; k++){
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
} /* for k state loop */
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}/* For each latch loop*/
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCnfGenerateClausesFromStateToState | ( | Ntk_Network_t * | network, |
| int | from, | ||
| int | to, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable, | ||
| int | loop | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF formula for a path from state 'from' to state 'to']
Description [Unfold the transition relation 'k' states (k = to-from +1), and generate clauses for each state. For a multi-valued latch of 4 vlaues. Two binary variables are used to rpresent X, x1 and x0. For this latch, there exist three multi-valued functions. One for the binary reoresentation of the variable. For example the second entry of the mvf = 1, iff ~x1 and x0. The second mfv is for the data input of the latch. If the And/Inv graph attached to an entry of this mvf equal to 1, X equal to the binary representation corresponding to this entry. For example, if the And/ INV graph attached to the first entry =1, then X = ~x1 & ~x0. To generate the CNF to the transition relation, first generate CNF to next state varaible using mvf of the latch. Then, generate CNF for latch data input using current state variavles. Finaly, generate CNF for the AND of these two MVF. This for every entry of the MVF. Then OR the results. The third MVF is for the initial value of the latch. It is treat the same as the latch data input except if the initial value is constant. ]
SideEffects []
SeeAlso []
Definition at line 2134 of file bmcUtil.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_generator *stGen;
Ntk_Node_t *latch, *latchData;
MvfAig_Function_t *dataMvfAig, *latchMvfAig;
bAigEdge_t *latchBAig, *dataBAig;
int i, mvfSize;
st_foreach_item(CoiTable, stGen, &latch, NULL) {
latchData = Ntk_LatchReadDataInput(latch);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
if (dataMvfAig == NIL(MvfAig_Function_t)){
(void) fprintf(vis_stdout,
"No multi-valued function for this node %s \n",
Ntk_NodeReadName(latchData));
return;
}
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
}
mvfSize = array_n(dataMvfAig);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i));
}
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize,
from, to, cnfClauses, loop);
FREE(dataBAig);
FREE(latchBAig);
} /* For each latch loop*/
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCnfInsertClause | ( | BmcCnfClauses_t * | cnfClauses, |
| array_t * | clause | ||
| ) |
Function********************************************************************
Synopsis [Add clause to the clauseArray]
Description [Add a clause to the clause array. clause is of type array_t. The user must free clause.]
SideEffects []
SeeAlso []
Definition at line 2425 of file bmcUtil.c.
{
int i, lit;
if (clause != NIL(array_t)){
if (array_n(clause) == 0){ /* empty clause */
cnfClauses->emptyClause = TRUE;
return;
}
for (i=0; i< array_n(clause); i++){
lit = array_fetch(int, clause, i);
array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, lit);
}
array_insert(int, cnfClauses->clauseArray, cnfClauses->nextIndex++, 0); /*End Of clause*/
cnfClauses->noOfClauses++;
cnfClauses->emptyClause = FALSE;
}
return;
}/* BmcCnfInsertClause() */
Here is the caller graph for this function:
| int BmcCnfReadOrInsertNode | ( | BmcCnfClauses_t * | cnfClauses, |
| nameType_t * | nodeName, | ||
| int | state, | ||
| int * | nodeIndex | ||
| ) |
Function********************************************************************
Synopsis [Return the cnfIndex of the node]
Description [If CNF was generated for this node, return its cnfIndex, otherwise insert the name of this node in the cnfIndexTable, and return its cnfIndex. The key to the cnfIndexTable is (nodeName_state).]
SideEffects []
Definition at line 2473 of file bmcUtil.c.
{
nameType_t *varName;
int index;
char *stateStr = util_inttostr(state);
varName = util_strcat3(nodeName, "_", stateStr);
FREE(stateStr);
if (!st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
index = cnfClauses->cnfGlobalIndex++;
st_insert(cnfClauses->cnfIndexTable, varName, (char*) (long) index);
if(cnfClauses->freezed == TRUE){
array_insert_last(nameType_t *, cnfClauses->freezedKeys, varName);
}
*nodeIndex = index;
return 0; /* Inserted */
}
else { /* The node has been visited */
*nodeIndex = index;
FREE(varName);
return 1;
}
}
Here is the caller graph for this function:
| mdd_t* BmcComputeCloseCube | ( | mdd_t * | aSet, |
| mdd_t * | target, | ||
| int * | dist, | ||
| array_t * | Support, | ||
| mdd_manager * | mddMgr | ||
| ) |
Function********************************************************************
Synopsis [Compute cube that is close to target states. Support is an array of mddids representing the total support; that is, all the variables on which aSet may depend. It dos the function only if CUDD is the BDD package.]
SideEffects []
Definition at line 202 of file bmcUtil.c.
{
if (bdd_get_package_name() == CUDD && target != NIL(mdd_t)) {
mdd_t *range; /* range of Support */
mdd_t *legalSet; /* aSet without the don't cares */
mdd_t *closeCube;
/* Check that support of set is contained in Support.
assert(SetCheckSupport(aSet, Support, mddMgr)); */
assert(!mdd_is_tautology(aSet, 0));
range = mdd_range_mdd(mddMgr, Support);
legalSet = bdd_and(aSet, range, 1, 1);
mdd_free(range);
closeCube = mdd_closest_cube(legalSet, target, dist);
mdd_free(legalSet);
return closeCube;
} else {
return aSet;
/*return BMC_ComputeAMinterm(aSet, Support, mddMgr);*/
}/* if CUDD */
} /* BmcComputeCloseCube */
Here is the caller graph for this function:
| mAigEdge_t BmcCreateMaigOfInitialStates | ( | Ntk_Network_t * | network, |
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Build AND/INV graph for intial states]
Description [Build AND/INV graph for intial states. Returns bAig Id of the bAig Function that represents the intial states.
The initial states are computed as follows. For each latch i, the relation (x_i = g_i(u)) is built, where x_i is the present state variable of latch i, and g_i(u) is the multi-valued initialization function of latch i, in terms of the input variables u. These relations are then conjuncted. ]
SideEffects []
SeeAlso []
Definition at line 253 of file bmcUtil.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
st_generator *stGen;
Ntk_Node_t *latch, *latchInit;
MvfAig_Function_t *initMvfAig, *latchMvfAig;
bAigEdge_t resultAnd = bAig_One;
bAigEdge_t resultOr;
int i;
st_foreach_item(CoiTable, stGen, &latch, NULL) {
latchInit = Ntk_LatchReadInitialInput(latch);
/* Get the multi-valued function for each node*/
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
if (initMvfAig == NIL(MvfAig_Function_t)){
(void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
return bAig_NULL;
}
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
resultOr = bAig_Zero;
for(i=0; i<array_n(initMvfAig); i++){
resultOr = mAig_Or(manager, resultOr,
bAig_Eq(manager,
bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(initMvfAig, i)),
bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(latchMvfAig, i))
)
);
if(resultOr == bAig_One){
break;
}
}
resultAnd = mAig_And(manager, resultAnd, resultOr);
if(resultAnd == bAig_Zero){
break;
}
}/* for each latch*/
return resultAnd;
}
Here is the call graph for this function:
| mAigEdge_t BmcCreateMaigOfPropFormula | ( | Ntk_Network_t * | network, |
| mAig_Manager_t * | manager, | ||
| Ctlsp_Formula_t * | formula | ||
| ) |
Function********************************************************************
Synopsis [Builds AND/INVERTER graph (aig) for a propsitional formula]
Description [Builds AND/INVERTER graph for a propsitional formula. Returns bAig ID of the function that is quivalent to the propositional fomula]
SideEffects []
SeeAlso []
Definition at line 322 of file bmcUtil.c.
{
mAigEdge_t left, right, result;
if (formula == NIL(Ctlsp_Formula_t)) {
return mAig_NULL;
}
if (formula->type == Ctlsp_TRUE_c){
return mAig_One;
}
if (formula->type == Ctlsp_FALSE_c){
return mAig_Zero;
}
assert(Ctlsp_isPropositionalFormula(formula));
if (formula->type == Ctlsp_ID_c){
char *nodeNameString = Ctlsp_FormulaReadVariableName(formula);
char *nodeValueString = Ctlsp_FormulaReadValueName(formula);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
Var_Variable_t *nodeVar;
int nodeValue;
MvfAig_Function_t *tmpMvfAig;
st_table *nodeToMvfAigTable; /* maps each node to its mvfAig */
if (node == NIL(Ntk_Node_t)) {
(void) fprintf(vis_stderr, "bmc error: Could not find node corresponding to the name\t %s\n", nodeNameString);
return mAig_NULL;
}
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
(void) fprintf(vis_stderr, "bmc error: please run build_partiton_maigs first");
return mAig_NULL;
}
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
if (tmpMvfAig == NIL(MvfAig_Function_t)){
tmpMvfAig = Bmc_NodeBuildMVF(network, node);
array_free(tmpMvfAig);
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
}
nodeVar = Ntk_NodeReadVariable(node);
if (Var_VariableTestIsSymbolic(nodeVar)) {
nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
if ( nodeValue == -1 ) {
(void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
}
else {
int check;
check = StringCheckIsInteger(nodeValueString, &nodeValue);
if( check == 0 ) {
(void) fprintf(vis_stderr,"Illegal value in the RHS\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
if( check == 1 ) {
(void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
(void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
return mAig_NULL;
}
if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
(void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return mAig_NULL;
}
}
result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
return bAig_GetCanonical(manager, result);
}
/*
right can be mAig_NULL for unery operators, but left can't be mAig_Null
*/
left = BmcCreateMaigOfPropFormula(network, manager, formula->left);
if (left == mAig_NULL){
return mAig_NULL;
}
right = BmcCreateMaigOfPropFormula(network, manager, formula->right);
switch(formula->type) {
case Ctlsp_NOT_c:
result = mAig_Not(left);
break;
case Ctlsp_OR_c:
result = mAig_Or(manager, left, right);
break;
case Ctlsp_AND_c:
result = mAig_And(manager, left, right);
break;
case Ctlsp_THEN_c:
result = mAig_Then(manager, left, right);
break;
case Ctlsp_EQ_c:
result = mAig_Eq(manager, left, right);
break;
case Ctlsp_XOR_c:
result = mAig_Xor(manager, left, right);
break;
default:
fail("Unexpected LTL type");
}
return result;
} /* BmcCreateMaigOfPropFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* BmcCreateMddOfSafetyProperty | ( | Fsm_Fsm_t * | fsm, |
| Ctlsp_Formula_t * | formula | ||
| ) |
Function********************************************************************
Synopsis [Build MDD for safety property in form of AG(p). Where p is either a propositional formula or a path formula contains only the temporal property X.]
Description [Build MDD for a safety formula. Returns NIL if the conversion fails. The calling application is responsible for freeing the returned MDD.]
SideEffects []
SeeAlso [Ctlsp_FormulaReadClass]
Definition at line 447 of file bmcUtil.c.
{
mdd_manager *manager = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(fsm));
mdd_t *left, *right, *result;
if (formula == NIL(Ctlsp_Formula_t)) {
return NIL(mdd_t);
}
if (formula->type == Ctlsp_TRUE_c){
return bdd_one(manager);
}
if (formula->type == Ctlsp_FALSE_c){
return mdd_zero(manager);
}
#if 0
if (!Ctlsp_isPropositionalFormula(formula)) {
(void) fprintf(vis_stderr, "bmc error: Only propositional formula can be converted to bdd \n");
fprintf(vis_stdout, "\nFormula: ");
Ctlsp_FormulaPrint(vis_stdout, formula);
fprintf(vis_stdout, "\n");
return NIL(mdd_t);
}
#endif
/*
Atomic proposition.
*/
if (formula->type == Ctlsp_ID_c){
return BmcModelCheckAtomicFormula(fsm, formula);
}
/*
right can be NIL(mdd_t) for unery operators, but left can't be NIL(mdd_t)
*/
left = BmcCreateMddOfSafetyProperty(fsm, formula->left);
if (left == NIL(mdd_t)){
return NIL(mdd_t);
}
right = BmcCreateMddOfSafetyProperty(fsm, formula->right);
assert(right != NIL(mdd_t));
switch(formula->type) {
case Ctlsp_NOT_c:
result = mdd_not(left);
break;
case Ctlsp_OR_c:
result = mdd_or(left, right, 1, 1);
break;
case Ctlsp_AND_c:
result = mdd_and(left, right, 1, 1);
break;
case Ctlsp_THEN_c:
result = mdd_or(left, right, 0, 1);
break;
case Ctlsp_EQ_c:
result = mdd_xnor(left, right);
break;
case Ctlsp_XOR_c:
result = mdd_xor(left, right);
break;
case Ctlsp_X_c:
result = BmcFsmEvaluateX(fsm, left);
break;
default:
/*
return NIL(mdd_t) if the type is not supported
*/
return NIL(mdd_t);
/*
fail("Unexpected type");
*/
}
return result;
}
Here is the call graph for this function:
| mdd_t* BmcFsmEvaluateX | ( | Fsm_Fsm_t * | modelFsm, |
| mdd_t * | targetMdd | ||
| ) |
Function********************************************************************
Synopsis [Evaluate states satisfying X target]
Description [Evaluate states satisfying X target.]
SideEffects []
Definition at line 153 of file bmcUtil.c.
{
mdd_t *fromLowerBound;
mdd_t *fromUpperBound;
mdd_t *result;
Img_ImageInfo_t * imageInfo;
mdd_t *careStates;
array_t *careStatesArray = array_alloc(array_t *, 0);
imageInfo = Fsm_FsmReadOrCreateImageInfo(modelFsm, 1, 0);
/*
* The lower bound is the conjunction of the fair states,
* and the target states.
*/
fromLowerBound = mdd_dup(targetMdd);
/*
* The upper bound is the same as the lower bound.
*/
fromUpperBound = mdd_dup(fromLowerBound);
/*
careSet is the set of all unreachabel states.
*/
careStates = mdd_one(Fsm_FsmReadMddManager(modelFsm));
array_insert(mdd_t *, careStatesArray, 0, careStates);
result = Img_ImageInfoComputePreImageWithDomainVars(imageInfo,
fromLowerBound, fromUpperBound, careStatesArray);
mdd_free(fromLowerBound);
mdd_free(fromUpperBound);
return result;
} /* BmcFsmEvaluateX */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcGenerateClausesFromStateTostate | ( | bAig_Manager_t * | manager, |
| bAigEdge_t * | fromAigArray, | ||
| bAigEdge_t * | toAigArray, | ||
| int | mvfSize, | ||
| int | fromState, | ||
| int | toState, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| int | outIndex | ||
| ) |
Function********************************************************************
Synopsis [ c = a <-> b = (a=0)*(b=0) + (a=1)*(b=1) .... For a given term (a=i)*(b=i), if either is Zero, don't generate clauses for this term. if both are One, don't generate clauses for c. ]
SideEffects []
Definition at line 959 of file bmcUtil.c.
{
array_t *clause, *tmpclause;
int toIndex, fromIndex, cnfIndex;
int i;
/* used to turn off the warning messages: might be left uninitialized.
We are sure that these two variables will not be used uninitialized.
*/
toIndex =0;
fromIndex = 0;
for(i=0; i< mvfSize; i++){
if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){
return; /* the clause is always true */
}
}
clause = array_alloc(int, 0);
for(i=0; i< mvfSize; i++){
if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){
if (toAigArray[i] != bAig_One){
/* to State */
toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i],
toState,cnfClauses);
}
if (fromAigArray[i] != bAig_One){
/* from State */
fromIndex = BmcGenerateCnfFormulaForAigFunction(manager,
fromAigArray[i],
fromState,
cnfClauses);
}
/*
Create new var for the output of this node. We don't create variable for this node, we only
use its index number.
*/
cnfIndex = cnfClauses->cnfGlobalIndex++; /* index of the output of the OR of T(from, to) */
assert(abs(cnfIndex) <= cnfClauses->cnfGlobalIndex);
assert(abs(fromIndex) <= cnfClauses->cnfGlobalIndex);
assert(abs(toIndex) <= cnfClauses->cnfGlobalIndex);
if (toAigArray[i] == bAig_One){
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, -fromIndex);
array_insert(int, tmpclause, 1, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, fromIndex);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
} else if (fromAigArray[i] == bAig_One){
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, -toIndex);
array_insert(int, tmpclause, 1, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, toIndex);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
} else {
tmpclause = array_alloc(int, 3);
array_insert(int, tmpclause, 0, -toIndex);
array_insert(int, tmpclause, 1, -fromIndex);
array_insert(int, tmpclause, 2, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, toIndex);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, fromIndex);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
}
array_insert_last(int, clause, cnfIndex);
} /* if */
} /* for i loop */
if (outIndex != 0 ){
array_insert_last(int, clause, -outIndex);
}
BmcCnfInsertClause(cnfClauses, clause);
array_free(clause);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int BmcGenerateCnfFormulaForAigFunction | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | node, | ||
| int | k, | ||
| BmcCnfClauses_t * | cnfClauses | ||
| ) |
Function********************************************************************
Synopsis [Generate the CNF formula of a given function represented by AND/INVERTER graph]
Description [Generate an array of clausese for a function represented in AND/INVERETER graph structure.
the CNF formula of node to the output file specifies by cnfFile. It stores CNF index for each node in the cnfIndexTable. The generated CNF is in dimacs format. It is an error to call this function on a constand zero/one node.]
SideEffects []
SeeAlso []
Definition at line 543 of file bmcUtil.c.
{
int leftIndex, rightIndex, nodeIndex;
array_t *clause;
assert( (node != bAig_One) && (node != bAig_Zero));
if(bAig_IsInverted(node)){
/*
The generated clauses are in dimacs formate that uses negative number to indicate complement
*/
return -1*BmcGenerateCnfFormulaForAigFunction(manager, bAig_NonInvertedEdge(node), k, cnfClauses);
}
if (BmcCnfReadOrInsertNode(cnfClauses, bAig_NodeReadName(manager, node), k, &nodeIndex)){
return nodeIndex;
}
if (bAig_isVarNode(manager, node)){
return nodeIndex;
}
leftIndex = BmcGenerateCnfFormulaForAigFunction(manager,
bAig_GetCanonical(manager, leftChild(node)),
k, cnfClauses);
rightIndex = BmcGenerateCnfFormulaForAigFunction(manager,
bAig_GetCanonical(manager, rightChild(node)),
k, cnfClauses);
clause = array_alloc(int, 3);
array_insert(int, clause, 0, -leftIndex );
array_insert(int, clause, 1, -rightIndex);
array_insert(int, clause, 2, nodeIndex );
BmcCnfInsertClause(cnfClauses, clause);
array_free(clause);
clause = array_alloc(int, 2);
array_insert(int, clause, 0, leftIndex);
array_insert(int, clause, 1, -nodeIndex);
BmcCnfInsertClause(cnfClauses, clause);
array_free(clause);
clause = array_alloc(int, 2);
array_insert(int, clause, 0, rightIndex);
array_insert(int, clause, 1, -nodeIndex);
BmcCnfInsertClause(cnfClauses, clause);
array_free(clause);
return(nodeIndex);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int BmcGenerateCnfFormulaForBdd | ( | bdd_t * | bddFunction, |
| int | k, | ||
| BmcCnfClauses_t * | cnfClauses | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF for bdd function]
Description [ The function of each node f = var*thenChild + -var*elseChild var is the variable at this node. For each node there are four cases:
- both childeren are constant -> do nothing.
- the then child is constant 1 -> generate clauses for f = var + elseChild.
- the else child is constant 0 -> generate clauses for f = var * thenChild.
- the else child is constant 1 -> generate clauses for f = -var + thenChild.
- else -> generate clauses for f = var*thenChild + -var*elseChild. ------------------------------------------------ function | clauses ------------------------------------------------ c = a*b | (-a + -b + c)*(a + -c)*(b + -c) c = a+b | (a + b + -c)*(-a + c)*(-b + c) f = c*a + -c*b | (-a + -c + f)*(a + -c + -f)* | (-b + c + f)*(b + c + -f)
return the cnf index of the bdd function ]
SideEffects []
SeeAlso []
Definition at line 624 of file bmcUtil.c.
{
bdd_manager *bddManager = bdd_get_manager(bddFunction);
bdd_node *node, *thenNode, *elseNode, *funcNode;
int is_complemented;
int nodeIndex=0, thenIndex, elseIndex;
bdd_gen *gen;
int varIndex, flag;
array_t *tmpClause;
st_table *bddToCnfIndexTable;
bdd_t *currentBddNode;
int cut = 5;
if (bddFunction == NULL){
return 0;
}
funcNode = bdd_get_node(bddFunction, &is_complemented);
if (bdd_is_constant(funcNode)){
if (is_complemented){
/* add an empty clause to indicate FALSE (un-satisfiable)*/
BmcAddEmptyClause(cnfClauses);
}
return 0;
}
if(bdd_size(bddFunction) <= cut){
return BmcGenerateCnfFormulaForBddOffSet(bddFunction, k, cnfClauses);
}
bddToCnfIndexTable = st_init_table(st_numcmp, st_numhash);
foreach_bdd_node(bddFunction, gen, node){
if (bdd_is_constant(node)){ /* do nothing */
continue;
}
/*
bdd_size() returns 1 if bdd is constant one.
*/
/*
Use offset method to generate CNF if the size of the node <= cut (include the constant 1 node).
*/
/*#if 0*/
if(bdd_size(currentBddNode = bdd_construct_bdd_t(bddManager, bdd_regular(node))) <= cut){
if (bdd_size(currentBddNode) == cut){
nodeIndex = BmcGenerateCnfFormulaForBddOffSet(currentBddNode, k, cnfClauses);
st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(node), (char *) (long)nodeIndex);
continue;
}
continue;
}
/*#endif*/
varIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses);
nodeIndex = varIndex;
thenNode = bdd_bdd_T(node);
elseNode = bdd_bdd_E(node);
if (!((bdd_is_constant(thenNode)) && (bdd_is_constant(elseNode)))){
nodeIndex = cnfClauses->cnfGlobalIndex++; /* index of the function of this node */
if (bdd_is_constant(thenNode)){ /* the thenNode can be only constant one*/
flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex);
assert(flag);
/*
test if the elseNode is complemented arc?
*/
if (bdd_is_complement(elseNode)){
elseIndex = -1*elseIndex;
}
BmcCnfGenerateClausesForOR(elseIndex, varIndex, nodeIndex, cnfClauses);
} else if (bdd_is_constant(elseNode)){ /* one or zero */
flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex);
assert(flag);
/*
test if the elseNode is complemented arc?
*/
if (bdd_is_complement(elseNode)){ /* Constant zero */
BmcCnfGenerateClausesForAND(thenIndex, varIndex, nodeIndex, cnfClauses);
} else { /* Constant one */
BmcCnfGenerateClausesForOR(thenIndex, -varIndex, nodeIndex, cnfClauses);
}
} else {
flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(thenNode), &thenIndex);
if(flag == 0){
thenIndex = BmcGenerateCnfFormulaForBddOffSet(bdd_construct_bdd_t(bddManager, bdd_regular(thenNode)), k, cnfClauses);
st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(thenNode), (char *) (long)thenIndex);
}
/*assert(flag);*/
flag = st_lookup_int(bddToCnfIndexTable, bdd_regular(elseNode), &elseIndex);
if(flag == 0){
elseIndex = BmcGenerateCnfFormulaForBddOffSet( bdd_construct_bdd_t(bddManager, bdd_regular(elseNode)), k, cnfClauses);
st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(elseNode), (char *)(long) elseIndex);
}
/*assert(flag);*/
/*
test if the elseNode is complemented arc?
*/
if (bdd_is_complement(elseNode)){
elseIndex = -1*elseIndex;
}
tmpClause = array_alloc(int, 3);
assert(abs(thenIndex) <= cnfClauses->cnfGlobalIndex);
assert(abs(varIndex) <= cnfClauses->cnfGlobalIndex);
assert(abs(nodeIndex) <= cnfClauses->cnfGlobalIndex);
array_insert(int, tmpClause, 0, -thenIndex);
array_insert(int, tmpClause, 1, -varIndex);
array_insert(int, tmpClause, 2, nodeIndex);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_insert(int, tmpClause, 0, thenIndex);
array_insert(int, tmpClause, 1, -varIndex);
array_insert(int, tmpClause, 2, -nodeIndex);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_insert(int, tmpClause, 0, -elseIndex);
array_insert(int, tmpClause, 1, varIndex);
array_insert(int, tmpClause, 2, nodeIndex);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_insert(int, tmpClause, 0, elseIndex);
array_insert(int, tmpClause, 1, varIndex);
array_insert(int, tmpClause, 2, -nodeIndex);
BmcCnfInsertClause(cnfClauses, tmpClause);
array_free(tmpClause);
}
}
st_insert(bddToCnfIndexTable, (char *) (long) bdd_regular(node), (char *) (long) nodeIndex);
} /* foreach_bdd_node() */
st_free_table(bddToCnfIndexTable);
return (is_complemented? -nodeIndex: nodeIndex);
} /* BmcGenerateCnfFormulaForBdd() */
Here is the call graph for this function:
| int BmcGenerateCnfFormulaForBddOffSet | ( | bdd_t * | bddFunction, |
| int | k, | ||
| BmcCnfClauses_t * | cnfClauses | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF for bdd function based on the off set of the bdd function]
Description [Express the negation of bdd function in disjunctive normal form(DNF), and generate a clause for each disjunct in the DNF.]
SideEffects []
SeeAlso []
Definition at line 781 of file bmcUtil.c.
{
bdd_manager *bddManager = bdd_get_manager(bddFunction);
bdd_node *node, *funcNode;
int is_complemented;
bdd_gen *gen;
int varIndex;
array_t *tmpClause;
array_t *cube;
int i, value;
bdd_t *newVar;
if (bddFunction == NULL){
return 0;
}
/*
Because the top node of bddFunction represents a variable in
bddFunction, newVar is used to represent the function of
bddFunction. Setting the cnfIndex of newVar to 1(0) is like
setting the function of bddFunction to 1(0).
*/
newVar = bdd_create_variable(bddManager);
bddFunction = bdd_xnor(newVar, bddFunction);
funcNode = bdd_get_node(bddFunction, &is_complemented);
if (bdd_is_constant(funcNode)){
if (is_complemented){
/* add an empty clause to indicate FALSE (un-satisfiable)*/
BmcAddEmptyClause(cnfClauses);
}
return 0;
}
bddFunction = bdd_not(bddFunction);
foreach_bdd_cube(bddFunction, gen, cube){
tmpClause = array_alloc(int,0);
arrayForEachItem(int, cube, i, value) {
if (value != 2){
node = bdd_bdd_ith_var(bddManager, i);
varIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(node), k, cnfClauses);
if (value == 1){
varIndex = -varIndex;
}
array_insert_last(int, tmpClause, varIndex);
}
}
BmcCnfInsertClause(cnfClauses, tmpClause);
array_free(tmpClause);
}/* foreach_bdd_cube() */
varIndex = BmcGetCnfVarIndexForBddNode(bddManager,
bdd_regular(bdd_get_node(newVar, &is_complemented)),
k, cnfClauses);
return (varIndex);
} /* BmcGenerateCnfFormulaForBddOffSet() */
Here is the call graph for this function:
Here is the caller graph for this function:
| int BmcGetCnfVarIndexForBddNode | ( | bdd_manager * | bddManager, |
| bdd_node * | node, | ||
| int | state, | ||
| BmcCnfClauses_t * | cnfClauses | ||
| ) |
Function********************************************************************
Synopsis [return the cnf index for a bdd node]
SideEffects []
Definition at line 2783 of file bmcUtil.c.
{
array_t *mvar_list = mdd_ret_mvar_list(bddManager);
array_t *bvar_list = mdd_ret_bvar_list(bddManager);
char name[100];
char *nodeName;
bvar_type bv;
mvar_type mv;
int nodeIndex = bdd_node_read_index(node);
int index, rtnNodeIndex, rtnCode;
/*
If the node is for a multi-valued varaible.
*/
if (nodeIndex < array_n(bvar_list)){
bv = array_fetch(bvar_type, bvar_list, nodeIndex);
/*
get the multi-valued varaible.
*/
mv = array_fetch(mvar_type, mvar_list, bv.mvar_id);
arrayForEachItem(int, mv.bvars, index, rtnNodeIndex) {
if (nodeIndex == rtnNodeIndex){
break;
}
}
assert(index < mv.encode_length);
/*
printf("Name of bdd node %s %d\n", mv.name, index);
*/
sprintf(name, "%s_%d", mv.name, index);
} else {
sprintf(name, "Bdd_%d", nodeIndex);
}
nodeName = util_strsav(name);
rtnCode = BmcCnfReadOrInsertNode(cnfClauses, nodeName, state, &nodeIndex);
if(rtnCode == 1) {
FREE(nodeName);
}
return nodeIndex;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcGetCoiForLtlFormula | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | formula, | ||
| st_table * | ltlCoiTable | ||
| ) |
Function********************************************************************
Synopsis [Find the Cone of Influnce (COI) for an LTL formula]
Description [Return a list of state variables (latches) that are in the COI of the LTL formula.]
SideEffects []
Definition at line 2513 of file bmcUtil.c.
{
st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
BmcGetCoiForLtlFormulaRecursive(network, formula, ltlCoiTable, visited);
st_free_table(visited);
return;
} /* BmcGetCoiForLtlFormula() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcGetCoiForLtlFormulaRecursive | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | formula, | ||
| st_table * | ltlCoiTable, | ||
| st_table * | visited | ||
| ) |
Function********************************************************************
Synopsis [Recursive function to find the COI of a network node.]
Description []
SideEffects []
Definition at line 2535 of file bmcUtil.c.
{
if (formula == NIL(Ctlsp_Formula_t)) {
return;
}
/* leaf node */
if (formula->type == Ctlsp_ID_c){
char *name = Ctlsp_FormulaReadVariableName(formula);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
int tmp;
if (st_lookup_int(visited, (char *) node, &tmp)){
/* Node already visited */
return;
}
BmcGetCoiForNtkNode(node, ltlCoiTable, visited);
return;
}
BmcGetCoiForLtlFormulaRecursive(network, formula->left, ltlCoiTable, visited);
BmcGetCoiForLtlFormulaRecursive(network, formula->right, ltlCoiTable, visited);
return;
} /* BmcGetCoiForLtlFormulaRecursive() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcGetCoiForNtkNode | ( | Ntk_Node_t * | node, |
| st_table * | CoiTable, | ||
| st_table * | visited | ||
| ) |
Function********************************************************************
Synopsis [Genrate COI for a non-latch network node]
Description [For each fanins of the given node, if its latch, add it to the CoiTable and return. If it is not latch, call this function to look for any latches in the fanins of this node.]
SideEffects []
Definition at line 2575 of file bmcUtil.c.
{
int i, j;
Ntk_Node_t *faninNode;
if(node == NIL(Ntk_Node_t)){
return;
}
if (st_lookup_int(visited, (char *) node, &j)){
/* Node already visited */
return;
}
st_insert(visited, (char *) node, (char *) 0);
if (Ntk_NodeTestIsLatch(node)){
st_insert(CoiTable, (char *) node, (char *) 0);
}
Ntk_NodeForEachFanin(node, i, faninNode) {
BmcGetCoiForNtkNode(faninNode, CoiTable, visited);
}
return;
} /* BmcGetCoiForNtkNode() */
Here is the call graph for this function:
Here is the caller graph for this function:
| mdd_t* BmcModelCheckAtomicFormula | ( | Fsm_Fsm_t * | modelFsm, |
| Ctlsp_Formula_t * | ctlFormula | ||
| ) |
Function********************************************************************
Synopsis [Find Mdd for states satisfying Atomic Formula.]
Description [An atomic formula defines a set of states in the following way: it states a designated ``net'' (specified by the full path name) takes a certain value. The net should be purely a function of latches; as a result an evaluation of the net yields a set of states.]
SideEffects []
Definition at line 2615 of file bmcUtil.c.
{
mdd_t * resultMdd;
mdd_t *tmpMdd;
Ntk_Network_t *network = Fsm_FsmReadNetwork(modelFsm);
char *nodeNameString = Ctlsp_FormulaReadVariableName(ctlFormula);
char *nodeValueString = Ctlsp_FormulaReadValueName(ctlFormula);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
Var_Variable_t *nodeVar;
int nodeValue;
graph_t *modelPartition;
vertex_t *partitionVertex;
Mvf_Function_t *MVF;
nodeVar = Ntk_NodeReadVariable(node);
if (Var_VariableTestIsSymbolic(nodeVar)) {
nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
}
else {
nodeValue = atoi(nodeValueString);
}
modelPartition = Part_NetworkReadPartition(network);
if (!(partitionVertex = Part_PartitionFindVertexByName(modelPartition,
nodeNameString))) {
lsGen tmpGen;
Ntk_Node_t *tmpNode;
array_t *mvfArray;
array_t *tmpRoots = array_alloc(Ntk_Node_t *, 0);
st_table *tmpLeaves = st_init_table(st_ptrcmp, st_ptrhash);
array_insert_last(Ntk_Node_t *, tmpRoots, node);
Ntk_NetworkForEachCombInput(network, tmpGen, tmpNode) {
st_insert(tmpLeaves, (char *) tmpNode, (char *) NTM_UNUSED);
}
mvfArray = Ntm_NetworkBuildMvfs(network, tmpRoots, tmpLeaves,
NIL(mdd_t));
MVF = array_fetch(Mvf_Function_t *, mvfArray, 0);
array_free(tmpRoots);
st_free_table(tmpLeaves);
array_free(mvfArray);
tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
resultMdd = mdd_dup(tmpMdd);
Mvf_FunctionFree(MVF);
}
else {
MVF = Part_VertexReadFunction(partitionVertex);
tmpMdd = Mvf_FunctionReadComponent(MVF, nodeValue);
resultMdd = mdd_dup(tmpMdd);
}
if (Part_PartitionReadMethod(modelPartition) == Part_Frontier_c &&
Ntk_NodeTestIsCombOutput(node)) {
array_t *psVars = Fsm_FsmReadPresentStateVars(modelFsm);
mdd_manager *mgr = Ntk_NetworkReadMddManager(Fsm_FsmReadNetwork(modelFsm));
array_t *supportList;
st_table *supportTable = st_init_table(st_numcmp, st_numhash);
int i, j;
int existIntermediateVars;
int mddId;
Mvf_Function_t *mvf;
vertex_t *vertex;
array_t *varBddRelationArray, *varArray;
mdd_t *iv, *ivMdd, *relation;
for (i = 0; i < array_n(psVars); i++) {
mddId = array_fetch(int, psVars, i);
st_insert(supportTable, (char *)(long)mddId, NULL);
}
existIntermediateVars = 1;
while (existIntermediateVars) {
existIntermediateVars = 0;
supportList = mdd_get_support(mgr, resultMdd);
for (i = 0; i < array_n(supportList); i++) {
mddId = array_fetch(int, supportList, i);
if (!st_lookup(supportTable, (char *)(long)mddId, NULL)) {
vertex = Part_PartitionFindVertexByMddId(modelPartition, mddId);
mvf = Part_VertexReadFunction(vertex);
varBddRelationArray = mdd_fn_array_to_bdd_rel_array(mgr, mddId, mvf);
varArray = mdd_id_to_bdd_array(mgr, mddId);
assert(array_n(varBddRelationArray) == array_n(varArray));
for (j = 0; j < array_n(varBddRelationArray); j++) {
iv = array_fetch(mdd_t *, varArray, j);
relation = array_fetch(mdd_t *, varBddRelationArray, j);
ivMdd = bdd_cofactor(relation, iv);
mdd_free(relation);
tmpMdd = resultMdd;
resultMdd = bdd_compose(resultMdd, iv, ivMdd);
mdd_free(tmpMdd);
mdd_free(iv);
mdd_free(ivMdd);
}
array_free(varBddRelationArray);
array_free(varArray);
existIntermediateVars = 1;
}
}
array_free(supportList);
}
st_free_table(supportTable);
}
return resultMdd;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcPrintCounterExample | ( | Ntk_Network_t * | network, |
| st_table * | nodeToMvfAigTable, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| array_t * | result, | ||
| int | length, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options, | ||
| array_t * | loopClause | ||
| ) |
Function********************************************************************
Synopsis [Print CounterExample.]
SideEffects [Print a counterexample that was returned from the SAT solver in term of an array of integer "result". The counterexample starts from state 0 and of lenght eqaual to "length". If loopClause is not empty, this function print a loopback from the last state to a state in loopClause that exist in "result".]
Definition at line 1381 of file bmcUtil.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
lsGen gen;
st_generator *stGen;
Ntk_Node_t *node;
int k;
array_t *latches = array_alloc(int, 0);
int *prevValueLatches;
array_t *inputs = array_alloc(int, 0);
int *prevValueInputs;
int tmp;
int loop;
st_table *resultTable = st_init_table(st_numcmp, st_numhash);
/*
Initialize resultTable from the result to speed up the search in the result array.
*/
for(k=0; k< array_n(result); k++){
st_insert(resultTable, (char *) (long) array_fetch(int, result, k), (char *) 0);
}
/* sort latches by name */
st_foreach_item(CoiTable, stGen, &node, NULL) {
array_insert_last(char*, latches, Ntk_NodeReadName(node));
}
array_sort(latches, nameCompare);
/*
Use to store the last value of each latch. If the current value of a latch
differs from its corresponding value in this array, we will print the new values.
*/
prevValueLatches = ALLOC(int, array_n(latches));
prevValueInputs = 0;
if(options->printInputs == TRUE){
/* sort inputs by name */
Ntk_NetworkForEachInput(network, gen, node){
array_insert_last(char*, inputs, Ntk_NodeReadName(node));
}
array_sort(inputs, nameCompare);
prevValueInputs = ALLOC(int, array_n(inputs));
}
loop = -1; /* no loop back */
if(loopClause != NIL(array_t)){
for(k=0; k < array_n(loopClause); k++){
/* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
loop = k;
break;
}
}
}
/*
Ntk_NetworkForEachPrimaryOutput(network, gen, node){
array_insert_last(char*, outputs, Ntk_NodeReadName(node));
}
array_sort(outputs, nameCompare);
*/
for (k=0; k<= length; k++){
if (k == 0){
(void) fprintf(vis_stdout, "\n--State %d:\n", k);
} else {
(void) fprintf(vis_stdout, "\n--Goes to state %d:\n", k);
}
/*
Print the current values of the latches if they are different form their
previous values.
*/
printValue(manager, network, nodeToMvfAigTable, cnfClauses,
latches, resultTable, k, prevValueLatches);
#if 0
(void) fprintf(vis_stdout, "--Primary output:\n");
printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
#endif
if((options->printInputs == TRUE) && (k !=0)) {
(void) fprintf(vis_stdout, "--On input:\n");
printValue(manager, network, nodeToMvfAigTable, cnfClauses,
inputs, resultTable, k-1, prevValueInputs);
}
} /* for k loop */
if(loop != -1){
(void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
printValue(manager, network, nodeToMvfAigTable, cnfClauses,
latches, resultTable, loop, prevValueLatches);
if((options->printInputs == TRUE)) {
(void) fprintf(vis_stdout, "--On input:\n");
printValue(manager, network, nodeToMvfAigTable, cnfClauses,
inputs, resultTable, length, prevValueInputs);
}
}
array_free(latches);
FREE(prevValueLatches);
if(options->printInputs == TRUE){
array_free(inputs);
FREE(prevValueInputs);
}
st_free_table(resultTable);
return;
} /* BmcPrintCounterExample() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcPrintCounterExampleAiger | ( | Ntk_Network_t * | network, |
| st_table * | nodeToMvfAigTable, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| array_t * | result, | ||
| int | length, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options, | ||
| array_t * | loopClause | ||
| ) |
Function********************************************************************
Synopsis [Print CounterExample in Aiger format.]
SideEffects [Print a counterexample that was returned from the SAT solver in term of an array of integer "result". The counterexample starts from state 0 and of lenght eqaual to "length". If loopClause is not empty, this function print a loopback from the last state to a state in loopClause that exist in "result".]
Definition at line 1499 of file bmcUtil.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
lsGen gen;
st_generator *stGen;
Ntk_Node_t *node;
int k;
array_t *latches = array_alloc(int, 0);
int *prevValueLatches;
array_t *inputs = array_alloc(int, 0);
array_t *outputs = array_alloc(int, 0);
int *prevValueInputs;
int *prevValueOutputs;
int tmp;
int loop;
st_table *resultTable = st_init_table(st_numcmp, st_numhash);
char *nodeName;
/*
Initialize resultTable from the result to speed up the search in the result array.
*/
for(k=0; k< array_n(result); k++){
st_insert(resultTable, (char *) (long) array_fetch(int, result, k), (char *) 0);
}
/* sort latches by name */
st_foreach_item(CoiTable, stGen, &node, NULL) {
array_insert_last(char*, latches, Ntk_NodeReadName(node));
}
/*
Use to store the last value of each latch. If the current value of a latch
differs from its corresponding value in this array, we will print the new values.
*/
/* the file generation needs to be removed for final vis release */
FILE *order = Cmd_FileOpen("inputOrder.txt", "w", NIL(char *), 0);
for (k=0; k< array_n(latches); k++)
{
nodeName = array_fetch(char *, latches, k);
if((nodeName[0] == '$') && (nodeName[1] == '_'))
{
fprintf(order, "%s\n", &nodeName[2]);
}
}
fclose(order);
prevValueLatches = ALLOC(int, array_n(latches));
Ntk_NetworkForEachInput(network, gen, node){
array_insert_last(char*, inputs, Ntk_NodeReadName(node));
}
prevValueInputs = ALLOC(int, array_n(inputs));
loop = -1; /* no loop back */
if(loopClause != NIL(array_t)){
for(k=0; k < array_n(loopClause); k++){
/* if (searchArray(result, array_fetch(int, loopClause, k)) > -1){ */
if (st_lookup_int(resultTable, (char *)(long)array_fetch(int, loopClause, k), &tmp)){
loop = k;
break;
}
}
}
Ntk_NetworkForEachPrimaryOutput(network, gen, node){
array_insert_last(char*, outputs, Ntk_NodeReadName(node));
}
prevValueOutputs = ALLOC(int, array_n(outputs));
for (k=0; k< length; k++){
/* This will print latches whose name doesn't start with $_. The latches whose
name starts with $_ are latches added to the model by the aigtoblif translator.
*/
printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
latches, resultTable, k, prevValueLatches);
fprintf(vis_stdout, " ");
#if 0
(void) fprintf(vis_stdout, "--Primary output:\n");
printValue(manager, network, nodeToMvfAigTable, cnfClauses, outputs, result, k);
#endif
if((loop<0)||(k<length))
{
/* we augment the original .mv model with latches in front of inputs and hence
instead of inputs we print out the value of latches, this would have to be
restored in the final release */
printValueAigerInputs(manager, network, nodeToMvfAigTable, cnfClauses,
latches, resultTable, k, prevValueInputs);
fprintf(vis_stdout, " ");
/* the sat-solver doesn't propagate the values to output so we generate the output
1 knowing when ouptut would be 1, we will have to remove this for vis release */
if((k+1)==length)
{
fprintf(vis_stdout, "1 ");
}
else
{
fprintf(vis_stdout, "0 ");
}
printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
latches, resultTable, k+1, prevValueLatches);
}
if((loop < 0)||(k!=length))
{
fprintf(vis_stdout, "\n");
}
} /* for k loop */
if(loop != -1){
(void) fprintf(vis_stdout, "\n--Goes back to state %d:\n", loop);
printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
latches, resultTable, loop, prevValueLatches);
(void) fprintf(vis_stdout, "--On input:\n");
printValueAiger(manager, network, nodeToMvfAigTable, cnfClauses,
inputs, resultTable, length, prevValueInputs);
}
array_free(latches);
FREE(prevValueLatches);
if(options->printInputs == TRUE){
array_free(inputs);
FREE(prevValueInputs);
}
st_free_table(resultTable);
return;
} /* BmcPrintCounterExampleAiger() */
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* BmcReadFairnessConstraints | ( | FILE * | fp | ) |
Function********************************************************************
Synopsis [Read fairness constraints from file and check for errors.]
Description []
SideEffects []
SeeAlso []
Definition at line 2737 of file bmcUtil.c.
{
array_t *constraintArray; /* raw fairness constraints */
array_t *ltlConstraintArray; /* constraints converted to LTL */
if (fp == NIL(FILE) ) {
/* Nothing to be done. */
return NIL(array_t);
}
/* Read constraints from file and check for errors. */
constraintArray = Ctlsp_FileParseFormulaArray(fp);
if (constraintArray == NIL(array_t)) {
(void) fprintf(vis_stderr,
"** ctlsp error: error reading fairness constraints.\n");
return NIL(array_t);
}
if (array_n(constraintArray) == 0) {
(void) fprintf(vis_stderr, "** ctlsp error: fairness file is empty.\n");
return NIL(array_t);
}
/*
* Check that each constraint is an LTL formula.
*/
ltlConstraintArray = Ctlsp_FormulaArrayConvertToLTL(constraintArray);
Ctlsp_FormulaArrayFree(constraintArray);
if (ltlConstraintArray == NIL(array_t)) {
(void) fprintf(vis_stderr,
"** ctlsp error: fairness constraints are not LTL formulae.\n");
return NIL(array_t);
}
return ltlConstraintArray;
} /* BmcReadFairnessConstraints */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcWriteClauses | ( | mAig_Manager_t * | maigManager, |
| FILE * | cnfFile, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| BmcOption_t * | options | ||
| ) |
Function********************************************************************
Synopsis [Write the set of clauses in diamacs format to the output file.]
SideEffects []
Definition at line 1076 of file bmcUtil.c.
{
st_generator *stGen;
char *name;
int cnfIndex, i, k;
if (options->verbosityLevel == BmcVerbosityMax_c) {
fprintf(vis_stdout,
"Number of Variables = %d Number of Clauses = %d\n",
cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses);
}
st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) {
fprintf(cnfFile, "c %s %d\n",name, cnfIndex);
}
(void) fprintf(cnfFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1,
cnfClauses->noOfClauses);
if (cnfClauses->clauseArray != NIL(array_t)) {
for (i = 0; i < cnfClauses->nextIndex; i++) {
k = array_fetch(int, cnfClauses->clauseArray, i);
(void) fprintf(cnfFile, "%d%c", k, (k == 0) ? '\n' : ' ');
}
}
return;
}
Here is the caller graph for this function:
| static int nameCompare | ( | const void * | name1, |
| const void * | name2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Compare procedure for name comparison.]
Description [Compare procedure for name comparison.]
SideEffects []
Definition at line 2871 of file bmcUtil.c.
{
return(strcmp(*(char**)name1, *(char **)name2));
} /* end of signatureCompare */
Here is the caller graph for this function:
| static void printValue | ( | mAig_Manager_t * | manager, |
| Ntk_Network_t * | network, | ||
| st_table * | nodeToMvfAigTable, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| array_t * | varNames, | ||
| st_table * | resultTable, | ||
| int | state, | ||
| int * | prevValue | ||
| ) | [static] |
Function********************************************************************
Synopsis [Print the valuse of variables in the variable list "varNames".]
Description [For each variable in the variable list, this functions prints its value in the resultTable if it is different for its value in prevValue. If this variable is a symbolic variable, this function prints its symbolic value.]
SideEffects []
Definition at line 2894 of file bmcUtil.c.
{
Ntk_Node_t *node;
int i, j;
bAigEdge_t bAigId;
nameType_t *varName, *nodeName;
int value, index;
MvfAig_Function_t *MvfAig;
int changed = 0;
int tmp;
for (j=0; j< array_n(varNames); j++) {
if (state == 0){
prevValue[j] = -1;
}
nodeName = array_fetch(char *, varNames, j);
/*
Fetch the node corresponding to this node name.
*/
node = Ntk_NetworkFindNodeByName(network, nodeName);
/*
Get the multi-valued function for each node
*/
MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
/*
In case of the multi-valued function is not build for this node, do nothing.
We may notify the user.
*/
if (MvfAig == NIL(MvfAig_Function_t)){
continue;
}
/*
No CNF index for this variable at time "state in the "
*/
value = -1;
for (i=0; i< array_n(MvfAig); i++) {
bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
/*
constant value
*/
if (bAigId == bAig_One){
/*
This variable equal the constant i.
*/
value = i;
break;
}
if (bAigId != bAig_Zero){
char *tmpStr;
nodeName = bAig_NodeReadName(manager, bAigId);
/*
Build the variable name at state "state".
*/
tmpStr = util_inttostr(state);
varName = util_strcat3(nodeName, "_", tmpStr);
if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
if (bAig_IsInverted(bAigId)){
index = -index;
}
/*if (searchArray(result, index) > -1){*/
if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
value = i;
break;
}
} /* if st_lookup_int() */
FREE(tmpStr);
FREE(varName);
} /* if (bAigId != bAig_Zero) */
}
if (value >= 0){
if (value != prevValue[j]){
Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
prevValue[j] = value;
changed = 1;
if (Var_VariableTestIsSymbolic(nodeVar)) {
char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
(void) fprintf(vis_stdout,"%s:%s\n", Ntk_NodeReadName(node), symbolicValue);
}
else {
(void) fprintf(vis_stdout,"%s:%d\n", Ntk_NodeReadName(node), value);
}
}
} else {
/*
This variable does not have value in the current time frame. It means its value
is not important at this time frame.
*/
(void) fprintf(vis_stdout,"%s:X\n", Ntk_NodeReadName(node));
}
} /* for j loop */
if (changed == 0){
fprintf( vis_stdout, "<Unchanged>\n");
}
}/* end of printValue() */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void printValueAiger | ( | mAig_Manager_t * | manager, |
| Ntk_Network_t * | network, | ||
| st_table * | nodeToMvfAigTable, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| array_t * | varNames, | ||
| st_table * | resultTable, | ||
| int | state, | ||
| int * | prevValue | ||
| ) | [static] |
Function********************************************************************
Synopsis [Print the valuse of variables in the variable list "varNames".]
Description [For each variable in the variable list, this functions prints the values of names, which do not start with $_ as these are true latches of the model. Since this is in aiger format, hence all the values are printed even if they didn't change from the previous values.]
SideEffects []
Definition at line 3017 of file bmcUtil.c.
{
Ntk_Node_t *node;
int i, j;
bAigEdge_t bAigId;
nameType_t *varName, *nodeName;
int value, index;
MvfAig_Function_t *MvfAig;
int tmp;
char * NodeName;
for (j=0; j< array_n(varNames); j++) {
if (state == 0){
prevValue[j] = -1;
}
nodeName = array_fetch(char *, varNames, j);
/*
Fetch the node corresponding to this node name.
*/
node = Ntk_NetworkFindNodeByName(network, nodeName);
/*
Get the multi-valued function for each node
*/
MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
/*
In case of the multi-valued function is not build for this node, do nothing.
We may notify the user.
*/
if (MvfAig == NIL(MvfAig_Function_t)){
continue;
}
/*
No CNF index for this variable at time "state in the "
*/
value = -1;
for (i=0; i< array_n(MvfAig); i++) {
bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
/*
constant value
*/
if (bAigId == bAig_One){
/*
This variable equal the constant i.
*/
value = i;
break;
}
if (bAigId != bAig_Zero){
char *tmpStr;
nodeName = bAig_NodeReadName(manager, bAigId);
/*
Build the variable name at state "state".
*/
tmpStr = util_inttostr(state);
varName = util_strcat3(nodeName, "_", tmpStr);
if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
if (bAig_IsInverted(bAigId)){
index = -index;
}
/*if (searchArray(result, index) > -1){*/
if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
value = i;
break;
}
} /* if st_lookup_int() */
FREE(tmpStr);
FREE(varName);
} /* if (bAigId != bAig_Zero) */
}
NodeName = Ntk_NodeReadName(node);
if(!((NodeName[0] == '$') && (NodeName[1] == '_')))
{
if (value >= 0){
Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
prevValue[j] = value;
if (Var_VariableTestIsSymbolic(nodeVar)) {
char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
(void) fprintf(vis_stdout,"%s", symbolicValue);
}
else {
(void) fprintf(vis_stdout,"%d", value);
}
} else {
/*
This variable does not have value in the current time frame. It means its value
is not important at this time frame.
*/
(void) fprintf(vis_stdout,"x" );
}
} /* these nodes are latches in front of inputs so they will be printed out as inputs */
} /* for j loop */
}/* end of printValueAiger() */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void printValueAigerInputs | ( | mAig_Manager_t * | manager, |
| Ntk_Network_t * | network, | ||
| st_table * | nodeToMvfAigTable, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| array_t * | varNames, | ||
| st_table * | resultTable, | ||
| int | state, | ||
| int * | prevValue | ||
| ) | [static] |
Function********************************************************************
Synopsis [Print the valuse of variables in the variable list "varNames".]
Description [For each variable in the variable list, this functions checks if the name starts with $_, which means that those latches are actually storing the value of inputs. This modification to the model is externally done and not done by VIS so this method is only specific to certain type of model, the output of aigtoblif translator.]
SideEffects []
Definition at line 3137 of file bmcUtil.c.
{
Ntk_Node_t *node;
int i, j;
bAigEdge_t bAigId;
nameType_t *varName, *nodeName;
int value, index;
MvfAig_Function_t *MvfAig;
int tmp;
char * NodeName;
for (j=0; j< array_n(varNames); j++) {
if (state == 0){
prevValue[j] = -1;
}
nodeName = array_fetch(char *, varNames, j);
/*
Fetch the node corresponding to this node name.
*/
node = Ntk_NetworkFindNodeByName(network, nodeName);
/*
Get the multi-valued function for each node
*/
MvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
/*
In case of the multi-valued function is not build for this node, do nothing.
We may notify the user.
*/
if (MvfAig == NIL(MvfAig_Function_t)){
continue;
}
/*
No CNF index for this variable at time "state in the "
*/
value = -1;
for (i=0; i< array_n(MvfAig); i++) {
bAigId = MvfAig_FunctionReadComponent(MvfAig, i);
/*
constant value
*/
if (bAigId == bAig_One){
/*
This variable equal the constant i.
*/
value = i;
break;
}
if (bAigId != bAig_Zero){
char *tmpStr;
nodeName = bAig_NodeReadName(manager, bAigId);
/*
Build the variable name at state "state".
*/
tmpStr = util_inttostr(state);
varName = util_strcat3(nodeName, "_", tmpStr);
if (st_lookup_int(cnfClauses->cnfIndexTable, varName, &index)) {
if (bAig_IsInverted(bAigId)){
index = -index;
}
/*if (searchArray(result, index) > -1){*/
if (st_lookup_int(resultTable, (char *)(long)index, &tmp)){
value = i;
break;
}
} /* if st_lookup_int() */
FREE(tmpStr);
FREE(varName);
} /* if (bAigId != bAig_Zero) */
}
NodeName = Ntk_NodeReadName(node);
if((NodeName[0] == '$') && (NodeName[1] == '_'))
{
if (value >= 0){
Var_Variable_t *nodeVar = Ntk_NodeReadVariable(node);
prevValue[j] = value;
if (Var_VariableTestIsSymbolic(nodeVar)) {
char *symbolicValue = Var_VariableReadSymbolicValueFromIndex(nodeVar, value);
(void) fprintf(vis_stdout,"%s", symbolicValue);
}
else {
(void) fprintf(vis_stdout,"%d", value);
}
} else {
/*
This variable does not have value in the current time frame. It means its value
is not important at this time frame.
*/
(void) fprintf(vis_stdout,"x" );
}
} /* these nodes are latches in front of inputs so they will be printed out as inputs */
} /* for j loop */
}/* end of printValueAigerInputs() */
Here is the call graph for this function:
Here is the caller graph for this function:
| static int StringCheckIsInteger | ( | char * | string, |
| int * | value | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Test that the given string is an integer. Returns 0 if string is not an integer, 1 if the integer is too big for int, and 2 if integer fits in int.]
SideEffects [Sets the pointer value if the string is an integer small enough for int.]
Definition at line 2845 of file bmcUtil.c.
{
char *ptr;
long l;
l = strtol (string, &ptr, 0) ;
if(*ptr != '\0')
return 0;
if ((l > MAXINT) || (l < -1 - MAXINT))
return 1 ;
*value = (int) l;
return 2 ;
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: bmcUtil.c,v 1.82 2010/04/10 04:07:06 fabio Exp $" [static] |
CFile***********************************************************************
FileName [bmcUtil.c]
PackageName [bmc]
Synopsis [Utilities for BMC package]
Author [Mohammad Awedh]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
