
/* ###--------------------------------------------------------------### */
/* 									*/
/* file		: beh_makbdd.c						*/
/* date		: Sep  9 1993						*/
/* version	: v106							*/
/* authors	: VUONG H.N., L.A. TABUSSE, P. BAZARGAN			*/
/* description	: high level function					*/
/*									*/
/* ###--------------------------------------------------------------### */

#include <stdio.h>
#include MUT_H
#include LOG_H
#include BEH_H

static struct chain *ptr_ctrlst = NULL;

/* ###--------------------------------------------------------------### */
/* function	: beh_error						*/
/* description	: print an errorr message				*/
/* called func.	: none							*/
/* ###--------------------------------------------------------------### */

static int beh_error (code, str1)

int   code;
char *str1;

  {
  (void) fprintf (stderr, "BEH : Error %d :", code);

  switch (code)
    {
    case 1:
      (void) fprintf (stderr, "combinatory loop : `%s`\n", str1);
      break;
    case 2:
      (void) fprintf (stderr, "cannot make bdd of empty expression\n");
      break;
    case 3:
      (void) fprintf (stderr, "cannot find terminal `%s`\n", str1);
      break;
    case 4:
      (void) fprintf (stderr, "STABLE attribut on non terminal expression\n");
      break;
    case 5:
      (void) fprintf (stderr, "cannot simplify internal signals\n");
      break;
    default:
      (void) fprintf (stderr, "syntax error\n");
      break;
    }

  return (1);
  }

/* ###--------------------------------------------------------------### */
/* function	: beh_abl2bdd						*/
/* description	: transform recursively abl in bdd 			*/
/* algorithm    : if ATOM(expr)is an operand --terminal variable, 	*/
/*		  then 							*/
/*		    if (it is a constant or a primary variable)		*/
/*		    then return that bdd that is already known 		*/
/*		    else 						*/
/*		      if ((it is an auxiliary variable)&&		*/
/*			  (there is no self-dependence))		*/
/*	   	      then return beh_abl2bdd(that terminal variable)	*/
/*		      else ERROR					*/
/*		  else apply OPER(expr) 				*/
/*			to beh_abl2bdd(every operands) 			*/
/* called func.	: searchInputCct, createNodeTermBdd, addListBdd,	*/
/*		  beh_abl2bdd   , applyBdd         , addchain  ,	*/
/*		  freechain     , delchain         , beh_error ,	*/
/* ###--------------------------------------------------------------### */

static pNode beh_abl2bdd (ptr_befig, expr)

