src/puresat/puresatIPUtil.c File Reference
#include "puresatInt.h"
Include dependency graph for puresatIPUtil.c:
Go to the source code of this file.
Functions | |
| static int | NodeIndexCompare (const void *x, const void *y) |
| static int | StringCheckIsInteger (char *string, int *value) |
| RTnode_t | RTCreateNode (RTManager_t *rm) |
| IP_Manager_t * | IPManagerAlloc () |
| void | IPManagerFree (IP_Manager_t *ipm) |
| int | PureSat_IdentifyConflict (satManager_t *cm, long left, bAigEdge_t right, bAigEdge_t node) |
| void | PureSatBmcGetCoiForNtkNode_New (Ntk_Node_t *node, st_table *CoiTable, st_table *visited) |
| void | PureSatBmcGetCoiForLtlFormulaRecursive_New (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable, st_table *visited) |
| void | PureSatBmcGetCoiForLtlFormula_New (Ntk_Network_t *network, Ctlsp_Formula_t *formula, st_table *ltlCoiTable) |
| void | PureSat_MarkTransitiveFaninForNode (satManager_t *cm, bAigEdge_t v, unsigned int mask) |
| void | PureSat_MarkTransitiveFaninForArray (satManager_t *cm, satArray_t *arr, unsigned int mask) |
| void | PureSat_MarkTransitiveFaninForNode2 (mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask) |
| void | PureSat_MarkTransitiveFaninForArray2 (mAig_Manager_t *manager, satArray_t *arr, unsigned int mask) |
| void | PureSat_MarkTransitiveFaninForNode3 (mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask) |
| void | PureSat_MarkTransitiveFaninForArray3 (mAig_Manager_t *manager, satArray_t *arr, unsigned int mask) |
| void | PureSat_MarkTransitiveFaninForNode4 (mAig_Manager_t *manager, bAigEdge_t v, unsigned int mask, int bound) |
| void | PureSat_MarkTransitiveFaninForArray4 (mAig_Manager_t *manager, satArray_t *arr, unsigned int mask, int bound) |
| void | PureSat_CleanMask (mAig_Manager_t *manager, unsigned int mask) |
| void | PureSat_SetCOI (satManager_t *cm) |
| void | PureSat_ResetCoi (satManager_t *cm) |
| void | PureSatSetLatchCOI (Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, st_table *AbsTable, int from, int to) |
| void | PureSatSetLatchCOI2 (Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, bAigEdge_t obj, int bound) |
| void | PureSatSetCOI (Ntk_Network_t *network, PureSat_Manager_t *pm, satManager_t *cm, st_table *AbsTable, int from, int to, int bound) |
| void | PureSatAbstractLatch (bAig_Manager_t *manager, bAigEdge_t v, st_table *tmpTable) |
| void | PureSatKillPseudoGVNode (bAig_Manager_t *manager, bAigEdge_t v, st_table *tmpTable) |
| void | PureSatKillPseudoGV (Ntk_Network_t *network, PureSat_Manager_t *pm, st_table *AbsTable, int from, int to) |
| int | PureSat_CountNodesInCoi (satManager_t *cm) |
| void | PureSat_Check (bAig_Manager_t *manager, bAigEdge_t v) |
| void | PureSat_CheckFanoutFanin (bAig_Manager_t *manager) |
| void | PureSat_ResetManager (mAig_Manager_t *manager, satManager_t *cm, int clean) |
| void | PureSat_RestoreAigForDummyNode (mAig_Manager_t *manager, int oldPosition) |
| void | PureSatProcessFanout (satManager_t *cm) |
| long | PureSatRecoverFanoutNode (satManager_t *cm, bAigEdge_t v) |
| void | PureSatRecoverISVNode (satManager_t *cm, bAigEdge_t v) |
| void | PureSatRecoverFanout (satManager_t *cm, PureSat_Manager_t *pm) |
| void | PureSatCheckCoiNode (bAig_Manager_t *manager, bAigEdge_t node) |
| void | PureSatCheckCoi (bAig_Manager_t *manager) |
| void | PureSatPreprocess (Ntk_Network_t *network, satManager_t *cm, PureSat_Manager_t *pm, st_table *vertexTable, int Length) |
| void | PureSatPostprocess (bAig_Manager_t *manager, satManager_t *cm, PureSat_Manager_t *pm) |
| int | PureSat_TestConvergeForIP (mAig_Manager_t *manager, PureSat_Manager_t *pm, satManager_t *cm, bAigEdge_t state1, bAigEdge_t state2) |
| int | PureSat_TestConvergeForIP_AbRf (Ntk_Network_t *network, satManager_t *cm, PureSat_Manager_t *pm, array_t *CoiArray, bAigEdge_t state1, bAigEdge_t state2) |
| satManager_t * | PureSat_SatManagerAlloc (bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t object, array_t *auxObjectArray) |
| satManager_t * | PureSat_SatManagerAlloc_WOCOI (mAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t object, array_t *auxObjectArray) |
| void | PureSat_SatFreeManager (satManager_t *cm) |
| void | PureSat_PrintAigStatus (mAig_Manager_t *manager) |
| void | PureSat_MarkGlobalVar (bAig_Manager_t *manager, int length) |
| void | PureSat_UnMarkGlobalVar (bAig_Manager_t *manager, int length) |
| void | PureSat_MarkGlobalVar_AbRf (bAig_Manager_t *manager, int length) |
| void | PuresatMarkVisibleVarWithVPGV (Ntk_Network_t *network, array_t *visibleArray, PureSat_Manager_t *pm, int from, int to) |
| void | PuresatMarkVisibleVar (Ntk_Network_t *network, array_t *visibleArray, PureSat_Manager_t *pm, int from, int to) |
| bAigEdge_t | PureSat_MapIPRecur (mAig_Manager_t *manager, bAigEdge_t node, st_table *tmpTable) |
| bAigEdge_t | PureSat_MapIP (mAig_Manager_t *manager, bAigEdge_t node, int from, int to) |
| void | PureSatProcessDummy (bAig_Manager_t *manager, satManager_t *cm, RTnode_t RTnode) |
| bAigEdge_t | PureSat_FindNodeByName (bAig_Manager_t *manager, nameType_t *name, int bound) |
| bAigEdge_t | PureSatCreatebAigOfPropFormula (Ntk_Network_t *network, bAig_Manager_t *manager, int bound, Ctlsp_Formula_t *ltl, int withInitialState) |
| void | PureSatMarkObj (bAig_Manager_t *manager, long from, long to) |
| boolean | PureSat_ConcretTest (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *sufArray, bAigEdge_t property, array_t *previousResultArray, int Con, int satStat, int inc) |
| boolean | PureSat_ConcretTest_Core (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *sufArray, bAigEdge_t property, array_t *previousResultArray, st_table *junkTable) |
| void | PureSatGenerateRingForNode (Ntk_Network_t *network, PureSat_Manager_t *pm, Ntk_Node_t *node1, array_t *ringArray, int *dfs) |
| array_t * | PureSatGenerateRing (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *coreArray, int *dfs) |
| void | PureSatGenerateDfs (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *vertexArray) |
| array_t * | PureSatComputeOrder_2 (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *vertexArray, array_t *invisibleArray, int *sccArray, int *NumInSecondLevel) |
| void | PureSatAddIdenLatchToAbs (Ntk_Network_t *network, PureSat_Manager_t *pm, array_t *nameArray) |
| void | PureSatCreateInitAbsByAIG (bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t node, st_table *tmpTable) |
| void | PureSat_GetLatchForNode (bAig_Manager_t *manager, PureSat_Manager_t *pm, bAigEdge_t node, array_t *nameArray, st_table *tmpTable, int cut) |
| st_table * | PureSatGetAigCoi (Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property) |
| void | PureSatPreProcLatch (Ntk_Network_t *network, PureSat_Manager_t *pm) |
| void | PureSatGetIndenticalLatch (Ntk_Network_t *network, PureSat_Manager_t *pm) |
Function Documentation
| IP_Manager_t* IPManagerAlloc | ( | ) |
Function********************************************************************
Synopsis [Allocate an interpolation manager]
Description [Allocate an interpolation manager]
SideEffects []
SeeAlso []
Definition at line 227 of file puresatIPUtil.c.
{
IP_Manager_t * ipm = ALLOC(IP_Manager_t, 1);
memset(ipm,0,sizeof(IP_Manager_t));
return ipm;
}
Here is the caller graph for this function:
| void IPManagerFree | ( | IP_Manager_t * | ipm | ) |
Function********************************************************************
Synopsis [Free an interpolation manager]
Description [Free an interpolation manager]
SideEffects []
SeeAlso []
Definition at line 248 of file puresatIPUtil.c.
{
FREE(ipm);
}
| static int NodeIndexCompare | ( | const void * | x, |
| const void * | y | ||
| ) | [static] |
CFile***********************************************************************
FileName [puresatIPUtil.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 [Comparison function for sorting]
Description [Comparison function for sorting]
SideEffects []
SeeAlso []
Definition at line 116 of file puresatIPUtil.c.
{
int n1, n2;
n1 = *(int *)x;
n2 = *(int *)y;
return(n1 > n2);
}
Here is the caller graph for this function:
| void PureSat_Check | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | v | ||
| ) |
Function********************************************************************
Synopsis [Sanity check for one node for abstraction processsing]
Description [Sanity check for one node for abstraction processsing]
SideEffects []
SeeAlso []
Definition at line 1128 of file puresatIPUtil.c.
{
bAigEdge_t *fan,*fan1,nfan1;
bAigEdge_t nfan,cur,child,tmpchild,v1,other,cur1;
int size,i,j,find=0,inver,left,left1;
nfan = nFanout(v);
fan = (bAigEdge_t *)fanout(v);
if(fan == 0){
assert(nfan==0);
return;
}
size = 0;
for(i=0; fan[i]!=0; i++){
size++;
cur = fan[i];
left = 1;
inver = 0;
if(SATisInverted(cur))
left = 0;
cur >>= 1;
if(SATisInverted(cur))
inver = 1;
cur = SATnormalNode(cur);
child = inver? SATnormalNode(v)+1:SATnormalNode(v);
if(left)
tmpchild = leftChild(cur);
else
tmpchild = rightChild(cur);
assert(tmpchild == child);
/*check the other child*/
find = 0;
other = left?rightChild(cur):leftChild(cur);
assert(other!=bAig_NULL);
v1 = SATnormalNode(other);
nfan1 = nFanout(v1);
fan1 = (bAigEdge_t *)fanout(v1);
assert(nfan1!=0&&fan1!=0);
for(j=0; fan1[j]!=0; j++){
cur1 = fan1[j];
left1 = 1;
if(SATisInverted(cur1))
left1 = 0;
assert(j<nfan1);
if((SATnormalNode(cur1>>1)==cur)&&(left1!=left)){
find = 1;
break;
}
}
assert(find);
}
assert(nfan==size);
}
Here is the caller graph for this function:
| void PureSat_CheckFanoutFanin | ( | bAig_Manager_t * | manager | ) |
Function********************************************************************
Synopsis [Sanity check for abstraction processsing]
Description [Sanity check for abstraction processsing]
SideEffects []
SeeAlso []
Definition at line 1201 of file puresatIPUtil.c.
{
bAigEdge_t i,v;
for(i=bAigNodeSize;i<manager->nodesArraySize;i+=bAigNodeSize){
v = i;
if((flags(v) & IsCNFMask))
continue;
PureSat_Check(manager,v);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_CleanMask | ( | mAig_Manager_t * | manager, |
| unsigned int | mask | ||
| ) |
Function********************************************************************
Synopsis [clean a certain mask for all the aig nodes]
Description [clean a certain mask for all the aig nodes]
SideEffects []
SeeAlso []
Definition at line 688 of file puresatIPUtil.c.
{
bAigEdge_t i;
for(i=bAigNodeSize; i<manager->nodesArraySize;i+=bAigNodeSize)
flags(i)&=mask;
}
Here is the caller graph for this function:
| boolean PureSat_ConcretTest | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | sufArray, | ||
| bAigEdge_t | property, | ||
| array_t * | previousResultArray, | ||
| int | Con, | ||
| int | satStat, | ||
| int | inc | ||
| ) |
Function********************************************************************
Synopsis [procedure of concretization]
Description []
SideEffects []
SeeAlso []
Definition at line 3027 of file puresatIPUtil.c.
{
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
int status,i,nodes_in_coi=0;
satManager_t *cm;
char *name;
double t1,t2;
satArray_t *saved;
st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
bAigEdge_t from,*lp;
arrayForEachItem(char *,sufArray,i,name){
st_insert(SufAbsNameTable,name,(char*)0);
}
manager->assertArray = sat_ArrayAlloc(1);
sat_ArrayInsert(manager->assertArray,manager->InitState);
cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
cm->option->coreGeneration = 0;
cm->option->RT = 0;
cm->option->AbRf = 1;
if(inc){
cm->option->incTraceObjective = 1;
cm->savedConflictClauses = pm->savedConCls;
pm->savedConCls = 0;
}
t1 = util_cpu_ctime();
PureSat_CleanMask(manager,ResetVisibleVarMask);
PuresatMarkVisibleVar(network,sufArray,pm,0,pm->Length+1);
if(!Con){
from = manager->nodesArraySize;
PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length);
PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length);
if(inc){
PureSatMarkObj(manager,from,manager->nodesArraySize-bAigNodeSize);
}
PureSat_ResetManager(manager,cm,0);
PureSatProcessFanout(cm);
}
else{
sat_MarkTransitiveFaninForNode(cm,property,CoiMask);
sat_MarkTransitiveFaninForNode(cm,manager->InitState,CoiMask);
cm->option->AbRf = 0;
}
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(pm->verbosity>=1){
nodes_in_coi = PureSat_CountNodesInCoi(cm);
fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
}
st_free_table(SufAbsNameTable);
manager->assertArray2 = cm->assertArray2;
sat_Main(cm);
if(satStat)
sat_ReportStatistics(cm,cm->each);
cm->option->AbRf = 1;
manager->NodesArray = cm->nodesArray;
t1 = util_cpu_ctime();
if(!Con){
PureSatRecoverFanout(cm,pm);
PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
PureSat_CleanMask(manager,ResetVisited3Mask);
}
/*record conflict*/
if(inc && cm->savedConflictClauses ){
if(!Con){
int num=0;
saved = cm->savedConflictClauses;
pm->savedConCls = sat_ArrayAlloc(1);
for(i=0, lp=saved->space; i<saved->num; i++, lp++){
sat_ArrayInsert(pm->savedConCls,*lp);
if(*lp<0)
num++;
}
assert(num%2==0);
if(pm->verbosity>=2)
fprintf(vis_stdout,"record %d ConCls for incremental concretization\n",num/2);
}
else
pm->savedConCls = 0;
sat_ArrayFree(cm->savedConflictClauses);
cm->savedConflictClauses = 0;
}
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);
sat_ArrayFree(manager->assertArray);
status = cm->status;
cm->option->coreGeneration = 1;
PureSat_SatFreeManager(cm);
if(status == SAT_SAT){
if(pm->verbosity>=1)
fprintf(vis_stdout,"CEX exist\n");
return FALSE; /* cex exists*/
}
else{
if(pm->verbosity>=1)
fprintf(vis_stdout,"no CEX\n");
return TRUE; /* no cex*/
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean PureSat_ConcretTest_Core | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | sufArray, | ||
| bAigEdge_t | property, | ||
| array_t * | previousResultArray, | ||
| st_table * | junkTable | ||
| ) |
Function********************************************************************
Synopsis [Concretization procedure for unsat proof-based refinement minimization]
Description []
SideEffects []
SeeAlso []
Definition at line 3159 of file puresatIPUtil.c.
{
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
int status,i,nodes_in_coi=0;
satManager_t *cm;
char *name;
double t1,t2;
st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
array_t * tmpRef1;
st_table *refTable = st_init_table(strcmp,st_strhash);
arrayForEachItem(char *,sufArray,i,name){
st_insert(SufAbsNameTable,name,(char*)0);
}
manager->assertArray = sat_ArrayAlloc(1);
sat_ArrayInsert(manager->assertArray,manager->InitState);
cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
cm->option->coreGeneration = 1;
cm->option->AbRf = 1;
cm->option->IP = 1;
t1 = util_cpu_ctime();
PureSat_CleanMask(manager,ResetVisibleVarMask);
PuresatMarkVisibleVarWithVPGV(network,sufArray,pm,0,pm->Length+1);
PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length);
PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length);
PureSat_ResetManager(manager,cm,0);
PureSatProcessFanout(cm);
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(pm->verbosity>=1){
nodes_in_coi = PureSat_CountNodesInCoi(cm);
fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
}
manager->assertArray2 = cm->assertArray2;
sat_Main(cm);
manager->NodesArray = cm->nodesArray;
t1 = util_cpu_ctime();
PureSatRecoverFanout(cm,pm);
PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
PureSat_CleanMask(manager,ResetVisited3Mask);
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_UNSAT){
tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);
arrayForEachItem(char*,tmpRef1,i,name)
st_insert(refTable,name,(char*)0);
arrayForEachItem(char*,sufArray,i,name){
if(!st_lookup(refTable,name,NIL(char*))&&
!st_lookup(pm->vertexTable,name,NIL(char*))){
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s can be gotten rid of\n",name);
st_insert(junkTable,name,(char*)0);
}
}
array_free(tmpRef1);
}
st_free_table(SufAbsNameTable);
st_free_table(refTable);
RT_Free(cm->rm);
sat_ArrayFree(manager->assertArray);
status = cm->status;
cm->option->coreGeneration = 1;
PureSat_SatFreeManager(cm);
if(status == SAT_SAT){
if(pm->verbosity>=1)
fprintf(vis_stdout,"CEX exist\n");
return FALSE; // cex exists
}
else{
if(pm->verbosity>=1)
fprintf(vis_stdout,"no CEX\n");
return TRUE; // no cex
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int PureSat_CountNodesInCoi | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Count number of nodes in COI]
Description [Count number of nodes in COI]
SideEffects []
SeeAlso []
Definition at line 1100 of file puresatIPUtil.c.
{
int ct=0;
bAigEdge_t i;
for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
if(SATflags(i) & CoiMask){
ct++;
}
}
/*fprintf(vis_stdout,"There are %d node in COI\n",ct);*/
return ct;
}
Here is the caller graph for this function:
| bAigEdge_t PureSat_FindNodeByName | ( | bAig_Manager_t * | manager, |
| nameType_t * | name, | ||
| int | bound | ||
| ) |
Function********************************************************************
Synopsis [Find an aig node from its name]
Description []
SideEffects []
SeeAlso []
Definition at line 2815 of file puresatIPUtil.c.
{
bAigEdge_t node;
if (!st_lookup(manager->SymbolTableArray[bound], name, &node)){
node = bAig_NULL;
}
return bAig_GetCanonical(manager, node);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_GetLatchForNode | ( | bAig_Manager_t * | manager, |
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | node, | ||
| array_t * | nameArray, | ||
| st_table * | tmpTable, | ||
| int | cut | ||
| ) |
Function********************************************************************
Synopsis [Get support latches for one aig node]
Description []
SideEffects []
SeeAlso []
Definition at line 3554 of file puresatIPUtil.c.
{
bAigTimeFrame_t * tf = manager->timeframeWOI;
char * name;
st_table * table;
st_generator * stgen;
if(node==bAig_NULL)
return;
node = bAig_NonInvertedEdge(node);
if(flags(node)&VisitedMask)
return;
flags(node) |= VisitedMask;
if(flags(node)&StateBitMask){
if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){
int retVal = st_lookup(tf->idx2name,(char*)node,&name);
assert(retVal);
if(!st_lookup(tmpTable,name,NIL(char*))){
st_insert(tmpTable,name,(char*)0);
array_insert_last(char *,nameArray,name);
if(pm->verbosity>=2)
fprintf(vis_stdout,"insert %s\n",name);
}
}
else{
st_foreach_item(table,stgen,&name,NIL(char*)){
if(!st_lookup(tmpTable,name,NIL(char*))){
st_insert(tmpTable,name,(char*)0);
array_insert_last(char *,nameArray,name);
if(pm->verbosity>=2)
fprintf(vis_stdout,"insert %s\n",name);
}
}
}
}
if(cut==2){
if(flags(node)&Visited2Mask)
return;
}
else{
if(cut==1){
if(flags(node)&Visited3Mask)
return;
}
else{
fprintf(vis_stdout,"wrong cut\n");
exit(0);
}
}
PureSat_GetLatchForNode(manager,pm,leftChild(node),nameArray,tmpTable,cut);
PureSat_GetLatchForNode(manager,pm,rightChild(node),nameArray,tmpTable,cut);
}
Here is the caller graph for this function:
| int PureSat_IdentifyConflict | ( | satManager_t * | cm, |
| long | left, | ||
| bAigEdge_t | right, | ||
| bAigEdge_t | node | ||
| ) |
Function********************************************************************
Synopsis [Find the type of conflict, return the value to caller]
Description [
0 1 1 1 1 1 | | | | | | 20---33,49--- 9,13--- 17 --- 5 --- 1--- / \ / \ / \ / \ / \ / \ 1 1 X 0 0 X 1 0 0 1 0 0
Bing note: For case 1, maybe solving conflict with both childern is better, but in sat package, only conflict with left child is solved ]
SideEffects []
SeeAlso []
Definition at line 277 of file puresatIPUtil.c.
{
int result; /*1:left 2:right 3:both*/
int value = SATgetValue(left,right,node);
switch(value){
case 1:
case 5:
case 9:
case 13:
result = 1;
break;
case 17:
case 33:
case 49:
result = 2;
break;
case 20:
result = 3;
break;
default:
fprintf(vis_stdout,"can't identify the conflict, exit\n");
exit(0);
}
return result;
}
Here is the caller graph for this function:
| bAigEdge_t PureSat_MapIP | ( | mAig_Manager_t * | manager, |
| bAigEdge_t | node, | ||
| int | from, | ||
| int | to | ||
| ) |
Function********************************************************************
Synopsis [Maping interpolant from a timeframe to another timeframe]
Description []
SideEffects []
SeeAlso []
Definition at line 2688 of file puresatIPUtil.c.
{
bAigTimeFrame_t *tf = manager->timeframeWOI;
st_table *tmpTable = st_init_table(st_numcmp,st_numhash);
bAigEdge_t * L1,*L0,result,v1,v0;
int i;
if(node==bAig_One||node==bAig_Zero)
return node;
L1 = tf->latchInputs[from];
L0 = tf->latchInputs[to];
for(i=0;i<tf->nLatches;i++){
v1 = L1[i];
v0 = L0[i];
if(SATisInverted(v1)){
v1 = SATnot(v1);
v0 = SATnot(v0);
}
st_insert(tmpTable,(char*)v1,(char*)v0);
}
L1 = tf->blatchInputs[from];
L0 = tf->blatchInputs[to];
for(i=0;i<tf->nbLatches;i++){
v1 = L1[i];
v0 = L0[i];
if(SATisInverted(v1)){
v1 = SATnot(v1);
v0 = SATnot(v0);
}
st_insert(tmpTable,(char*)v1,(char*)v0);
}
manager->class_ = to;
result = PureSat_MapIPRecur(manager,node,tmpTable);
st_free_table(tmpTable);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t PureSat_MapIPRecur | ( | mAig_Manager_t * | manager, |
| bAigEdge_t | node, | ||
| st_table * | tmpTable | ||
| ) |
Function********************************************************************
Synopsis [Recursively mapping interpolant from a timeframe to another timeframe]
Description []
SideEffects []
SeeAlso []
Definition at line 2639 of file puresatIPUtil.c.
{
bAigEdge_t v,result,left,right;
int isInverted;
#if DBG
assert(node!=bAig_NULL);
#endif
if(node == bAig_One || node == bAig_Zero){
return node;
}
if(st_lookup(tmpTable,(char *)bAig_NonInvertedEdge(node),&v)){
if(bAig_IsInverted(node))
result = bAig_Not(v);
else
result = v;
return result;
}
left = PureSat_MapIPRecur(manager,leftChild(node),tmpTable);
right = PureSat_MapIPRecur(manager,rightChild(node),tmpTable);
v = PureSat_And(manager,left,right);
isInverted = bAig_IsInverted(node);
result = isInverted ? bAig_Not(v) : v;
st_insert(tmpTable,(char *)bAig_NonInvertedEdge(node),(char *)v);
//fprintf(vis_stdout,"return %d->%d\n",node,result);
return result;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_MarkGlobalVar | ( | bAig_Manager_t * | manager, |
| int | length | ||
| ) |
Function********************************************************************
Synopsis [Mark global variables]
Description [Mark global variables]
SideEffects []
SeeAlso []
Definition at line 2347 of file puresatIPUtil.c.
{
bAigTimeFrame_t * tf = manager->timeframeWOI;
bAigEdge_t * li,* bli,node;
int i;
li = tf->latchInputs[length];
bli = tf->blatchInputs[length];
for(i=0; i<tf->nLatches; i++){
node = bAig_NonInvertedEdge(li[i]);
manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
}
for(i=0; i<tf->nbLatches; i++){
node = bAig_NonInvertedEdge(bli[i]);
manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
}
}
Here is the caller graph for this function:
| void PureSat_MarkGlobalVar_AbRf | ( | bAig_Manager_t * | manager, |
| int | length | ||
| ) |
Function********************************************************************
Synopsis [Makr global variable for abstraction refinement]
Description []
SideEffects []
SeeAlso []
Definition at line 2414 of file puresatIPUtil.c.
{
bAigTimeFrame_t * tf = manager->timeframeWOI;
bAigEdge_t * li,* bli,node;
int i;
li = tf->latchInputs[length];
bli = tf->blatchInputs[length];
for(i=0; i<tf->nLatches; i++){
node = bAig_NonInvertedEdge(li[i]);
if(flags(node)&VisibleVarMask)
manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
}
for(i=0; i<tf->nbLatches; i++){
node = bAig_NonInvertedEdge(bli[i]);
if(flags(node)&VisibleVarMask)
manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
}
}
Here is the caller graph for this function:
| void PureSat_MarkTransitiveFaninForArray | ( | satManager_t * | cm, |
| satArray_t * | arr, | ||
| unsigned int | mask | ||
| ) |
Function********************************************************************
Synopsis [Mark transitive fanin for an array of aig nodes]
Description [Mark transitive fanin for an array of aig nodes]
SideEffects []
SeeAlso []
Definition at line 465 of file puresatIPUtil.c.
{
int i, size;
bAigEdge_t v;
if(arr == 0) return;
size = arr->num;
for(i=0; i<size; i++) {
v = arr->space[i];
PureSat_MarkTransitiveFaninForNode(cm, v, mask);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_MarkTransitiveFaninForArray2 | ( | mAig_Manager_t * | manager, |
| satArray_t * | arr, | ||
| unsigned int | mask | ||
| ) |
Function********************************************************************
Synopsis [Mark transitive fanin for an array of aig nodes]
Description [Mark transitive fanin for an array of aig nodes]
SideEffects []
SeeAlso []
Definition at line 525 of file puresatIPUtil.c.
{
bAigEdge_t v;
int i, size;
if(arr == 0) return;
size = arr->num;
for(i=0; i<size; i++) {
v = arr->space[i];
PureSat_MarkTransitiveFaninForNode2(manager, v, mask);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_MarkTransitiveFaninForArray3 | ( | mAig_Manager_t * | manager, |
| satArray_t * | arr, | ||
| unsigned int | mask | ||
| ) |
Function********************************************************************
Synopsis [Mark transitive fanin for an array of aig nodes]
Description [Mark transitive fanin for an array of aig nodes]
SideEffects []
SeeAlso []
Definition at line 585 of file puresatIPUtil.c.
{
bAigEdge_t v;
int i, size;
if(arr == 0) return;
size = arr->num;
for(i=0; i<size; i++) {
v = arr->space[i];
PureSat_MarkTransitiveFaninForNode3(manager, v, mask);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_MarkTransitiveFaninForArray4 | ( | mAig_Manager_t * | manager, |
| satArray_t * | arr, | ||
| unsigned int | mask, | ||
| int | bound | ||
| ) |
Function********************************************************************
Synopsis [Mark transitive fanin for an array of aig nodes]
Description [Mark transitive fanin for an array of aig nodes]
SideEffects []
SeeAlso []
Definition at line 653 of file puresatIPUtil.c.
{
bAigEdge_t v;
int i, size;
if(arr == 0) return;
size = arr->num;
for(i=0; i<size; i++) {
v = arr->space[i];
v = SATnormalNode(v);
PureSat_MarkTransitiveFaninForNode4(manager,v,mask,bound);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_MarkTransitiveFaninForNode | ( | satManager_t * | cm, |
| bAigEdge_t | v, | ||
| unsigned int | mask | ||
| ) |
Function********************************************************************
Synopsis [Mark transitive fanin for an aig node]
Description [Mark transitive fanin for an aig node]
SideEffects []
SeeAlso []
Definition at line 434 of file puresatIPUtil.c.
{
if(v == bAig_NULL) return;
v = SATnormalNode(v);
if(SATflags(v) & mask) return;
SATflags(v) |= mask;
if(SATflags(v) & Visited3Mask) return;
PureSat_MarkTransitiveFaninForNode(cm, SATleftChild(v), mask);
PureSat_MarkTransitiveFaninForNode(cm, SATrightChild(v), mask);
}
Here is the caller graph for this function:
| void PureSat_MarkTransitiveFaninForNode2 | ( | mAig_Manager_t * | manager, |
| bAigEdge_t | v, | ||
| unsigned int | mask | ||
| ) |
Function********************************************************************
Synopsis [Mark transitive fanin for an aig node]
Description [Mark transitive fanin for an aig node]
SideEffects []
SeeAlso []
Definition at line 494 of file puresatIPUtil.c.
{
if(v == bAig_NULL) return;
v = SATnormalNode(v);
if(flags(v) & mask) return;
flags(v) |= mask;
if(flags(v) & Visited3Mask) return;
PureSat_MarkTransitiveFaninForNode2(manager, leftChild(v), mask);
PureSat_MarkTransitiveFaninForNode2(manager, rightChild(v), mask);
}
Here is the caller graph for this function:
| void PureSat_MarkTransitiveFaninForNode3 | ( | mAig_Manager_t * | manager, |
| bAigEdge_t | v, | ||
| unsigned int | mask | ||
| ) |
Function********************************************************************
Synopsis [Mark transitive fanin for an array of aig nodes]
Description [Mark transitive fanin for an array of aig nodes]
SideEffects []
SeeAlso []
Definition at line 556 of file puresatIPUtil.c.
{
if(v == 2) return;
v = SATnormalNode(v);
if(flags(v) & mask) return;
flags(v) |= mask;
PureSat_MarkTransitiveFaninForNode3(manager, leftChild(v), mask);
PureSat_MarkTransitiveFaninForNode3(manager, rightChild(v), mask);
}
Here is the caller graph for this function:
| void PureSat_MarkTransitiveFaninForNode4 | ( | mAig_Manager_t * | manager, |
| bAigEdge_t | v, | ||
| unsigned int | mask, | ||
| int | bound | ||
| ) |
Function********************************************************************
Synopsis [Mark transitive fanin for an array of aig nodes]
Description [Mark transitive fanin for an array of aig nodes]
SideEffects []
SeeAlso []
Definition at line 616 of file puresatIPUtil.c.
{
if(v == bAig_NULL) return;
v = SATnormalNode(v);
if(flags(v) & mask) return;
flags(v) |= mask;
if((flags(v)&StateBitMask)&&
!(flags(v)&VisibleVarMask)&&
(bAig_Class(v)>0)){
return;
}
PureSat_MarkTransitiveFaninForNode4(manager, leftChild(v), mask,bound);
PureSat_MarkTransitiveFaninForNode4(manager, rightChild(v), mask,bound);
}
Here is the caller graph for this function:
| void PureSat_PrintAigStatus | ( | mAig_Manager_t * | manager | ) |
Function********************************************************************
Synopsis [Print the status of AIG]
Description [Print the status of AIG]
SideEffects []
SeeAlso []
Definition at line 2325 of file puresatIPUtil.c.
{
(void) fprintf(vis_stdout,"Maximum number of nodes: %ld\n",
manager->maxNodesArraySize/bAigNodeSize);
(void) fprintf(vis_stdout,"Current number of nodes: %ld\n",
manager->nodesArraySize/bAigNodeSize);
fprintf(vis_stdout,"Current Max Node Index: %ld\n\n",
manager->nodesArraySize);
}
Here is the caller graph for this function:
| void PureSat_ResetCoi | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Reset COI mask for all nodes]
Description [Reset COI mask for all nodes]
SideEffects []
SeeAlso []
Definition at line 733 of file puresatIPUtil.c.
{
bAigEdge_t i;
for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
if(SATflags(i) & CoiMask)
SATflags(i) &= ResetCoiMask;
}
}
Here is the caller graph for this function:
| void PureSat_ResetManager | ( | mAig_Manager_t * | manager, |
| satManager_t * | cm, | ||
| int | clean | ||
| ) |
Function********************************************************************
Synopsis [Reset a sat manager]
Description [Reset a sat manager]
SideEffects []
SeeAlso []
Definition at line 1227 of file puresatIPUtil.c.
{
int i;
satVariable_t var;
satLevel_t *d;
if(cm->variableArray) {
for(i=0; i<cm->initNumVariables; i++) {
var = cm->variableArray[i];
if(var.wl[0]) {
sat_ArrayFree(var.wl[0]);
var.wl[0] = 0;
}
if(var.wl[1]) {
sat_ArrayFree(var.wl[1]);
var.wl[1] = 0;
}
}
free(cm->variableArray);
cm->variableArray = 0;
}
if(cm->decisionHead) {
for(i=0; i<cm->decisionHeadSize; i++) {
d = &(cm->decisionHead[i]);
if(d->implied)
sat_ArrayFree(d->implied);
if(d->satisfied)
sat_ArrayFree(d->satisfied);
}
free(cm->decisionHead);
cm->decisionHead = 0;
cm->decisionHeadSize = 0;
cm->currentDecision = 0;
}
if(cm->literals){
sat_FreeLiteralsDB(cm->literals);
cm->literals=0;
sat_AllocLiteralsDB(cm);
}
if(cm->each){
FREE(cm->each);
cm->each = sat_InitStatistics();
}
if(cm->queue) sat_FreeQueue(cm->queue);
if(cm->BDDQueue) sat_FreeQueue(cm->BDDQueue);
if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
cm->queue = 0;
cm->BDDQueue = 0;
cm->unusedAigQueue = 0;
if(cm->nonobjUnitLitArray) sat_ArrayFree(cm->nonobjUnitLitArray);
if(cm->objUnitLitArray) sat_ArrayFree(cm->objUnitLitArray);
if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
if(cm->dormantConflictArray) sat_ArrayFree(cm->dormantConflictArray);
if(cm->shrinkArray) sat_ArrayFree(cm->shrinkArray);
cm->nonobjUnitLitArray = 0;
cm->objUnitLitArray = 0;
cm->orderedVariableArray = 0;
cm->dormantConflictArray = 0;
cm->shrinkArray = 0;
/*change initNumVariable after cm->variableArray has been freed,
otherwise, initNumVariable may change*/
cm->nodesArray = manager->NodesArray;
cm->nodesArraySize = manager->nodesArraySize;
cm->initNodesArraySize = manager->nodesArraySize;
cm->maxNodesArraySize = manager->maxNodesArraySize;
cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
cm->initNumClauses = 0;
cm->initNumLiterals = 0;
cm->ipm = manager->ipm;
cm->assertArray = manager->assertArray;
cm->assertArray2 = manager->assertArray2;
cm->InitState = manager->InitState;
cm->CoiAssertArray = manager->CoiAssertArray;
cm->EqArray = manager->EqArray;
cm->currentVarPos = 0;
cm->currentTopConflict = 0;
cm->currentTopConflictCount = 0;
cm->lowestBacktrackLevel = 0;
cm->implicatedSoFar = 0;
//cm->status = 0;
if(clean){
for(i=bAigNodeSize;i<cm->nodesArraySize;i+=bAigNodeSize)
cm->nodesArray[i] = 2;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_RestoreAigForDummyNode | ( | mAig_Manager_t * | manager, |
| int | oldPosition | ||
| ) |
Function********************************************************************
Synopsis [Restore AIG to get rid of Dummy nodes]
Description [Restore AIG to get rid of Dummy nodes]
SideEffects []
SeeAlso []
Definition at line 1338 of file puresatIPUtil.c.
{
bAigEdge_t i;
for(i=manager->nodesArraySize-bAigNodeSize;
i>oldPosition;i=i-bAigNodeSize){
#if DBG
assert(leftChild(i)==bAig_NULL&&
rightChild(i)==bAig_NULL);
assert(flags(i)&DummyMask);
#endif
FREE(fanout(i));
}
manager->nodesArraySize = oldPosition+bAigNodeSize;
return;
}
Here is the caller graph for this function:
| void PureSat_SatFreeManager | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Free a PureSAT manager]
Description [Free a PureSAT manager]
SideEffects []
SeeAlso []
Definition at line 2221 of file puresatIPUtil.c.
{
satVariable_t var;
satLevel_t *d;
int i;
if(cm->option->coreGeneration){
st_free_table(cm->anteTable);
st_free_table(cm->RTreeTable);
cm->anteTable=0;
cm->RTreeTable=0;
}
/*timeframe, timeframeWOI,HashTable can't be freed*/
if(cm->option) sat_FreeOption(cm->option);
if(cm->total) sat_FreeStatistics(cm->total);
if(cm->each) sat_FreeStatistics(cm->each);
if(cm->literals) sat_FreeLiteralsDB(cm->literals);
cm->option=0;
cm->total=0;
cm->each=0;
cm->literals=0;
if(cm->decisionHead) {
for(i=0; i<cm->decisionHeadSize; i++) {
d = &(cm->decisionHead[i]);
if(d->implied)
sat_ArrayFree(d->implied);
if(d->satisfied)
sat_ArrayFree(d->satisfied);
}
free(cm->decisionHead);
cm->decisionHead = 0;
cm->decisionHeadSize = 0;
}
if(cm->queue) sat_FreeQueue(cm->queue);
if(cm->BDDQueue) sat_FreeQueue(cm->BDDQueue);
if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
cm->queue = 0;
cm->BDDQueue = 0;
cm->unusedAigQueue = 0;
if(cm->auxObj) sat_ArrayFree(cm->auxObj);
if(cm->obj) sat_ArrayFree(cm->obj);
if(cm->unitLits) sat_ArrayFree(cm->unitLits);
if(cm->pureLits) sat_ArrayFree(cm->pureLits);
if(cm->assertion) sat_ArrayFree(cm->assertion);
if(cm->auxArray) sat_ArrayFree(cm->auxArray);
if(cm->nonobjUnitLitArray) sat_ArrayFree(cm->nonobjUnitLitArray);
if(cm->objUnitLitArray) sat_ArrayFree(cm->objUnitLitArray);
if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
if(cm->savedConflictClauses) sat_ArrayFree(cm->savedConflictClauses);
cm->auxObj = 0;
cm->obj = 0;
cm->unitLits = 0;
cm->pureLits = 0;
cm->assertion = 0;
cm->auxArray = 0;
cm->nonobjUnitLitArray = 0;
cm->objUnitLitArray = 0;
cm->orderedVariableArray = 0;
if(cm->variableArray) {
for(i=0; i<cm->initNumVariables; i++) {
var = cm->variableArray[i];
if(var.wl[0]) {
sat_ArrayFree(var.wl[0]);
var.wl[0] = 0;
}
if(var.wl[1]) {
sat_ArrayFree(var.wl[1]);
var.wl[1] = 0;
}
}
free(cm->variableArray);
cm->variableArray = 0;
}
if(cm->comment) free(cm->comment);
cm->comment=0;
FREE(cm);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| satManager_t* PureSat_SatManagerAlloc | ( | bAig_Manager_t * | manager, |
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | object, | ||
| array_t * | auxObjectArray | ||
| ) |
Function********************************************************************
Synopsis [Allocate a PureSAT Manager]
Description [Allocate a PureSAT Manager]
SideEffects []
SeeAlso []
Definition at line 1999 of file puresatIPUtil.c.
{
satManager_t * cm;
satOption_t *option;
int i,size;
bAigEdge_t tv;
cm = ALLOC(satManager_t, 1);
memset(cm, 0, sizeof(satManager_t));
cm->nodesArraySize = manager->nodesArraySize;
cm->initNodesArraySize = manager->nodesArraySize;
cm->maxNodesArraySize = manager->maxNodesArraySize;
cm->nodesArray = manager->NodesArray;
cm->HashTable = manager->HashTable;
cm->literals = manager->literals;
cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
cm->initNumClauses = 0;
cm->initNumLiterals = 0;
cm->comment = ALLOC(char, 2);
cm->comment[0] = ' ';
cm->comment[1] = '\0';
cm->stdErr = vis_stderr;
cm->stdOut = vis_stdout;
cm->status = 0;
cm->orderedVariableArray = 0;
cm->unitLits = sat_ArrayAlloc(16);
cm->pureLits = sat_ArrayAlloc(16);
cm->option = 0;
cm->each = 0;
cm->decisionHead = 0;
cm->variableArray = 0;
cm->queue = 0;
cm->BDDQueue = 0;
cm->unusedAigQueue = 0;
cm->ipm = manager->ipm;
cm->assertArray = manager->assertArray;
cm->assertArray2 = manager->assertArray2;
cm->InitState = manager->InitState;
cm->CoiAssertArray = manager->CoiAssertArray;
cm->EqArray = manager->EqArray;
if(auxObjectArray) {
cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
size = auxObjectArray->num;
for(i=0; i<size; i++) {
tv = array_fetch(bAigEdge_t, auxObjectArray, i);
if(tv == 1) continue;
else if(tv == 0) {
cm->status = SAT_UNSAT;
break;
}
sat_ArrayInsert(cm->auxObj, tv);
}
}
if(object == 0) cm->status = SAT_UNSAT;
else if(object == 1) cm->status = SAT_SAT;
if(cm->status == 0) {
if(object!=-1){
cm->obj = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->obj, object);
}
/* initialize option*/
option = sat_InitOption();
option->coreGeneration = 1;
option->ForceFinish = 1;
option->clauseDeletionHeuristic = 0;
option->includeLevelZeroLiteral = 1;
option->minimizeConflictClause = 0;
option->IP = 1;
option->RT = 1;
option->verbose = pm->verbosity;
cm->anteTable = st_init_table(st_numcmp,st_numhash);
cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash);
cm->option = option;
cm->each = sat_InitStatistics();
BmcRestoreAssertion(manager,cm);
/* value reset..*/
sat_CleanDatabase(cm);
/* set cone of influence*/
sat_SetConeOfInfluence(cm);
sat_AllocLiteralsDB(cm);
}
return cm;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| satManager_t* PureSat_SatManagerAlloc_WOCOI | ( | mAig_Manager_t * | manager, |
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | object, | ||
| array_t * | auxObjectArray | ||
| ) |
Function********************************************************************
Synopsis [Allocate a PureSAT Manager without setting COI]
Description [Allocate a PureSAT Manager without setting COI]
SideEffects []
SeeAlso []
Definition at line 2111 of file puresatIPUtil.c.
{
satManager_t * cm;
satOption_t *option;
int i,size;
bAigEdge_t tv;
cm = ALLOC(satManager_t, 1);
memset(cm, 0, sizeof(satManager_t));
cm->nodesArraySize = manager->nodesArraySize;
cm->initNodesArraySize = manager->nodesArraySize;
cm->maxNodesArraySize = manager->maxNodesArraySize;
cm->nodesArray = manager->NodesArray;
cm->HashTable = manager->HashTable;
cm->literals = manager->literals;
cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
cm->initNumClauses = 0;
cm->initNumLiterals = 0;
cm->comment = ALLOC(char, 2);
cm->comment[0] = ' ';
cm->comment[1] = '\0';
cm->stdErr = vis_stderr;
cm->stdOut = vis_stdout;
cm->status = 0;
cm->orderedVariableArray = 0;
cm->unitLits = sat_ArrayAlloc(16);
cm->pureLits = sat_ArrayAlloc(16);
cm->option = 0;
cm->each = 0;
cm->decisionHead = 0;
cm->variableArray = 0;
cm->queue = 0;
cm->BDDQueue = 0;
cm->unusedAigQueue = 0;
cm->ipm = manager->ipm;
cm->assertArray = manager->assertArray;
cm->assertArray2 = manager->assertArray2;
cm->InitState = manager->InitState;
cm->CoiAssertArray = manager->CoiAssertArray;
cm->EqArray = manager->EqArray;
if(auxObjectArray) {
cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
size = auxObjectArray->num;
for(i=0; i<size; i++) {
tv = array_fetch(bAigEdge_t, auxObjectArray, i);
if(tv == 1) continue;
else if(tv == 0) {
cm->status = SAT_UNSAT;
break;
}
sat_ArrayInsert(cm->auxObj, tv);
}
}
if(object == 0) cm->status = SAT_UNSAT;
else if(object == 1) cm->status = SAT_SAT;
if(cm->status == 0) {
if(object!=-1){
cm->obj = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->obj, object);
}
option = sat_InitOption();
option->ForceFinish = 1;
option->coreGeneration = 1;
option->clauseDeletionHeuristic = 0;
option->includeLevelZeroLiteral = 1;
option->minimizeConflictClause = 0;
option->IP = 0;
option->RT = 1;
option->verbose = pm->verbosity;
cm->anteTable = st_init_table(st_numcmp,st_numhash);
cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash);
cm->option = option;
cm->each = sat_InitStatistics();
BmcRestoreAssertion(manager,cm);
sat_CleanDatabase(cm);
/* WOCOI: NO set cone of influence*/
sat_AllocLiteralsDB(cm);
}
return cm;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_SetCOI | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Set COI mask for SAT solver]
Description [Set COI mask for SAT solver]
SideEffects []
SeeAlso []
Definition at line 711 of file puresatIPUtil.c.
{
PureSat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask);
PureSat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask);
PureSat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
}
Here is the call graph for this function:
| int PureSat_TestConvergeForIP | ( | mAig_Manager_t * | manager, |
| PureSat_Manager_t * | pm, | ||
| satManager_t * | cm, | ||
| bAigEdge_t | state1, | ||
| bAigEdge_t | state2 | ||
| ) |
Function********************************************************************
Synopsis [Convergence test for flat interpolation algorithm]
Description [Convergence test for flat interpolation algorithm]
SideEffects []
SeeAlso []
Definition at line 1799 of file puresatIPUtil.c.
{
satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7;
int status, nodes_in_coi = 0;
if(state2 == bAig_Zero)
return 1;
if(state1 == bAig_One)
return 1;
if(state1 == bAig_Zero && state2 != bAig_Zero)
return 0;
if(state1 != bAig_One && state2 == bAig_One)
return 0;
if(pm->verbosity>=1)
fprintf(vis_stdout,"Test convergence:\n");
PureSat_ResetCoi(cm);
if(pm->verbosity>=1){
fprintf(vis_stdout,"after reset COI\n");
nodes_in_coi = PureSat_CountNodesInCoi(cm);
fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
}
tmp1 = cm->obj;
tmp2 = cm->auxObj;
tmp3 = cm->assertion;
tmp4 = cm->assertArray;
//Bing:
tmp5 = cm->unitLits;
tmp6 = cm->pureLits;
tmp7 = cm->nonobjUnitLitArray;
cm->obj = 0;
cm->auxObj = 0;
cm->assertion = 0;
//cm->assertArray2 = 0;
cm->assertArray = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->assertArray,SATnot(state1));
sat_ArrayInsert(cm->assertArray,state2);
sat_SetConeOfInfluence(cm);
if(pm->verbosity>=1){
fprintf(vis_stdout,"after add new init states:\n");
nodes_in_coi = PureSat_CountNodesInCoi(cm);
fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
}
cm->option->coreGeneration = 0;
//cm->option->effIP = 0;
cm->option->IP = 0;
cm->status = 0;
sat_Main(cm);
if(manager->NodesArray!=cm->nodesArray)
/*cm->nodesArray may be reallocated*/
manager->NodesArray = cm->nodesArray;
cm->obj = tmp1;
cm->auxObj = tmp2;
cm->assertion = tmp3;
sat_ArrayFree(cm->assertArray);
cm->assertArray = tmp4;
cm->unitLits = tmp5;
cm->pureLits = tmp6;
cm->nonobjUnitLitArray = tmp7;
cm->option->coreGeneration = 1;
cm->option->IP = 1;
status = cm->status;
#if DBG
assert(cm->currentDecision>=-1);
#endif
if(cm->currentDecision!=-1)
sat_Backtrack(cm,-1);
cm->status = 0;
if(status == SAT_UNSAT)
/*state2 contains state1, reach convergence*/
return 1;
else
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int PureSat_TestConvergeForIP_AbRf | ( | Ntk_Network_t * | network, |
| satManager_t * | cm, | ||
| PureSat_Manager_t * | pm, | ||
| array_t * | CoiArray, | ||
| bAigEdge_t | state1, | ||
| bAigEdge_t | state2 | ||
| ) |
Function********************************************************************
Synopsis [Convergence test for interpolation algorithm with abstraction refinement ]
Description [Convergence test for flat interpolation algorithmwith abstraction refinement ]
SideEffects []
SeeAlso []
Definition at line 1899 of file puresatIPUtil.c.
{
satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7;
int status, nodes_in_coi = 0;
mAig_Manager_t * manager;
if(state2 == bAig_Zero)
return 1;
if(state1 == bAig_One)
return 1;
if(state1 == bAig_Zero && state2 != bAig_Zero)
return 0;
if(state1 != bAig_One && state2 == bAig_One)
return 0;
manager = Ntk_NetworkReadMAigManager(network);
if(pm->verbosity>=1)
fprintf(vis_stdout,"Test convergence:\n");
PureSat_ResetCoi(cm);
if(pm->verbosity>=1){
fprintf(vis_stdout,"after reset COI\n");
nodes_in_coi = PureSat_CountNodesInCoi(cm);
fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
}
tmp1 = cm->obj;
tmp2 = cm->auxObj;
tmp3 = cm->assertion;
tmp4 = cm->assertArray;
tmp5 = cm->unitLits;
tmp6 = cm->pureLits;
tmp7 = cm->nonobjUnitLitArray;
cm->obj = 0;
cm->auxObj = 0;
cm->assertion = 0;
cm->unitLits = 0;
cm->pureLits = 0;
cm->nonobjUnitLitArray = 0;
cm->assertArray = sat_ArrayAlloc(1);
sat_ArrayInsert(cm->assertArray,SATnot(state1));
sat_ArrayInsert(cm->assertArray,state2);
sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
if(pm->verbosity>=1){
fprintf(vis_stdout,"after add new init states:\n");
nodes_in_coi = PureSat_CountNodesInCoi(cm);
fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
}
cm->option->coreGeneration = 0;
cm->status = 0;
cm->option->AbRf = 0;
sat_Main(cm);
cm->option->AbRf = 1;
if(manager->NodesArray!=cm->nodesArray)
/*cm->nodesArray may be reallocated*/
manager->NodesArray = cm->nodesArray;
sat_ArrayFree(cm->assertArray);
manager->assertArray = tmp4;
cm->obj = tmp1;
cm->auxObj = tmp2;
cm->assertion = tmp3;
cm->assertArray = tmp4;
cm->unitLits = tmp5;
cm->pureLits = tmp6;
cm->nonobjUnitLitArray = tmp7;
cm->option->coreGeneration = 1;
status = cm->status;
if(cm->currentDecision!=-1)
sat_Backtrack(cm,-1);
cm->status = 0;
if(status == SAT_UNSAT)
/*state2 contains state1, reach convergence*/
return 1;
else
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_UnMarkGlobalVar | ( | bAig_Manager_t * | manager, |
| int | length | ||
| ) |
Function********************************************************************
Synopsis [UnMark global variables]
Description [UnMark global variables]
SideEffects []
SeeAlso []
Definition at line 2380 of file puresatIPUtil.c.
{
bAigTimeFrame_t * tf = manager->timeframeWOI;
bAigEdge_t * li,* bli,node;
int i;
li = tf->latchInputs[length];
bli = tf->blatchInputs[length];
for(i=0; i<tf->nLatches; i++){
node = bAig_NonInvertedEdge(li[i]);
manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask;
}
for(i=0; i<tf->nbLatches; i++){
node = bAig_NonInvertedEdge(bli[i]);
manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask;
}
}
Here is the caller graph for this function:
| void PureSatAbstractLatch | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | v, | ||
| st_table * | tmpTable | ||
| ) |
Function********************************************************************
Synopsis [Build abstraction from concrete model]
Description [Build abstraction from concrete model]
SideEffects []
SeeAlso []
Definition at line 894 of file puresatIPUtil.c.
{
bAigEdge_t nv;
/*fanin: set left and right to bAig_NULL*/
nv = bAig_NonInvertedEdge(v);
if(leftChild(nv)!=bAig_NULL){
if(!(flags(leftChild(nv))&CoiMask))
flags(leftChild(nv)) |= Visited3Mask;
manager->NodesArray[nv+bAigLeft]=bAig_NULL;
}
if(rightChild(nv)!=bAig_NULL){
if(!(flags(rightChild(nv))&CoiMask))
flags(rightChild(nv)) |= Visited3Mask;
manager->NodesArray[nv+bAigRight]=bAig_NULL;
}
}
Here is the caller graph for this function:
| void PureSatAddIdenLatchToAbs | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | nameArray | ||
| ) |
Function********************************************************************
Synopsis [Some latches have the same aig node, add them all to abstractions once one is added. ]
Description []
SideEffects []
SeeAlso []
Definition at line 3441 of file puresatIPUtil.c.
{
int i;
st_generator * stgen;
st_table* table;
char *name,*name1;
st_table *table1 = st_init_table(st_ptrcmp,st_ptrhash);
array_t * tmpArray = array_alloc(char*,0);
st_foreach_item(pm->vertexTable,stgen,&name,NIL(char*))
st_insert(table1,name,(char*)0);
arrayForEachItem(char*,nameArray,i,name)
st_insert(table1,name,(char*)0);
arrayForEachItem(char*,nameArray,i,name){
if(st_lookup(pm->IdenLatchTable,name,&table)){
st_foreach_item(table,stgen,&name1,NIL(char*)){
if(!st_lookup(table1,name1,NIL(char*))){
st_insert(table1,name1,(char*)0);
array_insert_last(char*,tmpArray,name1);
}
}
}
}
arrayForEachItem(char*,tmpArray,i,name){
array_insert_last(char*,nameArray,name);
if(pm->verbosity>=2)
fprintf(vis_stdout,"add %s to refineArray\n",name);
}
array_free(tmpArray);
st_free_table(table1);
}
Here is the caller graph for this function:
| void PureSatBmcGetCoiForLtlFormula_New | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | formula, | ||
| st_table * | ltlCoiTable | ||
| ) |
Function********************************************************************
Synopsis [Get COI nodes for a LTL formula]
Description [Get COI nodes for a LTL formula]
SideEffects []
SeeAlso []
Definition at line 408 of file puresatIPUtil.c.
{
st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula, ltlCoiTable, visited);
st_free_table(visited);
return;
} /* BmcGetCoiForLtlFormula() */
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatBmcGetCoiForLtlFormulaRecursive_New | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | formula, | ||
| st_table * | ltlCoiTable, | ||
| st_table * | visited | ||
| ) |
Function********************************************************************
Synopsis [Recursively get COI nodes for a LTL formula]
Description [Recursively get COI nodes for a LTL formula]
SideEffects []
SeeAlso []
Definition at line 367 of file puresatIPUtil.c.
{
if (formula == NIL(Ctlsp_Formula_t)) {
return;
}
/* leaf node */
if (formula->type == Ctlsp_ID_c){
char *name = Ctlsp_FormulaReadVariableName(formula);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
int tmp;
if (st_lookup_int(visited, (char *) node, &tmp)){
/* Node already visited */
return;
}
PureSatBmcGetCoiForNtkNode_New(node, ltlCoiTable, visited);
return;
}
PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->left, ltlCoiTable, visited);
PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->right, ltlCoiTable, visited);
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatBmcGetCoiForNtkNode_New | ( | Ntk_Node_t * | node, |
| st_table * | CoiTable, | ||
| st_table * | visited | ||
| ) |
Function********************************************************************
Synopsis [Get COI for a network node]
Description [Get COI for a network node]
SideEffects []
SeeAlso []
Definition at line 322 of file puresatIPUtil.c.
{
int i;
Ntk_Node_t *faninNode;
if(node == NIL(Ntk_Node_t)){
return;
}
if (st_lookup_int(visited, (char *) node, NIL(int))){
return;
}
st_insert(visited, (char *) node, (char *) 0);
if(Ntk_NodeTestIsInput(node))
return;
if (Ntk_NodeTestIsLatch(node)){
st_insert(CoiTable, (char *) node, (char *)0);
}
Ntk_NodeForEachFanin(node, i, faninNode) {
PureSatBmcGetCoiForNtkNode_New(faninNode, CoiTable, visited);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatCheckCoi | ( | bAig_Manager_t * | manager | ) |
Function********************************************************************
Synopsis [sanity check for abstraction processing]
Description [sanity check for abstraction processing]
SideEffects []
SeeAlso []
Definition at line 1718 of file puresatIPUtil.c.
{
long i;
for(i=bAigNodeSize;i<manager->nodesArraySize;i+=bAigNodeSize){
if(flags(i) & IsCNFMask)
continue;
if(!(flags(i) & CoiMask))
continue;
PureSatCheckCoiNode(manager,i);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatCheckCoiNode | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | node | ||
| ) |
Function********************************************************************
Synopsis [sanity check for one node for abstraction processing]
Description [sanity check for one node for abstraction processing]
SideEffects []
SeeAlso []
Definition at line 1671 of file puresatIPUtil.c.
{
int i;
long *fan;
long nfan,child, cur;
int left,inv;
nfan = nFanout(node);
fan = (bAigEdge_t*)fanout(node);
if(fan==0) return;
/*check child*/
assert((leftChild(node)==bAig_NULL)||
(flags(leftChild(node))&CoiMask));
assert((rightChild(node)==bAig_NULL)||
(flags(rightChild(node))&CoiMask));
if((leftChild(node)==bAig_NULL)||(rightChild(node)==bAig_NULL))
assert((leftChild(node)==bAig_NULL)&&(rightChild(node)==bAig_NULL));
/*check fanout*/
for(i=0; i<nfan; i++){
cur = fan[i]>>1;
assert(flags(cur)&CoiMask);
left=SATisInverted(fan[i])?0:1;
inv=SATisInverted(cur)?1:0;
child = inv?SATnormalNode(node)+1:SATnormalNode(node);
if(left){
assert(child==leftChild(cur));
}
else{
assert(child==rightChild(cur));
}
}
}
Here is the caller graph for this function:
| array_t* PureSatComputeOrder_2 | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | vertexArray, | ||
| array_t * | invisibleArray, | ||
| int * | sccArray, | ||
| int * | NumInSecondLevel | ||
| ) |
Function********************************************************************
Synopsis [Sort latch candidate based on BFS ring and RC information]
Description []
SideEffects []
SeeAlso []
Definition at line 3409 of file puresatIPUtil.c.
{
array_t * RCArray;
PureSatGenerateDfs(network,pm,vertexArray);
RCArray = PureSatGenerateRCArray_2(network,pm,invisibleArray,
NumInSecondLevel);
return RCArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t PureSatCreatebAigOfPropFormula | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | manager, | ||
| int | bound, | ||
| Ctlsp_Formula_t * | ltl, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Create Aig for a ltl formula]
Description []
SideEffects []
SeeAlso []
Definition at line 2844 of file puresatIPUtil.c.
{
int index;
bAigEdge_t result, left, right, *li;
bAigTimeFrame_t *timeframe;
if (ltl == NIL(Ctlsp_Formula_t)) return bAig_NULL;
if (ltl->type == Ctlsp_TRUE_c) return bAig_One;
if (ltl->type == Ctlsp_FALSE_c) return bAig_Zero;
assert(Ctlsp_isPropositionalFormula(ltl));
if(withInitialState) timeframe = manager->timeframe;
else timeframe = manager->timeframeWOI;
if (ltl->type == Ctlsp_ID_c){
char *nodeNameString = Ctlsp_FormulaReadVariableName(ltl);
char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, nodeNameString);
Var_Variable_t *nodeVar;
int nodeValue;
MvfAig_Function_t *tmpMvfAig;
st_table *nodeToMvfAigTable; /* maps each node to its mvfAig */
if (node == NIL(Ntk_Node_t)) {
char *nameKey;
char tmpName[100];
sprintf(tmpName, "%s_%d", nodeNameString, bound);
nameKey = util_strsav(tmpName);
result = PureSat_FindNodeByName(manager, nameKey,bound);
if(result == bAig_NULL){
result = PureSat_CreateVarNode(manager, nameKey);
} else {
FREE(nameKey);
}
return result;
}
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
assert(nodeToMvfAigTable != NIL(st_table));
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
if (tmpMvfAig == NIL(MvfAig_Function_t)){
tmpMvfAig = Bmc_NodeBuildMVF(network, node);
array_free(tmpMvfAig);
tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
}
nodeVar = Ntk_NodeReadVariable(node);
if (Var_VariableTestIsSymbolic(nodeVar)) {
nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
if ( nodeValue == -1 ) {
(void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return bAig_NULL;
}
}
else {
int check;
check = StringCheckIsInteger(nodeValueString, &nodeValue);
if( check == 0 ) {
(void) fprintf(vis_stderr,"Illegal value in the RHS\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return bAig_NULL;
}
if( check == 1 ) {
(void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
(void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
return bAig_NULL;
}
if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
(void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
(void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
return bAig_NULL;
}
}
result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
result = bAig_GetCanonical(manager, result);
if(st_lookup(timeframe->li2index, (char *)result, &index)) {
li = timeframe->latchInputs[bound];
result = bAig_GetCanonical(manager, li[index]);
}
else if(st_lookup(timeframe->o2index, (char *)result, &index)) {
li = timeframe->outputs[bound];
result = bAig_GetCanonical(manager, li[index]);
}
else if(st_lookup(timeframe->i2index, (char *)result, &index)) {
li = timeframe->internals[bound];
result = bAig_GetCanonical(manager, li[index]);
}
return result;
}
left = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->left, withInitialState);
if (left == bAig_NULL){
return bAig_NULL;
}
right = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->right, withInitialState);
if (right == bAig_NULL && ltl->type ==Ctlsp_NOT_c ){
return bAig_Not(left);
}
else if(right == bAig_NULL) {
return bAig_NULL;
}
switch(ltl->type) {
case Ctlsp_OR_c:
result = PureSat_Or(manager, left, right);
break;
case Ctlsp_AND_c:
result = PureSat_And(manager, left, right);
break;
case Ctlsp_THEN_c:
result = PureSat_Then(manager, left, right);
break;
case Ctlsp_EQ_c:
result = PureSat_Eq(manager, left, right);
break;
case Ctlsp_XOR_c:
result = PureSat_Xor(manager, left, right);
break;
default:
fail("Unexpected type");
}
return result;
} /* BmcCirCUsCreatebAigOfPropFormula */
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatCreateInitAbsByAIG | ( | bAig_Manager_t * | manager, |
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | node, | ||
| st_table * | tmpTable | ||
| ) |
Function********************************************************************
Synopsis [Create initial abstraction from aig]
Description []
SideEffects []
SeeAlso []
Definition at line 3492 of file puresatIPUtil.c.
{
bAigTimeFrame_t * tf = manager->timeframeWOI;
char * name;
st_table * table;
st_generator * stgen;
if(node==bAig_NULL)
return;
node = bAig_NonInvertedEdge(node);
if(flags(node)&VisitedMask)
return;
flags(node) |= VisitedMask;
if(flags(node)&StateBitMask){
if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){
int retVal = st_lookup(tf->idx2name,(char*)node,&name);
assert(retVal);
if(!st_lookup(tmpTable,name,NIL(char*))){
st_insert(tmpTable,name,(char*)0);
}
}
else{
st_foreach_item(table,stgen,&name,NIL(char*)){
if(!st_lookup(tmpTable,name,NIL(char*))){
st_insert(tmpTable,name,(char*)0);
}
}
}
}
if(flags(node)&StateBitMask)
return;
PureSatCreateInitAbsByAIG(manager,pm,leftChild(node),tmpTable);
PureSatCreateInitAbsByAIG(manager,pm,rightChild(node),tmpTable);
}
Here is the caller graph for this function:
| void PureSatGenerateDfs | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | vertexArray | ||
| ) |
Function********************************************************************
Synopsis [Generate the ring information for the whole circuit]
Description []
SideEffects []
SeeAlso []
Definition at line 3344 of file puresatIPUtil.c.
{
int dfs = 1,i,ct=0;
char *name;
Ntk_Node_t *node;
array_t * ringArray = array_alloc(char *,0);
array_t * coreArray;
lsGen gen;
st_generator * stgen;
Ntk_NetworkForEachNode( network, gen, node ) {
PureSatNodeSetColor( node, dfsWhite_c );
}
arrayForEachItem(char *,vertexArray,i,name){
st_insert(pm->node2dfsTable,name,(char*)(long)dfs);
node = Ntk_NetworkFindNodeByName(network,name);
PureSatNodeSetColor(node,dfsBlack_c);
ct++;
}
coreArray = array_dup(vertexArray);
while(coreArray->num>0){
dfs++;
ringArray = PureSatGenerateRing(network,pm,coreArray,
&dfs);
arrayForEachItem(char*,ringArray,i,name){
st_insert(pm->node2dfsTable,name,(char*)(long)dfs);
ct++;
}
array_free(coreArray);
coreArray = ringArray;
}
st_foreach_item(pm->CoiTable,stgen,&node,NIL(char*)){
name = Ntk_NodeReadName(node);
if(!st_lookup(pm->node2dfsTable,name,NIL(char*))){
st_insert(pm->node2dfsTable,name,(char*)LARGEDFS);
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s LARGEDFS is inserted into node2dfsTable\n",name);
}
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* PureSatGenerateRing | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| array_t * | coreArray, | ||
| int * | dfs | ||
| ) |
Function********************************************************************
Synopsis [Generate BFS ring for one array]
Description []
SideEffects []
SeeAlso []
Definition at line 3311 of file puresatIPUtil.c.
{
array_t * ringArray = array_alloc(char *,0);
int i,j;
char *name;
Ntk_Node_t *node1,*node;
arrayForEachItem(char *,coreArray,i,name){
node1 = Ntk_NetworkFindNodeByName(network,name);
Ntk_NodeForEachFanin(node1,j,node){
PureSatGenerateRingForNode(network,pm,node,
ringArray,dfs);
}
}
return ringArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatGenerateRingForNode | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| Ntk_Node_t * | node1, | ||
| array_t * | ringArray, | ||
| int * | dfs | ||
| ) |
Function********************************************************************
Synopsis [Generate BFS ring for a network node]
Description []
SideEffects []
SeeAlso []
Definition at line 3271 of file puresatIPUtil.c.
{
Ntk_Node_t *node;
char *name;
int i;
if(PureSatNodeReadColor(node1) == dfsBlack_c)
return;
PureSatNodeSetColor(node1,dfsBlack_c);
if(Ntk_NodeTestIsLatch(node1)){
name = Ntk_NodeReadName(node1);
st_insert(pm->node2dfsTable,name,(char*)(long)(*dfs));
array_insert_last(char *,ringArray,name);
return;
}
Ntk_NodeForEachFanin(node1,i,node){
PureSatGenerateRingForNode(network,pm,node,ringArray,
dfs);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* PureSatGetAigCoi | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | property | ||
| ) |
Function********************************************************************
Synopsis [Get COI reduction based on aig, not ntk]
Description []
SideEffects []
SeeAlso []
Definition at line 3632 of file puresatIPUtil.c.
{
bAig_Manager_t *manager;
st_table * node2MvfAigTable,*tmpTable;
array_t * nameArray,*nameArray1;
bAigTimeFrame_t *tf;
char * name;
Ntk_Node_t *latch;
MvfAig_Function_t *mvfAig;
mAigMvar_t lmVar;
mAigBvar_t bVar;
array_t *bVarList,*mVarList;
int i,j,lmAigId;
long index,index1;
bAigEdge_t v, *li, *bli;
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(mAig_Manager_t)) {
(void) fprintf(vis_stdout,
"** bmc error: run build_partition_maigs command first\n");
exit(0);;
}
node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
tf = manager->timeframeWOI;
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
assert(manager->timeframeWOI->currentTimeframe>=2);
PureSat_CleanMask(manager,ResetVisitedMask);
PureSat_CleanMask(manager,ResetVisited2Mask);
PureSat_CleanMask(manager,ResetVisited3Mask);
li = tf->latchInputs[1];
for(i=0;i<tf->nLatches;i++)
flags(li[i])|=Visited3Mask;
li = tf->blatchInputs[1];
for(i=0;i<tf->nbLatches;i++)
flags(li[i])|=Visited3Mask;
li = tf->latchInputs[2];
for(i=0;i<tf->nLatches;i++)
flags(li[i])|=Visited2Mask;
li = tf->blatchInputs[2];
for(i=0;i<tf->nbLatches;i++)
flags(li[i])|=Visited2Mask;
nameArray = array_alloc(char *,0);
tmpTable = st_init_table(st_ptrcmp,st_ptrhash);
PureSat_GetLatchForNode(manager,pm,property,nameArray,tmpTable,2);
PureSat_CleanMask(manager,ResetVisitedMask);
li = tf->latchInputs[2];
bli = tf->blatchInputs[2];
while(nameArray->num>0){
nameArray1 = nameArray;
nameArray = array_alloc(char *,0);
arrayForEachItem(char*,nameArray1,i,name){
latch = Ntk_NetworkFindNodeByName(network,name);
st_lookup(node2MvfAigTable,latch,&mvfAig);
for(j=0;j<mvfAig->num;j++){
int retVal;
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
if(v==bAig_Zero||v==bAig_One)
continue;
retVal = st_lookup(tf->li2index,(char*)v,&index);
assert(retVal);
if(li[index]==bAig_Zero||li[index]==bAig_One)
continue;
PureSat_GetLatchForNode(manager,pm,li[index],nameArray,tmpTable,1);
}
lmAigId = Ntk_NodeReadMAigId(latch);
lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
int retVal;
bVar = array_fetch(mAigBvar_t,bVarList,index1);
if(bVar.node==bAig_Zero||bVar.node==bAig_One)
continue;
retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
assert(retVal);
if(bli[index]==bAig_Zero||bli[index]==bAig_One)
continue;
PureSat_GetLatchForNode(manager,pm,bli[index],nameArray,tmpTable,1);
}
}
array_free(nameArray1);
}
array_free(nameArray);
PureSat_CleanMask(manager,ResetVisitedMask);
PureSat_CleanMask(manager,ResetVisited2Mask);
PureSat_CleanMask(manager,ResetVisited3Mask);
return tmpTable;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatGetIndenticalLatch | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Generate identical latch clusters]
Description []
SideEffects []
SeeAlso []
Definition at line 3825 of file puresatIPUtil.c.
{
bAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
bAigTimeFrame_t * tf = manager->timeframeWOI;
bAigEdge_t *li=tf->latchInputs[2],*bli = tf->blatchInputs[2];
int i;
bAigEdge_t v;
st_table *table;
st_generator *stgen,*stgen1;
char *name,*name1;
st_table *table2,*table1=st_init_table(st_ptrcmp,st_ptrhash);
pm->IdenLatchTable = st_init_table(st_ptrcmp,st_ptrhash);
for(i=0;i<tf->nLatches;i++){
v=bAig_NonInvertedEdge(li[i]);
if(!st_lookup(table1,(char*)v,NIL(char*))){
if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){
int init=0;
st_foreach_item(table,stgen,&name,NIL(char*)){
if(!st_lookup(pm->IdenLatchTable,name,&table2)){
st_insert(pm->IdenLatchTable,name,table);
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s and ",name);
init = 1;
}
/*insert everything in table 2 into table
name is already in another group, put everything of current group
into that group*/
else{
st_foreach_item(table,stgen1,&name1,NIL(char*)){
st_insert(table2,name1,(char*)0);
st_insert(pm->IdenLatchTable,name1,table2);
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s and ",name1);
}
if(pm->verbosity>=2)
fprintf(vis_stdout,"are the same\n");
break;
}
}
if(init){
if(pm->verbosity>=2)
fprintf(vis_stdout,"are the same\n");
}
}
st_insert(table1,(char*)v,(char*)0);
}
}
for(i=0;i<tf->nbLatches;i++){
v=bAig_NonInvertedEdge(bli[i]);
if(!st_lookup(table1,(char*)v,NIL(char*))){
if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){
int init=0;
st_foreach_item(table,stgen,&name,NIL(char*)){
if(!st_lookup(pm->IdenLatchTable,name,table2)){
st_insert(pm->IdenLatchTable,name,table);
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s and ",name);
init = 1;
}
/*insert everything in table 2 into table
name is already in another group, put everything of current group
into that group*/
else{
st_foreach_item(table,stgen1,&name1,NIL(char*)){
st_insert(table2,name1,(char*)0);
st_insert(pm->IdenLatchTable,name1,table2);
if(pm->verbosity>=2)
fprintf(vis_stdout,"%s and ",name1);
}
if(pm->verbosity>=2)
fprintf(vis_stdout,"are the same\n");
break;
}
}
if(init){
if(pm->verbosity>=2)
fprintf(vis_stdout,"are the same\n");
}
}
st_insert(table1,(char*)v,(char*)0);
}
}
st_free_table(table1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatKillPseudoGV | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| st_table * | AbsTable, | ||
| int | from, | ||
| int | to | ||
| ) |
Function********************************************************************
Synopsis [Kill all pseudo global variables for interpolation computation]
Description [Kill all pseudo global variables for interpolation computation]
SideEffects []
SeeAlso []
Definition at line 1013 of file puresatIPUtil.c.
{
bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
bAigTimeFrame_t *tf = manager->timeframeWOI;
array_t *bVarList,*mVarList;
bAigEdge_t * li, *bli,node;
int i,j;
st_table * tmpTable, *DoneTable;
pm->oldPos = manager->nodesArraySize-bAigNodeSize;
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
if(from < 1)
from = 1;
if(to>pm->Length)
to=pm->Length;
li = tf->latchInputs[1];
bli = tf->blatchInputs[1];
for(j=0;j<tf->nLatches;j++)
flags(li[j])&=ResetPGVMask;
for(j=0;j<tf->nbLatches;j++)
flags(bli[j])&=ResetPGVMask;
for(i=from;i<=to;i++){
li = tf->latchInputs[i];
bli = tf->blatchInputs[i];
manager->class_ = i;
tmpTable = st_init_table(st_numcmp,st_numhash);
DoneTable = st_init_table(st_numcmp,st_numhash);
for(j=0; j<tf->nLatches; j++){
node = bAig_NonInvertedEdge(li[j]);
if(st_lookup(DoneTable,(char*)node,NIL(char*)))
continue;
st_insert(DoneTable,(char*)node,(char*)0);
if((flags(node)&StateBitMask)&&
!(flags(node)&VisibleVarMask)&&
(flags(node)&CoiMask)){
if(i==1)
PureSatKillPseudoGVNode(manager,node,tmpTable);
else
PureSatAbstractLatch(manager,node,tmpTable);
}
}
for(j=0; j<tf->nbLatches; j++){
node = bAig_NonInvertedEdge(bli[j]);
if(st_lookup(DoneTable,(char*)node,NIL(char*)))
continue;
st_insert(DoneTable,(char*)node,(char*)0);
if((flags(node)&StateBitMask)&&
!(flags(node)&VisibleVarMask)&&
(flags(node)&CoiMask)){
if(i==1)
PureSatKillPseudoGVNode(manager,node,tmpTable);
else
PureSatAbstractLatch(manager,node,tmpTable);
}
}
st_free_table(tmpTable);
st_free_table(DoneTable);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatKillPseudoGVNode | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | v, | ||
| st_table * | tmpTable | ||
| ) |
Function********************************************************************
Synopsis [Kill all pseudo global variables for one node for interpolation computation]
Description [Kill all pseudo global variables for one node for interpolation computation]
SideEffects []
SeeAlso []
Definition at line 929 of file puresatIPUtil.c.
{
long size = nFanout(v),i,inv=0;
bAigEdge_t v1,v2,nv;
bAigEdge_t * fan = (bAigEdge_t *)fanout(v),left;
/*fanin: set left and right to bAig_NULL*/
nv = bAig_NonInvertedEdge(v);
flags(nv) |= PGVMask;
if(leftChild(nv)!=bAig_NULL){
if(!(flags(leftChild(nv))&CoiMask))
flags(leftChild(nv)) |= Visited3Mask;
manager->NodesArray[nv+bAigLeft]=bAig_NULL;
}
if(rightChild(nv)!=bAig_NULL){
if(!(flags(rightChild(nv))&CoiMask))
flags(rightChild(nv)) |= Visited3Mask;
manager->NodesArray[nv+bAigRight]=bAig_NULL;
}
manager->class_ = 2;
/*fanout: connection to vars in next tf is disconnected, and a new pseudo var
is created, and used as a replacement*/
for(i=0;i<size;i++){
v1 = bAig_NonInvertedEdge(fan[i]>>1);
if(!(flags(v1)&CoiMask))
continue;
if(bAig_Class(v1)>1){
/*igonre invSV since its left and right will be processed to 2*/
if(!(flags(v1)&VisibleVarMask)&&(flags(v1)&StateBitMask))
continue;
/*if nonSV, create new Node as replacement*/
if(!st_lookup(tmpTable,(char*)nv,&v2)){
v2 = bAig_CreateNode(manager,bAig_NULL, bAig_NULL);
flags(v2) |= DummyMask;
st_insert(tmpTable,(char*)nv,(char*)v2);
}
left = 1;
if(bAig_IsInverted(fan[i]))
left = 0;
inv = bAig_IsInverted(fan[i]>>1)?1:0;
v2 = inv ? bAig_Not(v2) : v2;
if(left){
#if DBG
assert(manager->NodesArray[v1+bAigLeft] != v2);
#endif
manager->NodesArray[v1+bAigLeft] = v2;
PureSat_connectOutput(manager, v2, v1,0);
flags(v2) |= CoiMask;
}
else{
#if DBG
assert(manager->NodesArray[v1+bAigRight] != v2);
#endif
manager->NodesArray[v1+bAigRight] = v2;
PureSat_connectOutput(manager, v2, v1,1);
flags(v2) |= CoiMask;
}
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatMarkObj | ( | bAig_Manager_t * | manager, |
| long | from, | ||
| long | to | ||
| ) |
Function********************************************************************
Synopsis [Mark all node between from and to with obj mask]
Description []
SideEffects []
SeeAlso []
Definition at line 3002 of file puresatIPUtil.c.
{
long v;
for(v=from;v<=to;v+=bAigNodeSize)
flags(v)|=ObjMask;
}
Here is the caller graph for this function:
| void PuresatMarkVisibleVar | ( | Ntk_Network_t * | network, |
| array_t * | visibleArray, | ||
| PureSat_Manager_t * | pm, | ||
| int | from, | ||
| int | to | ||
| ) |
Function********************************************************************
Synopsis [Mark visible latch variables]
Description []
SideEffects []
SeeAlso []
Definition at line 2555 of file puresatIPUtil.c.
{
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
MvfAig_Function_t *mvfAig;
bAigTimeFrame_t * tf = manager->timeframeWOI;
mAigMvar_t lmVar;
mAigBvar_t bVar;
array_t *bVarList,*mVarList;
int i,j,k,lmAigId,index,index1;
char * name;
Ntk_Node_t * latch;
bAigEdge_t node,v, *li, *bli;
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
if(from<0)
from=0;
if(to>pm->Length+1)
to=pm->Length+1;
for(i=from;i<=to;i++){
li = tf->latchInputs[i];
bli = tf->blatchInputs[i];
arrayForEachItem(char *,visibleArray,k,name){
latch = Ntk_NetworkFindNodeByName(network,name);
st_lookup(node2MvfAigTable,latch,&mvfAig);
/*multi val var*/
for(j=0;j<mvfAig->num;j++){
int retVal;
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
if(v==bAig_Zero||v==bAig_One)
continue;
retVal = st_lookup(tf->li2index,(char*)v,&index);
assert(retVal);
if(li[index]==bAig_Zero||li[index]==bAig_One)
continue;
node = bAig_NonInvertedEdge(li[index]);
manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
}
/*binary var*/
lmAigId = Ntk_NodeReadMAigId(latch);
lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
int retVal;
bVar = array_fetch(mAigBvar_t,bVarList,index1);
if(bVar.node==bAig_Zero||bVar.node==bAig_One)
continue;
retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
assert(retVal);
if(bli[index]==bAig_Zero||bli[index]==bAig_One)
continue;
node = bAig_NonInvertedEdge(bli[index]);
manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
}
}// arrayForEachItem(char *,visibleArray,k,name)
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PuresatMarkVisibleVarWithVPGV | ( | Ntk_Network_t * | network, |
| array_t * | visibleArray, | ||
| PureSat_Manager_t * | pm, | ||
| int | from, | ||
| int | to | ||
| ) |
Function********************************************************************
Synopsis [Mark visible variable and also mark visible pseudo global variable]
Description []
SideEffects []
SeeAlso []
Definition at line 2452 of file puresatIPUtil.c.
{
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
MvfAig_Function_t *mvfAig;
bAigTimeFrame_t * tf = manager->timeframeWOI;
mAigMvar_t lmVar;
mAigBvar_t bVar;
array_t *bVarList,*mVarList;
int i,j,k,lmAigId,index,index1;
char * name;
Ntk_Node_t * latch;
bAigEdge_t node,v, *li, *bli;
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
/*Although some SV in tf 0 are not marked as visiblevar,
//they actually visible since all SV of tf 0 are visible*/
if(from<0)
from=0;
if(to>pm->Length+1)
to=pm->Length+1;
/*clean VPGV mask*/
li = tf->latchInputs[1];
bli = tf->blatchInputs[1];
for(j=0;j<tf->nLatches;j++)
flags(li[j])&=ResetVPGVMask;
for(j=0;j<tf->nbLatches;j++)
flags(bli[j])&=ResetVPGVMask;
for(i=from;i<=to;i++){
li = tf->latchInputs[i];
bli = tf->blatchInputs[i];
arrayForEachItem(char *,visibleArray,k,name){
int retVal;
latch = Ntk_NetworkFindNodeByName(network,name);
st_lookup(node2MvfAigTable,latch,&mvfAig);
for(j=0;j<mvfAig->num;j++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
if(v==bAig_Zero||v==bAig_One)
continue;
retVal = st_lookup(tf->li2index,(char*)v,&index);
assert(retVal);
if(li[index]==bAig_Zero||li[index]==bAig_One)
continue;
node = bAig_NonInvertedEdge(li[index]);
manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
/*marking PGV*/
if(i==1){
if(!st_lookup(pm->vertexTable,name,NIL(char*))){
flags(node) |= VPGVMask;
}
}
}
lmAigId = Ntk_NodeReadMAigId(latch);
lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
int retVal;
bVar = array_fetch(mAigBvar_t,bVarList,index1);
if(bVar.node==bAig_Zero||bVar.node==bAig_One)
continue;
retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
assert(retVal);
if(bli[index]==bAig_Zero||bli[index]==bAig_One)
continue;
node = bAig_NonInvertedEdge(bli[index]);
manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
/*marking PGV*/
if(i==1){
if(!st_lookup(pm->vertexTable,name,NIL(char*)))
flags(node) |= VPGVMask;
}
}
}
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatPostprocess | ( | bAig_Manager_t * | manager, |
| satManager_t * | cm, | ||
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Recovery step after SAT solving]
Description [Recovery step after SAT solving]
SideEffects []
SeeAlso []
Definition at line 1774 of file puresatIPUtil.c.
{
PureSatRecoverFanout(cm,pm);
PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
PureSat_CleanMask(manager,ResetVisited3Mask);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatPreprocess | ( | Ntk_Network_t * | network, |
| satManager_t * | cm, | ||
| PureSat_Manager_t * | pm, | ||
| st_table * | vertexTable, | ||
| int | Length | ||
| ) |
Function********************************************************************
Synopsis [Preprocess to form SAT instances]
Description [Preprocess to form SAT instances]
SideEffects []
SeeAlso []
Definition at line 1744 of file puresatIPUtil.c.
{
bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
PureSatSetCOI(network,pm,cm,vertexTable,0, Length,Length);
/*for interpolation*/
PureSatKillPseudoGV(network,pm,vertexTable,1,Length);
PureSat_ResetManager(manager,cm,0);
/*for abstraction*/
PureSatProcessFanout(cm);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatPreProcLatch | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [There are some latches whose DI is empty, put them into abstraction will not add any burden to model checker]
Description []
SideEffects []
SeeAlso []
Definition at line 3748 of file puresatIPUtil.c.
{
st_generator * stgen;
bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
bAigTimeFrame_t * tf = manager->timeframeWOI;
mAigMvar_t lmVar;
mAigBvar_t bVar;
array_t *bVarList,*mVarList;
int j,lmAigId,id,index1;
char * name;
Ntk_Node_t * latch;
bAigEdge_t v, **li, **bli;
MvfAig_Function_t *mvfAig;
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
li = tf->latchInputs;
bli = tf->blatchInputs;
st_foreach_item(pm->CoiTable,stgen,&latch,NIL(char*)){
int checkbin=1;
st_lookup(node2MvfAigTable,latch,&mvfAig);
for(j=0;j<mvfAig->num;j++){
int retVal;
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
if(v==bAig_Zero||v==bAig_One)
continue;
retVal = st_lookup(tf->li2index,(char*)v,&id);
assert(retVal);
if(li[0][id]==li[1][id]&&li[1][id]==li[2][id]){
name = Ntk_NodeReadName(latch);
st_insert(pm->vertexTable,name,(char*)0);
if(pm->verbosity>=2)
fprintf(vis_stdout,"preproc: add %s to abs\n",name);
checkbin = 0;
break;
}
}
if(checkbin){
lmAigId = Ntk_NodeReadMAigId(latch);
lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
int retVal;
bVar = array_fetch(mAigBvar_t,bVarList,index1);
if(bVar.node==bAig_Zero||bVar.node==bAig_One)
continue;
retVal = st_lookup(tf->bli2index,(char*)bVar.node,&id);
assert(retVal);
if(bli[0][id]==bli[1][id]&&bli[1][id]==bli[2][id]){
name = Ntk_NodeReadName(latch);
st_insert(pm->vertexTable,name,(char*)0);
if(pm->verbosity>=2)
fprintf(vis_stdout,"preproc BINARY: add %s to abs\n",name);
break;
}
}
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatProcessDummy | ( | bAig_Manager_t * | manager, |
| satManager_t * | cm, | ||
| RTnode_t | RTnode | ||
| ) |
Function********************************************************************
Synopsis [process dummy nodes]
Description [In UNSAT core, there may be dummy nodes, but in manager, they don't exist any more. This funct is to mark them]
SideEffects []
SeeAlso []
Definition at line 2748 of file puresatIPUtil.c.
{
int i;
bAigEdge_t *lp,node;
RTManager_t *rm = cm->rm;
if(RT_flag(RTnode)&RT_VisitedMask){
return;
}
RT_flag(RTnode) |= RT_VisitedMask;
if(RT_pivot(RTnode)==0){ /*leaf*/
#if DBG
assert(RT_oriClsIdx(RTnode)==0);
#endif
if(RT_oriClsIdx(RTnode))
lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
else
lp = RT_formula(RTnode) + cm->rm->fArray;
for(i=0;i<RT_fSize(RTnode);i++,lp++){
assert(*lp>0);/* not processed yet*/
if(RT_oriClsIdx(RTnode))/*is CNF*/
node = SATgetNode(*lp);
else /*is AIG*/
node = *lp;
node = SATnormalNode(node);
if(node>=manager->nodesArraySize){
#if DBG
assert(flags(node)&DummyMask);
#endif
*lp = DUMMY;
}
}
} /*leaf*/
/*not leaf*/
else{
if(RT_pivot(RTnode)>=manager->nodesArraySize){
int class_ = bAig_Class(RT_pivot(RTnode));
RT_pivot(RTnode) = DUMMY+class_;
}
PureSatProcessDummy(manager,cm,RT_left(RTnode));
PureSatProcessDummy(manager,cm,RT_right(RTnode));
}
return ;
}
Here is the caller graph for this function:
| void PureSatProcessFanout | ( | satManager_t * | cm | ) |
Function********************************************************************
Synopsis [Process fanout nodes to generate abstraction]
Description [Process fanout nodes to generate abstraction]
SideEffects []
SeeAlso []
Definition at line 1374 of file puresatIPUtil.c.
{
long bufSize, bufIndex;
bAigEdge_t *buf,left,right,*fan,v,cur;
int i, j;
long size, tsize;
int InvStateVar,l;
bufSize = 1024;
bufIndex = 0;
buf = malloc(sizeof(bAigEdge_t) * bufSize);
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
v = i;
if(!(SATflags(v) & CoiMask))
continue;
InvStateVar = 0;
if((SATflags(v)&StateBitMask)&&
!(SATflags(v)&VisibleVarMask))
InvStateVar = 1;
size = SATnFanout(v);
if(size >= bufSize) {
bufSize <<= 1;
if(size >= bufSize)
bufSize = size + 1;
buf = realloc(buf, sizeof(bAigEdge_t) * bufSize);
}
bufIndex = 0;
for(j=0, fan = SATfanout(v); j<size; j++) {
cur = fan[j];
cur >>= 1;
cur = SATnormalNode(cur);
/*Not in COI , pass */
if(!(SATflags(cur) & CoiMask))
continue;
/*cur is invisible var*/
left = SATleftChild(cur);
right = SATrightChild(cur);
if(left==bAig_NULL||right==bAig_NULL){
#if DBG
assert(left==bAig_NULL&&right==bAig_NULL);
assert((SATflags(cur)&StateBitMask)&&
!(SATflags(cur)&VisibleVarMask));
#endif
continue;
}
/*v itself is InvStateVar and cur is not InvSV*/
if(SATflags(v)&PGVMask){
if(SATclass(cur)>=2){
l = SATisInverted(fan[j]) ? 0 : 1;
if(l){
#if DBG
bAigEdge_t v1 = SATnormalNode(SATleftChild(cur));
assert(v1!=v);
assert(SATflags(v1)&DummyMask);
#endif
}
else{
#if DBG
bAigEdge_t v1 = SATnormalNode(SATrightChild(cur));
assert(v1!=v);
assert(SATflags(v1)&DummyMask);
#endif
}
continue;
}
}
buf[bufIndex++] = fan[j];
}
if(bufIndex > 0) {
tsize = bufIndex;
for(j=0, fan=SATfanout(v); j<size; j++) {
cur = fan[j];
cur >>= 1;
cur = SATnormalNode(cur);
if(!(SATflags(cur) & CoiMask)) {
buf[bufIndex++] = fan[j];
continue;
}
left = SATleftChild(cur);
right = SATrightChild(cur);
if(left==bAig_NULL||right==bAig_NULL){
buf[bufIndex++] = fan[j];
continue;
}
if(SATflags(v)&PGVMask){
if(SATclass(cur)>=2){
buf[bufIndex++] = fan[j];
continue;
}
}
}/*for(j=0, fan=SATfanout(v); j<size; j++) {*/
buf[bufIndex] = 0;
memcpy(fan, buf, sizeof(bAigEdge_t)*(size+1));
SATnFanout(v) = tsize;
}
else
SATnFanout(v) = 0;
}
free(buf);
for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
v = i;
if(!(SATflags(v) & CoiMask))
continue;
fan = SATfanout(v);
size = SATnFanout(v);
qsort(fan, size, sizeof(bAigEdge_t), NodeIndexCompare);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatRecoverFanout | ( | satManager_t * | cm, |
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Recover fanout of nodes]
Description [Recover fanout of nodes]
SideEffects []
SeeAlso []
Definition at line 1635 of file puresatIPUtil.c.
{
bAigEdge_t i, v;
/*dummy node can't be recovered*/
for(i=satNodeSize; i<=pm->oldPos; i+=satNodeSize) {
v = i;
if(SATflags(v) & IsCNFMask)
continue;
if((SATflags(v)&CoiMask)){
SATnFanout(v) = PureSatRecoverFanoutNode(cm, v);
continue;
}
/*for some node not in coi, but a child of one coi(ISV) node*/
if(SATflags(v)&Visited3Mask){
PureSatRecoverISVNode(cm,v);
continue;
}
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| long PureSatRecoverFanoutNode | ( | satManager_t * | cm, |
| bAigEdge_t | v | ||
| ) |
Function********************************************************************
Synopsis [Recover from abstractions]
Description [Recover from abstractions]
SideEffects []
SeeAlso []
Definition at line 1512 of file puresatIPUtil.c.
{
bAigEdge_t *fan,nfan,child,cur;
long i;
int left,inver;
int InvStateVar = 0;
if(!(SATflags(v)&VisibleVarMask)&&(SATflags(v)&StateBitMask))
InvStateVar = 1;
nfan = SATnFanout(v);
fan = SATfanout(v);
if(fan == 0) return(0);
/*recover left and right children for latch nodes*/
for(i=nfan; fan[i]!=0; i++){
cur = fan[i];
if(!(SATflags(SATnormalNode(cur>>1))&CoiMask))
continue;
/*cur is InvSV*/
if((SATleftChild(SATnormalNode(cur>>1))==bAig_NULL)||
(SATrightChild(SATnormalNode(cur>>1))==bAig_NULL)){
#if DBG
assert((SATflags(SATnormalNode(cur>>1))&StateBitMask)&&
!(SATflags(SATnormalNode(cur>>1))&VisibleVarMask));
#endif
left = 1;
inver = 0;
if(SATisInverted(cur))
left = 0;
cur >>= 1;
if(SATisInverted(cur))
inver = 1;
cur = SATnormalNode(cur);
child = inver? SATnormalNode(v)+1:SATnormalNode(v);
if(left)
SATleftChild(cur)=child;
else
SATrightChild(cur)=child;
continue;
}
/*v is InvSV, cur is not InvSV*/
if(SATflags(v)&PGVMask){
if(SATclass(SATnormalNode(cur>>1))>=2){
left = 1;
inver = 0;
if(SATisInverted(cur))
left = 0;
cur >>= 1;
if(SATisInverted(cur))
inver = 1;
cur = SATnormalNode(cur);
child = inver? SATnormalNode(v)+1:SATnormalNode(v);
if(left)
SATleftChild(cur)=child;
else
SATrightChild(cur)=child;
}
}
}
//recover all fanout
return(i);
}
Here is the caller graph for this function:
| void PureSatRecoverISVNode | ( | satManager_t * | cm, |
| bAigEdge_t | v | ||
| ) |
Function********************************************************************
Synopsis [Recover invisible state variable node]
Description [Recover invisible state variable node]
SideEffects []
SeeAlso []
Definition at line 1594 of file puresatIPUtil.c.
{
bAigEdge_t size = SATnFanout(v),cur,node,child;
bAigEdge_t * fan = SATfanout(v);
int inv,i,left;
for(i=0;i<size;i++){
cur = fan[i]>>1;
node = SATnormalNode(cur);
/*not in coi*/
if(!(SATflags(node)&CoiMask))
continue;
/*not invisible var*/
if(!((SATflags(node)&StateBitMask)&&
!(SATflags(node)&VisibleVarMask)))
continue;
left=SATisInverted(fan[i])?0:1;
inv=SATisInverted(cur)?1:0;
child = inv?SATnormalNode(v)+1:SATnormalNode(v);
if(left)
SATleftChild(node) = child;
else
SATrightChild(node) = child;
}
}
Here is the caller graph for this function:
| void PureSatSetCOI | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| satManager_t * | cm, | ||
| st_table * | AbsTable, | ||
| int | from, | ||
| int | to, | ||
| int | bound | ||
| ) |
Function********************************************************************
Synopsis [Set COI for form the SAT problem]
Description [Set COI for form the SAT problem]
SideEffects []
SeeAlso []
Definition at line 859 of file puresatIPUtil.c.
{
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
bAigEdge_t property;
if(cm->obj->num>0){
property = cm->obj->space[0];
PureSatSetLatchCOI2(network,pm,cm,property,bound);
}
else{
PureSatSetLatchCOI(network,pm,cm,AbsTable,from,to);
PureSat_CleanMask(manager,ResetVisited3Mask);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatSetLatchCOI | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| satManager_t * | cm, | ||
| st_table * | AbsTable, | ||
| int | from, | ||
| int | to | ||
| ) |
Function********************************************************************
Synopsis [Set COI for latch nodes]
Description [Set COI for latch nodes]
SideEffects []
SeeAlso []
Definition at line 754 of file puresatIPUtil.c.
{
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
bAigTimeFrame_t *tf = manager->timeframeWOI;
int i,j;
bAigEdge_t *L0,*L1,*bL0,*bL1;
satArray_t * assert;
int nLatches = tf->nLatches, nbLatches = tf->nbLatches;
if(from>=to) return;
PureSat_ResetCoi(cm);
assert = sat_ArrayAlloc(1);
sat_ArrayInsert(assert,manager->InitState);
PureSat_MarkTransitiveFaninForArray3(manager,assert,CoiMask);
sat_ArrayFree(assert);
for(i=from; i<to; i++){
assert = sat_ArrayAlloc(1);
L0 = tf->latchInputs[i];
L1 = tf->latchInputs[i+1];
bL0 = tf->blatchInputs[i];
bL1 = tf->blatchInputs[i+1];
for(j=0;j<nLatches;j++){
if(L1[j]!=bAig_One&&L1[j]!=bAig_Zero){
if(flags(L1[j])&VisibleVarMask)
sat_ArrayInsert(assert,L1[j]);
}
if(L0[j]!=bAig_One&&L0[j]!=bAig_Zero&&
!(flags(L0[j])&VisibleVarMask))
flags(L0[j]) |= Visited3Mask;
}
for(j=0;j<nbLatches;j++){
if(bL1[j]!=bAig_One&&bL1[j]!=bAig_Zero){
if(flags(bL1[j])&VisibleVarMask)
sat_ArrayInsert(assert,bL1[j]);
}
if(bL0[j]!=bAig_One&&bL0[j]!=bAig_Zero&&
!(flags(bL0[j])&VisibleVarMask))
flags(bL0[j]) |= Visited3Mask;
}
PureSat_MarkTransitiveFaninForArray2(manager,assert,CoiMask);
sat_ArrayFree(assert);
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatSetLatchCOI2 | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| satManager_t * | cm, | ||
| bAigEdge_t | obj, | ||
| int | bound | ||
| ) |
Function********************************************************************
Synopsis [Set COI for latch nodes]
Description [Set COI for latch nodes]
SideEffects []
SeeAlso []
Definition at line 827 of file puresatIPUtil.c.
{
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
satArray_t * assert;
PureSat_ResetCoi(cm);
assert = sat_ArrayAlloc(1);
sat_ArrayInsert(assert,obj);
PureSat_MarkTransitiveFaninForArray4(manager,assert,CoiMask,bound);
PureSat_MarkTransitiveFaninForArray4(manager,cm->assertArray,CoiMask,bound);
sat_ArrayFree(assert);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| RTnode_t RTCreateNode | ( | RTManager_t * | rm | ) |
AutomaticEnd Function********************************************************************
Synopsis [Create a node for resolution tree]
Description [Create a node for resolution tree]
SideEffects []
SeeAlso []
Definition at line 173 of file puresatIPUtil.c.
{
RTnode_t node;
if(rm->nArray==0){
rm->nArray = ALLOC(long, RTnodeSize*RT_BLOCK);
rm->maxSize = RTnodeSize*RT_BLOCK;
rm->aSize = 0;
}
if(rm->maxSize<=rm->aSize+RTnodeSize){
rm->nArray = REALLOC(long, rm->nArray,rm->maxSize+RTnodeSize*RT_BLOCK);
if(rm->nArray == 0){
fprintf(vis_stdout,"memout when alloc %ld bytes\n",
(rm->maxSize+RTnodeSize*RT_BLOCK)*4);
exit(0);
}
rm->maxSize = rm->maxSize+RTnodeSize*1000;
}
rm->aSize += RTnodeSize;
node = rm->aSize;
RT_fSize(node) = 0;
RT_formula(node) = 0;
RT_oriClsIdx(node) = 0;
RT_pivot(node) = 0;
RT_flag(node) = 0;
RT_IPnode(node) = -1;
RT_left(node) = 0;
RT_right(node) = 0;
if(rm->fArray==0){
rm->fArray = ALLOC(long,FORMULA_BLOCK);
rm->cpos = 0;
rm->maxpos = FORMULA_BLOCK;
}
return node;
}
Here is the caller graph for this function:
| static int StringCheckIsInteger | ( | char * | string, |
| int * | value | ||
| ) | [static] |
Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 138 of file puresatIPUtil.c.
{
char *ptr;
long l;
l = strtol (string, &ptr, 0) ;
if(*ptr != '\0')
return 0;
if ((l > MAXINT) || (l < -1 - MAXINT))
return 1 ;
*value = (int) l;
return 2 ;
}
Here is the caller graph for this function:
