source: vis_dev/vis-2.3/src/amc/amcCmd.c @ 67

/**CFile***********************************************************************

  FileName    [amcCmd.c]

  PackageName [amc]

  Synopsis    [Command interface for the amc package.]

  Author      [Woohyuk Lee <woohyuk@duke.colorado.edu>]

  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.]

******************************************************************************/

#include "amcInt.h"

static char rcsid[] UNUSED = "$Id: amcCmd.c,v 1.44 2005/05/19 02:36:36 awedh Exp $";


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

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

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

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

static jmp_buf timeOutEnv;

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

/**AutomaticStart*************************************************************/

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

static int CommandAmc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static void ApproximateModelCheckUsage(void);
static void TimeOutHandle(void);

/**AutomaticEnd***************************************************************/


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

/**Function********************************************************************

  Synopsis    [Initializes the amc package.]

  SideEffects []

  SeeAlso     [Amc_End]

******************************************************************************/
void
Amc_Init(void)
{
  Cmd_CommandAdd("approximate_model_check", CommandAmc, 0);
/*  Cmd_CommandAdd("approximate_compute_reach", CommandApproxReach, 0); */
}


/**Function********************************************************************

  Synopsis    [Ends the amc package.]

  SideEffects []

  SeeAlso     [Amc_Init]

******************************************************************************/
void
Amc_End(void)
{
}


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


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

