/****************************************************************************/
/*                                                                          */
/*                      Chaine de CAO & VLSI   Alliance                     */
/*                                                                          */
/*    Produit :  preuve formelle 				       	    */
/*    Fichier :  proof.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 : 09/08/1991     */
/*                                                                          */
/*    Modifie par :                                     le : 13/11/1991     */
/*    Modifie par :                                     le : ../../....     */
/*    Modifie par :                                     le : ../../....     */
/*                                                                          */
/****************************************************************************/

#include <stdio.h>
#include MUT_H
#include LOG_H
#include BEH_H
#include "../compil/lax_param.h"
#include "../synthe/sl_type.h"
#include "../compil/sl_util.h"
#include "../synthe/sl_system.h"
#include "../bddorder/bdd_order.h"
#include "proof.h"

		/* on ne verifie pas si les fichiers existent ...*/

#define VERIFILE 0

/*----------------------------------------------------------------------------
verifArgsProof	: verifie les arguments de la ligne de commande.
------------------------------------------------------------------------------
retour		: un entier a 1 si OK, 1 sinon.
------------------------------------------------------------------------------*/

int verifArgsProof(argc,argv)
int argc;
char *argv[];
{
FILE *fic;
FILE *fopen();

if (argc < 3  || argc > 6)
   {
   printf("\n");
   printf("proof 2.00   \nusage  :   proof -option");
   printf(" <file_entity1> <file_entity2> \n");
   printf("option :  -d   display the logical functions\n");
   printf("          -a   the common auxiliary signals are saved\n");
   printf("          -p   the polarity of the edge triggered is changed within the first description\n");
   return(0) ;
   }
if (argc > 3)
   {
   if(strcmp(argv[1],"-d") && strcmp(argv[1],"-a") && strcmp(argv[1],"-p"))
   	{
	printf("\nproof 2.00    : unknown option '%s'\n\n",argv[1]) ;
	return(0) ;
	}
   }
if (argc > 4)
   {
   if(strcmp(argv[2],"-d") && strcmp(argv[2],"-a") && strcmp(argv[2],"-p"))
   	{
	printf("\nproof 2.00    : unknown option '%s'\n\n",argv[2]) ;
	return(0) ;
	}
   }
if (argc > 5)
   {
   if(strcmp(argv[3],"-d") && strcmp(argv[3],"-a") && strcmp(argv[3],"-p"))
   	{
	printf("\nproof 2.00    : unknown option '%s'\n\n",argv[2]) ;
	return(0) ;
	}
   }
if (VERIFILE)
   {
   if(!(fic = fopen(genNAME("%s",argv[argc-2]),"r")))
	{
	printf("\nproof 2.00    : unable to open '%s'\n\n",argv[argc-2]) ;
	return(0) ;
	}
   if(!(fic = fopen(genNAME("%s",argv[argc-1]),"r")))
	{
	printf("\nproof 2.00    : unable to open '%s'\n\n",argv[argc-1]) ;
	return(0) ;
	}
   }
return(1);
}

	/* recherche d'une expression a partir d'un nom de sortie */

chain_list *searchExprOutBeh(beh,name)
befig_list *beh;
char *name;
{
beout_list *out = beh->BEOUT;

while (out)
   {
   if (!strcmp(out->NAME,name))
      return (out->ABL);
   out = out->NEXT;
   }
return ((chain_list *) NULL);
}


/*------------------------------------------------------------------------
substExprBeh : substitue dans toutes les expressions de 'beh'
               'name' par 'expr' 
--------------------------------------------------------------------------
retour       : rien
--------------------------------------------------------------------------*/
void substExprBeh(beh,name,sexpr)
befig_list *beh;
char *name;
chain_list *sexpr;
{
beout_list *out;
bereg_list *reg;
bebus_list *bus;
bebux_list *bux;
biabl_list *biabl;
beaux_list *aux;
chain_list *expr;


aux = beh->BEAUX;
while (aux)
   {
   if (aux->ABL)
      {
      expr = substExpr(aux->ABL,name,sexpr);
      freeExpr(aux->ABL);
      aux->ABL = expr;
      }
   aux = aux->NEXT;
   }
 
out = beh->BEOUT;
while (out)
   {
   if (out->ABL)
      {
      expr = substExpr(out->ABL,name,sexpr);
      freeExpr(out->ABL);
      out->ABL = expr;
      }
   out = out->NEXT;
   }
 
reg = beh->BEREG;
while (reg)
   {
   biabl = reg->BIABL;
   while (biabl)
      {
      if (biabl->CNDABL && biabl->VALABL)
         {
         expr = substExpr(biabl->CNDABL,name,sexpr);
         freeExpr(biabl->CNDABL);
         biabl->CNDABL = expr;

         expr = substExpr(biabl->VALABL,name,sexpr);
         freeExpr(biabl->VALABL);
         biabl->VALABL = expr;
         }
      biabl = biabl->NEXT;
      }
   reg = reg->NEXT;
   }
 
bus = beh->BEBUS;
while (bus)
   {
   biabl = bus->BIABL;
   while (biabl)
      {
      if (biabl->CNDABL && biabl->VALABL)
         {
         expr = substExpr(biabl->CNDABL,name,sexpr);
         freeExpr(biabl->CNDABL);
         biabl->CNDABL = expr;

         expr = substExpr(biabl->VALABL,name,sexpr);
         freeExpr(biabl->VALABL);
         biabl->VALABL = expr;
         }
      biabl = biabl->NEXT;
      }
   bus = bus->NEXT;
   }
 
bux = beh->BEBUX;
while (bux)
   {
   biabl = bux->BIABL;
   while (biabl)
      {
      if (biabl->CNDABL && biabl->VALABL)
         {
         expr = substExpr(biabl->CNDABL,name,sexpr);
         freeExpr(biabl->CNDABL);
         biabl->CNDABL = expr;

         expr = substExpr(biabl->VALABL,name,sexpr);
         freeExpr(biabl->VALABL);
         biabl->VALABL = expr;
         }
      biabl = biabl->NEXT;
      }
   bux = bux->NEXT;
   }
}

/*------------------------------------------------------------------------
polarBDBeh : inverse la polarite des BD d'une befig 
--------------------------------------------------------------------------
retour       : rien
--------------------------------------------------------------------------*/
void polarBDBeh(beh)
befig_list *beh;
{
bereg_list *reg;
biabl_list *biabl;

	/* inversion de polarite des cones DATA des BD */

reg = beh->BEREG;
while (reg)
   {
   int BD = 0;

   biabl = reg->BIABL;
   while (biabl)
      {
      if (biabl->USER)  /* BD detectee */
         {
         BD = 1;
			/* inversion de polarite */

         biabl->VALABL = notExpr(biabl->VALABL);
         }
      biabl = biabl->NEXT;
      }

   if (BD)
      substExprBeh(beh,reg->NAME,notExpr(createAtom(reg->NAME)));

   reg = reg->NEXT;
   }
}

/*------------------------------------------------------------------------
elimInoutBeh : patch qui permet de voir un inout comme un out
--------------------------------------------------------------------------
retour       : rien
--------------------------------------------------------------------------*/
void elimInoutBeh(beh)
befig_list *beh;
{
bepor_list *port;
chain_list *expr;

		/* recherche des INOUT qui ne sont pas des bus */

port = beh->BEPOR;
while (port)
   {
   if (port->DIRECTION == 'B' && port->TYPE == 'B')
      {
      printf("WARNING : %s is considered as an output signal\n",port->NAME);

		/* on recherche l'expression associee */

      expr = searchExprOutBeh(beh,port->NAME);
      if (expr == NULL)
         {
         printf("elimInoutSignal : error signal hasn't expression\n");
         exit(-1);
         }
      beh->BEAUX = beh_addbeaux(beh->BEAUX,port->NAME,expr,NULL);

		/* elimination de la liste des BERIN */

      beh->BERIN = beh_rmvberin(beh->BERIN,port->NAME);
      }
   port = port->NEXT;
   }
}

/*------------------------------------------------------------------------
elimBusMuxBeh : transformation des bus mutiplex en mutiplex combinatoire 
                il est necessaire d'avoir deja calculer les BDD
--------------------------------------------------------------------------
retour        : 1 si un bus a ete transforme, 0 sinon
--------------------------------------------------------------------------*/
int elimBusMuxBeh(beh)
befig_list *beh;
{
bebus_list *bus;
bebux_list *bux;
beaux_list *aux;
biabl_list *biabl;
binode_list *binode;
chain_list *delBus = NULL;
int retour = 0;


bus = beh->BEBUS;
while (bus)
   {
   if (sumCNDBinode(bus->BINODE) == one)
      {
      delBus = addchain(delBus,bus);
      beh->BEOUT = beh_addbeout(beh->BEOUT,bus->NAME,
                                sumBiabl(bus->BIABL),NULL);

      retour = 1;
      }
   bus = bus->NEXT;
   } 

while (delBus)
   {
   beh->BEBUS = beh_delbebus(beh->BEBUS,(bebus_list *)(delBus->DATA),'Y');
   delBus = delBus->NEXT;
   }

delBus = NULL;

bux = beh->BEBUX;
while (bux)
   {
   if (sumCNDBinode(bux->BINODE) == one)
      {
      delBus = addchain(delBus,bux);
      beh->BEAUX = beh_addbeaux(beh->BEAUX,bux->NAME,
                                sumBiabl(bux->BIABL),NULL);

		/* pour les bus internes (points d'arret) 
                   on elimine leur occurence dans BERIN */

      beh->BERIN = beh_rmvberin(beh->BERIN,bux->NAME);
      retour = 1;
      }
   bux = bux->NEXT;
   } 

while (delBus)
   {
   beh->BEBUX = beh_delbebux(beh->BEBUX,(bebux_list *)(delBus->DATA),'Y');
   delBus = delBus->NEXT;
   }

return retour;
}

/*------------------------------------------------------------------------
orderProofBeh      : calcul d'un ordonnancement pour 2 circuits 
--------------------------------------------------------------------------
retour        : 1 si un bus a ete transforme, 0 sinon
--------------------------------------------------------------------------*/
void orderProofBeh(bef1,bef2,argv,argc)
befig_list *bef1,*bef2;
char *argv[];
int argc;
{
chain_list *order;
chain_list *ptChain;
beaux_list *aux;
int vhb_reorder = 2;
chain_list *makeOrderAbl();

order = makeOrderAbl(bef1,1,1);

videBddBefig(bef1);
videBddBefig(bef2);

                /* creation des bdd */
 
bef1->CIRCUI =  initializeCct(bef1->NAME,5*countInputBeh(bef1),100);
bef2->CIRCUI =  initializeCct(bef2->NAME,5*countInputBeh(bef2),100);
 

ptChain = order;
while (ptChain)
   {
   addInputCct(bef1->CIRCUI,ptChain->DATA);
   ptChain = ptChain->NEXT ;
   }
 
		/* recherche des auxiliaires communs */

if(!strcmp(argv[1],"-a") || !strcmp(argv[2],"-a") || 
   (argc > 4 && !strcmp(argv[3],"-a")))
   {
   aux = bef1->BEAUX;
   printf("Looking for the common auxiliary signals :\n");
   while (aux)
      {
      if (existAuxBeh(bef2,aux->NAME))
         {
         addInputCct(bef1->CIRCUI,aux->NAME);
         printf("%s ",aux->NAME);
         order = addchain(order,aux->NAME);
         }
      aux = aux->NEXT;
      } 
   printf("\n\n");
   }

while (makeBddBeh(bef1,bef1->CIRCUI,vhb_reorder,1,100,10000000,NULL) == 1 )
   {
   gcNodeBeh(bef1);
   order = makeOrderBddBeh(bef1,0,NULL,NULL,2,30,1,0,12,-1,NULL);
   vhb_reorder--;
   }

printf("---> final number of nodes = %d",(sysBdd.pRT)->compteur);
 
gcNodeBeh(bef1);
      
printf("(%d)\n\n",(sysBdd.pRT)->compteur);
     
		/* calcul des graphes pour le 2eme circuit */

cpOrderCct(bef1->CIRCUI,bef2->CIRCUI);

		/* ajout des inputs specifiques a bef2 */

ptChain = berinToChain_list(bef2);
while (ptChain)
   {
   if (searchInputCct(bef2->CIRCUI,ptChain->DATA) == EMPTYTH)
      {
      printf("Warning : Input '%s' only exists in the second description\n",
              ptChain->DATA); 
      addInputCct(bef2->CIRCUI,ptChain->DATA);
      }
   ptChain = ptChain->NEXT ;
   }

makeBddBeh(bef2,bef2->CIRCUI,0,1,100,100000000,NULL);
}

/*======================================================================/
/		                MAIN					/
/======================================================================*/

main(argc,argv)
int argc ;
char *argv[];
{
chain_list *ptChain,*order;
befig_list *bef1,*bef2;
pCircuit CC1,CC2;
char *path;
char *auxpath;
char *getenv();
int elimBusBef1,elimBusBef2;

		/* verification de la validite des arguments */

VHB_HEDFIG = NULL;

path = (char *) malloc (100);
auxpath = (char *) malloc (100);

if (!getenv("MBK_WORK_LIB"))
   strcpy(path,".");
else
   strcpy(path,getenv("MBK_WORK_LIB"));

if (!getenv("MBK_CATA_LIB"))
   strcpy(auxpath,".");
else
   strcpy(auxpath,getenv("MBK_CATA_LIB"));

if (argc > 2)
   {
   argv[argc-2] = (char *) genNAME("%s.vbe",argv[argc-2]);
   argv[argc-1] = (char *) genNAME("%s.vbe",argv[argc-1]);
   }

if (!verifArgsProof(argc,argv)) exit(-1);

alliancebanner("Proof","2.00","Formal Proof","90-93","2.0");

printf("================================  Environment  ==============================\n");
printf("MBK_WORK_LIB       = %s\n",path);
printf("MBK_CATA_LIB       = %s\n",auxpath);
printf("=======================  Files, Options and Parameters  =======================\n");
printf("First VHDL file           = %s\n",argv[argc-2]);
printf("Second VHDL file          = %s\n",argv[argc-1]);

if(!strcmp(argv[1],"-a") || !strcmp(argv[2],"-a") || 
   (argc > 4 && !strcmp(argv[3],"-a")))
   printf("The common auxiliary signals are saved\n");
else
   printf("The auxiliary signals are erased\n");

if(!strcmp(argv[1],"-d") || !strcmp(argv[2],"-d") || 
   (argc > 4 && !strcmp(argv[3],"-d")))

printf("Errors are displayed\n");

printf("===============================================================================\n");
printf("\n");


if (argc > 2 && argc < 6)
   {

   initializeBdd(2);

		/* compilation du VHDL du premier circuit */
		/* on ne calcule pas les graphes tout de suite */

   if (compileVHDL(argv[argc-2],NULL,0,NULL,1,0,0,0,1,nameIntVect,NULL) == NULL)
      {
      printf("*** Compilation aborted...\n");
      exit(-1);
      }

   bef1 = VHB_HEDFIG;

		/* compactage */

   if(!strcmp(argv[1],"-a") || !strcmp(argv[2],"-a") || 
      (argc > 4 && !strcmp(argv[3],"-a")))
      compactBeh(bef1);

		/* compilation du VHDL du deuxieme circuit */
		/* on ne calcule pas les graphes tout de suite */

   if (compileVHDL(argv[argc-1],NULL,0,NULL,1,0,0,0,1,nameIntVect,NULL) == NULL)
      {
      printf("compilation aborted\n");
      printf("*** Compilation aborted...\n");
      exit(-1);
      }

   bef2 = VHB_HEDFIG;


		/* changement de polarite des BD de bef1 */

   if(!strcmp(argv[1],"-p") || !strcmp(argv[2],"-p") || 
      (argc > 4 && !strcmp(argv[3],"-p")))
      polarBDBeh(bef1);

		/* elimination des INOUT */

   elimInoutBeh(bef1);
   elimInoutBeh(bef2);

		/* calcul d'ordonnancement */

   orderProofBeh(bef1,bef2,argv,argc);

		/* re-ecriture des bus multiplex */
   
   elimBusBef1 = elimBusMuxBeh(bef1);
   elimBusBef2 = elimBusMuxBeh(bef2);

   if (elimBusBef1 || elimBusBef2) 
      {
			/* re-ordonnancement */

      orderProofBeh(bef1,bef2,argv,argc);
      }

		/*  renomage des befig */

   bef1->NAME = (char *) genNAME("%s/%s",path,bef1->NAME);
   bef2->NAME = (char *) genNAME("%s/%s",path,bef2->NAME);

   if(!strcmp(argv[1],"-d") || !strcmp(argv[2],"-d") || 
      (argc > 4 && !strcmp(argv[3],"-d")))
      {
      int ret = proofBeh(bef1,bef2,1,0); 
      printf("\n\n\n");
      if (ret)
         exit(-1);
      else
         exit(0);
      }
   else
      {
      int ret = proofBeh(bef1,bef2,0,0); 
      printf("                      Formal Proof : ");
      if (ret > 0) 
         {
         printf("%d error%s\n",ret,(ret > 1)?"s":"");
         exit(-1);
         }
      else 
         {
         printf("OK\n\n\n");
         exit(0);
         }
      }
   }
   printf("\n\n\n");
   exit(-1);
}
