src/baig/baigCmd.c

Go to the documentation of this file.

#include "maig.h"
#include "ntk.h"
#include "cmd.h"
#include "baig.h"
#include "baigInt.h"
#include "ctlsp.h"

static char rcsid[] UNUSED = "$Id: baigCmd.c,v 1.32 2009/04/12 00:14:03 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static jmp_buf timeOutEnv;
static int bmcTimeOut;          /* timeout value */
static long alarmLapTime;       /* starting CPU time for timeout */


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

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);

/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

void
bAig_Init(void)
{
  Cmd_CommandAdd("print_partition_aig_dot", CommandPrintPartitionAig, 0);
  Cmd_CommandAdd("print_aig_stats", CommandPrintAigStats, 0);
  Cmd_CommandAdd("check_invariant_sat", CommandCheckInvariantSat, 0);
}


void
bAig_End(void)
{
}

bAig_Manager_t *
bAig_initAig(
  int maxSize /* maximum number of nodes in the AIG graph */
)
{
  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 */


void
bAig_quit(
  bAig_Manager_t *manager)
{
  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? */
}

void 
bAig_NodePrint(
   bAig_Manager_t *manager,
   bAigEdge_t node)
{
  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 */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

static int
CommandPrintPartitionAig(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  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;
}

static int
CommandPrintAigStats(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  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 */
}

static int
CommandCheckInvariantSat(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
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);
}


static void
TimeOutHandle(void)
{
  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 */