/**Function********************************************************************

  Synopsis         [The approximate_model_check command.]

  CommandName      [approximate_model_check]

  CommandSynopsis  [perform ACTL model checking on an abstracted 
                   and flattened network]

  CommandArguments [\[-h\] \[-v &lt;verbosity_level&gt;\] &lt;ctl_file&gt; ]
  
  CommandDescription [Performs ACTL model checking on an abstracted and
  flattened network.  Predefined abstractions are performed prior to model
  checking.  Before calling this command, the user should have initialized the
  design by calling the command <a href="init_verifyCmd.html"> <code>
  init_verify</code></a>.  <p>
   
  The command includes two dual algorithms. The user should set appropriate
  environment parameters associated with the command to execute proper
  algorithm.  By default, the command makes its effort to prove whether given
  ACTL formula is positive. To check whether the ACTL formula is negative, user
  should set the environment parameter <b>amc_prove_false</b> prior to
  executing the command.  See <a href="#environment">below</a> for the
  environment parameters associated with this command.  <p>

  Properties to be verified should be provided as ACTL formulas in the file
  <code>&lt;ctl_file&gt;</code>. The command only accepts ACTL formulas.
  Mixed, ECTL expressions are not supported.  
  ACTL formulas are those in which all quantifiers are universal and 
  negation is only allowed at the level of atomic propositions.
  For the precise syntax of CTL formulas, see the <a href="../ctl/ctl/ctl.html"> 
  VIS CTL and LTL syntax manual</a>.<p>

  The command is designed to tackle the state explosion problem we encounter
  when dealing with large and complex circuits. Based on the initial size of
  the group, the command constructs over- or under-approximation of the
  transition relation of the system. A group (subsystem) is a portion of
  the original circuit containing a subset of the latches and
  their next state functions.  The initial size of a group can be set with
  the <a href="#sizeofgroup">amc_sizeof_group</a> environment variable.
  These initial approximations may not contain every detail of the exact 
  system. However they may contain enough information to
  determine whether the formula is positive or negative.  Starting from an
  initial coarse approximation, the command makes its effort to prove whether
  given ACTL formula is positive or negative. When the procedure fails to prove
  correctness of the formula with initial approximations, it automatically
  refines the approximations. It repeats the process until the algorithm
  produces a reliable result or the available resources are exhausted.<p>

  Due to the overhead procedures, for some circuits, the exact <a
  href="model_checkCmd.html"><code>model_check</code> </a> method may evaluate
  formulas faster with less resources.  If any formula evaluates to
  <em>false</em>, a debug trace is reported.<p>

  The command does not use fairness constraints even if they have been read
  with the <a href="read_fairnessCmd.html"><code>read_fairness</code></a> 
  command. <p>

   
   <b>Command options: </b>
   <p>

   <dl>
   
   <dt><code> -h </code>
   <dd> Print the command usage.

   <p>
          
   <dt><code> -v  &lt;verbosity_level&gt; </code>
   <dd> Specify verbosity level. <code> verbosity_level</code> must be one of 
   the following:
   <p>

         <code> 0 </code> : No feedback provided. This is the default. <br>
         <code> 1 </code> : Some feedback. <br>
         <code> 2 </code> : Lots of feedback.
         <p>

   <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
   <dd> Specify the time out period (in seconds) after which the command
   aborts. By default this option is set to infinity.
   <p>
          
   <dt> <code> &lt;ctl_file&gt; </code>
   <dd> File containing ACTL formulas to be model checked.
   <p>

   </dl>

   <b><A NAME="environment">Environment Parameters:</A></b>
   <p>

        Environment parameters should be set using the set command
        from the VIS shell <br>
        (e.g. <code>vis\> set amc_prove_false</code>).

   <p>

   <dl>

   <dt> <b><code> amc_prove_false  </code></b>
   <br>
        When the parameter is set, the command makes its effort to prove
        whether given ACTL formula is negative. The command constructs a set of
        under-approximations of the transition relations of the system. When
        the formula evaluates to <em>false</em>, a debug trace is reported by
        default.  <p>

   <dt> <b><code> amc_grouping_method &lt;grouping method&gt; </code></b>
   <br>
        Specifies grouping method. Grouping method is a method for grouping 
        number of latches into single subsystem. Two methods are supported. 
   <p>
        <dd> <b>Grouping based on hierarchy<code>(default)</code></b> : The 
             method groups latches based on the hierarchy of the system. 
             Normally, complex circuits are designed in multiple
             processes. Furthermore, processes form a hierarchy.  The method
             uses this information provided by the original design.  When a
             design described in high level description language is transformed
             into low level BLIF format, the processes are transformed into
             subcircuits. The method groups those latches that are within same
             subcircuit.<p>

        <dd> <b>Grouping based on latch dependencies(latch_dependency)</b>: The 
             method groups those latches
             that are closely related. Closely related latches are those who has
             many (transitive) connections between them.
   <p>

        When the parameter is not specified, the command by default uses
        hierarchical grouping method.
   <p>

   <dt> <b><A NAME="sizeofgroup"><code> amc_sizeof_group &lt;integer value&gt; </code></A></b>
   <br>
        Determines the number of latches in each group(subsystem). The default
        value is 8. The initial size of the subsystem determines the initial
        degree of approximations of the transition relations. There's no proven
        rule of setting the value. Some experimental results show that setting
        the value to about 5-20% of overall number of latches is
        reasonable(e.g.  if the system contains 100 latches set the value to
        5-20).  However, the suggested range may not work well with some
        examples.  <p>
        
   <dt> <b><code> amc_DC_level &lt;integer value&gt; </code></b>
   <br>
        Specifies don't care levels. Default level is 0. Absence of the
        parameter sets the amc_DC_level to 0.
   <br>
          amc_DC_level must be one of the following:<p>
     <dl>
          <dt><code>0</code>: No don't cares are used. This is the default.<br>
          <dt><code>1</code>: Use unreachable states as don't cares. <br>
          <dt><code>2</code>: Aggressively use DC's to simplify MDD's in model 
          checking. <br>
     </dl>
   <p>

        Using don't cares may take more time for some examples since the
        approximate model checker computes the reachable states for each
        subsystem. For some large circuits it is undesirable to set don't care
        level.  <p>

  <dt> Related "set" options: <p>
  <dt> ctl_change_bracket &lt;yes/no&gt;
  <dd> Vl2mv automatically converts "\[\]" to "&lt;&gt;" in node names,
  therefore CTL parser does the same thing. However, in some cases a user
  does not want to change node names in CTL parsing. Then, use this set
  option by giving "no". Default is "yes".
  <p>

  <dt> See also commands : model_check, incremental_ctl_verification <p>

  </dl>

   <b>Examples:</b> <br>
   Here are some example sequences of the VIS executions using the approximate
   model checker.<br>
   <p>

   <code>
        read_blif_mv abp/abp.mv <br>
        flatten_hierarchy <br>
        static_order <br>
        build_partition_mdds <br>
        set amc_sizeof_group 4 <br>
        approximate_model_check abp/abpt.ctl <br>
        time <br>
        quit <br>
  <p>

        read_blif_mv coherence/coherence.mv <br>
        flatten_hierarchy <br>
        static_order <br>
        build_partition_mdds <br>
        set amc_sizeof_group 8 <br>
        set amc_prove_false <br>
        set amc_DC_level 0 <br>
        approximate_model_check coherence/coherence2.ctl <br>
        time <br>
        quit <br>
  <p>


  The algorithm used by approximate_model_check is described in detail in
  <a href="ftp://vlsi.colorado.edu/pub/iccad96.ps">
  ftp://vlsi.colorado.edu/pub/iccad96.ps</a>
  ]


  SideEffects []

******************************************************************************/
static int
CommandAmc(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  static int            timeOutPeriod;    /* CPU seconds allowed */
  char                  *ctlFileName;     /* Name of file containing formulas */
  FILE                  *ctlFile;         /* File to read the formulas from */
  Ntk_Network_t         *network;         /* Pointer to the current network */
  array_t               *ctlFormulaArray; /* Array of read ctl formulas */
  array_t               *ctlNormalForm;   /* Array of normal ctl formulas */
  Ctlp_Formula_t        *currentFormula;  /* Formula being verified */
  int                   c, i;
  Amc_VerbosityLevel    verbosity;        /* Verbosity level */

  long initialTime;
  long finalTime;


  /* Initialize Default Values */
  timeOutPeriod   = 0;
  ctlFileName     = NIL(char);
  verbosity       = Amc_VerbosityNone_c;

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "ht:v:")) != EOF) {
    switch(c) {
      case 'h':
        ApproximateModelCheckUsage();
        return 1;
      case 't':
        timeOutPeriod = atoi(util_optarg);
        break;
      case 'v':
        verbosity = (Amc_VerbosityLevel) atoi(util_optarg);
        break;
      default:
        ApproximateModelCheckUsage();
        return 1;
    }
  }

  /* Make sure the CTL file has been provided */
  if (argc == util_optind) {
    ApproximateModelCheckUsage();
    return 1;
  }
  else {
    ctlFileName = argv[util_optind];
  }

  /* 
   * Obtain the network from the hierarchy manager 
   */
  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }
  /*
   * Check whether the fairness was read.
   */
  {
    Fsm_Fsm_t      *exactFsm = Fsm_NetworkReadOrCreateFsm(network);
    Fsm_Fairness_t *fairCons =  Fsm_FsmReadFairnessConstraint(exactFsm);
    int numOfDisjuncts = Fsm_FairnessReadNumDisjuncts(fairCons);
    if (numOfDisjuncts > 1) {
      /* non-Buchi */
      fprintf(vis_stdout, "** amc warning: Fairness Constraint is not supported.\n");
    }
    else {
      int numOfConj     = Fsm_FairnessReadNumConjunctsOfDisjunct(fairCons, 0);
      if (numOfConj > 1) {
        /* Buchi */
        fprintf(vis_stdout, "** amc warning: Fairness Constraint is not supported.\n");
      }
    }
  } 

  /* 
   * Read in the array of CTL formulas provided in ctlFileName 
   */
  ctlFile = Cmd_FileOpen(ctlFileName, "r", NIL(char *), 0);
  if (ctlFile == NIL(FILE)) {
    return 1;
  }
  ctlFormulaArray = Ctlp_FileParseFormulaArray(ctlFile);
  fclose(ctlFile);

  if (ctlFormulaArray == NIL(array_t)) {
    (void) fprintf(vis_stderr, "** amc error: Error while parsing ctl formulas in file.\n");
    return 1;
  } 

  ctlNormalForm = Ctlp_FormulaArrayConvertToExistentialFormTree(ctlFormulaArray);

  /* 
   * Start the timer. 
   */
  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void (*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);

    /* The second time setjmp is called, it returns here !!*/
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stdout, "# AMC: timeout ocurred after %d seconds.\n",
                     timeOutPeriod);
      alarm(0);

      /* Note that there is a huge memory leak here. */
      Ctlp_FormulaArrayFree(ctlFormulaArray);
      Ctlp_FormulaArrayFree(ctlNormalForm);
      return 1;
    } 
  }


  /* 
   * Loop over every CTL formula in the array 
   */
  arrayForEachItem(Ctlp_Formula_t *, ctlNormalForm, i, currentFormula) {
    boolean validFormula;

    validFormula = FormulaTestIsForallQuantifier(currentFormula); 
    if (!validFormula) {
      fprintf(vis_stderr, "Formula ");
      Ctlp_FormulaPrint(vis_stderr, currentFormula);
      fprintf(vis_stderr, " is not a valid ACTL formula. Skipping it\n");
    }
    else if (!Mc_FormulaStaticSemanticCheckOnNetwork(currentFormula, network,
                                                     FALSE)) {
      (void) fprintf(vis_stdout, "\n** amc error: Error in parsing Atomic Formula:\n%s\n", error_string());
      error_init();
      Ctlp_FormulaFree( currentFormula );
      continue;
    }
    else {
      error_init();
      initialTime = util_cpu_time();
      Amc_AmcEvaluateFormula(network, currentFormula, verbosity);
      finalTime = util_cpu_time();
      if(verbosity == Amc_VerbosityVomit_c) {
        (void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =",
                       (finalTime - initialTime) / 1000);
      }
      fprintf(vis_stdout, "\n");
    }

  } /* End of arrayForEachItem in ctlFormulaArray */



  /* Deactivate the alarm */
  alarm(0);


  /* Clean up */
  Ctlp_FormulaArrayFree(ctlFormulaArray);
  Ctlp_FormulaArrayFree(ctlNormalForm);
  error_cleanup();


  /* normal exit */
  return 0;
}

/**Function********************************************************************

  Synopsis [Prints the usage of the approximate_model_checking command.]

  SideEffects        []

  SeeAlso            [CommandAmc]

******************************************************************************/
static void
ApproximateModelCheckUsage(void)
{
  (void) fprintf(vis_stderr, "usage: approximate_model_check [-h] ");
  (void) fprintf(vis_stderr, "[-t secs] [-v] ctlfile\n");
  (void) fprintf(vis_stderr, "   -h        print the command usage\n");
  (void) fprintf(vis_stderr, "   -t secs   Seconds allowed for computation\n");
  (void) fprintf(vis_stderr, "   -v number verbosity level\n");
  (void) fprintf(vis_stderr, "   ctlfile   File containing the ctl formulas\n");

  return;
} /* End of ApproximateModelCheckUsage */



/**Function********************************************************************

  Synopsis           [Tests recursively if a formula is a valid ACTL formula.]

  Description [This function implements the recursive steps needed for the
  function FormulaTestIsForallQuantifier.]

  SideEffects        []

  SeeAlso            [CommandAmc]

******************************************************************************/
boolean
FormulaTestIsForallQuantifier(
  Ctlp_Formula_t *formula)
{
  Ctlp_Formula_t    *newFormula;
  boolean           converted; 
  Ctlp_FormulaClass result;

  if (!Ctlp_FormulaTestIsConverted(formula)) {
    newFormula = Ctlp_FormulaConvertToExistentialForm(formula);
    converted = TRUE;
  }
  else {
    newFormula = formula;
    converted = FALSE;
  }

  result = Ctlp_CheckClassOfExistentialFormula(newFormula);

  if (converted) {
    Ctlp_FormulaFree(newFormula);
  } /* End of if */

  return result == Ctlp_ACTL_c || result == Ctlp_QuantifierFree_c;

} /* End of FormulaTestIsForallQuantifier */


/**Function********************************************************************

  Synopsis           [Handle the timeout signal.]

  Description [This function is called when the time out occurs. In principle
  it could do something smarter, but so far it just transfers control to the
  point in the code where setjmp was called.]

  SideEffects [This function gains control at any point in the middle of the
  computation, therefore the memory allocated so far leaks.]

******************************************************************************/
static void
TimeOutHandle(void)
{
  longjmp(timeOutEnv, 1);
} /* End of TimeOutHandle */