src/puresat/puresatIPAbRf.c File Reference
#include "maigInt.h"#include "puresatInt.h"
Include dependency graph for puresatIPAbRf.c:
Go to the source code of this file.
Functions | |
| boolean | PureSatIPOnCon (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, PureSat_Manager_t *pm) |
| boolean | PureSat_CheckAceByIP (Ntk_Network_t *network, PureSat_Manager_t *pm, PureSat_IncreSATManager_t *pism, array_t *vertexArray, int *k, Ctlsp_Formula_t *ltlFormula, bAigEdge_t *returnProp, array_t *previousResultArray) |
| boolean | PureSatCheckInv_IP (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, PureSat_Manager_t *pm) |
Function Documentation
| boolean PureSat_CheckAceByIP | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| PureSat_IncreSATManager_t * | pism, | ||
| array_t * | vertexArray, | ||
| int * | k, | ||
| Ctlsp_Formula_t * | ltlFormula, | ||
| bAigEdge_t * | returnProp, | ||
| array_t * | previousResultArray | ||
| ) |
Function********************************************************************
Synopsis [Using interpolation on abstractions]
Description []
SideEffects []
SeeAlso []
Definition at line 321 of file puresatIPAbRf.c.
{
int oldPos;
boolean firstTime,fork=0,ExistACE;
int round,oldLength,coiCon,coiAbs;
bAigEdge_t property;
double t1,t2,t3,t4,t5, threshold_sw=0;
satManager_t * cm;
array_t *bVarList,*mVarList;
bAigEdge_t state, tmpState;
BmcOption_t *options = BmcOptionAlloc();
bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
options->printInputs = TRUE;
options->verbosityLevel = BmcVerbosityMax_c;
assert(*k>=1);
manager->test2LevelMini = 1;
bAig_PureSat_ExpandTimeFrame(network, manager, pm,*k,
BMC_NO_INITIAL_STATES);
manager->test2LevelMini = 0;
PureSat_CleanMask(manager,ResetVisibleVarMask);
PuresatMarkVisibleVar(network,vertexArray,pm,0,*k+1);
PureSat_CleanMask(manager,ResetGlobalVarMask);
PureSat_MarkGlobalVar_AbRf(manager,1);
oldLength = *k;
while(1){
if(fork){
oldLength = pm->Length;
(*k) += round-1;
pm->Length = *k;
}
fork=1;
if(pm->verbosity>=1)
fprintf(vis_stdout,"\nk = %d InitState = %ld\n",*k,manager->InitState);
manager->test2LevelMini = 1;
t1 = util_cpu_ctime();
bAig_PureSat_ExpandTimeFrame(network, manager, pm,*k,
BMC_NO_INITIAL_STATES);
t2 = util_cpu_ctime();
pm->tExp += t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
(double)((t2-t1)/1000.0),pm->tExp/1000);
manager->test2LevelMini = 0;
PureSat_CleanMask(manager,ResetVisibleVarMask);
PuresatMarkVisibleVar(network,vertexArray,pm,0,*k+1);
manager->class_ = *k+1;
property = PureSatCreatebAigOfPropFormula(network,
manager, *k, ltlFormula, BMC_NO_INITIAL_STATES);
property = bAig_Not(property);
*returnProp = property;
if(pm->verbosity>=1)
fprintf(vis_stdout,"property is %ld\n",property);
oldPos = manager->nodesArraySize-bAigNodeSize;
if(pm->verbosity>=1){
fprintf(vis_stdout,"After expanding TF and building property\n");
PureSat_PrintAigStatus(manager);
}
firstTime = TRUE;
round = 0;
state = manager->InitState;
/*for one length*/
while(1){
round++;
if(pm->verbosity>=1)
fprintf(vis_stdout,"round:%d for k = %d\n",round,*k);
manager->assertArray = sat_ArrayAlloc(1);
if(state!=bAig_One)
sat_ArrayInsert(manager->assertArray,state);
cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
cm->option->IP = 1;
cm->option->AbRf = 1;
if(round == 1){
PureSat_ResetCoi(cm);
sat_SetConeOfInfluence(cm);
if(pm->verbosity>=1)
fprintf(vis_stdout,"COI nodes if check concrete model:\n");
coiCon = PureSat_CountNodesInCoi(cm);
if(pm->verbosity>=1)
fprintf(vis_stdout,"There are %d node in COI\n",coiCon);
}
t1 = util_cpu_ctime();
PureSatSetCOI(network,pm,cm,pm->vertexTable,0, *k,*k);
t2 = util_cpu_ctime();
pm->tPro += t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"process time:%g,total:%g\n",
(double)((t2-t1)/1000.0),pm->tPro/1000);
/*switch to concrete model*/
if(pm->verbosity>=1)
fprintf(vis_stdout,"normal COI:\n");
coiAbs = PureSat_CountNodesInCoi(cm);
if(round == 1){
if(pm->verbosity>=1)
fprintf(vis_stdout,"Coi of abs divided by Coi of con: %g\n",
(double)coiAbs/(double)coiCon);
#if SWITCH_DA
if((double)coiAbs/(double)coiCon >= 0.68&&*k>=5){
if(pm->switch_da == 0){
if(pm->verbosity>=1)
fprintf(vis_stdout,"Switch to DirAdd mode\n");
pm->switch_da = 1;
}
}
#endif
if(pm->Switch)
threshold_sw = 0.68;
else
threshold_sw = 1.1;
if(((double)coiAbs/(double)coiCon) >= threshold_sw&&*k>=5){
t3 = util_cpu_ctime();
sat_ArrayFree(manager->assertArray);
manager->assertArray = 0;
if(pm->verbosity>=1)
fprintf(vis_stdout,"Abs model is large, go to Concrete model\n");
ExistACE = PureSatIPOnCon(network,ltlFormula,pm);
PureSat_SatFreeManager(cm);
t1 = util_cpu_ctime();
if(pm->verbosity>=1)
fprintf(vis_stdout,"Run on concrete model: %g\n",(double)((t1-t3)/1000.0));
if(ExistACE){
pm->returnVal = 1;
return FALSE;
}
else{
pm->returnVal = -1;
return TRUE;
}
}
}
PureSatKillPseudoGV(network,pm,pm->vertexTable,1,*k);
PureSat_ResetManager(manager,cm,0);
PureSatProcessFanout(cm);
t1 = util_cpu_ctime();
sat_Main(cm);
if(pm->verbosity>=2)
sat_ReportStatistics(cm,cm->each);
cm->option->IP = 0;
if(manager->NodesArray!=cm->nodesArray)
/*cm->nodesArray may be reallocated*/
manager->NodesArray = cm->nodesArray;
t2 = util_cpu_ctime();
pm->tIPUnsat += t2 - t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for Unsat:%g, total:%g\n",
(double)((t2-t1)/1000.0),pm->tIPUnsat/1000);
t1 = util_cpu_ctime();
PureSatPostprocess(manager,cm,pm);
/*clean masks*/
sat_CleanDatabase(cm);
if(cm->status==SAT_UNSAT){
PureSatProcessDummy(manager,cm,cm->rm->root);
ResetRTree(cm->rm);
}
t2 = util_cpu_ctime();
pm->tPro += t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"process time:%g,total:%g\n",
(double)((t2-t1)/1000.0),pm->tPro/1000);
if(cm->status == SAT_SAT){
/*SAT: first time->find bug, otherwise increase length*/
if(firstTime){
if(pm->verbosity>=1)
fprintf(vis_stdout,"found abstract CEX of length %d\n",*k);
PureSat_UnMarkGlobalVar(manager,1);
RT_Free(cm->rm);
PureSat_SatFreeManager(cm);
sat_ArrayFree(manager->assertArray);
return TRUE;
}
else{
if(pm->verbosity>=1)
fprintf(vis_stdout,"find bogus bug at length k=%d,round=%d,increase length\n",*k,round);
sat_ArrayFree(manager->assertArray);
RT_Free(cm->rm);
PureSat_SatFreeManager(cm);
break;
}
}
else{
/*UNSAT: get IP, add to init states, until reach convergence, which
//means property is true
//Bing: IP generation*/
assert(cm->currentDecision>=-1);
if(cm->currentDecision!=-1)
sat_Backtrack(cm, -1);
PureSat_ResetManager(manager,cm,1);//get rid of Conflict Clauses
if(cm->option->coreGeneration&&cm->status == SAT_UNSAT){
manager->class_ = 1;
t1 = util_cpu_ctime();
tmpState = sat_GenerateFwdIP(manager,cm,cm->rm->root,1);
manager->IPState = PureSat_MapIP(manager,tmpState,1,0);
/*Wheneven there is baigNode generated, Reset_Manager is necessary,
//since NodeArray may be reallocated, # of Nodes changed*/
PureSat_ResetManager(manager,cm,0);
t2 = util_cpu_ctime();
pm->tIPGen += t2 -t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for generating and mapping IP:%g, total:%g\n",
(double)((t2-t1)/1000.0),pm->tIPGen/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"After generate IP,%ld:\n",manager->IPState);
PureSat_PrintAigStatus(manager);
}
manager->class_ = 2;
if(pm->verbosity>=1)
fprintf(vis_stdout,"After generate IP2:%ld\n",tmpState);
t4 = util_cpu_ctime();
RT_Free(cm->rm);
t5 = util_cpu_ctime();
pm->tGFree += (t5-t4);
if(pm->verbosity>=2)
fprintf(vis_stdout,"GFree time :%g\n",(t5-t4)/1000);
if(pm->verbosity>=1)
PureSat_PrintAigStatus(manager);
}
t1 = util_cpu_ctime();
if(PureSat_TestConvergeForIP_AbRf(network,cm,pm,vertexArray,
state,manager->IPState)){
t2 = util_cpu_ctime();
pm->tIPCon += t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
(double)((t2-t1)/1000.0),pm->tIPCon/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"After test convergence:\n");
PureSat_PrintAigStatus(manager);
}
fprintf(vis_stdout,"property is true\n");
PureSat_SatFreeManager(cm);
sat_ArrayFree(manager->assertArray);
return FALSE;
}
else{
t2 = util_cpu_ctime();
pm->tIPCon += t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
(double)((t2-t1)/1000.0),pm->tIPCon/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"After test convergence:\n");
PureSat_PrintAigStatus(manager);
}
manager->class_ = 0;
state = PureSat_Or(manager,state,manager->IPState);
if(pm->verbosity>=1)
fprintf(vis_stdout,"new InitState:%ld\n",state);
}
}/*else */
sat_ArrayFree(manager->assertArray);
PureSat_SatFreeManager(cm);
firstTime = FALSE;
}/*inner While(1){*/
}/*outer While(1){*/
return FALSE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean PureSatCheckInv_IP | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Main procedure of interpolation-based PureSat]
Description []
SideEffects []
SeeAlso []
Definition at line 621 of file puresatIPAbRf.c.
{
lsGen gen;
st_generator *stGen;
int NumofCurrentLatch=0,Length=0,tmp=0,NumofLatch=0,i,j,k;
int addtoAbs,latchThreshHold;
int NumInSecondLevel=0;
array_t * visibleArray = array_alloc(char *,0);
array_t * invisibleArray = array_alloc(char *,0);
array_t * refinement= array_alloc(char *,0);
array_t * CoiArray = array_alloc(char *,0);
array_t * arrayRC = array_alloc(char *,0);
array_t *tmpRefinement = array_alloc(char *,0);
array_t *tmpRefinement1 = array_alloc(char *,0),*previousResultArray ;
char * nodeName;
Ntk_Node_t * node, *latch;
boolean ExistACE = FALSE,realRefine=TRUE;
boolean firstTime = TRUE;
bAig_Manager_t *manager;
BmcOption_t * options;
bAigEdge_t property;
st_table * nodeToMvfAigTable;
double t1,t2,t5, t0,t3,t4,t4total=0;
PureSat_IncreSATManager_t * pism1;
IP_Manager_t * ipm = IPManagerAlloc();
satManager_t *cm;
int * sccArray=NULL, orderCt, satStat=0;
st_table * tmpTable;
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(bAig_Manager_t)) {
(void) fprintf(vis_stdout,
"** bmc error: run build_partition_maigs command first\n");
return 1;
}
nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
pm->supportTable = st_init_table(st_ptrcmp,st_ptrhash);
pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
pm->oldCoiTable = st_init_table(st_ptrcmp,st_ptrhash);
pm->vertexTable = st_init_table(strcmp, st_strhash);
pism1 = PureSatIncreSATManagerAlloc(pm);
t0 = util_cpu_ctime();
options = BmcOptionAlloc();
options->verbosityLevel = BmcVerbosityMax_c;
options->printInputs = TRUE;
t1 = util_cpu_ctime();
previousResultArray = array_alloc(bAigEdge_t, 0);
manager->class_ = 0;
manager->ipm = ipm;
manager->test2LevelMini = 1;
t3 = util_cpu_ctime();
bAig_PureSat_InitTimeFrame(network,manager,pm,0);
t5 = util_cpu_ctime();
pm->tExp += t5-t3;
if(pm->verbosity>=2)
fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
(double)((t5-t3)/1000.0),pm->tExp/1000);
manager->test2LevelMini = 0;
if(pm->verbosity>=1){
fprintf(vis_stdout,"after Init timeframe:\n");
PureSat_PrintAigStatus(manager);
}
manager->class_ = 1;
property = PureSatCreatebAigOfPropFormula(network,
manager, 0, ltlFormula, BMC_NO_INITIAL_STATES);
property = bAig_Not(property);
if(pm->verbosity>=1)
fprintf(vis_stdout,"property is %ld\n",property);
if(property==0)
return TRUE;
if(property==1)
return FALSE;
manager->assertArray = sat_ArrayAlloc(1);
sat_ArrayInsert(manager->assertArray,manager->InitState);
cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
cm->option->coreGeneration = 0;
cm->option->IP = 0;
if(pm->verbosity>=1)
fprintf(vis_stdout,"test length 0\n");
sat_Main(cm);
manager->NodesArray = cm->nodesArray;
if(cm->status==SAT_SAT){
fprintf(vis_stdout,"find counter example of length 0\n");
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
0, 0,options, BMC_NO_INITIAL_STATES);
return FALSE;
}
cm->option->coreGeneration = 1;
PureSat_SatFreeManager(cm);
manager->test2LevelMini = 1;
t3 = util_cpu_ctime();
bAig_PureSat_ExpandTimeFrame(network, manager,pm,1, BMC_NO_INITIAL_STATES);
t5 = util_cpu_ctime();
pm->tExp += t5-t3;
if(pm->verbosity>=2)
fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
(double)((t5-t3)/1000.0),pm->tExp/1000);
manager->class_ = 2;
manager->test2LevelMini = 0;
property = PureSatCreatebAigOfPropFormula(network,
manager, 1, ltlFormula, BMC_NO_INITIAL_STATES);
property = bAig_Not(property);
if(pm->verbosity>=1)
fprintf(vis_stdout,"property is %ld\n",property);
if(property==0)
return TRUE;
if(property==1)
return FALSE;
manager->assertArray = sat_ArrayAlloc(1);
sat_ArrayInsert(manager->assertArray,manager->InitState);
cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
cm->option->coreGeneration = 0;
cm->option->IP = 0;
if(pm->verbosity>=1)
fprintf(vis_stdout,"test length 1\n");
sat_Main(cm);
manager->NodesArray = cm->nodesArray;
if(cm->status==SAT_SAT){
fprintf(vis_stdout,"find counter example of length 1\n");
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
1, 0,options, BMC_NO_INITIAL_STATES);
return FALSE;
}
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"Time for testing Length 0 and 1: %g\n",(double)((t2-t1)/1000.0));
cm->option->coreGeneration = 1;
PureSat_SatFreeManager(cm);
Length = 2;
pm->Length = Length;
pism1->Length = Length;
manager->test2LevelMini = 1;
t3 = util_cpu_ctime();
bAig_PureSat_ExpandTimeFrame(network, manager,pm,2, BMC_NO_INITIAL_STATES);
t5 = util_cpu_ctime();
pm->tExp += t5-t3;
if(pm->verbosity>=2)
fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
(double)((t5-t3)/1000.0),pm->tExp/1000);
manager->class_ = 3;
manager->test2LevelMini = 0;
property = PureSatCreatebAigOfPropFormula(network,
manager, 2, ltlFormula, BMC_NO_INITIAL_STATES);
property = bAig_Not(property);
if(property==0)
return TRUE;
if(property==1)
return FALSE;
if(pm->verbosity>=1)
fprintf(vis_stdout,"property is %ld\n",property);
manager->test2LevelMini = 1;
NumofCurrentLatch=0;
t3 = util_cpu_ctime();
PureSatBmcGetCoiForLtlFormula_New(network, ltlFormula,pm->oldCoiTable);
t5 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"Compute NTK COI :%g\n",(t5-t3)/1000);
pm->CoiTable = st_copy(pm->oldCoiTable);
/*new COI computation*/
t3 = util_cpu_ctime();
tmpTable = PureSatGetAigCoi(network,pm,property);
st_foreach_item(tmpTable,stGen,&nodeName,NIL(char*)){
latch = Ntk_NetworkFindNodeByName(network,nodeName);
#if 1
if(!st_lookup(pm->CoiTable,latch,NIL(char*)))
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s is not in CoiTable\n",nodeName);
#endif
st_insert(pm->CoiTable,latch,(char*)0);
}
#if 1
st_foreach_item(pm->CoiTable,stGen,&latch,NIL(char*)){
nodeName = Ntk_NodeReadName(latch);
if(!st_lookup(tmpTable,nodeName,NIL(char*)))
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s is not in Aig CoiTable\n",nodeName);
}
#endif
st_free_table(tmpTable);
t5 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"Compute AIG COI :%g\n",(t5-t3)/1000);
t3 = util_cpu_ctime();
pm->vertexTable = PureSatCreateInitialAbstraction(network,
ltlFormula,&NumofCurrentLatch,pm);
t5 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"the time to create init abs:%g\n",(t5-t3)/1000);
tmpTable = st_init_table(strcmp,st_strhash);
PureSatCreateInitAbsByAIG(manager,pm,property,tmpTable);
st_foreach_item(tmpTable,stGen,&nodeName,NIL(char*)){
if(!st_lookup(pm->vertexTable,nodeName,NIL(char*))){
st_insert(pm->vertexTable,nodeName,(char*)0);
if(pm->verbosity>=1)
fprintf(vis_stdout,"insert %s into init abs model\n",nodeName);
}
}
st_free_table(tmpTable);
t3 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"the time to create init AIG abs:%g\n",(t3-t5)/1000);
PureSatPreProcLatch(network,pm);
t5 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"the time to preproc:%g\n",(t5-t3)/1000);
/*put indentical latches of visible latch into abs*/
t3 = util_cpu_ctime();
PureSatGetIndenticalLatch(network,pm);
st_foreach_item(pm->vertexTable,stGen,&nodeName,NIL(char*))
array_insert_last(char*,visibleArray,nodeName);
PureSatAddIdenLatchToAbs(network,pm,visibleArray);
arrayForEachItem(char*,visibleArray,i,nodeName)
st_insert(pm->vertexTable,nodeName,(char*)0);
array_free(visibleArray);
visibleArray = array_alloc(char*,0);
t5 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"Merge identical latch:%g\n",(t5-t3)/1000);
NumofCurrentLatch = st_count(pm->vertexTable);
t3 = util_cpu_ctime();
pm->AbsTable = st_init_table(st_ptrcmp,st_ptrhash);
Ntk_NetworkForEachLatch(network, gen, node){
if (st_lookup_int(pm->CoiTable, (char *) node, &tmp)){
NumofLatch++;
nodeName = Ntk_NodeReadName(node);
if(st_lookup(pm->vertexTable,nodeName,NIL(char *)))
{
array_insert_last(char *,visibleArray,nodeName);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
PureSatComputeTableForLatch(network,pm->AbsTable,latch);
}
else
array_insert_last(char *,invisibleArray,nodeName);
}
}
t5 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"the time to cmpute abs table:%g\n",(t5-t3)/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
}
CoiArray = array_dup(visibleArray);
array_append(CoiArray,invisibleArray);
pm->nicTable = st_init_table(strcmp,st_strhash);
pm->niaTable = st_init_table(strcmp,st_strhash);
PureSatComputeNumGatesInCone(network,pm,CoiArray);
t3 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"the time to cmpute gates in cone:%g\n",(t3-t5)/1000);
/*Using DFS + Dir Cone in abs*/
pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);
while(NumofCurrentLatch < NumofLatch)
{
t3 = util_cpu_ctime();
if(pm->verbosity>=1)
fprintf(vis_stdout,"Current Latches: %d, COI latches:%d,NEW Length:%d,\n",
NumofCurrentLatch,NumofLatch,pm->Length);
if(pm->verbosity>=2)
fprintf(vis_stdout,"General time: %g\n",(double)((t3-t0)/1000.0));
t1 = util_cpu_ctime();
tmpRefinement = array_alloc(char *,0);
memset(manager->ipm,0,sizeof(IP_Manager_t));
firstTime = TRUE;
pm->SufAbsTable = st_init_table(st_ptrcmp,st_ptrhash);
if(realRefine){
arrayForEachItem(char *,refinement,i,nodeName)
{
latch = Ntk_NetworkFindNodeByName(network,nodeName);
PureSatComputeTableForLatch(network,pm->AbsTable,latch);
st_insert(pm->vertexTable,nodeName,(char*)0);
}
array_append(visibleArray,refinement);
array_free(invisibleArray);
invisibleArray = array_alloc(char *,0);
st_foreach_item(pm->CoiTable,stGen,&latch,&i)
{
nodeName = Ntk_NodeReadName(latch);
if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
array_insert_last(char *,invisibleArray,nodeName);
}
}
st_free_table(pm->node2dfsTable);
pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);
arrayRC = PureSatComputeOrder_2(network,pm,visibleArray,invisibleArray,sccArray,&NumInSecondLevel);
t4 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for compute order: %g\n",(t4-t1)/1000);
if(pm->RefPredict){
orderCt=0;
if(array_n(pm->latchArray)>0){
if(pm->verbosity>=1)
fprintf(vis_stdout,"\n%d: Adding high RC value latch into abs model\n",orderCt++);
PureSatAddIdenLatchToAbs(network,pm,pm->latchArray);
NumofCurrentLatch+=array_n(pm->latchArray);
arrayForEachItem(char *,pm->latchArray,i,nodeName){
latch = Ntk_NetworkFindNodeByName(network,nodeName);
PureSatComputeTableForLatch(network,pm->AbsTable,latch);
st_insert(pm->vertexTable,nodeName,(char*)0);
}
array_append(visibleArray,pm->latchArray);
array_free(pm->latchArray);
array_free(invisibleArray);
invisibleArray = array_alloc(char *,0);
st_foreach_item(pm->CoiTable,stGen,&latch,&i)
{
nodeName = Ntk_NodeReadName(latch);
if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
array_insert_last(char *,invisibleArray,nodeName);
}
}
st_free_table(pm->node2dfsTable);
pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);
arrayRC = PureSatComputeOrder_2(network,pm,visibleArray,invisibleArray,sccArray,&NumInSecondLevel);
}
array_free(pm->latchArray);
}
PureSat_CleanMask(manager,ResetVisibleVarMask);
PuresatMarkVisibleVar(network,visibleArray,pm,0,pm->Length);
addtoAbs =(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)5)+1;
addtoAbs = addtoAbs >50 ? 50: addtoAbs;
array_free(invisibleArray);
invisibleArray = array_alloc(char *,0);
st_foreach_item(pm->CoiTable,stGen,&latch,&i)
{
nodeName = Ntk_NodeReadName(latch);
if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
array_insert_last(char *,invisibleArray,nodeName);
}
}
if(pm->verbosity>=1){
fprintf(vis_stdout,"After adding high RC latches:\n");
fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
}
t4 = util_cpu_ctime();
t4total += t4-t3;
if(pm->verbosity>=2)
fprintf(vis_stdout,"compute and add high RC latch and recompute order:%g,total:%g\n",
(t4-t3)/1000,(t4total/1000.0));
if(pm->verbosity>=1)
fprintf(vis_stdout,"NumInSecondLevel is %d ",NumInSecondLevel);
latchThreshHold = NumInSecondLevel;
if(pm->verbosity>=2){
fprintf(vis_stdout,"New latchThreshHold is %d\n",latchThreshHold);
}
t2 = util_cpu_ctime();
if(pm->verbosity>=2){
fprintf(vis_stdout,"Recompute Order: %g\n",(double)((t2-t1)/1000.0));
}
array_free(refinement);
refinement = array_alloc(char *,0);
}/* if(realRefine)*/
/* means no ref, just Length++.*/
realRefine =FALSE;
t1 = util_cpu_ctime();
ExistACE = PureSat_CheckAceByIP(network,pm,pism1, visibleArray,&Length,
ltlFormula, &property,previousResultArray);
if(ExistACE)
{
if(pm->returnVal == -1){
PureSatIncreSATManagerFree(pm,pism1);
/*PureSatManagerFree(pm);*/
array_free(CoiArray);
BmcOptionFree(options);
return FALSE;
}
pm->Length = Length;
pism1->Length = Length;
t2 = util_cpu_ctime();
pm->tIP += t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"Solve on IP: %g, total: %g\n",
(double)((t2-t1)/1000.0),(double)pm->tIP/1000.0);
if(ExistACE)
{
int Con=0;
if(pm->verbosity>=1)
fprintf(vis_stdout,"found Abstract Counterexample at length %d\n", pm->Length);
realRefine = TRUE;
/*incrementally check Concrete Model*/
if(pm->verbosity>=1)
fprintf(vis_stdout,"Begin building a new abstract model\n");
for(i=0;i<array_n(arrayRC);i=i+latchThreshHold)
{
Con = 0;
if(i>0)
latchThreshHold = array_n(arrayRC)-latchThreshHold;
for(j=0;j<latchThreshHold;j++)
{
if((i+j)<array_n(arrayRC))
{
nodeName = array_fetch(char *,arrayRC,i+j);
array_insert_last(char *,tmpRefinement,nodeName);
if(pm->verbosity>=2)
if(pm->verbosity>=2)
fprintf(vis_stdout, "picking %s\n",nodeName);
if((i+j)==(array_n(arrayRC)-1))
Con = 1;
}
else{
Con = 1;
break;
}
}/* for(j=0;*/
tmpRefinement1=array_dup(visibleArray);
array_append(tmpRefinement1,tmpRefinement);
t1 = util_cpu_ctime();
if(pm->verbosity>=2)
satStat = 1;
if(!PureSat_ConcretTest(network,pm,tmpRefinement1,property,previousResultArray,Con,satStat,1)){
t2 = util_cpu_ctime();
pm->tCon = pm->tCon+t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for finding a sufficient set on model: %g, total:%g\n",
(double)((t2-t1)/1000.0),(double)pm->tCon/1000.0);
if((i+j)>=array_n(arrayRC)){
fprintf(vis_stdout,"found real counterexamples\n");
PureSatIncreSATManagerFree(pm, pism1);
/*PureSatManagerFree(pm);*/
array_free(CoiArray);
BmcOptionFree(options);
return FALSE;
}
/* else{
;
}*/
}
else{
t2 = util_cpu_ctime();
pm->tCon = pm->tCon+t2-t1;
if(pm->verbosity>=1)
fprintf(vis_stdout,"found a sufficient model\n");
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for finding a sufficient set on model: %g, total:%g\n",
(double)((t2-t1)/1000.0),(double)pm->tCon/1000.0);
firstTime = FALSE;
arrayForEachItem(char *,tmpRefinement1,k,nodeName){
node = Ntk_NetworkFindNodeByName(network, nodeName);
if(!st_lookup(pm->SufAbsTable,(char *)node,NIL(char *)))
st_insert(pm->SufAbsTable,(char *)node, (char *)0);
else{
fprintf(vis_stdout,"wrong in sufabstable \n");
exit(0);
}
}
array_free(tmpRefinement1);
break;
}
array_free(tmpRefinement1);
}
t1 = util_cpu_ctime();
#if 1
if(pm->savedConCls){
sat_ArrayFree(pm->savedConCls);
pm->savedConCls = 0;
}
#endif
#if SWITCH_DA
refinement = PureSat_RefineOnAbs_DA(network,pm,property,previousResultArray,
latchThreshHold,sccArray,tmpRefinement);
#else
refinement = PureSat_RefineOnAbs(network,pm,property,previousResultArray,
latchThreshHold,sccArray,tmpRefinement);
#endif
array_free(tmpRefinement);
t2 = util_cpu_ctime();
pm->tRef = pm->tRef+t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for RefOnAbs: %g, total:%g\n",
(t2-t1)/1000.0,pm->tRef/1000);
st_free_table(pm->SufAbsTable);
pm->SufAbsTable = 0;
/*adjust parameters*/
NumofCurrentLatch+=array_n(refinement);
pm->Length++;
pism1->Length++;
Length++;
}/* if(pism2->cm->status == SAT_SAT)*/
} /*if(ExistACE)*/
else /* if TRUE from IP*/
{
t2 = util_cpu_ctime();
pm->tIP = pm->tIP+t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"Solve on IP: %g, total: %g\n",
(t2-t1)/1000.0,pm->tIP/1000.0);
fprintf(vis_stdout,"Convergence reached, exit\n");
PureSatIncreSATManagerFree(pm,pism1);
/*PureSatManagerFree(pm);*/
array_free(CoiArray);
BmcOptionFree(options);
return TRUE;
}
}/* while(NumofCurrentLatch < NumofLatch)*/
/*st_free_table(AbsTable);*/
/*Now go to the concrete model*/
if(pm->verbosity>=1)
fprintf(vis_stdout,"reach concrete model\n");
array_append(visibleArray,refinement);
array_free(refinement);
ExistACE = PureSatIPOnCon(network,ltlFormula,pm);
ExistACE = !ExistACE;
PureSatIncreSATManagerFree(pm,pism1);
/*PureSatManagerFree(pm);*/
array_free(CoiArray);
BmcOptionFree(options);
if(ExistACE)
return FALSE;
else
return TRUE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean PureSatIPOnCon | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| PureSat_Manager_t * | pm | ||
| ) |
CFile***********************************************************************
FileName [puresatAbRf.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 [Interpolation test for concrete model]
Description [used by dynamic switching]
SideEffects []
SeeAlso []
Definition at line 103 of file puresatIPAbRf.c.
{
int k;
bAig_Manager_t *manager;
bAigEdge_t property;
double t1,t2;
array_t *previousResultArray=0;
boolean firstTime;
int round;
st_table * tmpTable;
int oldPos1,nodes_in_coi=0;
satManager_t * cm;
bAigEdge_t state, tmpState;
double tCon=0;
RTManager_t *rm;
manager = Ntk_NetworkReadMAigManager(network);
if(pm->verbosity>=1)
fprintf(vis_stdout,"go to concrete model\n");
k = pm->Length;
round = 1;
PureSat_CleanMask(manager,ResetGlobalVarMask);
PureSat_MarkGlobalVar(manager,1);
while(1){
k += round-1;
pm->Length = k;
if(pm->verbosity>=1)
fprintf(vis_stdout,"\nk = %d InitState = %ld\n",k,manager->InitState);
manager->test2LevelMini = 1;
t1 = util_cpu_ctime();
bAig_PureSat_ExpandTimeFrame(network, manager,pm, k, BMC_NO_INITIAL_STATES);
t2 = util_cpu_ctime();
pm->tExp += t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
(double)((t2-t1)/1000.0),pm->tExp/1000);
manager->test2LevelMini = 0;
if(pm->verbosity>=1){
fprintf(vis_stdout,"After expand TF\n");
PureSat_PrintAigStatus(manager);
}
manager->class_ = k+1;
property = BmcCirCUsCreatebAigOfPropFormula(network,
manager, k, ltlFormula, BMC_NO_INITIAL_STATES);
property = bAig_Not(property);
if(property==0){
return TRUE;
}
if(property==1){
return FALSE;
}
oldPos1 = manager->nodesArraySize-bAigNodeSize;
if(pm->verbosity>=1){
fprintf(vis_stdout,"After expanding TF and building property\n");
PureSat_PrintAigStatus(manager);
}
firstTime = TRUE;
round = 0;
state = manager->InitState;
while(1){
round++;
if(pm->verbosity>=1)
fprintf(vis_stdout,"round:%d for k = %d\n",round,k);
manager->assertArray = sat_ArrayAlloc(1);
if(state!=bAig_One)
sat_ArrayInsert(manager->assertArray,state);
cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
cm->option->IP = 1;
if(cm->status==0){
if(pm->verbosity>=1)
fprintf(vis_stdout,"normal COI:\n");
if(pm->verbosity>=1) {
nodes_in_coi = PureSat_CountNodesInCoi(cm);
fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
}
t1 = util_cpu_ctime();
sat_Main(cm);
rm = cm->rm;
cm->option->IP = 0;
if(manager->NodesArray!=cm->nodesArray)
/*cm->nodesArray may be reallocated */
manager->NodesArray = cm->nodesArray;
t2 = util_cpu_ctime();
pm->tIPUnsat += t2 - t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for Unsat:%g, total:%g\n",
(double)((t2-t1)/1000.0),pm->tIPUnsat/1000);
}
if(cm->status == SAT_SAT){
/*SAT: first time->find bug, otherwise increase length*/
if(firstTime){
fprintf(vis_stdout,"found CEX of length %d\n",k);
sat_ArrayFree(manager->assertArray);
manager->assertArray = 0;
RT_Free(cm->rm);
PureSat_SatFreeManager(cm);
return FALSE;
}
else{
if(pm->verbosity>=1)
fprintf(vis_stdout,"find bogus bug at length k=%d,round=%d,increase length\n",k,round);
sat_ArrayFree(manager->assertArray);
RT_Free(cm->rm);
PureSat_SatFreeManager(cm);
break;
}
}
else{
/*UNSAT: get IP, add to init states, until reach convergence, which
means property is true
Bing: IP generation*/
assert(cm->currentDecision>=-1);
if(cm->currentDecision!=-1)
sat_Backtrack(cm, -1);
/*get rid of Conflict Clauses*/
PureSat_ResetManager(manager,cm,1);
if(cm->option->coreGeneration&&cm->status == SAT_UNSAT){
manager->class_ = 1;
t1 = util_cpu_ctime();
tmpState = sat_GenerateFwdIP(manager,cm,cm->rm->root,1);
manager->IPState = PureSat_MapIP(manager,tmpState,1,0);
/*Wheneven there is baigNode generated, Reset_Manager is necessary,
//since NodeArray may be reallocated, # of Nodes changed*/
PureSat_ResetManager(manager,cm,0);
t2 = util_cpu_ctime();
pm->tIPGen += t2 -t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for generating and mapping IP:%g, total:%g\n",
(double)((t2-t1)/1000.0),pm->tIPGen/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"After generate IP,IP2:%ld,%ld:\n",manager->IPState,tmpState);
PureSat_PrintAigStatus(manager);
}
manager->class_ = 2;
t1 = util_cpu_ctime();
RT_Free(cm->rm);
if(pm->verbosity>=1)
PureSat_PrintAigStatus(manager);
}
t1 = util_cpu_ctime();
if(PureSat_TestConvergeForIP(manager,pm,cm,state,manager->IPState)){
t2 = util_cpu_ctime();
tCon = tCon+t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for generating Convergence:%g, Total:%g\n",
(double)((t2-t1)/1000.0),tCon/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"After test convergence:\n");
PureSat_PrintAigStatus(manager);
}
fprintf(vis_stdout,"property is true\n");
PureSat_SatFreeManager(cm);
sat_ArrayFree(manager->assertArray);
return TRUE;
}
else{
t2 = util_cpu_ctime();
pm->tIPCon += t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
(double)((t2-t1)/1000.0),pm->tIPCon/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"After test convergence:\n");
PureSat_PrintAigStatus(manager);
}
manager->class_ = 0;
state = PureSat_Or(manager,state,manager->IPState);
PureSat_ResetManager(manager,cm,0);
if(pm->verbosity>=1)
fprintf(vis_stdout,"new InitState:%ld\n",state);
}
}/*else*/
sat_ArrayFree(manager->assertArray);
manager->assertArray = 0;
PureSat_SatFreeManager(cm);
firstTime = FALSE;
}/*inner While(1){*/
/*sat_ArrayInsert(previousResultArray, bAig_Not(property)); */
}/*outer While(1){*/
st_free_table(tmpTable);
sat_ArrayFree(manager->EqArray);
return TRUE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
