src/puresat/puresatRefine.c File Reference
#include "puresatInt.h"
Include dependency graph for puresatRefine.c:
Go to the source code of this file.
Functions | |
| array_t * | PureSatRefineOnAbs (Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property, int latchThreshHold) |
Function Documentation
| array_t* PureSatRefineOnAbs | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | property, | ||
| int | latchThreshHold | ||
| ) |
CFile***********************************************************************
FileName [puresatRefine.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 [Refinement procedure of PURESAT algorithm]
Description [Refinement procedure of PURESAT algorithm]
SideEffects []
SeeAlso []
Definition at line 101 of file puresatRefine.c.
{
mAig_Manager_t *maigManager = Ntk_NetworkReadMAigManager(network);
lsGen gen;
Ntk_Node_t *latch;
FILE *fp, *fp1;
BmcOption_t *options,*option2;
int i,j,k,Length,beginPosition=0;
int NumInSecondLevel=0;
array_t * tmpRefinement,*tmpArray1,*tmpArray2;
array_t *tmpModel,*tmpRefinement1;
/*st_table * RefinementTable, *CandidateTable;*/
array_t *Pclause, *tmpRefinement2, *tmpRefinement3, *oriSufArray;
char buffer[1024],str[100];
char *name, *coreFile, *tmpCoreFile, *coreFile1=(char *)0;
int oldLength=0,oriCoreSize, CoreSize,weight;
st_table *nodeToMvfAigTable;
BmcCnfStates_t *cnfstate;
int oldNumOfLatchInCore;
int newNumOfLatchInCore,NumOfLatchInModel,round;
boolean VarInCoreIsEnough = FALSE, LatchFromCore = FALSE;
boolean firstTime = TRUE;
long t1,t2,t3,t4;
st_table * localSufAbsTable;
PureSat_IncreSATManager_t * pism = PureSatIncreSATManagerAlloc(pm);
satManager_t * cm = pism->cm;
BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
st_table *vertexTable = pm->vertexTable;
st_table *SufAbsTable = pm->SufAbsTable;
/*st_table *CoiTable = pm->CoiTable;*/
/*st_table *supportTable = pm->supportTable;*/
/* st_table *AbsTable = pm->AbsTable;*/
t1 = util_cpu_ctime();
cm->option->clauseDeletionHeuristic = 0;
cm->option->incTraceObjective = 0;
pism->Length = pm->Length;
Length = pm->Length;
coreFile = BmcCreateTmpFile();
tmpCoreFile = BmcCreateTmpFile();
strcpy(str,"coreFile: ");
strcat(str,coreFile);
strcat(str,", tmpCoreFile: ");
strcat(str,tmpCoreFile);
strcat(str,"\n");
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s",str);
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\n");
exit (0);
}
option2 = BmcOptionAlloc();
option2->satInFile = BmcCreateTmpFile();
option2->satOutFile = BmcCreateTmpFile();
options = BmcOptionAlloc();
options->satInFile = BmcCreateTmpFile();
options->satOutFile = BmcCreateTmpFile();
newNumOfLatchInCore = 0;
NumOfLatchInModel = 0;
tmpModel = array_alloc(char *,0);
oriSufArray = array_alloc(char *,0);
Ntk_NetworkForEachLatch(network, gen, latch){
name = Ntk_NodeReadName(latch);
if(st_lookup(vertexTable,name,NIL(char *))){
array_insert_last(char *,tmpModel,name);
NumOfLatchInModel++;
}
else
if(st_lookup(SufAbsTable,latch,NIL(char *))){
newNumOfLatchInCore++;
array_insert_last(char *,oriSufArray,name);
}
}
localSufAbsTable = st_copy(SufAbsTable);
//tmpRefinement2 = array_alloc(char *,0);
tmpRefinement3 = array_alloc(char *,0);
//tmpArray1 = array_alloc(char *,0);
//tmpArray2 = array_alloc(char *,0);
weight = (NumOfLatchInModel+newNumOfLatchInCore+1)*10000;
round=0;
round++;
if(pm->verbosity>=2)
fprintf(vis_stdout,"round: %d\n",round);
oldNumOfLatchInCore = newNumOfLatchInCore;
pm->ClsidxToLatchTable = st_init_table(st_numcmp,st_numhash);
PureSatGenerateClausesForPath_EnhanceInit(network,0,Length,pism,pm,nodeToMvfAigTable,localSufAbsTable);
Pclause = array_alloc(int,0);
array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(maigManager,property,
Length, cnfClauses));
BmcCnfInsertClause(cnfClauses, Pclause);
array_free(Pclause);
CoreSize=cnfClauses->noOfClauses;
oriCoreSize = CoreSize;
cm->option->coreGeneration = 1;
cm->fp = fopen(tmpCoreFile, "w");
if(pm->verbosity>=2)
PureSatWriteClausesToFile(pism,maigManager,coreFile1);
t1 = util_cpu_ctime();
PureSatReadClauses(pism,pm);
sat_Main(cm);
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for SAT Solver(satMain): %g\n",(double)((t2-t1)/1000.0));
fclose(cm->fp);
if(cm->status == SAT_SAT){
fprintf(vis_stderr,"This instance is supposed to be UNSAT, wrong and exit\n");
exit(0);
}
cm->stdOut = vis_stdout;
cm->option->coreGeneration = 0;
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for satMain: %g\n",(double)((t2-t1)/1000.0));
CoreSize = cm->numOfClsInCore;
if(pm->verbosity>=2)
fprintf(vis_stdout,"CoreSize:%d/OriCoreSize:%d\n", CoreSize,oriCoreSize);
fp1 = fopen(coreFile, "w");
fp = fopen(tmpCoreFile, "r");
sprintf(buffer,"p cnf %d %d 0\n", cm->initNumVariables, cm->numOfClsInCore);
fputs(buffer, fp1);
while(fgets(buffer,1024,fp)){
fputs(buffer, fp1);
}
fclose(fp);
fclose(fp1);
//tmpRefinement1 = array_alloc(char *,0);
/* generate sufficient refinement */
st_free_table(localSufAbsTable);
localSufAbsTable = st_init_table(st_ptrcmp,st_ptrhash);
t3 = util_cpu_ctime();
tmpRefinement1 = PureSatGetLatchFromTable(network,pm,coreFile);
t4 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for PureSatGetLatchFromTable: %g\n",(double)((t4-t3)/1000.0));
if(array_n(tmpRefinement1)>array_n(oriSufArray)){
array_free(tmpRefinement1);
tmpRefinement1 = array_dup(oriSufArray);
}
else{
array_free(oriSufArray);
oriSufArray = array_dup(tmpRefinement1);
}
if(pm->verbosity>=2)
fprintf(vis_stdout,"All latches picked from UNSAT Proof:\n");
arrayForEachItem(char *,tmpRefinement1,i,name){
if(pm->verbosity>=2)
fprintf(vis_stdout," %s ",name);
latch = Ntk_NetworkFindNodeByName(network,name);
st_insert(localSufAbsTable,latch,(char *)0);
}
if(pm->verbosity>=2){
fprintf(vis_stdout,"\n");
fprintf(vis_stdout,"tmpModel: \n");
}
arrayForEachItem(char *,tmpModel,i,name){
if(pm->verbosity>=2)
fprintf(vis_stdout," %s ",name);
latch = Ntk_NetworkFindNodeByName(network,name);
st_insert(localSufAbsTable,latch,(char *)0);
}
if(pm->verbosity>=2)
fprintf(vis_stdout,"\n");
newNumOfLatchInCore = array_n(tmpRefinement1);
BmcCnfClausesFree(pism->cnfClauses);
if(pm->verbosity>=2)
fprintf(vis_stdout,"newNumOfLatchInCore/oldNumOfLatchInCore=%f\n",(double)newNumOfLatchInCore/(double)oldNumOfLatchInCore);
/* Add the refinement to vertexTable*/
arrayForEachItem(char *,tmpRefinement1,i,name){
st_insert(vertexTable, name,(char*)0);
}
pism->cnfClauses = BmcCnfClausesAlloc();
cnfClauses = pism->cnfClauses;
if(array_n(tmpRefinement1))
{
tmpRefinement = PureSatGenerateRingFromAbs(network,pm,tmpRefinement1,&NumInSecondLevel);
/* latchThreshHold = (latchThreshHold <= NumInSecondLevel) ? latchThreshHold:NumInSecondLevel;*/
array_free(tmpRefinement1);
LatchFromCore = TRUE;
for(i=0;i<array_n(tmpRefinement);i=i+latchThreshHold)
{
for(j=0;j<latchThreshHold;j++)
{
if((i+j)<array_n(tmpRefinement))
{
name = array_fetch(char *,tmpRefinement,i+j);
array_insert_last(char *,tmpRefinement3,name);
if(pm->verbosity>=1)
fprintf(vis_stdout, "picking %s\n",name);
}
else
break;
}
tmpRefinement2=array_dup(tmpModel);
array_append(tmpRefinement2,tmpRefinement3);
if(!PureSatExistCE(network,pism,option2,tmpRefinement2,property,pm,0)){
VarInCoreIsEnough = TRUE;
array_free(tmpRefinement2);
for(k=i+j;k<array_n(tmpRefinement);k++)
{
name = array_fetch(char *,tmpRefinement,k);
if(st_lookup(vertexTable,name,NIL(char *))){
st_delete(vertexTable,&name,NIL(char *));
}
}
break;
}
firstTime = FALSE;
beginPosition = array_n(tmpRefinement2);
array_free(tmpRefinement2);
oldLength = Length;
}
array_free(tmpRefinement);
tmpRefinement = array_dup(tmpRefinement3); /* now tmpRefinement1 contains the
latches in Core*/
array_free(tmpRefinement3);
oldLength=0;
beginPosition=0;
BmcCnfClausesFree(pism->cnfClauses);
pism->cnfClauses = BmcCnfClausesAlloc();
}
#if 1
if(!VarInCoreIsEnough){
fprintf(vis_stderr,"this should never happen, wrong\n");
exit(0);
}
#endif
//tmpRefinement = array_dup(tmpRefinement1);
//array_free(tmpRefinement1);
# if 1
/*Refinement Minimization
try all the candidates*/
for(i=array_n(tmpRefinement)-1;i>=0;i--)
{
name = array_fetch(char *,tmpRefinement,i);
if(pm->verbosity>=1)
fprintf(vis_stdout,"RefMin: testing %s\n",name);
tmpArray2 = PureSatRemove_char(tmpRefinement,i);
tmpArray1 = array_dup(tmpModel);
array_append(tmpArray1,tmpArray2);
cnfstate = BmcCnfClausesFreeze(pism->cnfClauses);
if(PureSatExistCE(network,pism,option2,tmpArray1,property,pm,0))
array_free(tmpArray2);
else /*delete it*/
{
/* i--;*/
name = array_fetch(char *, tmpRefinement,i);
if(st_lookup(vertexTable, name,NIL(char *)))
st_delete(vertexTable, &name, NIL(char *));
else
fprintf(vis_stderr," %s should be in vertexTable, Wrong!!!\n",name);
array_free(tmpRefinement);
tmpRefinement = tmpArray2;
}
array_free(tmpArray1);
BmcCnfClausesRestore(pism->cnfClauses, cnfstate);
FREE(cnfstate);
}
//BmcCnfClausesFree(pism->cnfClauses);
#endif
if(pm->verbosity>=1){
fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
arrayForEachItem(char *,tmpRefinement,i,name)
fprintf(vis_stdout,"%s\n",name);
}
BmcOptionFree(option2);
BmcOptionFree(options);
unlink(coreFile);
unlink(tmpCoreFile);
FREE(coreFile);
FREE(tmpCoreFile);
array_free(oriSufArray);
st_free_table(pm->ClsidxToLatchTable);
pm->ClsidxToLatchTable = NIL(st_table);
PureSatIncreSATManagerFree(pm,pism);
return tmpRefinement;
}
Here is the call graph for this function:
Here is the caller graph for this function:
