#include "bmc.h"#include "bmcInt.h"
Include dependency graph for bmcAutSat.c:
Go to the source code of this file.
Functions | |
| int | BmcAutLtlCheckForTermination (Ntk_Network_t *network, array_t *constraintArray, BmcCheckForTermination_t *terminationStatus, st_table *nodeToMvfAigTable, st_table *CoiTable, BmcOption_t *options) |
| void | BmcAutCnfGenerateClausesForPath (Ltl_Automaton_t *automaton, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses) |
| void | BmcAutCnfGenerateClausesForSimpleCompositePath (Ntk_Network_t *network, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) |
| void | BmcCnfNoLoopToAnyPreviouseCompositeStates (Ntk_Network_t *network, Ltl_Automaton_t *automaton, int fromState, int toState, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable, st_table *CoiTable) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: bmcAutSat.c,v 1.10 2005/04/16 18:02:25 awedh Exp $" |
Function Documentation
| void BmcAutCnfGenerateClausesForPath | ( | Ltl_Automaton_t * | automaton, |
| int | fromState, | ||
| int | toState, | ||
| int | initialState, | ||
| BmcCnfClauses_t * | cnfClauses | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF clauses that describe a path in the automaton.]
Description [Generate CNF clauses for a path in the automaton starting from "fromState" and ending at "toState". If "initialState" = BMC_INITIAL_STATES, the the path starts from an initial state.]
SideEffects []
SeeAlso []
Definition at line 502 of file bmcAutSat.c.
{
int k;
array_t *unitClause = array_alloc(int, 1);
if(initialState){
array_insert(int, unitClause, 0,
BmcAutGenerateCnfForBddOffSet(automaton->initialStates, 0, 0, cnfClauses, automaton->nsPsTable)
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
for(k=fromState; k<toState; k++){
array_insert(int, unitClause, 0,
BmcAutGenerateCnfForBddOffSet(automaton->transitionRelation, k, k+1, cnfClauses, automaton->nsPsTable)
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
array_free(unitClause);
} /* BmcAutCnfGenerateClausesForPath() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcAutCnfGenerateClausesForSimpleCompositePath | ( | Ntk_Network_t * | network, |
| Ltl_Automaton_t * | automaton, | ||
| int | fromState, | ||
| int | toState, | ||
| int | initialState, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF clauses for a simple path in the composite model]
Description [This function generates CNF clauses for a simple path from state "fromState" to state "toState" in the composition of network and automaton. A simple path is a path along which every state in the path is distinct. If Si and Sj in the path then Si != Sj.
If the value of "initialState" is BMC_INITIAL_STATES, then the path is an initialized path. Otherwise "initialState" is BMC_NO_INITIAL_STATES.]
SideEffects []
SeeAlso []
Definition at line 550 of file bmcAutSat.c.
{
int state;
/*
Generate clauses for a path from fromState to toState in the original model.
*/
BmcCnfGenerateClausesForPath(network, fromState, toState, initialState, cnfClauses, nodeToMvfAigTable, CoiTable);
/*
Generate clauses for a path from fromState to toState in the Automaton.
*/
BmcAutCnfGenerateClausesForPath(automaton, fromState, toState, initialState, cnfClauses);
/*
Restrict the above path to be simpe path.
*/
for(state= fromState + 1; state < toState; state++){
BmcCnfNoLoopToAnyPreviouseCompositeStates(network, automaton, fromState, state,
cnfClauses, nodeToMvfAigTable, CoiTable);
}
return;
} /* BmcAutCnfGenerateClausesForSimpleCompositePath */
Here is the call graph for this function:
Here is the caller graph for this function:
| int BmcAutLtlCheckForTermination | ( | Ntk_Network_t * | network, |
| array_t * | constraintArray, | ||
| BmcCheckForTermination_t * | terminationStatus, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable, | ||
| BmcOption_t * | options | ||
| ) |
AutomaticStart AutomaticEnd Function********************************************************************
Synopsis [Verify the general LTL formula passes by applying the termination criteria that are described in the paper "Proving More Properties with Bounded Model Checking"]
Description [Check for the termination on the composition of the automaton that describes the negation of the LTL formula and the model. We apply the termination criteria as described in the paper "Proving More Properties with Bounded Model Checking".]
Return value: -1 error in running BMC 0 no action 1 (m+n-1) <= options->maxK. If no counterexample of length up to (m+n-1), the property passes 2 (m+n-1) > options->maxK The property is undecided if no counterexample of length <= options->maxK. 3 Pass by early termination
SideEffects []
SeeAlso []
Definition at line 86 of file bmcAutSat.c.
{
BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t);
FILE *cnfFile;
array_t *result = NIL(array_t);
array_t *unitClause = array_alloc(int, 0);
array_t *orClause;
long startTime, endTime;
int k = terminationStatus->k;
int returnStatus = 0;
Ltl_Automaton_t *automaton = terminationStatus->automaton;
/*
If checkLevel == 0 --> check for beta' only and if UNSAT, m=k and chekLevel =1
If checkLevel == 1 --> check for beta only and if UNSAT, checkLevel = 2.
If checkLevel == 2 --> check for alpha only and if UNSAT, n=k and checkLevel = 3.
If gama is UNSAT up to (m+n-1) and checkLvel = 3, formula passes.
checkLevel = 4 if (m+n-1) > maxK;
*/
startTime = util_cpu_ctime();
/* ===========================
Early termination condition
=========================== */
if (options->earlyTermination) {
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
}
/*
Create clauses database
*/
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return -1;
}
BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
BmcCnfClausesFree(cnfClauses);
result = BmcCheckSAT(options);
if(options->satSolverError){
return -1;
}
if(result == NIL(array_t)) {
(void) fprintf(vis_stdout, "# BMC: by early ermination\n");
return 3;
}
} /* Early termination */
if((!automaton->fairSets) &&
(terminationStatus->checkLevel == 0)) {
/*
All the automaton states are fair states. So, beta' and beta are always UNSAT.
*/
terminationStatus->m = 0;
(void) fprintf(vis_stdout,"Value of m = %d\n", terminationStatus->m);
terminationStatus->checkLevel = 2;
}
/*
beta''(k)
*/
if(terminationStatus->checkLevel == 0){
int i;
/*
Create clauses database
*/
cnfClauses = BmcCnfClausesAlloc();
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta'' \n");
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return -1;
}
BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
for(i=1; i<=k+1; i++){
if(constraintArray != NIL(array_t)){
Ctlsp_Formula_t *formula;
int j;
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
array_insert(int, unitClause, 0,
- BmcGenerateCnfForLtl(network, formula, i, i, -1, cnfClauses)
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
}
array_insert(int, unitClause, 0,
- BmcAutGenerateCnfForBddOffSet(automaton->fairSets, i, i, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
if(constraintArray != NIL(array_t)){
Ctlsp_Formula_t *formula;
int j;
orClause = array_alloc(int, 0);
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
array_insert_last(int, orClause,
BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
);
}
array_insert_last(int, orClause,
BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
} else {
array_insert(int, unitClause, 0,
BmcAutGenerateCnfForBddOffSet(automaton->fairSets, 0, 0, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if(options->satSolverError){
return -1;
}
if(result == NIL(array_t)) {
terminationStatus->m = k;
(void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
terminationStatus->checkLevel = 1;
}
BmcCnfClausesFree(cnfClauses);
} /* Check for Beta' */
/*
beta'(k)
*/
if(terminationStatus->checkLevel == 0){
int i;
/*
Create clauses database
*/
cnfClauses = BmcCnfClausesAlloc();
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta' \n");
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return -1;
}
BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
for(i=0; i<=k; i++){
if(constraintArray != NIL(array_t)){
Ctlsp_Formula_t *formula;
int j;
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
array_insert(int, unitClause, 0,
- BmcGenerateCnfForLtl(network, formula, i, i, -1, cnfClauses)
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
}
array_insert(int, unitClause, 0,
- BmcAutGenerateCnfForBddOffSet(automaton->fairSets, i, i, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
if(constraintArray != NIL(array_t)){
Ctlsp_Formula_t *formula;
int j;
orClause = array_alloc(int, 0);
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
array_insert_last(int, orClause,
BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
);
}
array_insert_last(int, orClause,
BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
} else {
array_insert(int, unitClause, 0,
BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if(options->satSolverError){
return -1;
}
if(result == NIL(array_t)) {
terminationStatus->m = k;
(void)fprintf(vis_stdout,"Value of m = %d\n", terminationStatus->m);
terminationStatus->checkLevel = 1;
}
BmcCnfClausesFree(cnfClauses);
} /* Check for Beta' */
/*
Check for Beta.
*/
if(terminationStatus->checkLevel == 1){
cnfClauses = BmcCnfClausesAlloc();
{/* To print a witness */
/* lsGen lsGen;
vertex_t *vtx;
Ltl_AutomatonNode_t *state;
int i;
foreach_vertex(automaton->G, lsGen, vtx) {
state = (Ltl_AutomatonNode_t *) vtx->user_data;
state->cnfIndex = ALLOC(int, k+2);
for(i=0; i<=k+1; i++){
state->cnfIndex[i] = BmcAutGenerateCnfForBddOffSet(state->Encode, i,
i, cnfClauses, NIL(st_table));
}
} */
}/* To print a witness */
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta\n");
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return -1;
}
/*
Generate a simple path of length k+1.
*/
BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k+1, BMC_NO_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable,
CoiTable);
if(constraintArray != NIL(array_t)){
Ctlsp_Formula_t *formula;
int j;
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
array_insert(int, unitClause, 0,
- BmcGenerateCnfForLtl(network, formula, k, k, -1, cnfClauses)
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
}
array_insert(int, unitClause, 0,
- BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, unitClause);
if(constraintArray != NIL(array_t)){
Ctlsp_Formula_t *formula;
int j;
orClause = array_alloc(int, 0);
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
array_insert_last(int, orClause,
BmcGenerateCnfForLtl(network, formula, k+1, k+1, -1, cnfClauses)
);
}
array_insert_last(int, orClause,
BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
} else {
array_insert(int, unitClause, 0,
BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k+1, k+1, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
if(options->satSolverError){
return -1;
}
if(result == NIL(array_t)) {
terminationStatus->checkLevel = 2;
}
BmcCnfClausesFree(cnfClauses);
} /* Check Beta*/
if(terminationStatus->checkLevel == 2){ /* we check Alpha if Beta is unsatisfiable */
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Alpha \n");
}
cnfClauses = BmcCnfClausesAlloc();
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
(void)fprintf(vis_stderr,
"** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return -1;
}
BmcAutCnfGenerateClausesForSimpleCompositePath(network, automaton, 0, k, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, CoiTable);
if(automaton->fairSets){
if(constraintArray != NIL(array_t)){
Ctlsp_Formula_t *formula;
int j;
orClause = array_alloc(int, 0);
arrayForEachItem(Ctlsp_Formula_t *, constraintArray, j, formula) {
array_insert_last(int, orClause,
BmcGenerateCnfForLtl(network, formula, k, k, -1, cnfClauses)
);
}
array_insert_last(int, orClause,
BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
} else {
array_insert(int, unitClause, 0,
BmcAutGenerateCnfForBddOffSet(automaton->fairSets, k, k, cnfClauses, NIL(st_table))
);
BmcCnfInsertClause(cnfClauses, unitClause);
}
}
BmcWriteClauses(NIL(mAig_Manager_t), cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
BmcCnfClausesFree(cnfClauses);
if(options->satSolverError){
return -1;
}
if(result == NIL(array_t)) {
terminationStatus->n = k;
terminationStatus->checkLevel = 3;
(void)fprintf(vis_stderr,"m=%d n=%d\n",terminationStatus->m,terminationStatus->n);
if ((terminationStatus->m+terminationStatus->n-1) <= options->maxK){
terminationStatus->k = terminationStatus->m+terminationStatus->n-1;
if(k==0){
/*
By induction, the property passes.
*/
terminationStatus->k = 0;
}
returnStatus = 1;
} else {
terminationStatus->checkLevel = 4;
returnStatus = 2;
}
}
}/* Chek for Alpha */
array_free(unitClause);
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
return returnStatus;
} /* BmcAutLtlCheckForTermination */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCnfNoLoopToAnyPreviouseCompositeStates | ( | Ntk_Network_t * | network, |
| Ltl_Automaton_t * | automaton, | ||
| int | fromState, | ||
| int | toState, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Generate CNF clauses for no loop from last state to any of the previouse states of the path]
Description [Generate CNF 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 previous states.]
SideEffects []
SeeAlso []
Definition at line 599 of file bmcAutSat.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
bdd_manager *bddManager = bdd_get_manager(automaton->transitionRelation);
Ntk_Node_t *latch;
MvfAig_Function_t *latchMvfAig;
bAigEdge_t *latchBAig;
array_t *orClause;
int currentIndex, nextIndex, andIndex1, andIndex2;
int i, k, mvfSize, bddID;
st_generator *stGen;
/*
Generates CNF clauses to constrain that 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++){
currentIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], k ,cnfClauses);
nextIndex = BmcGenerateCnfFormulaForAigFunction(manager, latchBAig[i], toState ,cnfClauses);
andIndex1 = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesForAND(currentIndex, -nextIndex, andIndex1, cnfClauses);
andIndex2 = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesForAND(-currentIndex, nextIndex, andIndex2, cnfClauses);
array_insert_last(int, orClause, andIndex1);
array_insert_last(int, orClause, andIndex2);
}
FREE(latchBAig);
}/* For each latch loop*/
st_foreach_item(automaton->psNsTable, stGen, &bddID, NULL) {
currentIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_bdd_ith_var(bddManager, bddID)),
k, cnfClauses);
nextIndex = BmcGetCnfVarIndexForBddNode(bddManager, bdd_regular(bdd_bdd_ith_var(bddManager, bddID)),
toState, cnfClauses);
andIndex1 = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesForAND(currentIndex, -nextIndex, andIndex1, cnfClauses);
andIndex2 = cnfClauses->cnfGlobalIndex++;
BmcCnfGenerateClausesForAND(-currentIndex, nextIndex, andIndex2, cnfClauses);
array_insert_last(int, orClause, andIndex1);
array_insert_last(int, orClause, andIndex2);
}
BmcCnfInsertClause(cnfClauses, orClause);
array_free(orClause);
} /* foreach k*/
return;
} /* BmcCnfNoLoopToAnyPreviouseCompositeStates */
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: bmcAutSat.c,v 1.10 2005/04/16 18:02:25 awedh Exp $" [static] |
CFile***********************************************************************
FileName [bmcAutSat.c]
PackageName [bmc]
Synopsis [Automaton for BMC]
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.]
Definition at line 20 of file bmcAutSat.c.
