/**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.] ******************************************************************************/ #include "bmcInt.h" #include "sat.h" static char rcsid[] UNUSED = "$Id: bmcCirCUsUtil.c,v 1.22 2010/04/10 04:07:06 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ #define MAX_LENGTH 320 /* Max. length of a string while reading a file */ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Check for termination for safety properties.] Description [Check for termination for safety properties.] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcCirCUsAutLtlCheckTerminalAutomaton( Ntk_Network_t *network, bAig_Manager_t *aigManager, st_table *nodeToMvfAigTable, BmcCheckForTermination_t *terminationStatus, st_table *coiIndexTable, BmcOption_t *options) { 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 */ /**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] ******************************************************************************/ bAigEdge_t BmcCirCUsBdd2Aig( Ntk_Network_t *network, bdd_t *function, int current, int next, Ltl_Automaton_t *automaton, bAig_Manager_t *aigManager, int withInitialState) { 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 */ /**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 [] ******************************************************************************/ bAigEdge_t BmcCirCUsAutCreateAigForPath( Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState) { 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; ktransitionRelation, k, k+1, automaton, aigManager, initialState); aigFunction = bAig_And(aigManager , aigFunction, result); } return aigFunction; } /* BmcCirCUsAutCreateAigForPath */ /**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 [] ******************************************************************************/ bAigEdge_t BmcCirCUsAutCreateAigForSimplePath( Ntk_Network_t *network, bAig_Manager_t *aigManager, Ltl_Automaton_t *automaton, int fromState, int toState, int initialState) { 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 */ /**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 [] ******************************************************************************/ 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) { 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 */ /**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 [] ******************************************************************************/ void BmcCirCUsAutLtlCheckForTermination( Ntk_Network_t *network, bAig_Manager_t *aigManager, st_table *nodeToMvfAigTable, BmcCheckForTermination_t *terminationStatus, st_table *coiIndexTable, BmcOption_t *options) { 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 */ /**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 [] ******************************************************************************/ char * BmcCirCUsCallCirCUs( BmcOption_t *options) { 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 */ /**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 [] ******************************************************************************/ char * BmcCirCUsCallCusp(BmcOption_t *options) { 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 */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**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 [] ******************************************************************************/ static char * getBddName( bdd_manager *bddManager, bdd_node *node) { 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); } /**Function******************************************************************** Synopsis [] Description [] SideEffects [] ******************************************************************************/ static bAigEdge_t getAigAtTimeFrame( bAig_Manager_t *manager, bAigEdge_t node, int i, int withInitialState) { 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; } /**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 [] ******************************************************************************/ static bAigEdge_t getAigOfBddAtState( Ntk_Network_t *network, bdd_node *node, int state, int withInitialState) { 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 */