src/grab/grabBMC.c File Reference
#include "grabInt.h"#include "bmcInt.h"
Include dependency graph for grabBMC.c:
Go to the source code of this file.
Functions | |
| static bAigEdge_t | GrabConvertBddToBaig (bAig_Manager_t *bAigManager, bdd_t *fn, st_table *bddidToNames) |
| static st_table * | GrabBddGetSupportBaigNames (mdd_manager *mddManager, mdd_t *f) |
| static char * | GrabBddIdToBaigNames (mdd_manager *mddManager, int bddid) |
| boolean | Bmc_AbstractCheckAbstractTraces (Ntk_Network_t *network, array_t *synOnionRings, st_table *absLatches, int verbose, int dbgLevel, int printInputs) |
| boolean | Bmc_AbstractCheckAbstractTracesWithFineGrain (Ntk_Network_t *network, st_table *coiBnvTable, array_t *synOnionRings, st_table *absLatches, st_table *absBnvs) |
Function Documentation
| boolean Bmc_AbstractCheckAbstractTraces | ( | Ntk_Network_t * | network, |
| array_t * | synOnionRings, | ||
| st_table * | absLatches, | ||
| int | verbose, | ||
| int | dbgLevel, | ||
| int | printInputs | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Check if the abstract paths exist in the model.]
Description [Check if the abstract paths exist in the model. The paths are given as set of onion rings, where each ring is a set of states. The model is defined by the set of latches in absLatches.]
SideEffects []
Definition at line 77 of file grabBMC.c.
{
int pathLength = array_n(synOnionRings) -1;
mAig_Manager_t *maigManager = Ntk_NetworkReadMAigManager(network);
st_table *nodeToMvfAigTable = NIL(st_table);
BmcCnfClauses_t *cnfClauses;
FILE *cnfFile;
BmcOption_t *options;
array_t *result;
int i;
boolean CexExit = FALSE;
nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
fprintf(vis_stderr,
"** bmc error: please run buid_partiton_maigs first\n");
return CexExit;
}
options = BmcOptionAlloc();
if (verbose) {
options->dbgLevel = dbgLevel;
options->printInputs = printInputs;
}
options->satInFile = BmcCreateTmpFile();
if (options->satInFile == NIL(char)){
BmcOptionFree(options);
return CexExit;
}
/* create SAT Solver output file */
options->satOutFile = BmcCreateTmpFile();
if (options->satOutFile == NIL(char)){
BmcOptionFree(options);
fprintf(vis_stderr, "** bmc error: Cannot allocate a temp file name\n");
return CexExit;
}
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
if (cnfFile == NIL(FILE)) {
BmcOptionFree(options);
fprintf(vis_stderr, "** bmc error: Cannot create CNF output file %s\n",
options->satInFile);
return CexExit;
}
/* Unroll the model exactly 'pathLength' time frames
*/
cnfClauses = BmcCnfClausesAlloc();
BmcCnfGenerateClausesForPath(network, 0, pathLength, BMC_INITIAL_STATES,
cnfClauses, nodeToMvfAigTable, absLatches);
/* Generate the constraints from the abstract paths
* (1) build a bAigEdge_t (graph) for each ring
* (2) add all the cnf clauses that describe this graph
* (3) make the output bAigEdge_t equals to 1
*/
{
bAigEdge_t bAigState;
mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
array_t *clause = array_alloc(int, 1);
mdd_t *ring;
arrayForEachItem(mdd_t *, synOnionRings, i, ring) {
st_table *bddidTobAigNames;
bddidTobAigNames = GrabBddGetSupportBaigNames(mddManager, ring);
bAigState = GrabConvertBddToBaig(maigManager, ring, bddidTobAigNames);
{
st_generator *stgen;
long tmpId;
char *tmpStr;
st_foreach_item(bddidTobAigNames, stgen, &tmpId, &tmpStr) {
FREE(tmpStr);
}
st_free_table(bddidTobAigNames);
}
array_insert(int, clause, 0, BmcGenerateCnfFormulaForAigFunction(
maigManager, bAigState, i, cnfClauses));
BmcCnfInsertClause(cnfClauses, clause);
}
array_free(clause);
}
/* Call the SAT solver
*/
BmcWriteClauses(maigManager, cnfFile, cnfClauses, options);
fclose(cnfFile);
result = BmcCheckSAT(options);
if(result != NIL(array_t)){
if (verbose >= 1 && dbgLevel ==1) {
fprintf(vis_stdout,"Found Counterexample of length = %d\n", pathLength);
BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
result, pathLength+1, absLatches, options,
NIL(array_t));
}
if (verbose >=1 && dbgLevel == 2) {
BmcPrintCounterExampleAiger(network, nodeToMvfAigTable, cnfClauses,
result, pathLength+1, absLatches, options,
NIL(array_t));
}
CexExit = TRUE;
}
/* free all used memories */
BmcCnfClausesFree(cnfClauses);
array_free(result);
BmcOptionFree(options);
return CexExit;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean Bmc_AbstractCheckAbstractTracesWithFineGrain | ( | Ntk_Network_t * | network, |
| st_table * | coiBnvTable, | ||
| array_t * | synOnionRings, | ||
| st_table * | absLatches, | ||
| st_table * | absBnvs | ||
| ) |
Function********************************************************************
Synopsis [Check if the abstract paths exist in the fine-grain model.]
Description [Check if the abstract paths exist in the fine-grain model. The paths are given as set of onion rings, where each ring is a set of states. The model is defined by the set of latches (absLatches) and bnvs (absBnvs). The entire set of bnvs of the network are stored in the table coiBnvTable.
This procedure first build a NEW maig graph (for the fine-grain model), then check if the abstract paths exist in the model.
Before it returns, the previous maig graph is restored.]
SideEffects []
Definition at line 215 of file grabBMC.c.
{
boolean result;
mAigManagerState_t oldMaigState; /* to store the previous AIG */
mAig_Manager_t *maigManager;
lsGen lsgen;
Ntk_Node_t *node;
int mAigId;
int i;
st_generator *stgen;
st_table *leaves;
array_t *roots, *combInputs;
/* save the existing maigManager */
oldMaigState.manager = Ntk_NetworkReadMAigManager(network);
oldMaigState.nodeToMvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
oldMaigState.nodeToMAigIdTable = st_init_table(st_ptrcmp, st_ptrhash);
Ntk_NetworkForEachNode(network, lsgen, node) {
mAigId = Ntk_NodeReadMAigId(node);
st_insert(oldMaigState.nodeToMAigIdTable, node, (char *)(long)mAigId);
Ntk_NodeSetMAigId(node, ntmaig_UNUSED);
}
/* create a new maigManager */
maigManager = mAig_initAig();
Ntk_NetworkSetMAigManager(network, maigManager);
Ntk_NetworkSetApplInfo(network, MVFAIG_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) ntmAig_MvfAigTableFreeCallback,
(void *) st_init_table(st_ptrcmp, st_ptrhash));
/* roots are the visible latches, and the visible bnvs (some bnvs
* may not be in the transitive fan-in cone of the visible latches
*/
roots = array_alloc(Ntk_Node_t *, 0);
st_foreach_item(absLatches, stgen, &node, NIL(char *)) {
array_insert_last(Ntk_Node_t *, roots, Ntk_LatchReadDataInput(node));
array_insert_last(Ntk_Node_t *, roots, Ntk_LatchReadInitialInput(node));
}
st_foreach_item(absBnvs, stgen, &node, NIL(char *)) {
array_insert_last(Ntk_Node_t *, roots, node);
}
combInputs = Ntk_NodeComputeTransitiveFaninNodes(network, roots,
TRUE, /* stopAtLatches */
FALSE /* combInputsOnly*/
);
/* leaves are the combinational inputs or the invisible bnvs */
leaves = st_init_table(st_ptrcmp, st_ptrhash);
arrayForEachItem(Ntk_Node_t *, combInputs, i, node) {
if ( Ntk_NodeTestIsCombInput(node) ||
( st_is_member(coiBnvTable, node) &&
!st_is_member(absBnvs, node) ) ) {
st_insert(leaves, node, (char *) ntmaig_UNUSED);
Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
Ntk_NodeReadName(node),
Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
}
}
st_foreach_item(absLatches, stgen, &node, NIL(char *)) {
if (!st_is_member(leaves, node)) {
st_insert(leaves, node, (char *) ntmaig_UNUSED);
Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
Ntk_NodeReadName(node),
Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
}
}
array_free(combInputs);
#if 1
/* THIS SEEMS UNNECESSARY---IT'S HERE TO AVOID ERRORS IN CALLING
* ntmaig_NetworkBuildMvfAigs()
*/
Ntk_NetworkForEachCombInput(network, lsgen, node) {
if (Ntk_NodeReadMAigId(node) == NTK_UNASSIGNED_MAIG_ID) {
Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
Ntk_NodeReadName(node),
Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
}
}
#endif
/* build the new AIG graph */
ntmaig_NetworkBuildMvfAigs(network, roots, leaves);
array_free(roots);
st_free_table(leaves);
/* check the existence of the abstract path on the new AIG graph */
result = Bmc_AbstractCheckAbstractTraces(network,
synOnionRings,
absLatches,
0, 0, 0);
/* restore the previous maigManager */
mAig_quit(maigManager);
Ntk_NetworkFreeApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
Ntk_NetworkSetMAigManager(network, oldMaigState.manager);
Ntk_NetworkSetApplInfo(network, MVFAIG_NETWORK_APPL_KEY,
(Ntk_ApplInfoFreeFn) ntmAig_MvfAigTableFreeCallback,
(void *) oldMaigState.nodeToMvfAigTable);
st_foreach_item(oldMaigState.nodeToMAigIdTable, stgen, &node,
&mAigId) {
Ntk_NodeSetMAigId(node, mAigId);
}
st_free_table(oldMaigState.nodeToMAigIdTable);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static st_table * GrabBddGetSupportBaigNames | ( | mdd_manager * | mddManager, |
| mdd_t * | f | ||
| ) | [static] |
Function********************************************************************
Synopsis [Get a (bddId,baigName) table for the supporting variableS.]
SideEffects [Get a (bddId,baigName) table for the supporting variableS. The caller should free the returned table as well as the (char *) of its value field.]
SeeAlso []
Definition at line 462 of file grabBMC.c.
{
int numOfVars = bdd_num_vars(mddManager);
st_table *bddidTObaigNames = st_init_table(st_numcmp, st_numhash);
var_set_t *vset;
int i;
vset = bdd_get_support(f);
for (i=0; i<numOfVars; i++) {
if (var_set_get_elt(vset, i) == 1) {
st_insert(bddidTObaigNames, (char *)(long)i,
GrabBddIdToBaigNames(mddManager, i));
}
}
var_set_free(vset);
return bddidTObaigNames;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static char * GrabBddIdToBaigNames | ( | mdd_manager * | mddManager, |
| int | bddid | ||
| ) | [static] |
Function********************************************************************
Synopsis [return the baigName of a bddid]
SideEffects [The caller should free the returned char *. This function is based on the assumption that MDD and MAIG shares the same naming convention (which is true in VIS).]
SeeAlso []
Definition at line 495 of file grabBMC.c.
{
array_t *mvar_list = mdd_ret_mvar_list(mddManager);
array_t *bvar_list = mdd_ret_bvar_list(mddManager);
bvar_type bv;
mvar_type mv;
int mddid, index, id;
char *nodeName;
char baigName[1024];
/* 1. from bddid, get mddid and the index of this bddid in the mddid
*/
bv = array_fetch(bvar_type, bvar_list, bddid);
mddid = bv.mvar_id;
mv = array_fetch(mvar_type, mvar_list, mddid);
arrayForEachItem(int, mv.bvars, index, id) {
if (id == bddid)
break;
}
assert(index <= mv.encode_length -1);
/* 2. assumptions: (1) mv.name = nodeName,
* (2) index is the same for MDD and MAIG
*/
nodeName = mv.name;
/* 3. the baigEdge_t's name is ("%s_%d",nodeName,index)
*/
sprintf(baigName, "%s_%d", nodeName, index);
return util_strsav(baigName);
}
Here is the caller graph for this function:
| static bAigEdge_t GrabConvertBddToBaig | ( | bAig_Manager_t * | bAigManager, |
| bdd_t * | fn, | ||
| st_table * | bddidToNames | ||
| ) | [static] |
CFile***********************************************************************
FileName [grabBMC.c]
PackageName [grab]
Synopsis [Check abstract paths on a more concrete model using SAT.]
Description [Abstract paths are given in an array of MDDs, which capture multiple abstract paths at the same time. MDDs are encoded as AIG graph to allow the check in the more concrete model.]
Author [Chao Wang]
Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]AutomaticStart
Function********************************************************************
Synopsis [Build the binary Aig for a given bdd]
SideEffects [Build the binary Aig for a given bdd. We assume that the return bdd nodes from the foreach_bdd_node are in the order from childeren to parent. i.e all the childeren nodes are returned before the parent node.
bddidToNames is a hash table from bddid to its bAigEdge_t name. If provided, this table should contain entiries for all the bddid in the support.]
SideEffects []
SeeAlso []
Definition at line 355 of file grabBMC.c.
{
bdd_gen *gen;
bdd_node *node, *thenNode, *elseNode, *funcNode;
bdd_manager *bddManager = bdd_get_manager(fn);
bdd_node *one = bdd_read_one(bddManager);
/*bdd_node *zero = bdd_read_logic_zero(bddManager);*/
int is_complemented;
int flag;
bAigEdge_t var, left, right, result;
char *name;
st_table *bddTObaigTable;
bddTObaigTable = st_init_table(st_numcmp, st_numhash);
if (fn == NULL){
return bAig_NULL;
}
st_insert(bddTObaigTable, (char *) (long) bdd_regular(one),
(char *) bAig_One);
funcNode = bdd_get_node(fn, &is_complemented);
if (bdd_is_constant(funcNode)){
flag = st_lookup(bddTObaigTable,
(char *) (long) (funcNode),
&result);
assert(flag);
st_free_table(bddTObaigTable);
if (is_complemented)
return bAig_Not(result);
else
return result;
}
foreach_bdd_node(fn, gen, node){
/* if the node has been processed, skip it. (the constant ONE
* should be the only node falls into this category).
*/
if (st_is_member(bddTObaigTable, (char *) (long) bdd_regular(node)))
continue;
/* bdd_node_read_index() return the current level's bddId */
if (bddidToNames) {
flag = st_lookup(bddidToNames, (char *)(long)bdd_node_read_index(node),
&name);
assert(flag);
name = util_strsav(name);
}else {
char tempString[1024];
sprintf(tempString, "BDD%d", bdd_node_read_index(node));
name = util_strsav(tempString);
}
/* Create or Retrieve the bAigEdge_t w.r.t. 'name' */
var = bAig_CreateVarNode(bAigManager, name);
FREE(name);
thenNode = bdd_bdd_T(node);
flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(thenNode),
&left);
assert(flag);
elseNode = bdd_bdd_E(node);
flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(elseNode),
&right);
assert(flag);
/* should we test here whether elseNode is complemented arc? */
if (bdd_is_complement(elseNode))
right = bAig_Not(right);
result = bAig_Or(bAigManager, bAig_And(bAigManager, var, left),
bAig_And(bAigManager, bAig_Not(var), right));
st_insert(bddTObaigTable, (char *) (long) bdd_regular(node),
(char *) (long) result);
}
flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(funcNode),
&result);
assert(flag);
st_free_table(bddTObaigTable);
if (is_complemented){
return bAig_Not(result);
} else {
return result;
}
} /* end of bAig_bddtobAig() */
Here is the call graph for this function:
Here is the caller graph for this function:
