src/puresat/puresatFlatIP.c File Reference
#include "maigInt.h"#include "puresatInt.h"
Include dependency graph for puresatFlatIP.c:
Go to the source code of this file.
Functions | |
| boolean | PureSatCheckInv_FlatIP (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, PureSat_Manager_t *pm) |
Function Documentation
| boolean PureSatCheckInv_FlatIP | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| PureSat_Manager_t * | pm | ||
| ) |
CFile***********************************************************************
FileName [puresatFlatIP.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 []
Description []
SideEffects []
SeeAlso []Function********************************************************************
Synopsis [Interpolation algorithm without abstraction refinement]
Description [Interpolation algorithm without abstraction refinement]
SideEffects []
SeeAlso []
Definition at line 114 of file puresatFlatIP.c.
{
int NumofCurrentLatch=0,k;
bAig_Manager_t *manager;
bAigEdge_t property;
st_table * nodeToMvfAigTable;
double t1,t2,t0;
int first;
array_t *previousResultArray;
BmcOption_t *options = BmcOptionAlloc();
IP_Manager_t * ipm = IPManagerAlloc();
boolean firstTime;
int round=0, oldLength=0, nodes_in_coi=0;
st_table * tmpTable;
int oldPos1;
satManager_t * cm;
bAigEdge_t state, tmpState;
double tIP=0,tCon=0,tUnsat=0;
RTManager_t *rm;
pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
PureSatBmcGetCoiForLtlFormula(network, ltlFormula,pm->CoiTable);
ipm->CoiTable = pm->CoiTable;
options->printInputs = pm->printInputs;
options->dbgOut = pm->dbgOut;
pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
t0 = util_cpu_ctime();
NumofCurrentLatch=0;
t1 = util_cpu_ctime();
PureSatBmcGetCoiForLtlFormula_New(network, ltlFormula,pm->CoiTable);
t2 = util_cpu_ctime();
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(mAig_Manager_t)) {
(void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
BmcOptionFree(options);
return 1;
}
nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
previousResultArray = array_alloc(bAigEdge_t, 0);
first = 0;
manager->ipm = ipm;
t1 = util_cpu_ctime();
manager->test2LevelMini = 1;
bAig_PureSat_InitTimeFrame(network,manager,pm,0);
manager->test2LevelMini = 0;
if(pm->verbosity>=1) {
fprintf(vis_stdout,"after Init timeframe:\n");
PureSat_PrintAigStatus(manager);
}
manager->class_ = 1;
manager->test2LevelMini = 0;
property = PureSatCreatebAigOfPropFormula(network,
manager, 0, ltlFormula, BMC_NO_INITIAL_STATES);
property = bAig_Not(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);
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){
if(pm->dbgLevel == 1){
fprintf(vis_stdout,"find counter example of length 0\n");
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
0, 0,options, BMC_NO_INITIAL_STATES);
}
if(pm->dbgLevel == 2){
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
0, 0,options, BMC_NO_INITIAL_STATES);
}
return FALSE;
}
cm->option->coreGeneration = 1;
PureSat_SatFreeManager(cm);
manager->test2LevelMini = 1;
bAig_PureSat_ExpandTimeFrame(network, manager,pm,1, BMC_NO_INITIAL_STATES);
manager->class_ = 2;
manager->test2LevelMini = 0;
property = PureSatCreatebAigOfPropFormula(network,
manager, 1, 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,"after Init timeframe:\n");
PureSat_PrintAigStatus(manager);
}
state = manager->InitState;
cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
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){
if(pm->dbgLevel == 1){
fprintf(vis_stdout,"find counter example of length 1\n");
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
1, 0,options, BMC_NO_INITIAL_STATES);
}
if(pm->dbgLevel == 2){
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
1, 0,options, BMC_NO_INITIAL_STATES);
}
return FALSE;
}
cm->option->coreGeneration = 1;
PureSat_SatFreeManager(cm);
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));
pm->Length = k;
k = 1;
PureSat_CleanMask(manager,ResetGlobalVarMask);
PureSat_MarkGlobalVar(manager,1);
while(1){
oldLength = k;
if(k==1)
k++;
else
k += round-1;
pm->Length = k;
if(pm->verbosity>=1)
fprintf(vis_stdout,"\nk = %d InitState = %ld\n",k,manager->InitState);
manager->test2LevelMini = 1;
bAig_PureSat_ExpandTimeFrame(network, manager,pm, k, BMC_NO_INITIAL_STATES);
manager->test2LevelMini = 0;
if(pm->verbosity>=1) {
fprintf(vis_stdout,"After expand TF\n");
PureSat_PrintAigStatus(manager);
}
/*build property aig nodes*/
manager->class_ = k+1;
property = PureSatCreatebAigOfPropFormula(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);
if(cm->status==0){
if(pm->verbosity>=1)
fprintf(vis_stdout,"normal COI:\n");
nodes_in_coi = PureSat_CountNodesInCoi(cm);
if(pm->verbosity>=2)
fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
t1 = util_cpu_ctime();
sat_Main(cm);
if(pm->verbosity>=2)
sat_ReportStatistics(cm,cm->each);
rm = cm->rm;
t2 = util_cpu_ctime();
tUnsat = tUnsat+t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for Unsat:%g, Total:%g\n",
(double)((t2-t1)/1000.0),tUnsat/1000);
if(manager->NodesArray!=cm->nodesArray)
/*cm->nodesArray may be reallocated */
manager->NodesArray = cm->nodesArray;
}
if(cm->status == SAT_SAT){
/*SAT: first time->find bug, otherwise increase length*/
if(firstTime){
if(pm->dbgLevel == 1){
fprintf(vis_stdout,"found CEX of length %d\n",k);
BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
k, 0,options, BMC_NO_INITIAL_STATES);
}
if(pm->dbgLevel == 2){
BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
k, 0,options, BMC_NO_INITIAL_STATES);
}
sat_ArrayFree(manager->assertArray);
manager->assertArray = 0;
RT_Free(cm->rm);
PureSat_SatFreeManager(cm);
return FALSE;
}
/*find bogus bug, abort, increase length*/
else{
/* BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
k, 0,options, BMC_NO_INITIAL_STATES);*/
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
IP generation*/
assert(cm->currentDecision>=-1);
if(cm->currentDecision!=-1)
sat_Backtrack(cm, -1);
/*get rid of Conflict Clauses*/
PureSat_ResetManager(manager,cm,0);
/*Generate interpolant and test convergence*/
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);
ResetRTree(rm);
/*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();
tIP = tIP+t2-t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for generating IP:%g, Total:%g\n",
(double)((t2-t1)/1000.0),tIP/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"After generate IP,%ld:\n",manager->IPState);
PureSat_PrintAigStatus(manager);
}
manager->class_ = 2;
t1 = util_cpu_ctime();
RT_Free(cm->rm);
if(pm->verbosity>=1)
PureSat_PrintAigStatus(manager);
PureSat_ResetManager(manager,cm,0);
}
t1 = util_cpu_ctime();
/*Convergence test for interpolation*/
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);
return TRUE;
}
else{
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);
}
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){*/
}/*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:
