/**CHeaderFile*****************************************************************

  FileName    [eqv.h]

  PackageName [eqv]

  Synopsis    [Provides commands for doing combinational and sequential
  verification on two networks.]

  Description [The eqv package provides two commands - comb_verify and
  seq_verify for doing combinational and sequential verification respectively.
  Two networks along with options for partitioning and ordering form the input
  to the commands.<p>

  Combinational verification : Two sets of distinguished nodes, roots and
  leaves, are specified for each network. The leaves should form a complete
  support for the roots in both networks. The correspondence between the roots
  and leaves of the two networks can be specified in an input file. The format
  of the input file is as follows-<p>

  .roots<p>
  &lt;name1&gt; &lt;name2&gt;<p>
  .<p>
  .<p>
  .leaves<p>
  &lt;name1&gt; &lt;name2&gt;
  .<p>
  .<p>
  Here, name1 is a node name in the first network and name2 a node name in the
  second network.<p>

  If no input file is given, the combinational outputs are assumed to be roots
  and the combinational inputs are assumed to be leaves. comb_verify checks
  for each pair of corresponding roots whether the two are equivalent as
  logical functions of corresponding leaf variables. This is done by
  constructing BDD's for the roots in terms of the leaf variables. For each
  pair in which the two roots are not equivalent, a minterm where they are not
  equal is written out. Note that pseudo inputs are treated no differently
  from any other inputs.<p> 

  Sequential verification : Two inputs and an option for partitioning form the
  input for this command. A set of distinguished nodes called roots is
  specified for each network. The correspondence between the two sets can be
  specified in an input file as described above. If no input file is given,
  the primary outputs are assumed to be roots. seq_verify checks for each
  pair of corresponding roots whether the two roots have different values in a
  reachable state of the product machine of the networks for any input. For
  each pair that this happens, an error trace is written out.<p>

  The method used in sequential verification i.e. product machine cannot handle
  non-determinism. Therefore, the two networks shouldn't have any pseudo
  inputs.]

  SeeAlso     [ntk.h]

  Author      [Shaz Qadeer]

  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
  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.

  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

  Revision    [$Id: eqv.h,v 1.6 2002/09/08 23:28:36 fabio Exp $]

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

#ifndef _EQV
#define _EQV

#include "fsm.h"
#include "ord.h"
#include "io.h"

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


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/
typedef void (*OFT) (Ntk_Network_t *, Ntk_Network_t *, st_table *);

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


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


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


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

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

EXTERN void Eqv_Init(void);
EXTERN void Eqv_End(void);
EXTERN boolean Eqv_NetworkVerifyCombinationalEquivalence(Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *leavesMap, st_table *rootsMap, OFT AssignCommonOrder, Part_PartitionMethod method1, Part_PartitionMethod method2);
EXTERN boolean Eqv_NetworkVerifySequentialEquivalence(Ntk_Network_t *network1, Ntk_Network_t *network2, st_table *rootsTable, st_table *leavesTable, Part_PartitionMethod partMethod, boolean useBackwardReach, boolean reordering);

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

#endif /* _EQV */