struct befig *ptr_befig;	/* pointer on  behavioural figure	*/
chain_list   *expr     ;	/* pointer abl expression		*/

  {
  short         oper  ;
  pNode         ptr_bdd     = zero;
  struct chain *lstGbd      = NULL;
  struct chain *ptr_cntrl   = ptr_ctrlst;
  struct beaux *ptr_beaux   = ptr_befig->BEAUX;
  pCircuit      ptr_circuit = ptr_befig->CIRCUI;
  int           err_flg     = 0;
  int           index;
  char         *atom;
  char          name[256];

	/* ###------------------------------------------------------### */
	/*    check that the expression exists				*/
	/* ###------------------------------------------------------### */

  if (expr == NULL)
    err_flg = beh_error (2, NULL);
  else
    {

    if (ATOM(expr))
      {
	/* ###------------------------------------------------------### */
	/*    if the expression is a terminal (atom)			*/
	/* ###------------------------------------------------------### */

      atom = (char *) VALUE_ATOM (expr);

	/* ###------------------------------------------------------### */
	/*    if the terminal is a primary signal create a single node	*/
	/* with its index and return					*/
	/* ###------------------------------------------------------### */

      if ((index = searchInputCct (ptr_circuit, atom)) != VIDE)
        ptr_bdd = createNodeTermBdd (index);
      else
        {
	/* ###------------------------------------------------------### */
	/*    if the terminal is a secondary signal, search it in the	*/
	/* beaux list							*/
	/* ###------------------------------------------------------### */

        while ((ptr_beaux != NULL) && (ptr_beaux->NAME != atom))
          ptr_beaux = ptr_beaux->NEXT;

        if (ptr_beaux != NULL)
	  {
	/* ###------------------------------------------------------### */
	/*    check that the terminal (secondary signal to be		*/
	/* simplified) do not depend on itself. Then replace it by its	*/
	/* expression (bdd)						*/
	/* ###------------------------------------------------------### */

          while ((ptr_cntrl != NULL) && ((char *) ptr_cntrl->DATA != atom))
            ptr_cntrl = ptr_cntrl->NEXT;

          if (ptr_cntrl != NULL)
            {
	    err_flg = beh_error (1, atom);
            }
          else
            {
            if ((ptr_bdd = ptr_beaux->NODE) == NULL)
              {
              ptr_ctrlst      = addchain (ptr_ctrlst, atom);
              ptr_beaux->NODE = beh_abl2bdd (ptr_befig, ptr_beaux->ABL);
              ptr_ctrlst      = delchain (ptr_ctrlst, ptr_ctrlst);
              ptr_bdd         = ptr_beaux->NODE;
              }
            }
          }

        else
          {
	/* ###------------------------------------------------------### */
	/* the terminal should be a const. '0', '1' or 'd' (don't care)	*/
	/* ###------------------------------------------------------### */

          if ((!strcmp(atom, "'0'")) || (!strcmp(atom, "'d'")))
            ptr_bdd = zero;
          else
            {
            if (!strcmp(atom, "'1'"))
              ptr_bdd = one;
            else
              {
              err_flg = beh_error (3, atom);
              }
            }
          }
        }
      }
    else
      {
	/* ###------------------------------------------------------### */
	/*    if the expression is not a terminal (is a complex expr.)	*/
	/* get the operator, create the bdd of each operand then,	*/
	/* combine operands applying the operator			*/
	/* ###------------------------------------------------------### */

      lstGbd = NULL;

      if ((oper = OPER(expr)) != STABLE)
       {
       while ((expr = CDR(expr)) != NULL)
        lstGbd = addListBdd (lstGbd, beh_abl2bdd (ptr_befig, CAR(expr)));

       ptr_bdd = applyBdd (oper, lstGbd);
       freechain (lstGbd);
       }
      else
       {
	expr = CDR(expr);
	if (!ATOM(expr))
	  err_flg = beh_error (4, NULL);
        else
          {
	  atom = (char *)VALUE_ATOM (CAR(expr));

          if ((index = searchInputCct (ptr_circuit, atom)) != VIDE)
            {
            lstGbd = addListBdd (lstGbd, createNodeTermBdd (index));
	    sprintf (name, "%s'delayed", atom);
	    atom = namealloc (name);
            if ((index = searchInputCct (ptr_circuit, atom)) != VIDE)
              {
              lstGbd = addListBdd (lstGbd, createNodeTermBdd (index));
              ptr_bdd = applyBdd (NXOR, lstGbd);
              }
            else
	      err_flg = beh_error (3, atom);
            freechain (lstGbd);
            }
          else
	    err_flg = beh_error (3, atom);
          }
        }
      }
    }

  if (err_flg != 0)
    ptr_befig->ERRFLG = 1;

  return (ptr_bdd);
  }

/* ###--------------------------------------------------------------### */
/* function	: beh_mbddtot						*/
/* description	: make bdds for all primary signals: simple and bussed	*/
/*		  outputs, simple and bussed internal signals and	*/
/*		  registers						*/
/* called func.	: beh_abl2bdd, addchain , delchain,			*/
/* ###--------------------------------------------------------------### */

static void beh_mbddtot (ptr_befig, trace_flg)

struct befig *ptr_befig;		/* pointer on current BEFIG	*/
char          trace_flg;		/* trace signals when making bdd*/

  {
  struct beaux  *ptr_beaux;
  struct beaux  *ptr_bedly;
  struct bemsg  *ptr_bemsg;
  struct beout  *ptr_beout;
  struct bebus  *ptr_bebus;
  struct bebux  *ptr_bebux;
  struct bereg  *ptr_bereg;
  struct biabl  *ptr_biabl;
  struct binode *ptr_binode;

	/* ###------------------------------------------------------### */
	/*    make a bdd for each simple internal signal		*/
	/* ###------------------------------------------------------### */

  ptr_beaux = ptr_befig->BEAUX;

  while (ptr_beaux != NULL)
    {
    if (trace_flg == 1)
      printf ("internal signal : %s\n", ptr_beaux->NAME);

    if (ptr_beaux->NODE == NULL)
      {
      ptr_ctrlst      = addchain (ptr_ctrlst, ptr_beaux->NAME);
      ptr_beaux->NODE = beh_abl2bdd (ptr_befig, ptr_beaux->ABL);
      ptr_ctrlst      = delchain (ptr_ctrlst, ptr_ctrlst);
      }
    ptr_beaux = ptr_beaux->NEXT;
    }

	/* ###------------------------------------------------------### */
	/*    make a bdd for each delayed internal signal		*/
	/* ###------------------------------------------------------### */

  ptr_bedly = ptr_befig->BEDLY;
  while (ptr_bedly != NULL)
    {
    if (trace_flg == 1)
      printf ("delayed internal signal : %s\n", ptr_bedly->NAME);

    if (ptr_bedly->NODE == NULL)
      {
      ptr_ctrlst      = addchain (ptr_ctrlst, ptr_bedly->NAME);
      ptr_bedly->NODE = beh_abl2bdd (ptr_befig, ptr_bedly->ABL);
      ptr_ctrlst      = delchain (ptr_ctrlst, ptr_ctrlst);
      }
    ptr_bedly = ptr_bedly->NEXT;
    }

	/* ###------------------------------------------------------### */
	/*    make a bdd for each assertion				*/
	/* ###------------------------------------------------------### */

  ptr_bemsg = ptr_befig->BEMSG;
  while (ptr_bemsg != NULL)
    {
    if (ptr_bemsg->NODE == NULL)
      ptr_bemsg->NODE = beh_abl2bdd (ptr_befig, ptr_bemsg->ABL);

    ptr_bemsg = ptr_bemsg->NEXT;
    }

  /*--------------------------------------------------------------------*/
  /*  Evalue BDDs for each BEOUT					*/
  /*--------------------------------------------------------------------*/

  ptr_beout = ptr_befig->BEOUT;
  while (ptr_beout != NULL)
    {
    if (trace_flg == 1)
      printf ("simple output : %s\n", ptr_beout->NAME);

    if (ptr_beout->NODE == NULL)
      ptr_beout->NODE = beh_abl2bdd (ptr_befig, ptr_beout->ABL);

    ptr_beout = ptr_beout->NEXT;
    }

  /*--------------------------------------------------------------------*/
  /*  Evalue BDDs for each BEBUS					*/
  /*--------------------------------------------------------------------*/

  ptr_bebus = ptr_befig->BEBUS;
  while (ptr_bebus != NULL)
    {
    if (trace_flg == 1)
      printf ("bussed output : %s\n", ptr_bebus->NAME);

    ptr_biabl  = ptr_bebus->BIABL;
    ptr_binode = ptr_bebus->BINODE;

    while (ptr_biabl != NULL)
      {
      ptr_binode->CNDNODE = beh_abl2bdd (ptr_befig, ptr_biabl->CNDABL);
      ptr_binode->VALNODE = beh_abl2bdd (ptr_befig, ptr_biabl->VALABL);

      ptr_biabl = ptr_biabl->NEXT;
      ptr_binode = ptr_binode->NEXT;
      }

    ptr_bebus = ptr_bebus->NEXT;
    }

  /*--------------------------------------------------------------------*/
  /*  Evalue BDDs for each BEBUX					*/
  /*--------------------------------------------------------------------*/

  ptr_bebux = ptr_befig->BEBUX;
  while (ptr_bebux != NULL)
    {
    if (trace_flg == 1)
      printf ("internal bussed signal : %s\n", ptr_bebux->NAME);

    ptr_biabl  = ptr_bebux->BIABL;
    ptr_binode = ptr_bebux->BINODE;

    while (ptr_biabl != NULL)
      {
      ptr_binode->CNDNODE = beh_abl2bdd (ptr_befig, ptr_biabl->CNDABL);
      ptr_binode->VALNODE = beh_abl2bdd (ptr_befig, ptr_biabl->VALABL);

      ptr_biabl  = ptr_biabl->NEXT;
      ptr_binode = ptr_binode->NEXT;
      }
    ptr_bebux = ptr_bebux->NEXT;
    }

  /*--------------------------------------------------------------------*/
  /*  Evalue BDDs for each BEREG					*/
  /*--------------------------------------------------------------------*/

  ptr_bereg = ptr_befig->BEREG;
  while (ptr_bereg != NULL)
    {
    if (trace_flg == 1)
      printf ("register : %s\n", ptr_bereg->NAME);

    ptr_biabl  = ptr_bereg->BIABL;
    ptr_binode = ptr_bereg->BINODE;

    while (ptr_biabl != NULL)
      {
      ptr_binode->CNDNODE = beh_abl2bdd (ptr_befig, ptr_biabl->CNDABL);
      ptr_binode->VALNODE = beh_abl2bdd (ptr_befig, ptr_biabl->VALABL);

      ptr_biabl  = ptr_biabl->NEXT;
      ptr_binode = ptr_binode->NEXT;
      }
    ptr_bereg = ptr_bereg->NEXT;
    }

  }

