#include "bmcInt.h"#include "sat.h"
Include dependency graph for bmcCirCUsUtil.c:
Go to the source code of this file.
Defines | |
| #define | MAX_LENGTH 320 |
Functions | |
| static char * | getBddName (bdd_manager *bddManager, bdd_node *node) |
| static bAigEdge_t | getAigAtTimeFrame (bAig_Manager_t *manager, bAigEdge_t node, int i, int withInitialState) |
| static bAigEdge_t | getAigOfBddAtState (Ntk_Network_t *network, bdd_node *node, int state, int withInitialState) |
| void | BmcCirCUsAutLtlCheckTerminalAutomaton (Ntk_Network_t *network, bAig_Manager_t *aigManager, st_table *nodeToMvfAigTable, BmcCheckForTermination_t *terminationStatus, st_table *coiIndexTable, BmcOption_t *options) |
| bAigEdge_t | BmcCirCUsBdd2Aig (Ntk_Network_t *network, bdd_t *function, int current, int next, Ltl_Automaton_t *automaton, bAig_Manager_t *aigManager, int withInitialState) |
| bAigEdge_t | BmcCirCUsAutCreateAigForPath (Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState) |
| bAigEdge_t | BmcCirCUsAutCreateAigForSimplePath (Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState) |
| bAigEdge_t | BmcCirCUsCreateAigForSimpleCompositePath (Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, st_table *nodeToMvfAigTable, st_table *coiIndexTable, int initialState) |
| void | BmcCirCUsAutLtlCheckForTermination (Ntk_Network_t *network, bAig_Manager_t *aigManager, st_table *nodeToMvfAigTable, BmcCheckForTermination_t *terminationStatus, st_table *coiIndexTable, BmcOption_t *options) |
| char * | BmcCirCUsCallCirCUs (BmcOption_t *options) |
| char * | BmcCirCUsCallCusp (BmcOption_t *options) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: bmcCirCUsUtil.c,v 1.22 2010/04/10 04:07:06 fabio Exp $" |
Define Documentation
| #define MAX_LENGTH 320 |
Definition at line 26 of file bmcCirCUsUtil.c.
Function Documentation
| bAigEdge_t BmcCirCUsAutCreateAigForPath | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | aigManager, | ||
| Ltl_Automaton_t * | automaton, | ||
| int | fromState, | ||
| int | toState, | ||
| int | initialState | ||
| ) |
Function********************************************************************
Synopsis [Build AIG for a path in the automaton.]
Description [Build AIG for a path in the automaton starting from "fromState" and ending at "toState". If "initialState" = BMC_INITIAL_STATES, then the path starts from an initial state.]
SideEffects []
SeeAlso []
Definition at line 252 of file bmcCirCUsUtil.c.
{
int k;
bAigEdge_t result, aigFunction = bAig_One;
if(initialState){
result = BmcCirCUsBdd2Aig(network, automaton->initialStates, 0, -1,
automaton, aigManager, initialState);
aigFunction = result;
}
for(k=fromState; k<toState; k++){
result = BmcCirCUsBdd2Aig(network, automaton->transitionRelation, k, k+1,
automaton, aigManager, initialState);
aigFunction = bAig_And(aigManager , aigFunction, result);
}
return aigFunction;
} /* BmcCirCUsAutCreateAigForPath */
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsAutCreateAigForSimplePath | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | aigManager, | ||
| Ltl_Automaton_t * | automaton, | ||
| int | fromState, | ||
| int | toState, | ||
| int | initialState | ||
| ) |
Function********************************************************************
Synopsis [Build AIG for a simple path in the automaton.]
Description [Build AIG a simple 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 291 of file bmcCirCUsUtil.c.
{
int i, j, bddID;
bAigEdge_t result, aigFunction, next, current;
mdd_manager *bddManager = Ntk_NetworkReadMddManager(network);
st_generator *stGen;
bdd_node *node;
aigFunction = BmcCirCUsAutCreateAigForPath(network, aigManager, automaton,
fromState, toState, initialState);
/*
The path is simple path
*/
for(i = fromState + 1; i <= toState; i++){
for(j=fromState; j < i; j++){
result = bAig_Zero;
st_foreach_item(automaton->psNsTable, stGen,&bddID, NULL) {
node = bdd_bdd_ith_var(bddManager, bddID);
current = getAigOfBddAtState(network, node, i, initialState);
next = getAigOfBddAtState(network, node, j, initialState);
result = bAig_Or(aigManager, result,
bAig_Not(bAig_Eq(aigManager, current, next)));
}
aigFunction = bAig_And(aigManager, aigFunction, result);
}
}
return aigFunction;
} /* BmcCirCUsAutCreateAigForSimplePath */
Here is the call graph for this function:
| void BmcCirCUsAutLtlCheckForTermination | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | aigManager, | ||
| st_table * | nodeToMvfAigTable, | ||
| BmcCheckForTermination_t * | terminationStatus, | ||
| st_table * | coiIndexTable, | ||
| BmcOption_t * | options | ||
| ) |
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: 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 448 of file bmcCirCUsUtil.c.
{
long startTime, endTime;
int k = terminationStatus->k;
int returnStatus = 0;
Ltl_Automaton_t *automaton = terminationStatus->automaton;
Ctlsp_Formula_t *externalConstraints = terminationStatus->externalConstraints;
satInterface_t *tInterface, *etInterface;
bAigEdge_t autPath, property, tmp;
array_t *objArray;
array_t *previousResultArray;
array_t *previousResultArrayWOI;
/*
If checkLevel == 0 --> check for beta' and beta'' only and if either 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();
etInterface = 0;
tInterface = 0;
/*
Hold objects
*/
objArray = array_alloc(bAigEdge_t, 2);
previousResultArray = array_alloc(bAigEdge_t, 0);
previousResultArrayWOI = array_alloc(bAigEdge_t, 0);
/* ===========================
Early termination condition
===========================
*/
if (options->earlyTermination) {
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
}
autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
0, k, nodeToMvfAigTable,
coiIndexTable,
BMC_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 0, autPath);
array_insert(bAigEdge_t, objArray, 1, bAig_One);
options->cnfPrefix = k;
etInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
previousResultArray, options, etInterface);
if(etInterface->status == SAT_UNSAT){
(void) fprintf(vis_stdout, "# BMC: by early termination\n");
terminationStatus->action = 3;
return;
}
} /* 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;
printf("Value of m = %d\n", terminationStatus->m);
terminationStatus->checkLevel = 2;
}
/*
Check \beta''(k)
*/
if(terminationStatus->checkLevel == 0){
int i;
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta''\n");
}
autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
0, k+1, nodeToMvfAigTable,
coiIndexTable, BMC_NO_INITIAL_STATES);
property = bAig_One;
for(i=1; i<=k+1; i++){
tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, i, -1,
automaton, aigManager,
BMC_NO_INITIAL_STATES);
if(externalConstraints){
tmp = bAig_Or(aigManager, tmp,
BmcCirCUsCreatebAigOfPropFormula(network, aigManager, i,
externalConstraints,
BMC_NO_INITIAL_STATES));
}
property = bAig_And(aigManager, property, bAig_Not(tmp));
}
tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, 0, -1,
automaton, aigManager, BMC_NO_INITIAL_STATES);
if(externalConstraints){
tmp = bAig_Or(aigManager, tmp,
BmcCirCUsCreatebAigOfPropFormula(network, aigManager, 0,
externalConstraints,
BMC_NO_INITIAL_STATES));
}
property = bAig_And(aigManager, property, tmp);
options->cnfPrefix = k+1;
array_insert(bAigEdge_t, objArray, 0, property);
array_insert(bAigEdge_t, objArray, 1, autPath);
tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
previousResultArray, options, tInterface);
if(tInterface->status == SAT_UNSAT){
terminationStatus->m = k;
(void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
terminationStatus->checkLevel = 1;
}
} /* Check for Beta'' */
/*
Check \beta'(k)
*/
if(terminationStatus->checkLevel == 0){
int i;
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta'\n");
}
autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
0, k+1, nodeToMvfAigTable,
coiIndexTable, BMC_NO_INITIAL_STATES);
property = bAig_One;
for(i=0; i<=k; i++){
tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, i, -1,
automaton, aigManager,
BMC_NO_INITIAL_STATES);
if(externalConstraints){
tmp = bAig_Or(aigManager, tmp,
BmcCirCUsCreatebAigOfPropFormula(network, aigManager, i,
externalConstraints,
BMC_NO_INITIAL_STATES));
}
property = bAig_And(aigManager, property, bAig_Not(tmp));
}
tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
automaton, aigManager,
BMC_NO_INITIAL_STATES);
if(externalConstraints){
tmp = bAig_Or(aigManager, tmp,
BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k+1,
externalConstraints,
BMC_NO_INITIAL_STATES));
}
property = bAig_And(aigManager, property, tmp);
options->cnfPrefix = k+1;
array_insert(bAigEdge_t, objArray, 0, property);
array_insert(bAigEdge_t, objArray, 1, autPath);
tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
previousResultArray, options, tInterface);
if(tInterface->status == SAT_UNSAT){
terminationStatus->m = k;
(void)fprintf(vis_stderr,"m = %d\n", terminationStatus->m);
terminationStatus->checkLevel = 1;
}
} /* Check for Beta' */
/*
Check for Beta.
*/
if(terminationStatus->checkLevel == 1){
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "# BMC: Check Beta\n");
}
autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
0, k+1, nodeToMvfAigTable,
coiIndexTable, BMC_NO_INITIAL_STATES);
property = bAig_One;
tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
automaton, aigManager, BMC_NO_INITIAL_STATES);
if(externalConstraints){
tmp = bAig_Or(aigManager, tmp,
BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k,
externalConstraints,
BMC_NO_INITIAL_STATES));
}
property = bAig_And(aigManager, property, bAig_Not(tmp));
tmp = BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
automaton, aigManager, BMC_NO_INITIAL_STATES);
if(externalConstraints){
tmp = bAig_Or(aigManager, tmp,
BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k+1,
externalConstraints,
BMC_NO_INITIAL_STATES));
}
property = bAig_And(aigManager, property, tmp);
options->cnfPrefix = k+1;
array_insert(bAigEdge_t, objArray, 0, property);
array_insert(bAigEdge_t, objArray, 1, autPath);
tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
previousResultArray, options, tInterface);
if(tInterface->status == SAT_UNSAT){
terminationStatus->checkLevel = 2;
}
} /* 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");
}
autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
0, k, nodeToMvfAigTable,
coiIndexTable,
BMC_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 1, bAig_One);
property = bAig_Zero;
if(automaton->fairSets){
property = BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
automaton, aigManager, BMC_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 1, property);
}
if(externalConstraints){
property = bAig_Or(aigManager, property,
BmcCirCUsCreatebAigOfPropFormula(network, aigManager, k,
externalConstraints,
BMC_INITIAL_STATES));
array_insert(bAigEdge_t, objArray, 1, property);
}
options->cnfPrefix = k;
array_insert(bAigEdge_t, objArray, 0, autPath);
tInterface = 0;
tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network,
objArray, previousResultArray,
options, tInterface);
if(tInterface->status == SAT_UNSAT){
terminationStatus->n = k;
terminationStatus->checkLevel = 3;
(void)fprintf(vis_stdout,"Value of 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 */
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
terminationStatus->action = returnStatus;
} /* BmcAutLtlCheckForTermination */
Here is the call graph for this function:
Here is the caller graph for this function:
| void BmcCirCUsAutLtlCheckTerminalAutomaton | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | aigManager, | ||
| st_table * | nodeToMvfAigTable, | ||
| BmcCheckForTermination_t * | terminationStatus, | ||
| st_table * | coiIndexTable, | ||
| BmcOption_t * | options | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Check for termination for safety properties.]
Description [Check for termination for safety properties.] SideEffects []
SeeAlso []
Definition at line 71 of file bmcCirCUsUtil.c.
{
long startTime, endTime;
int k = terminationStatus->k;
int returnStatus = 0;
Ltl_Automaton_t *automaton = terminationStatus->automaton;
satInterface_t *tInterface, *etInterface;
bAigEdge_t autPath, property;
array_t *objArray;
array_t *previousResultArray;
startTime = util_cpu_ctime();
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nBMC: Check for termination\n");
}
etInterface = 0;
tInterface = 0;
/*
Hold objects
*/
objArray = array_alloc(bAigEdge_t, 2);
previousResultArray = array_alloc(bAigEdge_t, 0);
returnStatus = 0;
autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
0, k+1, nodeToMvfAigTable,
coiIndexTable,
BMC_NO_INITIAL_STATES);
property = bAig_Not(
BmcCirCUsBdd2Aig(network, automaton->fairSets, k, -1,
automaton, aigManager, BMC_NO_INITIAL_STATES));
property = bAig_And(aigManager, property,
BmcCirCUsBdd2Aig(network, automaton->fairSets, k+1, -1,
automaton, aigManager, BMC_NO_INITIAL_STATES));
options->cnfPrefix = k+1;
array_insert(bAigEdge_t, objArray, 0, property);
array_insert(bAigEdge_t, objArray, 1, autPath);
tInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
previousResultArray, options, tInterface);
if(tInterface->status == SAT_UNSAT){
returnStatus = 1;
}
/* ===========================
Early termination condition
===========================
*/
if ((options->earlyTermination)&&(returnStatus ==0)) {
if (options->verbosityLevel == BmcVerbosityMax_c) {
(void) fprintf(vis_stdout, "\nChecking the early termination at k= %d\n", k);
}
autPath = BmcCirCUsCreateAigForSimpleCompositePath(network, aigManager, automaton,
0, k+1, nodeToMvfAigTable,
coiIndexTable,
BMC_INITIAL_STATES);
array_insert(bAigEdge_t, objArray, 0, autPath);
array_insert(bAigEdge_t, objArray, 1, bAig_One);
options->cnfPrefix = k+1;
etInterface = BmcCirCUsInterfaceWithObjArr(aigManager, network, objArray,
previousResultArray, options, etInterface);
if(etInterface->status == SAT_UNSAT){
(void) fprintf(vis_stdout, "# BMC: by early termination\n");
returnStatus = 1;
}
} /* Early termination */
if (options->verbosityLevel != BmcVerbosityNone_c) {
endTime = util_cpu_ctime();
fprintf(vis_stdout, "-- Check for termination time time = %10g\n",
(double)(endTime - startTime) / 1000.0);
}
array_free(objArray);
array_free(previousResultArray);
terminationStatus->action = returnStatus;
} /* BmcCirCUsAutLtlCheckTerminalAutomaton */
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsBdd2Aig | ( | Ntk_Network_t * | network, |
| bdd_t * | function, | ||
| int | current, | ||
| int | next, | ||
| Ltl_Automaton_t * | automaton, | ||
| bAig_Manager_t * | aigManager, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Build AIG for a given function in BDD at a given time period]
Description [Build AIG for a BDD at a time period. If next != -1, then the passed BDD represents a transition relation.]
SideEffects []
SeeAlso [BmcAutEncodeAutomatonStates BmcAutBuildTransitionRelation]
Definition at line 175 of file bmcCirCUsUtil.c.
{
bdd_manager *bddManager;
bdd_node *node;
bdd_gen *gen;
array_t *cube;
int i, value;
int state = current;
bAigEdge_t aigFunction, andFunction, aigNode;
if (function == NULL){
return bAig_NULL;
}
/*
If BDD represents a constant value
*/
if(bdd_is_tautology(function, 0)){
return bAig_Zero;
}
if(bdd_is_tautology(function, 1)){
return bAig_One;
}
bddManager = bdd_get_manager(function);
aigFunction = bAig_Zero;
foreach_bdd_cube(function, gen, cube){
andFunction = bAig_One;
arrayForEachItem(int, cube, i, value){
if (value != 2){
int j;
/*
If the BDD varaible is a next state varaible, we use the corresponding
current state varaible but with next state index.
*/
if (next != -1 && st_lookup_int(automaton->nsPsTable, (char *)(long)i, &j)){
node = bdd_bdd_ith_var(bddManager, j);
state = next;
} else {
node = bdd_bdd_ith_var(bddManager, i);
state = current;
}
aigNode = getAigOfBddAtState(network, node, state, withInitialState);
if (value == 0){
aigNode = bAig_Not(aigNode);
}
andFunction = bAig_And(aigManager, andFunction, aigNode);
}
}
aigFunction = bAig_Or(aigManager, aigFunction, andFunction);
}/* foreach_bdd_cube */
return aigFunction;
} /* BmcCirCUsBdd2Aig */
Here is the call graph for this function:
Here is the caller graph for this function:
| char* BmcCirCUsCallCirCUs | ( | BmcOption_t * | options | ) |
Function********************************************************************
Synopsis [Call CirCUs SAT solver on a CNF file]
Description [Call CirCUs SAT solver on a CNF file. We use CirCUs as CNF SAT solver. The function returns a file name that contains the assignment if the set of clauses are satisfiable. ]
SideEffects []
Definition at line 735 of file bmcCirCUsUtil.c.
{
satOption_t *satOption;
satManager_t *cm;
int maxSize;
char *fileName = NIL(char);
satOption = sat_InitOption();
satOption->verbose = options->verbosityLevel-1;
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 << 8;
cm->nodesArray = ALLOC(bAigEdge_t, maxSize);
cm->maxNodesArraySize = maxSize;
cm->nodesArraySize = satNodeSize;
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);
}
if(!(cm->stdOut = fopen(options->satOutFile, "w"))) {
fprintf(stdout, "ERROR : Can't open file %s\n", options->satOutFile);
cm->stdOut = stdout;
cm->stdErr = stderr;
}
sat_PrintSatisfyingAssignment(cm);
fileName = options->satOutFile;
}
sat_FreeManager(cm);
return fileName;
} /* BmcCallCirCUs */
Here is the call graph for this function:
Here is the caller graph for this function:
| char* BmcCirCUsCallCusp | ( | BmcOption_t * | options | ) |
Function********************************************************************
Synopsis [Check the satisfiability of CNF formula written in file]
Description [Run external solver on a CNF file. The function returns a file name that contains the assignment if the set of clauses are satisfiable.]
SideEffects []
Definition at line 816 of file bmcCirCUsUtil.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;
char *fileName = NIL(char);
/*
Prepare to call external CNF SAT solver
*/
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(char);
}
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 external sat solver. It may not be in your path. Status = %d\n", satStatus);
options->satSolverError = TRUE;
return NIL(char);
}
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(char);
}
/* 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(char);
}
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;
}
(void) fclose(fp);
fp = Cmd_FileOpen(options->satOutFile, "w", NIL(char *), 0);
for(num=0; num < array_n(result); num++){
fprintf(fp,"%d ", array_fetch(int, result, num));
if(((num+1) %10) == 0){
fprintf(fp,"\n");
}
}
array_free(result);
(void) fclose(fp);
fileName = options->satOutFile;
} 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);
return fileName;
} /* BmcCirCUsCallCusp */
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t BmcCirCUsCreateAigForSimpleCompositePath | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | aigManager, | ||
| Ltl_Automaton_t * | automaton, | ||
| int | fromState, | ||
| int | toState, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | coiIndexTable, | ||
| int | initialState | ||
| ) |
Function********************************************************************
Synopsis [Build AIG for a simple path in the composite model]
Description [Build AIG a simple path in the composite mode 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 347 of file bmcCirCUsUtil.c.
{
int i, j, bddID;
bAigEdge_t result, aigFunction, next, current;
mdd_manager *bddManager = Ntk_NetworkReadMddManager(network);
st_generator *stGen;
bdd_node *node;
/*
Build a path in the original model
*/
bAig_ExpandTimeFrame(network, aigManager, toState+1, initialState);
/*
Build a path in the automaton
*/
aigFunction = BmcCirCUsAutCreateAigForPath(network, aigManager, automaton,
fromState, toState, initialState);
/*
Constrains the two paths to be simple paths
*/
for(i = fromState + 1; i <= toState; i++){
for(j=fromState; j < i; j++){
result = bAig_Zero;
/*
Unique states in the automaton
*/
st_foreach_item(automaton->psNsTable, stGen, &bddID, NULL) {
node = bdd_bdd_ith_var(bddManager, bddID);
current = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager, node), i, -1,
automaton, aigManager,
initialState);
next = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager,node), j, -1,
automaton, aigManager,
initialState);
/*
next = BmcCirCUsBdd2Aig(network, bdd_construct_bdd_t(bddManager,node), i, j,
automaton, aigManager,
initialState);
result = bAig_Or(aigManager, result,
bAig_Not(next));
*/
result = bAig_Or(aigManager, result,
bAig_Not(bAig_Eq(aigManager, current, next)));
}
/*
Unique states in the original model
*/
result = bAig_Or(aigManager, result,
bAig_Not(BmcCirCUsConnectFromStateToState(network, i-1, j,
nodeToMvfAigTable,
coiIndexTable,
initialState)));
aigFunction = bAig_And(aigManager, aigFunction, result);
}
}
return aigFunction;
} /* BmcCirCUsCreateAigForSimpleCompositePath */
Here is the call graph for this function:
Here is the caller graph for this function:
| static bAigEdge_t getAigAtTimeFrame | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | node, | ||
| int | i, | ||
| int | withInitialState | ||
| ) | [static] |
Function********************************************************************
Synopsis []
Description []
SideEffects []
Definition at line 1011 of file bmcCirCUsUtil.c.
{
bAigTimeFrame_t *timeframe;
bAigEdge_t result, *li;
int index;
result = bAig_NULL;
if(withInitialState) timeframe = manager->timeframe;
else timeframe = manager->timeframeWOI;
if(st_lookup_int(timeframe->li2index, (char *)node, &index)) {
li = timeframe->latchInputs[i];
result = bAig_GetCanonical(manager, li[index]);
}
else if(st_lookup_int(timeframe->o2index, (char *)node, &index)) {
li = timeframe->outputs[i];
result = bAig_GetCanonical(manager, li[index]);
}
else if(st_lookup_int(timeframe->i2index, (char *)node, &index)) {
li = timeframe->internals[i];
result = bAig_GetCanonical(manager, li[index]);
}
else if(st_lookup_int(timeframe->bli2index, (char *)node, &index)) {
li = timeframe->blatchInputs[i];
result = bAig_GetCanonical(manager, li[index]);
}
else if(st_lookup_int(timeframe->bpi2index, (char *)node, &index)) {
li = timeframe->binputs[i];
result = bAig_GetCanonical(manager, li[index]);
}
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static bAigEdge_t getAigOfBddAtState | ( | Ntk_Network_t * | network, |
| bdd_node * | node, | ||
| int | state, | ||
| int | withInitialState | ||
| ) | [static] |
Function********************************************************************
Synopsis [Get the AIG node corresponding to a BDD node at a given state]
Description [We use BDD name to get the corresponding AIG node. If no AIG node exists, we create one]
SideEffects []
SeeAlso []
Definition at line 1062 of file bmcCirCUsUtil.c.
{
mdd_manager *bddManager = Ntk_NetworkReadMddManager(network);
mAig_Manager_t *aigManager = Ntk_NetworkReadMAigManager(network);
char *nodeName, *nameKey;
char tmpName[100];
bAigEdge_t aigNode, rtnAig;
nodeName = getBddName(bddManager, bdd_regular(node));
aigNode = bAig_FindNodeByName(aigManager, nodeName);
if(aigNode == bAig_NULL){
sprintf(tmpName, "%s_%d_%d", nodeName, withInitialState, state);
nameKey = util_strsav(tmpName);
aigNode = bAig_FindNodeByName(aigManager, nameKey);
if(aigNode == bAig_NULL){
aigNode = bAig_CreateVarNode(aigManager, nameKey);
} else {
FREE(nameKey);
}
rtnAig = aigNode;
} else {
aigNode = bAig_GetCanonical(aigManager, aigNode);
rtnAig = getAigAtTimeFrame(aigManager, aigNode, state, withInitialState);
if(rtnAig == bAig_NULL){
rtnAig = bAig_CreateNode(aigManager, bAig_NULL, bAig_NULL);
}
}
return bAig_GetCanonical(aigManager, rtnAig);
} /* getAigOfBddAtState */
Here is the call graph for this function:
Here is the caller graph for this function:
| static char * getBddName | ( | bdd_manager * | bddManager, |
| bdd_node * | node | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [retun the name of bdd node]
Description [return the name of bdd node. If the bdd is for a multi-valued variable, then its name will be the name of the multi-valued variable concatenated with its index. It is the user responsibility to free the returned name]
SideEffects []
Definition at line 967 of file bmcCirCUsUtil.c.
{
array_t *mvar_list = mdd_ret_mvar_list(bddManager);
array_t *bvar_list = mdd_ret_bvar_list(bddManager);
char name[100];
bvar_type bv;
mvar_type mv;
int nodeIndex = bdd_node_read_index(node);
int index, rtnNodeIndex;
/*
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);
sprintf(name, "%s_%d", mv.name, index);
} else {
sprintf(name, "Bdd_%d", nodeIndex);
}
return util_strsav(name);
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: bmcCirCUsUtil.c,v 1.22 2010/04/10 04:07:06 fabio Exp $" [static] |
CFile***********************************************************************
FileName [bmcCirCUsUtil.c]
PackageName [bmc]
Synopsis [Utilities for bmcCirCUs]
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 bmcCirCUsUtil.c.
