/****************************************************************************/
/*                                                                          */
/*                      Chaine de CAO & VLSI   Alliance                     */
/*                                                                          */
/*    Produit :  preuve formelle 				       	    */
/*    Fichier :  proof_util.c                                               */
/*                                                                          */
/*    (c) copyright 1991 Laboratoire MASI equipe CAO & VLSI                 */
/*    Tous droits reserves                                                  */
/*    Support : e-mail cao-vlsi@masi.ibp.fr                                 */
/*                                                                          */
/*    Auteur(s) :  L. Burgun                            le : 14/10/1991     */
/*                                                                          */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*                                                                          */
/****************************************************************************/

#include MUT_H
#include LOG_H
#include BEH_H
#include "proof.h"
#include "../compil/sl_util.h"

	/* attention a ce DEFINE si on l'utilise dans des if imbriques */

#define PRINT if (mode == 1) printf

/*-------------------------------------------------------------------------
verifIOBeh 	: verifie la coherence des interfaces des deux befig. 
---------------------------------------------------------------------------
retour		: le nombre d'erreurs trouvees.
---------------------------------------------------------------------------*/
int verifIOBeh(beh1,beh2,mode)
befig_list *beh1,*beh2;
int mode;
{
berin_list *in1,*in2;
beout_list *out1,*out2;
bebus_list *bus1,*bus2;
bebux_list *bux1,*bux2;
bereg_list *reg1,*reg2;
binode_list *binode1,*binode2;
int numberError=0;


in1 = beh1->BERIN;
while (in1) 		/* les sorties primaires */
   {
   in2 = beh2->BERIN;
   while (in2 && strcmp(in1->NAME,in2->NAME))
      {
      in2 = in2->NEXT;
      }
   if (in2 == NULL) 
      {
      PRINT("Primary input '%s' exists only in '%s'\n",in1->NAME,beh1->NAME);
      PRINT("\n");
      numberError++; 
      }
   in1 = in1->NEXT;
   }
in2 = beh2->BERIN;
while (in2)
   {
   in1 = beh1->BERIN;
   while (in1 && strcmp(in1->NAME,in2->NAME))
      {
      in1 = in1->NEXT;
      }
   if (in1 == NULL) 
      {
      PRINT("Primary input '%s' exists only in '%s'\n",in2->NAME,beh2->NAME);
      PRINT("\n");
      numberError++; 
      }
   in2 = in2->NEXT;
   }


out1 = beh1->BEOUT;
while (out1) 		/* les sorties primaires */
   {
   out2 = beh2->BEOUT;
   while (out2 && strcmp(out1->NAME,out2->NAME))
      {
      out2 = out2->NEXT;
      }
   if (out2 == NULL) 
      {
      PRINT("Primary output '%s' exists only in '%s'\n",out1->NAME,beh1->NAME);
      PRINT("\n");
      numberError++; 
      }
   out1 = out1->NEXT;
   }

out2 = beh2->BEOUT;
while (out2)
   {
   out1 = beh1->BEOUT;
   while (out1 && strcmp(out1->NAME,out2->NAME))
      {
      out1 = out1->NEXT;
      }
   if (out1 == NULL) 
      {
      PRINT("Primary output '%s' exists only in '%s'\n",out2->NAME,beh2->NAME);
      PRINT("\n");
      numberError++; 
      }
   out2 = out2->NEXT;
   }
      

bus1 = beh1->BEBUS;
while (bus1) 		/* les bus */
   {
   bus2 = beh2->BEBUS;
   while (bus2 && strcmp(bus1->NAME,bus2->NAME)) /* recherche du meme ident. */
      {
      bus2 = bus2->NEXT;
      }
   if (bus2 == NULL) 
      {
      PRINT("Bus '%s' exists only in '%s'\n",
              bus1->NAME,beh1->NAME);
      numberError++;
      }
   bus1 = bus1->NEXT;
   }

bus2 = beh2->BEBUS;
while (bus2)
   {
   bus1 = beh1->BEBUS;
   while (bus1 && strcmp(bus1->NAME,bus2->NAME)) /* recherche du meme ident. */
      {
      bus1 = bus1->NEXT;
      }
   if (bus1 == NULL) 
      {
      PRINT("Bus '%s' exists only in '%s'\n",bus2->NAME,beh2->NAME);
      PRINT("\n");
      numberError++;
      }
   bus2 = bus2->NEXT;
   }
      

bux1 = beh1->BEBUX;
while (bux1) 		/* les bux */
   {
   bux2 = beh2->BEBUX;
   while (bus2 && strcmp(bux1->NAME,bux2->NAME)) /* recherche du meme ident. */
      {
      bux2 = bux2->NEXT;
      }
   if (bux2 == NULL) 
      {
      PRINT("Bux '%s' exists only in '%s'\n",
              bux1->NAME,beh1->NAME);
      numberError++;
      }
   bux1 = bux1->NEXT;
   }

bux2 = beh2->BEBUX;
while (bux2)
   {
   bux1 = beh1->BEBUX;
   while (bux1 && strcmp(bux1->NAME,bux2->NAME)) /* recherche du meme ident. */
      {
      bux1 = bux1->NEXT;
      }
   if (bux1 == NULL) 
      {
      PRINT("Bux '%s' exists only in '%s'\n",bux2->NAME,beh2->NAME);
      PRINT("\n");
      numberError++;
      }
   bux2 = bux2->NEXT;
   }

reg1 = beh1->BEREG;
while (reg1) 		/* les registres */
   {
   reg2 = beh2->BEREG;
   while (reg2 && strcmp(reg1->NAME,reg2->NAME)) /* recherche du meme ident. */
      {
      reg2 = reg2->NEXT;
      }
   if (reg2 == NULL) 
      {
      PRINT("Register '%s' exists only in '%s'\n",
              reg1->NAME,beh1->NAME);
      numberError++;
      }
   reg1 = reg1->NEXT;
   }

reg2 = beh2->BEREG;
while (reg2)
   {
   reg1 = beh1->BEREG;
   while (reg1 && strcmp(reg1->NAME,reg2->NAME)) /* recherche du meme ident. */
      {
      reg1 = reg1->NEXT;
      }
   if (reg1 == NULL) 
      {
      PRINT("Register '%s' exists only in '%s'\n",reg2->NAME,beh2->NAME);
      PRINT("\n");
      numberError++;
      }
   reg2 = reg2->NEXT;
   }

return(numberError);
}


/*-------------------------------------------------------------------------
verifPNode 	: verifie la coherence le calcul des graphes 
---------------------------------------------------------------------------
retour		: 1 si OK, 0 sinon. 
---------------------------------------------------------------------------*/
int verifPNode(beh1,beh2,mode)
befig_list *beh1,*beh2;
int mode;
{
beout_list *out;
beaux_list *aux;
bebus_list *bus;
bebux_list *bux;
bereg_list *reg;
binode_list *binode;


aux = beh1->BEAUX;
while (aux)
   {
   if (aux->NODE == NULL)
      {
      PRINT("Fatal error : auxiliary signal '%s' have no BDD in '%s'\n",
            aux->NAME,beh1->NAME);
      PRINT("\n");
      return(0);
      }
   aux = aux->NEXT;
   }

aux = beh2->BEAUX;
while (aux)
   {
   if (aux->NODE == NULL)
      {
      PRINT("Fatal error : auxiliary signal '%s' have no BDD in '%s'\n",
            aux->NAME,beh2->NAME);
      PRINT("\n");
      return(0);
      }
   aux = aux->NEXT;
   }

out = beh1->BEOUT;
while (out) 		/* les sorties primaires */
   {
   if (out->NODE == NULL)
      {
      PRINT("Fatal error : output signal '%s' have no BDD in '%s'\n",
            out->NAME,beh1->NAME);
      PRINT("\n");
      return(0);
      }
   out = out->NEXT;
   }
      
out = beh2->BEOUT;
while (out) 		/* les sorties primaires */
   {
   if (out->NODE == NULL)
      {
      PRINT("Fatal error : output signal '%s' have no BDD in '%s'\n",
            out->NAME,beh2->NAME);
      PRINT("\n");
      return(0);
      }
   out = out->NEXT;
   }

bux = beh1->BEBUX;
while (bux) 		/* les bux */
   {
   binode = bux->BINODE;
   if (binode->CNDNODE == NULL || binode->VALNODE == NULL)
      {
      PRINT("Fatal error : bux signal '%s' have no BDD in '%s'\n",
            bux->NAME,beh1->NAME);
      PRINT("\n");
      return(0);
      }
   bux = bux->NEXT;
   }

bux = beh2->BEBUX;
while (bux) 		/* les bux */
   {
   binode = bux->BINODE;
   if (binode->CNDNODE == NULL || binode->VALNODE == NULL)
      {
      PRINT("Fatal error : bux signal '%s' have no BDD in '%s'\n",
            bux->NAME,beh2->NAME);
      PRINT("\n");
      return(0);
      }
   bux = bux->NEXT;
   }

bus = beh1->BEBUS;
while (bus) 		/* les bus */
   {
   binode = bus->BINODE;
   if (binode->CNDNODE == NULL || binode->VALNODE == NULL)
      {
      PRINT("Fatal error : bus signal '%s' have no BDD in '%s'\n",
            bus->NAME,beh1->NAME);
      PRINT("\n");
      return(0);
      }
   bus = bus->NEXT;
   }

bus = beh2->BEBUS;
while (bus) 		/* les bus */
   {
   binode = bus->BINODE;
   if (binode->CNDNODE == NULL || binode->VALNODE == NULL)
      {
      PRINT("Fatal error : bus signal '%s' have no BDD in '%s'\n",
            bus->NAME,beh2->NAME);
      PRINT("\n");
      return(0);
      }
   bus = bus->NEXT;
   }

reg = beh1->BEREG;
while (reg)
   {
   binode = reg->BINODE;
   if (binode->CNDNODE == NULL || binode->VALNODE == NULL)
      {
      PRINT("Fatal error : bus signal '%s' have no BDD in '%s'\n",
            reg->NAME,beh1->NAME);
      PRINT("\n");
      return(0);
      }
   reg = reg->NEXT;
   }

reg = beh2->BEREG;
while (reg)
   {
   binode = reg->BINODE;
   if (binode->CNDNODE == NULL || binode->VALNODE == NULL)
      {
      PRINT("Fatal error : bus signal '%s' have no BDD in '%s'\n",
            reg->NAME,beh2->NAME);
      PRINT("\n");
      return(0);
      }
   reg = reg->NEXT;
   }

return(1);
}

/*-------------------------------------------------------------------------
sumBinode 	: calcule la FND (ON-set) d'un bus
---------------------------------------------------------------------------
retour		:un pNode. 
---------------------------------------------------------------------------*/
pNode sumBinode(binode)
binode_list *binode;
{
pNode res = zero;
while (binode)
   {
   res = applyBinBdd(OR,applyBinBdd(AND,binode->VALNODE,binode->CNDNODE),res); 
   binode = binode->NEXT;
   }
return res;
}

/*-------------------------------------------------------------------------
sumBiabl 	: calcule la FND  en ABL (ON-set) d'un bus
---------------------------------------------------------------------------
retour		:un chain_list *. 
---------------------------------------------------------------------------*/
chain_list *sumBiabl(biabl)
biabl_list *biabl;
{
chain_list *res = createAtom("'0'");

while (biabl)
   {
   res = OR2(AND2(copyExpr(biabl->VALABL),copyExpr(biabl->CNDABL)),res); 
   biabl = biabl->NEXT;
   }
flatArityExpr(res);
return res;
}

/*-------------------------------------------------------------------------
sumCNDBinode 	: calcule la somme des commandes d'un bus
---------------------------------------------------------------------------
retour		:un pNode. 
---------------------------------------------------------------------------*/
pNode sumCNDBinode(binode)
binode_list *binode;
{
pNode res = zero;
while (binode)
   {
   res = applyBinBdd(OR,binode->CNDNODE,res); 
   binode = binode->NEXT;
   }
return res;
}

/*-------------------------------------------------------------------------
busOnToBddBeh 	: calcule le ON-set d'un bus 
---------------------------------------------------------------------------
retour		:un pNode. 
---------------------------------------------------------------------------*/
pNode busOnToBddBeh(beh,name)
befig_list *beh;
char *name;
{
bebus_list *bus = beh->BEBUS;
binode_list *binode;
pNode res;

while (bus && strcmp(bus->NAME,name))
   bus = bus->NEXT;

if (bus == NULL)
   {
   printf("error : busOnToBdd %s doesn't exist as a bus in %s\n",
 	  name,beh->NAME);
   exit(-1);
   }

res = zero;
binode = bus->BINODE;
while (binode)
  {
  res = applyBinBdd(OR,applyBinBdd(AND,binode->VALNODE,binode->CNDNODE),res); 
  binode = binode->NEXT;
  }
return(res);
}

/*-------------------------------------------------------------------------
buxOnToBddBeh 	: calcule le ON-set d'un bux 
---------------------------------------------------------------------------
retour		:un pNode. 
---------------------------------------------------------------------------*/
pNode buxOnToBddBeh(beh,name)
befig_list *beh;
char *name;
{
bebux_list *bux = beh->BEBUX;
binode_list *binode;
pNode res;

while (bux && strcmp(bux->NAME,name))
   bux = bux->NEXT;

if (bux == NULL)
   {
   printf("error : buxOnToBdd %s doesn't exist as a bux in %s\n",
 	  name,beh->NAME);
   exit(-1);
   }

res = zero;
binode = bux->BINODE;
while (binode)
  {
  res = applyBinBdd(OR,applyBinBdd(AND,binode->VALNODE,binode->CNDNODE),res); 
  binode = binode->NEXT;
  }
return(res);
}


/*-------------------------------------------------------------------------
displayDiff 	: affiche si possible les equations differentes
	          que l'on a trouve dans chaque description. 
---------------------------------------------------------------------------
retour		: rien.
---------------------------------------------------------------------------*/
void displayDiff(pt1,pt2,beh1,beh2,mode)
pNode pt1,pt2;
befig_list *beh1,*beh2;
int mode;
{
if (pt1 == NULL || pt2 == NULL)
   {
   printf("displayDiff : bad args - pNode = NULL\n");
   exit(-1);
   }
else
   {
   PRINT("         Description %s :\n",beh1->NAME);
   if (numberAtomFact(pt1)>50)
      {
      PRINT("         Logical expression too big...impossible display!\n");
      }
   else
      {
      if (mode == 1)
         {
         printf("      ");
         displayExpr(bdd2Abl(pt1,(beh1->CIRCUI)->pNameI));
         }
      }
   PRINT("\n");
   PRINT("        Description %s :\n",beh2->NAME);
   if (numberAtomFact(pt2)>50)
      {
      PRINT("         Logical expression too big...impossible display!\n");
      }
   else
      {
      if (mode == 1)
         {
         printf("      ");
         displayExpr(bdd2Abl(pt2,(beh2->CIRCUI)->pNameI));
         }
      }
   PRINT("\n");
   }
}

/*-------------------------------------------------------------------------
proofBeh 	: Effectue une preuve formelle entre deux comportements. 
		  mode a 1 ==> affichage a l'ecran des erreurs.
 	          Tous les graphes doivent au prealable avoir ete calcule
	          dans les deux descriptions.
		  si exitIO est a 0, on ne sort pas si il existe une
                  difference dans l'interface.
---------------------------------------------------------------------------
retour		: le nombre d'erreurs trouvees.
---------------------------------------------------------------------------*/
int proofBeh(beh1,beh2,mode,exitIO)
befig_list *beh1,*beh2;
int mode,exitIO;
{
beout_list *out1,*out2;
beaux_list *aux1,*aux2;
bebus_list *bus1,*bus2;
bebux_list *bux1,*bux2;
bereg_list *reg1,*reg2;
binode_list *binode1,*binode2;
biabl_list *biabl1,*biabl2;
int numberError=0;

if (mode == 1)
   pTabExpr = createTH(10000);

PRINT("--------------------------------------------------------------------------------\n");
if (mode == 1)
PRINT("             Formal proof with Ordered Binary Decision Diagrams between   \n\n");
PRINT("             '%s'  and  '%s'\n",beh1->NAME,beh2->NAME);
PRINT("--------------------------------------------------------------------------------\n");
numberError = verifIOBeh(beh1,beh2,mode);
if (numberError > 0 && exitIO)
   {
   PRINT("Fatal error : IO or/and register declaration differs\n");
   PRINT("--------------------------------------------------------------------------------\n");
   return(numberError);
   }
if (verifPNode(beh1,beh2,mode) == 0)
   {
   PRINT("Warning : some OUT,AUX,REG or BUS have no expression  \n");
   }
PRINT("==============================  PRIMARY OUTPUT  ===============================\n");
out1 = beh1->BEOUT;
while (out1) 		/* les sorties primaires */
   {
   out2 = beh2->BEOUT;
   while (out2 && strcmp(out1->NAME,out2->NAME))
      {
      out2 = out2->NEXT;
      }
   if (out2) 
      {
      if (out1->NODE != out2->NODE)
         {
         PRINT("Error : Behaviour of primary output '%s' differs in the two descriptions\n",
                out1->NAME); 
         displayDiff(out1->NODE,out2->NODE,beh1,beh2,mode);
         PRINT("\n");
         numberError++;
         }
      }
   out1 = out1->NEXT;
   }

PRINT("=============================  AUXILIARY SIGNAL  ==============================\n");
aux1 = beh1->BEAUX;
while (aux1) 		/* les auxiliaires */
   {
   aux2 = beh2->BEAUX;
   while (aux2 && strcmp(aux1->NAME,aux2->NAME))
      {
      aux2 = aux2->NEXT;
      }
   if (aux2) 
      {
      if (aux1->NODE != aux2->NODE)
         {
         PRINT("Warning : Behaviour of auxiliary signal '%s' differs in the two descriptions\n",
                aux1->NAME); 
         displayDiff(aux1->NODE,aux2->NODE,beh1,beh2,mode);
         PRINT("\n");
         }
      }
   aux1 = aux1->NEXT;
   }


PRINT("===============================  EXTERNAL BUS =================================\n");
bus1 = beh1->BEBUS;
while (bus1) 		/* les bus */
   {
   bus2 = beh2->BEBUS;
   while (bus2 && strcmp(bus1->NAME,bus2->NAME)) /* recherche du meme ident. */
      {
      bus2 = bus2->NEXT;
      }
   if (bus2) 
      {
			/* difference fonctionnelle */

      if (busOnToBddBeh(beh1,bus1->NAME) != busOnToBddBeh(beh2,bus2->NAME))
   	 {
         binode1 = bus1->BINODE;
         while (binode1)	/* preuve sur les commandes et les valeurs */
            {
            binode2 = bus2->BINODE;   /* recherche de la meme commande */
            while (binode2 && (binode1->CNDNODE != binode2->CNDNODE))
               {
               binode2 = binode2->NEXT;
               }
            if (binode2)
               {
               if (binode1->VALNODE != binode2->VALNODE)
                  {
                  PRINT("Error : Behaviour of bus '%s' differs in the two descriptions\n",
                          bus1->NAME); 
                  PRINT("        ---> Value differs for the command =\n");
                  if (mode == 1)
                     displayExpr(bdd2Abl(binode1->CNDNODE,(beh1->CIRCUI)->pNameI));
                  PRINT("\n");
                  displayDiff(binode1->VALNODE,binode2->VALNODE,beh1,beh2,mode);
                  PRINT("\n");
                  numberError++;
                  }
               }
            else
               {
               PRINT("Error : Bus '%s' differs in the two descriptions\n",
                       bus1->NAME); 
               PRINT("        ---> Driver exist only in %s for the command  =\n",
                       beh1->NAME);
               if (mode == 1)
                  displayExpr(bdd2Abl(binode1->CNDNODE,(beh1->CIRCUI)->pNameI));
               PRINT("\n\n");
               numberError++;
               }
            binode1 = binode1->NEXT;
            }
         binode2 = bus2->BINODE;
         while (binode2)
            {
     	    binode1 = bus1->BINODE;
      	    while (binode1 && (binode1->CNDNODE != binode2->CNDNODE))
               binode1 = binode1->NEXT;
	
            if (binode1 == NULL)
               {
               PRINT("Error : Bus '%s' differs in the two descriptions\n",
                       bus2->NAME); 
               PRINT("        ---> Driver exist only in %s for the command  = \n",
                       beh2->NAME);
               if (mode == 1)
                  displayExpr(bdd2Abl(binode2->CNDNODE,(beh2->CIRCUI)->pNameI));
               PRINT("\n\n");
               numberError++;
               }
            binode2 = binode2->NEXT;
            }
         }
      }
   bus1 = bus1->NEXT;
   }


PRINT("================================ INTERNAL BUS =================================\n");
bux1 = beh1->BEBUX;
while (bux1) 		/* les bux */
   {
   bux2 = beh2->BEBUX;
   while (bux2 && strcmp(bux1->NAME,bux2->NAME)) /* recherche du meme ident. */
      {
      bux2 = bux2->NEXT;
      }
   if (bux2) 
      {
			/* difference fonctionnelle */

      if (buxOnToBddBeh(beh1,bux1->NAME) != buxOnToBddBeh(beh2,bux2->NAME))
   	 {
         binode1 = bux1->BINODE;
         while (binode1)	/* preuve sur les commandes et les valeurs */
            {
            binode2 = bux2->BINODE;   /* recherche de la meme commande */
            while (binode2 && (binode1->CNDNODE != binode2->CNDNODE))
               {
               binode2 = binode2->NEXT;
               }
            if (binode2)
               {
               if (binode1->VALNODE != binode2->VALNODE)
                  {
                  PRINT("Error : Behaviour of bus '%s' differs in the two descriptions\n",
                          bux1->NAME); 
                  PRINT("        ---> Value differs for the command =\n");
                  if (mode == 1)
                     displayExpr(bdd2Abl(binode1->CNDNODE,(beh1->CIRCUI)->pNameI));
                  PRINT("\n");
                  displayDiff(binode1->VALNODE,binode2->VALNODE,beh1,beh2,mode);
                  PRINT("\n");
                  numberError++;
                  }
               }
            else
               {
               PRINT("Error : Bus '%s' differs in the two descriptions\n",
                       bux1->NAME); 
               PRINT("        ---> Driver exist only in %s for the command  =\n",
                       beh1->NAME);
               if (mode == 1)
                  displayExpr(bdd2Abl(binode1->CNDNODE,(beh1->CIRCUI)->pNameI));
               PRINT("\n\n");
               numberError++;
               }
            binode1 = binode1->NEXT;
            }
         binode2 = bux2->BINODE;
         while (binode2)
            {
     	    binode1 = bux1->BINODE;
      	    while (binode1 && (binode1->CNDNODE != binode2->CNDNODE))
               binode1 = binode1->NEXT;
	
            if (binode1 == NULL)
               {
               PRINT("Error : Bus '%s' differs in the two descriptions\n",
                       bux2->NAME); 
               PRINT("        ---> Driver exist only in %s for the command  = \n",
                       beh2->NAME);
               if (mode == 1)
                  displayExpr(bdd2Abl(binode2->CNDNODE,(beh2->CIRCUI)->pNameI));
               PRINT("\n\n");
               numberError++;
               }
            binode2 = binode2->NEXT;
            }
         }
      }
   bux1 = bux1->NEXT;
   }

PRINT("==============================  REGISTER SIGNAL  ===============================\n");
reg1 = beh1->BEREG;
while (reg1) 		/* les registres */
   {
   reg2 = beh2->BEREG;
   while (reg2 && strcmp(reg1->NAME,reg2->NAME)) /* recherche du meme ident. */
      {
      reg2 = reg2->NEXT;
      }
   if (reg2) 
      {
      binode1 = reg1->BINODE;
      biabl1 = reg1->BIABL;
      while (binode1)		   /* preuve sur les commandes et les valeurs */
         {
         binode2 = reg2->BINODE;   /* recherche de la meme commande */
         biabl2 = reg2->BIABL; 
         while (binode2 && (binode1->CNDNODE != binode2->CNDNODE))
            {
            binode2 = binode2->NEXT;
            biabl2 = biabl2->NEXT;
            }
         if (binode2)
            {
            if (binode1->VALNODE != binode2->VALNODE)
               {
               PRINT("error : behaviour of register '%s' differs in the two descriptions\n",
                       reg1->NAME); 
               PRINT("        ---> Value differs for the command =\n");
               if (mode == 1)
                  displayExpr(bdd2Abl(binode1->CNDNODE,(beh1->CIRCUI)->pNameI));
               PRINT("\n");
               displayDiff(binode1->VALNODE,binode2->VALNODE,beh1,beh2,mode);
               PRINT("\n");
               numberError++;
               }

				/* bascule D ou latche */

            if ((biabl1->USER == 0 && biabl2->USER) ||
                (biabl2->USER == 0 && biabl1->USER))
               {
               PRINT("        ---> type of the register differs for the command =\n");
               if (mode == 1)
                  displayExpr(bdd2Abl(binode1->CNDNODE,(beh1->CIRCUI)->pNameI));

               if (biabl1->USER)
                  {
                  PRINT("        %s is a latch in %s but is an edge triggered in %s\n",
                        reg2->NAME,beh2->NAME,beh1->NAME);
                  }
               else
                  {
                  PRINT("        %s is a latch in %s but is an edge triggered in %s\n",
                        reg1->NAME,beh1->NAME,beh2->NAME);
                  }
               numberError++;
               }
            }
         else
            {
            PRINT("Error : Register '%s' differs in the two descriptions\n",
                    reg1->NAME); 
            PRINT("        ---> Driver exist only in %s for the command  =\n",
                    beh1->NAME);
            if (mode == 1)
               displayExpr(bdd2Abl(binode1->CNDNODE,(beh1->CIRCUI)->pNameI));
            PRINT("\n\n");
            numberError++;
            }
         binode1 = binode1->NEXT;
         biabl1 = biabl1->NEXT;
         }

      binode2 = reg2->BINODE;
      while (binode2)
         {
     	 binode1 = reg1->BINODE;
	 while (binode1 && (binode1->CNDNODE != binode2->CNDNODE))
            {
            binode1 = binode1->NEXT;
            }

         if (binode1 == NULL)
            {
            PRINT("Error : Register '%s' differs in the two descriptions\n",
                    reg2->NAME); 
            PRINT("        ---> Driver exist only in %s for the command  = \n",
                    beh2->NAME);
            if (mode == 1)
               displayExpr(bdd2Abl(binode2->CNDNODE,(beh2->CIRCUI)->pNameI));
            PRINT("\n\n");
            numberError++;
            }
         binode2 = binode2->NEXT;
         }
      }
   reg1 = reg1->NEXT;
   }

      
PRINT("\n                            Formal Proof : ");
if (numberError > 0) 
   {
   PRINT("%d error%s detected\n\n",numberError,(numberError > 1)?"s":"");
   }
else
   PRINT("OK\n\n");
PRINT("pppppppppppppppppppppppprrrrrrrrrrrrooooooooooooooooooooooooooooofffffffffffffff\n");
PRINT("--------------------------------------------------------------------------------\n");
if (mode == 1)
   destroyTH(pTabExpr);

return(numberError);
}