/* ###--------------------------------------------------------------### */
/* function	: beh_makbdd						*/
/* description	: make bdd for each signal of  a befig structure 	*/
/* 		: if aux_flg is 0, auxiliary variables disappear in bdd,*/
/* 		: and output, bus, and register signal depend only on 	*/
/* 		: primary variables that are inputs and register signals*/
/*              : if aux_flg is 1, auxiliary variables are kept.    	*/
/*              : trace_flg, permit to trace the signals transformed    */
/* called func.	: initializeCct, addInputCct, beh_mbddtot		*/
/* ###--------------------------------------------------------------### */

void beh_makbdd (ptr_befig, aux_flg, trace_flg)

struct befig *ptr_befig;
char aux_flg;
char trace_flg;

  {
  berin_list *ptr_rin;
  beaux_list *ptr_aux, *ptr_auxtmp;
  beout_list *ptr_out;
  bebus_list *ptr_bus;
  int         count_rin = 0;
  int         count_out = 0;
  int         err_flg   = 0;

        /* ###------------------------------------------------------### */
        /*    count inputs 						*/
        /* ###------------------------------------------------------### */

  ptr_rin = ptr_befig->BERIN;
  while (ptr_rin != NULL)
    {
    ptr_rin = ptr_rin->NEXT;
    count_rin++;
    }

        /* ###------------------------------------------------------### */
        /*    remove simple internal signals from primary signals' list	*/
        /* ###------------------------------------------------------### */

  if (aux_flg == 0)
    {
    if (ptr_befig->BEDLY == NULL)
      {
      ptr_aux = ptr_befig->BEAUX;
      while (ptr_aux != NULL)
        {
        ptr_befig->BERIN = beh_rmvberin (ptr_befig->BERIN, ptr_aux->NAME);
        ptr_aux = ptr_aux->NEXT;
        count_rin--;
        }
      }
    else
      err_flg = beh_error (5, NULL);
    }


        /* ###------------------------------------------------------### */
        /*    count outputs 						*/
        /* ###------------------------------------------------------### */

  ptr_out = ptr_befig->BEOUT;
  while (ptr_out != NULL)
    {
    ptr_out = ptr_out->NEXT;
    count_out++;
    }
  ptr_bus = ptr_befig->BEBUS;
  while (ptr_bus != NULL)
     {
     ptr_bus = ptr_bus->NEXT;
     count_out++;
     }

        /* ###------------------------------------------------------### */
        /*    initialization						*/
        /* ###------------------------------------------------------### */

  ptr_befig->CIRCUI = initializeCct (ptr_befig->NAME, count_rin*2, count_out);

        /* ###------------------------------------------------------### */
        /*    Define an index for each primary signal			*/
        /* ###------------------------------------------------------### */

  ptr_rin = ptr_befig->BERIN;
  while (ptr_rin != NULL)
    {
    addInputCct (ptr_befig->CIRCUI, ptr_rin->NAME);
    ptr_rin = ptr_rin->NEXT;
    }

        /* ###------------------------------------------------------### */
        /*    Change ABLs to BDDs for					*/
        /* ###------------------------------------------------------### */

  beh_mbddtot (ptr_befig, trace_flg);

        /* ###------------------------------------------------------### */
        /*    remove the whole BEAUX list				*/
        /* ###------------------------------------------------------### */

  if ((aux_flg == 0) && (ptr_befig->BEDLY == NULL))
    {
    ptr_aux = ptr_befig->BEAUX;
    while (ptr_aux != NULL)
      {
      ptr_auxtmp = ptr_aux->NEXT;
      mbkfree (ptr_aux);
      ptr_aux = ptr_auxtmp;
      }
    }

  if (err_flg != 0)
    ptr_befig->ERRFLG = 1;

  }
