#include "maig.h"#include "ntk.h"#include "cmd.h"#include "baig.h"#include "baigInt.h"#include "ctlsp.h"
Include dependency graph for baigCmd.c:
Go to the source code of this file.
Functions | |
| static int | CommandPrintPartitionAig (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static int | CommandPrintAigStats (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static int | CommandCheckInvariantSat (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static void | TimeOutHandle (void) |
| void | bAig_Init (void) |
| void | bAig_End (void) |
| bAig_Manager_t * | bAig_initAig (int maxSize) |
| void | bAig_quit (bAig_Manager_t *manager) |
| void | bAig_NodePrint (bAig_Manager_t *manager, bAigEdge_t node) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: baigCmd.c,v 1.32 2009/04/12 00:14:03 fabio Exp $" |
| static jmp_buf | timeOutEnv |
| static int | bmcTimeOut |
| static long | alarmLapTime |
Function Documentation
| void bAig_End | ( | void | ) |
| void bAig_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initialize baig package]
SideEffects [none]
SeeAlso [bAig_End]
Definition at line 83 of file baigCmd.c.
{
Cmd_CommandAdd("print_partition_aig_dot", CommandPrintPartitionAig, 0);
Cmd_CommandAdd("print_aig_stats", CommandPrintAigStats, 0);
Cmd_CommandAdd("check_invariant_sat", CommandCheckInvariantSat, 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAig_Manager_t* bAig_initAig | ( | int | maxSize | ) |
Function********************************************************************
Synopsis [Creates a new bAig manager.]
Description [Creates a new bAig manager, Create a NodeArray of size equal to maxSize * bAigNodeSize. Returns a pointer to the manager if successful; NULL otherwise.]
SideEffects [None]
SeeAlso []
Definition at line 119 of file baigCmd.c.
{
int i;
bAig_Manager_t *manager = ALLOC(bAig_Manager_t,1);
if (manager == NIL( bAig_Manager_t)){
return NIL( bAig_Manager_t);
}
/*Bing:*/
memset(manager,0,sizeof(bAig_Manager_t ));
maxSize = maxSize * bAigNodeSize; /* each node is a size of bAigNodeSize */
/* ??? */
/* maxSize = (maxSize/bAigNodeSize)*bAigNodeSize;
if (maxSize > bAigArrayMaxSize ) {
}*/
manager->NodesArray = ALLOC(bAigEdge_t, maxSize);
manager->maxNodesArraySize = maxSize;
manager->nodesArraySize = bAigFirstNodeIndex;
fanout(0) = 0;
canonical(0) = 0;
flags(0) = 0;
aig_value(0) = 2;
next(0) = bAig_NULL;
/*Bing:*/
memset(manager->NodesArray,0,maxSize*sizeof(bAigEdge_t));
manager->SymbolTable = st_init_table(strcmp,st_strhash);
manager->nameList = ALLOC(char *, manager->maxNodesArraySize/bAigNodeSize);
manager->bddIdArray = ALLOC(int, manager->maxNodesArraySize/bAigNodeSize);
manager->bddArray = ALLOC(bdd_t *, manager->maxNodesArraySize/bAigNodeSize);
manager->HashTable = ALLOC(bAigEdge_t, bAig_HashTableSize);
for (i=0; i<bAig_HashTableSize; i++)
manager->HashTable[i]= bAig_NULL;
manager->mVarList = array_alloc(mAigMvar_t, 0);
manager->bVarList = array_alloc(mAigBvar_t, 0);
manager->timeframe = 0;
manager->timeframeWOI = 0;
manager->literals = 0;
/* Bing: for MultiCut */
manager->SymbolTableArray = ALLOC(st_table *,100);
manager->HashTableArray = ALLOC(bAigEdge_t *,100);
manager->NumOfTable = 100;
/* Bing: for interpolation */
manager->class_ = 1;
manager->InitState = bAig_One;
manager->assertArray = (satArray_t *)0;
return(manager);
} /* end of bAig_Init */
Here is the caller graph for this function:
| void bAig_NodePrint | ( | bAig_Manager_t * | manager, |
| bAigEdge_t | node | ||
| ) |
Function********************************************************************
Synopsis []
Description []
SideEffects [None]
SeeAlso []
Definition at line 234 of file baigCmd.c.
{
if (node == bAig_Zero) {
printf("0");
return;
}
if (node == bAig_One) {
printf("1");
return;
}
if (bAig_IsInverted(node)){
printf(" NOT(");
}
if (bAigIsVar(manager,node)) {
printf("Var Node");
} else {
printf("(");
bAig_NodePrint(manager, leftChild(node));
printf("AND");
bAig_NodePrint(manager, rightChild(node));
printf(")");
}
if (bAig_IsInverted(node)){
printf(")");
}
} /* bAig_NodePrint */
| void bAig_quit | ( | bAig_Manager_t * | manager | ) |
Function********************************************************************
Synopsis [Quit bAig manager]
SideEffects []
SeeAlso []
Definition at line 190 of file baigCmd.c.
{
char *name;
st_generator *stGen;
bAigEdge_t varIndex;
if (manager->mVarList != NIL(array_t)){
array_free(manager->mVarList);
}
if (manager->bVarList != NIL(array_t)){
array_free(manager->bVarList);
}
FREE(manager->HashTable);
st_foreach_item(manager->SymbolTable, stGen, &name, &varIndex) {
FREE(name);
}
st_free_table(manager->SymbolTable);
/* i is too small to represent 80000
for (i=0; i< manager->maxNodesArraySize/bAigNodeSize ; i++){
FREE(manager->nameList[i]);
}
*/
FREE(manager->nameList);
FREE(manager->NodesArray);
bAig_FreeTimeFrame(manager->timeframe);
bAig_FreeTimeFrame(manager->timeframeWOI);
FREE(manager);
/* Free SymbolTableArray and HashTableArray? */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int CommandCheckInvariantSat | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [Implements the check_invariant_sat command.] CommandName [check_invariant_sat]
CommandSynopsis [Check invariant property using sat based unmounded model checking]
CommandArguments [\[-h\] \[-d\] \[-t <timeOutPeriod>\] \[-m <method>\] \[-v <verbosity_level>\] <inv_file> ]
CommandDescription [Perform SAT-based unbounded model checking on And-Inverter-Graph. The command compute fixed point of AG using AX operation. AX is implemented using AllSAT enumeration algorithm.
Command options:
- -d
Disable inclusion test on initial states.
- -v
<verbosity_level> Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
- -t
<timeOutPeriod> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
- -m
<method> Specify the method for AllSAT algorithm.
- -h
Print the command usage.
<inv_file> File containing Invariant formulae to be checked. ]
SideEffects []
SeeAlso []
Definition at line 563 of file baigCmd.c.
{
char *filename;
FILE *fin;
array_t *invarArray;
Ntk_Network_t *network;
bAig_Manager_t *manager;
bAigTransition_t *t;
Ctlsp_Formula_t *formula;
char c;int i, property;
int timeOutPeriod;
int passFlag, method;
int interface, verbose;
int inclusion_test;
int constrain;
int reductionUsingUnsat;
int disableLifting;
timeOutPeriod = -1;
method = 1;
interface = 0;
inclusion_test = 1;
verbose = 0;
constrain = 1;
reductionUsingUnsat = 0;
disableLifting = 0;
util_getopt_reset();
while ((c = util_getopt(argc, argv, "hicdt:m:v:ul")) != EOF) {
switch(c) {
case 'h':
goto usage;
case 'i' :
interface = 1;
break;
case 'd' :
inclusion_test = 0;
break;
case 'c' :
constrain = 0;
break;
case 'u' :
reductionUsingUnsat = 1;
break;
case 'l' :
disableLifting = 1;
break;
case 't' :
timeOutPeriod = atoi(util_optarg);
break;
case 'v' :
verbose = atoi(util_optarg);
break;
case 'm' :
method = atoi(util_optarg);
break;
}
}
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr, "** ERROR : file containing property file not provided\n");
goto usage;
}
else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** ERROR : too many arguments\n");
goto usage;
}
filename = util_strsav(argv[util_optind]);
if(!(fin = fopen(filename, "r"))) {
fprintf(vis_stdout, "Error : can't open invariant file %s\n", filename);
return(1);
}
invarArray = Ctlsp_FileParseFormulaArray(fin);
fclose(fin);
if (timeOutPeriod > 0) {
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stderr,
"** ERROR : timeout occurred after %d seconds.\n", timeOutPeriod);
alarm(0);
return 1;
}
}
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
manager = Ntk_NetworkReadMAigManager(network);
t = bAigCreateTransitionRelation(network, manager);
t->method = method;
t->interface = interface;
t->inclusionInitial = inclusion_test;
t->verbose = verbose;
t->constrain = constrain;
t->disableLifting = disableLifting;
t->reductionUsingUnsat = reductionUsingUnsat;
if(t->verbose > 1)
bAigPrintTransitionInfo(t);
fprintf(vis_stdout, "# INV: Summary of invariant pass/fail\n");
for(i=0; i<array_n(invarArray); i++) {
formula = array_fetch(Ctlsp_Formula_t *, invarArray, i);
Ctlsp_FormulaPrint(vis_stdout, formula);
fprintf(vis_stdout, "\n");
property = bAig_CreatebAigForInvariant(network, manager, formula);
passFlag = bAigCheckInvariantWithAG(t, property);
if(passFlag == 1) {
fprintf(vis_stdout, "# INV: formula passed --- ");
Ctlsp_FormulaPrint(vis_stdout, Ctlsp_FormulaReadOriginalFormula(formula));
fprintf(vis_stdout, "\n");
}
else {
fprintf(vis_stdout, "# INV: formula failed --- ");
Ctlsp_FormulaPrint(vis_stdout, Ctlsp_FormulaReadOriginalFormula(formula));
fprintf(vis_stdout, "\n");
}
}
return(0);
usage:
(void) fprintf(vis_stderr, "usage: check_invariant_sat [-h] <inv_file>\n");
(void) fprintf(vis_stderr, " -h \tprint the command usage\n");
(void) fprintf(vis_stderr, " -d \tdisable inclusion test on initial states\n");
(void) fprintf(vis_stderr, " -m : 0 disable lifting\n");
(void) fprintf(vis_stderr, " 1 enable lifting (default)\n");
(void) fprintf(vis_stderr, " <inv_file> Invariant file to be checked.\n");
return(1);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int CommandPrintAigStats | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
Function********************************************************************
Synopsis [Implements the print_aig_stats command.] CommandName [print_aig_stats]
CommandSynopsis [print statistics about the AND/INVERTER graph.]
CommandArguments [\[-h\] \[-n\]]
CommandDescription [Print the following statistics about the AND/INVERTER graph:
Maximum number of nodes: the maximum number of nodes in the AND/ INVERTER graph.
Current number of nodes: the number of nodes in the AND/INVERTER graph that are used.
Note that build_partition_maigs must be called before this command.
Command options:
- -n
Print the name of the nodes.
- -h
Print the command usage.
]
SideEffects []
SeeAlso []
Definition at line 460 of file baigCmd.c.
{
Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
mAig_Manager_t *manager;
int i;
int printVar = 0;
int c;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "hn")) != EOF) {
switch(c) {
case 'h':
goto usage;
case 'n':
printVar = 1;
break;
default:
goto usage;
}
}
if (network == NIL(Ntk_Network_t)) {
return 1;
}
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(mAig_Manager_t)) {
return 1;
}
(void) fprintf(vis_stdout,"And/Inverter graph Static Report\n");
(void) fprintf(vis_stdout,"Maximum number of nodes: %ld\n", manager->maxNodesArraySize/bAigNodeSize);
(void) fprintf(vis_stdout,"Current number of nodes: %ld\n\n", manager->nodesArraySize/bAigNodeSize);
if (printVar == 1){
(void) fprintf(vis_stdout,"Nodes name\n");
for(i=1; i< manager->nodesArraySize/bAigNodeSize; i++){
if (manager->nameList[i][0] != 'N'){
(void) fprintf(vis_stdout,"%s\n", manager->nameList[i]);
}
}
}
return 0;
usage:
(void) fprintf(vis_stderr, "usage: print_aig_stats [-h] [-n] \n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
(void) fprintf(vis_stderr, " -n list of variables\n");
return 1; /* error exit */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int CommandPrintPartitionAig | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Implements the print_partition_aig_dot command.]
CommandName [print_partition_aig_dot]
CommandSynopsis [Print a dot description of the AND/INVERTER graph that was built for the flattened network]
CommandArguments [\[-h\] <file_name>]
CommandDescription [Write a file in the format taken by the tool dot depicting the topology of the AND/INVERTER graph. Dot is a tool that given a description of a graph in a certain format it produces a postscript print of the graph. For more information about dot look in http://www.research.att.com/orgs/ssr/book/reuse. Once a dot file is produced with this command, the shell command dot -Tps <filename> ><file>.ps will produce the postscript file depicting the network.
If no argument is specified on the command line, the description is written to the standard output.
Command options:
- -h
- Print the command usage.
]
SideEffects []
SeeAlso []
Definition at line 309 of file baigCmd.c.
{
FILE *fp;
int c, i, mvfSize;
Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
mAig_Manager_t *manager;
MvfAig_Function_t *mvfAig;
bAigEdge_t v;
Ntk_Node_t *node, *latch;
st_table *node2MvfAigTable;
lsGen gen;
util_getopt_reset();
while ((c = util_getopt(argc,argv,"h")) != EOF){
switch(c){
case 'h':
goto usage;
default:
goto usage;
}
}
/* Check if the network has been read in */
if (network == NIL(Ntk_Network_t)) {
return 1;
}
if (argc == 1) {
fp = stdout;
}
else if (argc == 2) {
fp = Cmd_FileOpen(*(++argv), "w", NIL(char *), /* silent */ 1);
if (fp == NIL(FILE)) {
(void) fprintf(vis_stderr, "Cannot write to %s\n", *argv);
return 1;
}
}
else {
goto usage;
}
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(mAig_Manager_t)) {
return 1;
}
node2MvfAigTable =
(st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
Ntk_NetworkForEachLatch(network, gen, latch) {
node = Ntk_LatchReadDataInput(latch);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
}
}
Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
}
}
Ntk_NetworkForEachNode(network, gen, node) {
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
}
}
bAig_PrintDot(fp, manager);
Ntk_NetworkForEachLatch(network, gen, latch) {
node = Ntk_LatchReadInitialInput(latch);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
}
}
Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
}
}
Ntk_NetworkForEachNode(network, gen, node) {
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
}
}
return 0;
usage:
(void) fprintf(vis_stderr, "usage: print_partition_aig_dot [-h] [file]\n");
(void) fprintf(vis_stderr, " -h\t\tprint the command usage\n");
return 1;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Handle function for timeout.]
Description [This function is called when the time out occurs. Since alarm is set with an elapsed time, this function checks if the CPU time corresponds to the timeout of the command. If not, it reprograms the alarm to fire again later.]
SideEffects []
Definition at line 716 of file baigCmd.c.
{
int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);
if (seconds < bmcTimeOut) {
unsigned slack = (unsigned) (bmcTimeOut - seconds);
(void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
(void) alarm(slack);
} else {
longjmp(timeOutEnv, 1);
}
} /* TimeOutHandle */
Here is the caller graph for this function:
Variable Documentation
long alarmLapTime [static] |
int bmcTimeOut [static] |
jmp_buf timeOutEnv [static] |
char rcsid [] UNUSED = "$Id: baigCmd.c,v 1.32 2009/04/12 00:14:03 fabio Exp $" [static] |
CFile***********************************************************************
FileName [baigCmd.c]
PackageName [baig]
Synopsis [Functions to initialize and shut down the bAig manager.]
Author [Mohammad Awedh]
Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
