src/puresat/puresatBMC.c File Reference
#include "puresatInt.h"
Include dependency graph for puresatBMC.c:
Go to the source code of this file.
Functions | |
| void | PureSatInsertNewClauseForSimplePath (array_t *vertexArray, Ntk_Network_t *network, int step1, int step2, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable) |
| void | PureSatInsertNewClauseForInit (array_t *vertexArray, Ntk_Network_t *network, int step1, int step2, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable) |
| void | PureSatSetInitStatesForSimplePath (array_t *vertexArray, Ntk_Network_t *network, BmcCnfClauses_t *cnfClauses, st_table *nodeToMvfAigTable) |
| boolean | PureSatExistASimplePath (Ntk_Network_t *network, PureSat_IncreSATManager_t *pism, array_t *vertexArray, bAigEdge_t property, PureSat_Manager_t *pm) |
| boolean | PureSatExistCE (Ntk_Network_t *network, PureSat_IncreSATManager_t *pism, BmcOption_t *options, array_t *vertexArray, bAigEdge_t property, PureSat_Manager_t *pm, int extractCexInfo) |
| boolean | PureSatIncreExistCE (Ntk_Network_t *network, PureSat_IncreSATManager_t *pism, array_t *vertexArray, bAigEdge_t property, PureSat_Manager_t *pm) |
| boolean | PureSatIncreExistCEForRefineOnAbs (Ntk_Network_t *network, PureSat_IncreSATManager_t *pism, array_t *vertexArray, bAigEdge_t property, boolean firstTime, PureSat_Manager_t *pm) |
| void | PureSatGenerateClausesFromStateTostateWithTable (bAig_Manager_t *manager, bAigEdge_t *fromAigArray, bAigEdge_t *toAigArray, int mvfSize, int fromState, int toState, BmcCnfClauses_t *cnfClauses, int outIndex, st_table *ClsidxToLatchTable, char *nodeName) |
| void | PureSatGenerateClausesForPath_EnhanceInit (Ntk_Network_t *network, int from, int to, PureSat_IncreSATManager_t *pism, PureSat_Manager_t *pm, st_table *nodeToMvfAigTable, st_table *CoiTable) |
Function Documentation
| boolean PureSatExistASimplePath | ( | Ntk_Network_t * | network, |
| PureSat_IncreSATManager_t * | pism, | ||
| array_t * | vertexArray, | ||
| bAigEdge_t | property, | ||
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [k-induction checking from SSS'00 FMCAD paper ]
Description [k-induction checking from SSS'00 FMCAD paper ]
SideEffects []
SeeAlso []
P(S(i))
Definition at line 443 of file puresatBMC.c.
{
mAig_Manager_t *maigManager = Ntk_NetworkReadMAigManager(network);
Ntk_Node_t *latch, *latchData, *latchInit;
MvfAig_Function_t *initMvfAig, *dataMvfAig, *latchMvfAig;
bAigEdge_t *initBAig, *latchBAig, *dataBAig;
int i,j, k, mvfSize,propertyIndex;
char *nodeName;
array_t * Pclause = array_alloc(int,0);
st_table *nodeToMvfAigTable;
BmcCnfStates_t *cnfstate1,*cnfstate2;
array_t *supportLatches;
int status;
int beginPosition = pism->beginPosition;
int Length = pism->Length;
int oldLength = pism->oldLength;
BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
satManager_t * cm = pism->cm;
/* construct loopfree path;*/
nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
(void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
exit(0);
}
for(j=beginPosition;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
/* BmcGenerateClausesFromStateTostate(maigManager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
for (k=0; k < oldLength; k++){
BmcGenerateClausesFromStateTostate(maigManager, dataBAig,latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
} /*st_foreach_item(vertexTable,*/
if(oldLength<Length){
for(j=0;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
for (k=oldLength; k <Length; k++){
BmcGenerateClausesFromStateTostate(maigManager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
}/*if(oldLength!=0){*/
if(pm->verbosity>=1)
fprintf(vis_stdout,"forward simple path testing...\n");
cnfstate1 = BmcCnfClausesFreeze(cnfClauses);
/*generate NODE(i)!=NODE(i+1)*/
for(i=1;i<Length;i++)
for(j=i+1;j<=Length;j++)
PureSatInsertNewClauseForSimplePath(vertexArray,network,i,j,cnfClauses,nodeToMvfAigTable); /*Si!=Sj*/
cnfstate2 = BmcCnfClausesFreeze(cnfClauses);
supportLatches = PureSatGetImmediateSupportLatches(network, 0, vertexArray);
/*I(S0)*/
PureSatSetInitStatesForSimplePath(supportLatches/*vertexArray*/,network,cnfClauses,nodeToMvfAigTable);
/*generate all.!I(S(1...i)), the first constraint*/
for(i=1;i<=Length;i++)
PureSatInsertNewClauseForInit(supportLatches/*vertexArray*/,network,-1,i,cnfClauses,nodeToMvfAigTable);
array_free(supportLatches);
pism->propertyPos = cnfstate1->nextIndex;
PureSatReadClauses(pism,pm);
/*no incremental */
if(!pm->incre){
if(cm->savedConflictClauses)
sat_ArrayFree(cm->savedConflictClauses);
cm->savedConflictClauses = 0;
}
sat_Main(cm);
status = cm->status;
PureSatCleanSat(cm);
BmcCnfClausesRestore(cnfClauses, cnfstate1);
if(status == SAT_SAT)
{
if(pm->verbosity>=1)
fprintf(vis_stdout,"backward simple path testing...\n");
cnfstate2 = BmcCnfClausesFreeze(cnfClauses);
/*generate NODE(i)!=NODE(i+1)*/
for(i=1;i<Length;i++)
for(j=i+1;j<=Length;j++)
PureSatInsertNewClauseForSimplePath(vertexArray,network,i,j,cnfClauses,nodeToMvfAigTable);
propertyIndex = BmcGenerateCnfFormulaForAigFunction(maigManager,property, Length, cnfClauses);
array_insert_last(int, Pclause,propertyIndex);
BmcCnfInsertClause(cnfClauses, Pclause);
array_free(Pclause);
/*all.P(S(0,...i-1))*/
property = bAig_Not(property);
for(k=0; k <= Length-1; k++){
propertyIndex = BmcGenerateCnfFormulaForAigFunction(maigManager,property,k, cnfClauses);
Pclause = array_alloc(int,0);
array_insert_last(int, Pclause, propertyIndex);
BmcCnfInsertClause(cnfClauses, Pclause);
array_free(Pclause);
}
pism->propertyPos = cnfstate2->nextIndex;
PureSatReadClauses(pism,pm);
/*no incremental */
if(!pm->incre){
if(cm->savedConflictClauses)
sat_ArrayFree(cm->savedConflictClauses);
cm->savedConflictClauses = 0;
}
sat_Main(cm);
status = cm->status;
PureSatCleanSat(cm);
if(status == SAT_SAT)
{
BmcCnfClausesRestore(cnfClauses, cnfstate1);
FREE(cnfstate1);
FREE(cnfstate2);
return TRUE;
}
}
FREE(cnfstate1);
FREE(cnfstate2);
return FALSE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean PureSatExistCE | ( | Ntk_Network_t * | network, |
| PureSat_IncreSATManager_t * | pism, | ||
| BmcOption_t * | options, | ||
| array_t * | vertexArray, | ||
| bAigEdge_t | property, | ||
| PureSat_Manager_t * | pm, | ||
| int | extractCexInfo | ||
| ) |
Function********************************************************************
Synopsis [checking the existence of a path of certain length]
Description [checking the existence of a path of certain length ]
SideEffects []
SeeAlso []
Definition at line 628 of file puresatBMC.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
Ntk_Node_t *latch, *latchData, *latchInit;
MvfAig_Function_t *initMvfAig, *dataMvfAig, *latchMvfAig;
bAigEdge_t *initBAig, *latchBAig, *dataBAig;
int i,j, k, mvfSize;
char *nodeName;
array_t *result;
array_t *Pclause = array_alloc(int, 0);
FILE *cnfFile;
st_table *nodeToMvfAigTable;
BmcCnfStates_t *cnfstate;
int beginPosition = pism->beginPosition;
int oldLength = pism->oldLength;
int Length = pism->Length;
BmcCnfClauses_t *cnfClauses = pism->cnfClauses;
double t2, t1 = util_cpu_ctime();
options->verbosityLevel = (Bmc_VerbosityLevel) pm->verbosity;
nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
(void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
exit(0);
}
#if 1
{
array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
arrayForEachItem(char *, supportLatches, j, nodeName) {
latch = Ntk_NetworkFindNodeByName(network, nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
array_free(supportLatches);
}
for(j=beginPosition;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
/* BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
for (k=0; k <oldLength; k++){
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
} /*st_foreach_item(vertexTable,*/
#else
/*build TR for more latches*/
for(j=beginPosition;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
for (k=0; k <oldLength; k++){
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
} /*st_foreach_item(vertexTable,*/
#endif
/* for more length*/
if(oldLength<Length){
for(j=0;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
for (k=oldLength; k<Length; k++){
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
}
k=Length;
cnfstate = BmcCnfClausesFreeze(cnfClauses);
/* for(k=0; k <= Length; k++){*/
array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,k, cnfClauses));
/* } */
BmcCnfInsertClause(cnfClauses, Pclause);
array_free(Pclause);
cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
BmcWriteClauses(manager, cnfFile, cnfClauses, options);
(void) fclose(cnfFile);
result = BmcCheckSAT(options);
BmcCnfClausesRestore(cnfClauses, cnfstate);
FREE(cnfstate);
t2 = util_cpu_ctime();
/*timeElapse_Sol += t2-t1;*/
if(pm->verbosity>=2)
fprintf(vis_stdout, "timeElapse_sol_noIncre: += %g\n", (double)((t2-t1)/1000.0));
if(extractCexInfo && pm->dbgLevel>=1 && result!=NIL(array_t)){
pm->result = array_dup(result);
}
if(result!=NIL(array_t))
{
if(pm->verbosity>=2)
fprintf(vis_stdout, "find CEX\n");
array_free(result);
return TRUE;
}
else
{
if(pm->verbosity>=2)
fprintf(vis_stdout, "didn't find CEX\n");
return FALSE;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatGenerateClausesForPath_EnhanceInit | ( | Ntk_Network_t * | network, |
| int | from, | ||
| int | to, | ||
| PureSat_IncreSATManager_t * | pism, | ||
| PureSat_Manager_t * | pm, | ||
| st_table * | nodeToMvfAigTable, | ||
| st_table * | CoiTable | ||
| ) |
Function********************************************************************
Synopsis [Building the path with enhanced initail states]
Description [Building the path with enhanced initail states]
SideEffects []
SeeAlso []
Definition at line 1353 of file puresatBMC.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
lsGen gen;
Ntk_Node_t *latch, *latchData, *latchInit;
MvfAig_Function_t *initMvfAig, *dataMvfAig, *latchMvfAig;
bAigEdge_t *initBAig, *latchBAig, *dataBAig;
int i,j, k, mvfSize;
array_t * vertexArray = array_alloc(char *,0);
char * nodeName;
BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
st_table * ClsidxToLatchTable = pm->ClsidxToLatchTable;
if(from == 0){
if(pm->verbosity>=2)
fprintf(vis_stdout, "node in vertexArray: ");
Ntk_NetworkForEachLatch(network, gen, latch) {
int tmp;
if (!st_lookup_int(CoiTable, latch, &tmp)){
continue;
}
nodeName = Ntk_NodeReadName(latch);
array_insert_last(char *,vertexArray,nodeName);
if(pm->verbosity>=2)
fprintf(vis_stdout, "%s ",nodeName);
}
if(pm->verbosity>=2)
fprintf(vis_stdout, "\n");
}
if(from == 0){
array_t *supportLatches = PureSatGetImmediateSupportLatches(network, 0, vertexArray);
arrayForEachItem(char *, supportLatches, j, nodeName) {
latch = Ntk_NetworkFindNodeByName(network, nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
array_free(supportLatches);
array_free(vertexArray);
}
Ntk_NetworkForEachLatch(network, gen, latch) {
int tmp;
if (!st_lookup_int(CoiTable, latch, &tmp)){
continue;
}
nodeName = Ntk_NodeReadName(latch);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
/* Get the multi-valued function for each node*/
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
if (initMvfAig == NIL(MvfAig_Function_t)){
(void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
return;
}
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
if (dataMvfAig == NIL(MvfAig_Function_t)){
(void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData));
return;
}
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
/* Generate the CNF for the transition functions */
for (k=from; k < to; k++){
PureSatGenerateClausesFromStateTostateWithTable(manager, dataBAig,latchBAig, mvfSize, k,
k+1, cnfClauses,0,ClsidxToLatchTable, nodeName);
} /* for k state loop */
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
} /* ForEachLatch loop*/
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatGenerateClausesFromStateTostateWithTable | ( | bAig_Manager_t * | manager, |
| bAigEdge_t * | fromAigArray, | ||
| bAigEdge_t * | toAigArray, | ||
| int | mvfSize, | ||
| int | fromState, | ||
| int | toState, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| int | outIndex, | ||
| st_table * | ClsidxToLatchTable, | ||
| char * | nodeName | ||
| ) |
Function********************************************************************
Synopsis [Building the path together with ClsidxToLatchTable for later use by refinement extraction]
Description [Building the path together with ClsidxToLatchTable for later use by refinement extraction]
SideEffects []
SeeAlso []
Definition at line 1237 of file puresatBMC.c.
{
array_t *clause, *tmpclause;
int toIndex, fromIndex, cnfIndex;
int i;
toIndex =0;
fromIndex = 0;
for(i=0; i< mvfSize; i++){
if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){
return; /* the clause is always true */
}
}
clause = array_alloc(int, 0);
for(i=0; i< mvfSize; i++){
if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){
if (toAigArray[i] != bAig_One){
toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i],
toState,cnfClauses);
}
if (fromAigArray[i] != bAig_One){
fromIndex = BmcGenerateCnfFormulaForAigFunction(manager,fromAigArray[i],
fromState,cnfClauses);
}
cnfIndex = cnfClauses->cnfGlobalIndex++; /* index of the output of the OR of T(from, to) */
if (toAigArray[i] == bAig_One){
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, -fromIndex);
array_insert(int, tmpclause, 1, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, fromIndex);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
array_free(tmpclause);
} else if (fromAigArray[i] == bAig_One){
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, -toIndex);
array_insert(int, tmpclause, 1, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, toIndex);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
array_free(tmpclause);
} else {
tmpclause = array_alloc(int, 3);
array_insert(int, tmpclause, 0, -toIndex);
array_insert(int, tmpclause, 1, -fromIndex);
array_insert(int, tmpclause, 2, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, toIndex);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, fromIndex);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
array_free(tmpclause);
}
array_insert_last(int, clause, cnfIndex);
} /* if */
} /* for i loop */
if (outIndex != 0 ){
array_insert_last(int, clause, -outIndex);
}
BmcCnfInsertClause(cnfClauses, clause);
array_free(clause);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean PureSatIncreExistCE | ( | Ntk_Network_t * | network, |
| PureSat_IncreSATManager_t * | pism, | ||
| array_t * | vertexArray, | ||
| bAigEdge_t | property, | ||
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Incrementally checking the existence of a path of certain length]
Description [Incrementally checking the existence of a path of certain length ]
SideEffects []
SeeAlso []
Definition at line 855 of file puresatBMC.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
Ntk_Node_t *latch, *latchData, *latchInit;
MvfAig_Function_t *initMvfAig, *dataMvfAig, *latchMvfAig;
bAigEdge_t *initBAig, *latchBAig, *dataBAig;
int i,j, k, mvfSize;
int status;
char *nodeName;
array_t *Pclause = array_alloc(int, 0);
st_table *nodeToMvfAigTable;
BmcCnfStates_t *cnfstate;
int beginPosition = pism->beginPosition;
int Length = pism->Length;
int oldLength = pism->oldLength;
BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
satManager_t * cm = pism->cm;
nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
(void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
exit(0);
}
{
array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
arrayForEachItem(char *, supportLatches, j, nodeName) {
latch = Ntk_NetworkFindNodeByName(network, nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
array_free(supportLatches);
}
for(j=beginPosition;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
for (k=0; k <oldLength; k++){
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
/* for more length*/
if(oldLength<Length){
for(j=0;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
for (k=oldLength; k<Length; k++){
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
}
k=Length;
cnfstate = BmcCnfClausesFreeze(cnfClauses);
/* for(k=0; k <= Length; k++){*/
array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,k, cnfClauses));
/* }*/
BmcCnfInsertClause(cnfClauses, Pclause);
array_free(Pclause);
pism->propertyPos = cnfstate->nextIndex;
PureSatReadClauses(pism, pm);
/*no incremental */
if(!pm->incre){
if(cm->savedConflictClauses)
sat_ArrayFree(cm->savedConflictClauses);
cm->savedConflictClauses = 0;
}
cm->status = 0;
sat_Main(cm);
status = cm->status;
PureSatCleanSat(cm);
BmcCnfClausesRestore(cnfClauses, cnfstate);
FREE(cnfstate);
if(status == SAT_SAT)
{
if(pm->verbosity>=1)
fprintf(vis_stdout, "find CEX\n");
return TRUE;
}
else
{
if(pm->verbosity>=1)
fprintf(vis_stdout, "didn't find CEX\n");
return FALSE;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean PureSatIncreExistCEForRefineOnAbs | ( | Ntk_Network_t * | network, |
| PureSat_IncreSATManager_t * | pism, | ||
| array_t * | vertexArray, | ||
| bAigEdge_t | property, | ||
| boolean | firstTime, | ||
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Incrementally checking the existence of a path of certain length used by incremental concretization. For more information of incremental concretization, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"]
Description [Incrementally checking the existence of a path of certain length used by incremental concretization. For more information of incremental concretization, please check the BMC'03 and STTT'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", and " Abstraction in symbolic model checking using satisfiability as the only decision procedure"]
SideEffects []
SeeAlso []
Definition at line 1044 of file puresatBMC.c.
{
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
Ntk_Node_t *latch, *latchData, *latchInit;
MvfAig_Function_t *initMvfAig, *dataMvfAig, *latchMvfAig;
bAigEdge_t *initBAig, *latchBAig, *dataBAig;
int i,j, k, mvfSize, status;
char *nodeName;
array_t *Pclause = array_alloc(int, 0);
st_table *nodeToMvfAigTable;
int beginPosition = pism->beginPosition;
int Length = pism->Length;
int oldLength = pism->oldLength;
BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
satManager_t * cm = pism->cm;
nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable == NIL(st_table)){
(void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
exit(0);
}
{
array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
arrayForEachItem(char *, supportLatches, j, nodeName) {
latch = Ntk_NetworkFindNodeByName(network, nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
array_free(supportLatches);
}
for(j=beginPosition;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
/*BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
for (k=0; k <oldLength; k++){
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
/*for more length */
if(oldLength<Length){
for(j=0;j<array_n(vertexArray);j++){
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
latchData = Ntk_LatchReadDataInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
dataBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
dataBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
for (k=oldLength; k<Length; k++){
BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
}
FREE(initBAig);
FREE(dataBAig);
FREE(latchBAig);
}
}
/*cnfstate = BmcCnfClausesFreeze(cnfClauses);*/
if(firstTime){
/* pism->propertyPos = cnfstate->nextIndex;*/
array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager,
property,Length, cnfClauses));
BmcCnfInsertClause(cnfClauses, Pclause);
array_free(Pclause);
}
PureSatReadClauses(pism,pm);
sat_Main(cm);
if(pm->dbgLevel>=1 && cm->status==SAT_SAT){
pm->result = array_alloc(int, 0);
{
int size, value;
size = cm->initNumVariables * satNodeSize;
for(i=satNodeSize; i<=size; i+=satNodeSize) {
value = SATvalue(i);
if(value == 1) {
array_insert_last(int, pm->result, SATnodeID(i));
}
else if(value == 0) {
array_insert_last(int, pm->result, -(SATnodeID(i)));
}
}
}
}
status = cm->status;
PureSatCleanSat(cm);
/*FREE(cnfstate);*/
if(status == SAT_SAT)
{
if(pm->verbosity>=1)
fprintf(vis_stdout, "find CEX\n");
return TRUE;
}
else
{
if(pm->verbosity>=1)
fprintf(vis_stdout, "didn't find CEX\n");
return FALSE;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatInsertNewClauseForInit | ( | array_t * | vertexArray, |
| Ntk_Network_t * | network, | ||
| int | step1, | ||
| int | step2, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable | ||
| ) |
Function********************************************************************
Synopsis [Insert clauses of (Si!=I) for k-induction checking]
Description [Insert clauses of (Si!=I) for k-induction checking]
SideEffects []
SeeAlso []
Definition at line 221 of file puresatBMC.c.
{
int i,j,k,mvfSize,index1=0,index2=0, cnfIndex;
Ntk_Node_t * latch, *latchInit;
MvfAig_Function_t *initMvfAig,*latchMvfAig;
bAigEdge_t * latchBAig,* initBAig;
array_t * tmpclause, *clauseArray, * clause, * clause1,*latchClause;
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
char * Name;
boolean nextLatch = FALSE;
latchClause = array_alloc(int,0);
arrayForEachItem(char *,vertexArray,j,Name)
{
nextLatch = FALSE;
clause = array_alloc(int,0); /*(-A + -A1 + -A2 + -A3)*/
clauseArray = array_alloc(array_t *,0);/*(A + -A1)(A + -A2)(A + -A3)*/
latch = Ntk_NetworkFindNodeByName(network,Name);
latchInit = Ntk_LatchReadInitialInput(latch);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
mvfSize = array_n(latchMvfAig);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
initBAig = ALLOC(bAigEdge_t, mvfSize);
/* printf("mvfSize = %d \n",mvfSize);*/
for(i=0; i< mvfSize; i++){
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
for(i=0; i< mvfSize; i++){
if ((initBAig[i] == bAig_One) && (latchBAig[i] == bAig_One))
{
nextLatch=TRUE;
break; /* the clause is always true */
}
}
if(!nextLatch)
{
for(i=0; i< mvfSize; i++){
initBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig, i));
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
if(initBAig[i]==bAig_Zero ||latchBAig[i]==bAig_Zero)
{
continue;
}
if(initBAig[i]!=bAig_One)
{
index1 = BmcGenerateCnfFormulaForAigFunction(manager,initBAig[i],step1,cnfClauses);
}
if(latchBAig[i]!=bAig_One)
{
index2 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step2,cnfClauses);
}
cnfIndex = cnfClauses->cnfGlobalIndex++;
if (initBAig[i] == bAig_One){
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, -index2);
array_insert(int, tmpclause, 1, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, index2);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
} else if (latchBAig[i] == bAig_One){
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, -index1);
array_insert(int, tmpclause, 1, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, index1);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
} else {
tmpclause = array_alloc(int, 3);
array_insert(int, tmpclause, 0, -index2);
array_insert(int, tmpclause, 1, -index1);
array_insert(int, tmpclause, 2, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, index2);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, index1);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
}
/*(-A + A1 + A2 + A3)*/
array_insert_last(int,clause,cnfIndex);
/*(A + -A1)(A + -A2)(A + -A3)*/
clause1 = array_alloc(int,0);/*(A + -A1/2/3)*/
array_insert_last(int,clause1,-cnfIndex);
array_insert_last(array_t *,clauseArray,clause1);
}/* for(i=0; i< mvfSize;*/
cnfIndex = cnfClauses->cnfGlobalIndex++; /*A*/
/*(A + -A1)(A + -A2)(A + -A3)*/
arrayForEachItem(array_t *,clauseArray,k,clause1)
{
array_insert_last(int,clause1,cnfIndex);
BmcCnfInsertClause(cnfClauses,clause1);
array_free(clause1);
}
array_free(clauseArray);
/*(-A + A1 + A2 + A3)*/
array_insert_last(int,clause,-cnfIndex);
BmcCnfInsertClause(cnfClauses,clause);
array_free(clause);
/*(C + -A + -B)*/
array_insert_last(int,latchClause,-cnfIndex);
}/* if(!nextLatch)*/
FREE(latchBAig);
FREE(initBAig);
}/*arrayForEach..*/
cnfIndex = cnfClauses->cnfGlobalIndex++; /* C*/
array_insert_last(int,latchClause,cnfIndex); /*(C + -A + -B)*/
BmcCnfInsertClause(cnfClauses,latchClause);
array_free(latchClause);
/*(-C)*/
latchClause = array_alloc(int,0);
array_insert_last(int,latchClause,-cnfIndex);
BmcCnfInsertClause(cnfClauses,latchClause);
array_free(latchClause);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatInsertNewClauseForSimplePath | ( | array_t * | vertexArray, |
| Ntk_Network_t * | network, | ||
| int | step1, | ||
| int | step2, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable | ||
| ) |
CFile***********************************************************************
FileName [puresatMain.c]
PackageName [puresat]
Synopsis [Abstraction refinement for large scale invariant checking.]
Description [This file contains the functions to check invariant properties by the PureSAT abstraction refinement algorithm, which is entirely based on SAT solver, the input of which could be either CNF or AIG. It has several parts:
Localization-reduction base Abstraction K-induction or interpolation to prove the truth of a property Bounded Model Checking to find bugs Incremental concretization based methods to verify abstract bugs Incremental SAT solver to improve efficiency UNSAT proof based method to obtain refinement AROSAT to bring in only necessary latches into unsat proofs Bridge abstraction to get compact coarse refinement Refinement minization to guarrantee minimal refinements Unsat proof-based refinement minimization to eliminate multiple candidate by on SAT test Refinement prediction to decrease the number of refinement iterations Dynamic switching to redistribute computional resources to improve efficiency
For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", " Abstraction in symbolic model checking using satisfiability as the only decision procedure", "Efficient computation of small abstraction refinements", and "Efficient abstraction refinement in interpolation-based unbounded model checking"]
Author [Bing Li]
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 AutomaticEnd Function********************************************************************
Synopsis [Insert clauses of (Si!=Sj) for k-induction checking]
Description [Insert clauses of (Si!=Sj) for k-induction checking]
SideEffects []
SeeAlso []
Definition at line 100 of file puresatBMC.c.
{
int i,j,k,mvfSize,index1,index2, cnfIndex;
Ntk_Node_t * latch;
MvfAig_Function_t *latchMvfAig;
bAigEdge_t * latchBAig;
array_t * tmpclause, *clauseArray, * clause, * clause1,*latchClause;
mAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
char * Name;
boolean nextLatch = FALSE;
latchClause = array_alloc(int,0);
arrayForEachItem(char *,vertexArray,j,Name)
{
nextLatch = FALSE;
clause = array_alloc(int,0); /*(-A + -A1 + -A2 + -A3)*/
clauseArray = array_alloc(array_t *,0);/*(A + -A1)(A + -A2)(A + -A3)*/
latch = Ntk_NetworkFindNodeByName(network,Name);
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++){
if (latchBAig[i] == bAig_One)
nextLatch=TRUE;break; /* the clause is always true */
}
if(!nextLatch)
{
for(i=0; i< mvfSize; i++){
latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
index1 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step1,cnfClauses);
index2 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step2,cnfClauses);
cnfIndex = cnfClauses->cnfGlobalIndex++;
tmpclause = array_alloc(int, 3);
array_insert(int, tmpclause, 0, -index2);
array_insert(int, tmpclause, 1, -index1);
array_insert(int, tmpclause, 2, cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, index2);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
tmpclause = array_alloc(int, 2);
array_insert(int, tmpclause, 0, index1);
array_insert(int, tmpclause, 1, -cnfIndex);
BmcCnfInsertClause(cnfClauses, tmpclause);
array_free(tmpclause);
/*(-A + A1 + A2 + A3)*/
array_insert_last(int,clause,cnfIndex);
/*(A + -A1)(A + -A2)(A + -A3)*/
clause1 = array_alloc(int,0);/*(A + -A1/2/3)*/
array_insert_last(int,clause1,-cnfIndex);
array_insert_last(array_t *,clauseArray,clause1);
}
cnfIndex = cnfClauses->cnfGlobalIndex++; /*A*/
/*(A + -A1)(A + -A2)(A + -A3)*/
arrayForEachItem(array_t *,clauseArray,k,clause1)
{
array_insert_last(int,clause1,cnfIndex);
BmcCnfInsertClause(cnfClauses,clause1);
array_free(clause1);
}
array_free(clauseArray);
/*(-A + A1 + A2 + A3)*/
array_insert_last(int,clause,-cnfIndex);
BmcCnfInsertClause(cnfClauses,clause);
array_free(clause);
/*(C + -A + -B)*/
array_insert_last(int,latchClause,-cnfIndex);
}
FREE(latchBAig);
}
cnfIndex = cnfClauses->cnfGlobalIndex++; /* C*/
array_insert_last(int,latchClause,cnfIndex); /*(C + -A + -B)*/
BmcCnfInsertClause(cnfClauses,latchClause);
array_free(latchClause);
/*(-C)*/
latchClause = array_alloc(int,0);
array_insert_last(int,latchClause,-cnfIndex);
BmcCnfInsertClause(cnfClauses,latchClause);
array_free(latchClause);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatSetInitStatesForSimplePath | ( | array_t * | vertexArray, |
| Ntk_Network_t * | network, | ||
| BmcCnfClauses_t * | cnfClauses, | ||
| st_table * | nodeToMvfAigTable | ||
| ) |
Function********************************************************************
Synopsis [Insert clauses of initial states for k-induction checking]
Description [Insert clauses of initial states for k-induction checking]
SideEffects []
SeeAlso []
Definition at line 392 of file puresatBMC.c.
{
mAig_Manager_t *maigManager = Ntk_NetworkReadMAigManager(network);
Ntk_Node_t *latch, *latchInit;
MvfAig_Function_t *initMvfAig, *latchMvfAig;
bAigEdge_t *initBAig, *latchBAig;
int i,j, mvfSize;
char *nodeName;
for(j=0;j<array_n(vertexArray);j++)
{
nodeName = array_fetch(char *,vertexArray,j);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
latchInit = Ntk_LatchReadInitialInput(latch);
initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
if (latchMvfAig == NIL(MvfAig_Function_t)){
latchMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(latchMvfAig);
latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
}
mvfSize = array_n(initMvfAig);
initBAig = ALLOC(bAigEdge_t, mvfSize);
latchBAig = ALLOC(bAigEdge_t, mvfSize);
for(i=0; i< mvfSize; i++){
latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
initBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig, i));
}
BmcGenerateClausesFromStateTostate(maigManager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
FREE(initBAig);
FREE(latchBAig);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
