riscv
/
alliance
mirror of https://gitlab.lip6.fr/vlsi-eda/alliance.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

C'est vraiment du bon !

This commit is contained in:
Ludovic Jacomme 2002-04-18 12:47:46 +00:00
parent 29df2a0b4d
commit 9ae4cf6e8d
10 changed files with 3829 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
alliance/src/proof/Makefile.am Normal file
View File

@ -0,0 +1 @@
SUBDIRS = src man1

37
alliance/src/proof/configure.in Normal file
View File

@ -0,0 +1,37 @@
dnl Process this file with autoconf to produce a configure script.
AC_INIT(src/proof_main.c)
PROOF_MAJOR_VERSION=4
PROOF_MINOR_VERSION=9
PROOF_VERSION=$PROOF_MAJOR_VERSION.$PROOF_MINOR_VERSION
AC_SUBST(PROOF_MAJOR_VERSION)
AC_SUBST(PROOF_MINOR_VERSION)
AC_SUBST(PROOF_VERSION)
# For automake.
VERSION=$PROOF_VERSION
PACKAGE=proof
dnl Initialize automake stuff
AM_INIT_AUTOMAKE($PACKAGE, $VERSION)
dnl Checks for programs.
AC_PROG_CC
AM_PROG_LEX
AC_PROG_YACC
AC_PROG_RANLIB
AC_PROG_MAKE_SET
dnl Checks for typedefs, structures, and compiler characteristics.
AC_C_CONST
AC_CHECK_LIB(m, exp)
AM_ALLIANCE
AC_OUTPUT([
Makefile
man1/Makefile
src/Makefile
])

2
alliance/src/proof/man1/Makefile.am Normal file
View File

@ -0,0 +1,2 @@
man_MANS = proof.1
EXTRA_DIST = $(man_MANS)

57
alliance/src/proof/man1/proof.1 Normal file
View File

@ -0,0 +1,57 @@
.\" $Id: proof.1,v 1.1 2002/04/18 12:47:46 ludo Exp $
.\" @(#)Labo.l 1.2 91/11/01 UPMC; Author: BURGUN L.
.pl -.4
.TH PROOF 1 "October 1, 1997" "ASIM/LIP6" "CAO\-VLSI Reference Manual"
.SH NAME
.TP
proof
\- Formal proof between two behavioural descriptions
.so man1/alc_origin.1
.SH SYNOPSIS
.TP
\fBproof\fP [\fI-a\fP] [\fI-d\fP] \fIfile1\fP \fIfile2\fP
.br
.SH DESCRIPTION
.br
Made to run on a data-flow description, \fBproof\fP supports the same subset of VHDL as asimut and bop and scmap (for further informations about this subset, please call the VHDL manual). \fBproof\fP uses a Reduced Ordered Binary Decision Diagrams representation that permits the designer to prove easily the functionnal equivalence between two behavioral descriptions.
\fBproof\fP is generally used in order to compare a behavioural specification with an extracted behaviour obtained by \fByagle\fP.
.br
In default mode, a collapsing phase is done on the description by removing all the auxiliary signals (the BDD of the outputs, the registers and the buses are described from the inputs or the registers). The two descriptions must contain the same ressources (signals register with the same name).
It is possible to use the \fI.inf\fP file in \fByagle\fP to rename the registers in the extracted behavioural description (see man \fByagle\fP). The datas and the commands (the guarded expressions) must match separatly. The buses corresponding to completely specified logical functions are represented by a logical multiplexor in both descriptions.
The two descriptions must have the same interface (VHDL entity), if they do not, the formal \fBproof\fP is stopped.
.br
\fBproof\fP only uses two system environment variables related to the work directory.
.br
.SH ENVIRONMENT VARIABLES
.br
.HP
.ti 7
\fIMBK_WORK_LIB\fP gives the path for the behavioral descriptions. The default value is the current directory.
.br
.HP
.ti 7
\fIMBK_CATA_LIB\fP gives some auxiliary pathes for the behavioral descriptions. The default value is the current directory.
.SH OPTIONS
.br
Options may be given in any order before the filenames.
.HP
.ti 7
\-a
This option asks \fBproof\fP to keep the common auxiliary signals. \fBproof\fP keeps all intermediate signals that have the same name in both descriptions (A common signal is considered as an input and an output of each description). This option can be useful for descriptions containing large equations. It may be used when \fBproof\fP has failed or if you want to debug in step by step mode the two different descriptions.
.HP
.ti 7
\-d
The program displays errors when the behavioral descriptions are different. Equations are displayed when it's possible.
.br
.SH EXAMPLE
.br
proof -a -d adder1 adder2
.SH SEE ALSO
.br
\fBbop\fP (1), \fBglop\fP (1), \fBscmap\fP (1), \fBc4map\fP (1),
\fBasimut\fP(1), \fBvhdl\fP(5), \fByagle\fP(1), \fBvbe\fP(5).
.so man1/alc_bug_report.1

11
alliance/src/proof/src/Makefile.am Normal file
View File

@ -0,0 +1,11 @@
## Process this file with automake to produce Makefile.in
bin_PROGRAMS = proof
AM_CFLAGS = @ALLIANCE_CFLAGS@
proof_LDADD = @ALLIANCE_LIBS@ \
-lBvl -lBhl -lBeh -lLog -lMut
proof_SOURCES = \
proof_compile.c proof_main.c proof_util.c

630
alliance/src/proof/src/proof_compile.c Normal file
View File

@ -0,0 +1,630 @@
/*
* This file is part of the Alliance CAD System
* Copyright (C) Laboratoire LIP6 - Département ASIM
* Universite Pierre et Marie Curie
*
* Home page : http://www-asim.lip6.fr/alliance/
* E-mail support : mailto:alliance-support@asim.lip6.fr
*
* This progam is free software; you can redistribute it and/or modify it
* under the terms of the GNU General Public License as published by the
* Free Software Foundation; either version 2 of the License, or (at your
* option) any later version.
*
* Alliance VLSI CAD System is distributed in the hope that it will be
* useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
* Public License for more details.
*
* You should have received a copy of the GNU General Public License along
* with the GNU C Library; see the file COPYING. If not, write to the Free
* Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
*/
/*
* Tool : Logic Synthesis - boolean optimisation
* Date : 1991,92
* Author : Luc Burgun
* Modified by Czo <Olivier.Sirol@lip6.fr> 1996,97
* Modified by Ludo 2002
*/
#include <stdlib.h>
#include <stdio.h>
#include <string.h>
#include <math.h>
#include "mut.h"
#include "log.h"
#include "beh.h"
#include "bvl.h"
# include "proof_util.h"
befig_list *VHB_HEDFIG;
/*----------------------------------------------------------------------------
remegalExpr : elimine les horreurs du style
(not (xor a '0')) --> not a
(not (xor a '1')) --> a
------------------------------------------------------------------------------
retour : une expression
------------------------------------------------------------------------------*/
static chain_list *
remegalExpr (expr)
chain_list *expr;
{
if (ATOM (expr))
return (copyExpr (expr));
else
{
chain_list *ret;
if ((OPER (expr) == NOT) && !ATOM (CADR (expr)) && (OPER (CADR (expr)) == XOR))
{
chain_list *filsExpr;
chain_list *filsCst;
filsExpr = CADR (expr);
filsCst = CADR (CDR (filsExpr));
if (ATOM (filsCst) && !strcmp (VALUE_ATOM (filsCst), "'1'"))
{
return (copyExpr (CADR (filsExpr)));
}
if (ATOM (filsCst) && !strcmp (VALUE_ATOM (filsCst), "'0'"))
{
return (notExpr (copyExpr (CADR (filsExpr))));
}
}
ret = createExpr (OPER (expr));
while ((expr = CDR (expr)))
{
addQExpr (ret, remegalExpr (CAR (expr)));
}
return (ret);
}
}
/*-------------------------------------------------------------------------
renameExpr : renommage d'une expression avec une fonction
---------------------------------------------------------------------------
retour : un void.
---------------------------------------------------------------------------*/
void
renameExpr (expr, func)
chain_list *expr;
char *(*func) ();
{
if (ATOM (expr))
expr->DATA = (void *) (*func) (VALUE_ATOM (expr));
else
{
while ((expr = CDR (expr)))
{
renameExpr (CAR (expr), func);
}
}
}
/*-------------------------------------------------------------------------
renameBeh : renommage d'une befig
---------------------------------------------------------------------------
retour : un void.
---------------------------------------------------------------------------*/
void
renameBeh (beh, func)
befig_list *beh;
char *(*func) ();
{
beout_list *out;
bereg_list *reg;
bebus_list *bus;
bebux_list *bux;
biabl_list *biabl;
beaux_list *aux;
berin_list *in;
bepor_list *port;
bemsg_list *msg;
begen_list *generic;
int i;
for (generic = beh->BEGEN; generic; generic = generic->NEXT)
{
char *gen = generic->NAME;
char *val = generic->NAME;
/* on avance dans val jusqu'au '_' */
for (i = 0; i < strlen (gen) && gen[i] != '_'; i++)
val++;
if (i < strlen (gen)) /* le '_' existe bien */
{
char *newval;
char *field;
char *racine = (char *) mbkalloc (1024);
strncpy (racine, gen, ++i);
racine[i] = '\0';
val++;
newval = (*func) (val);
field = (char *) mbkalloc (1024 + strlen (newval));
sprintf (field, "%s%s", racine, newval);
generic->NAME = namealloc (field);
mbkfree (field); /* chaine */
mbkfree (racine); /* chaine */
}
}
port = beh->BEPOR;
while (port)
{
port->NAME = (*func) (port->NAME);
port = port->NEXT;
}
in = beh->BERIN;
while (in)
{
in->NAME = (*func) (in->NAME);
in = in->NEXT;
}
aux = beh->BEAUX;
while (aux)
{
aux->NAME = (*func) (aux->NAME);
if (aux->ABL)
{
renameExpr (aux->ABL, func);
}
aux = aux->NEXT;
}
msg = beh->BEMSG;
while (msg)
{
if (msg->ABL)
{
renameExpr (msg->ABL, func);
}
msg = msg->NEXT;
}
out = beh->BEOUT;
while (out)
{
out->NAME = (*func) (out->NAME);
if (out->ABL)
{
renameExpr (out->ABL, func);
}
out = out->NEXT;
}
reg = beh->BEREG;
while (reg)
{
reg->NAME = (*func) (reg->NAME);
biabl = reg->BIABL;
while (biabl)
{
if (biabl->CNDABL && biabl->VALABL)
{
renameExpr (biabl->CNDABL, func);
renameExpr (biabl->VALABL, func);
}
biabl = biabl->NEXT;
}
reg = reg->NEXT;
}
bus = beh->BEBUS;
while (bus)
{
bus->NAME = (*func) (bus->NAME);
biabl = bus->BIABL;
while (biabl)
{
if (biabl->CNDABL && biabl->VALABL)
{
renameExpr (biabl->CNDABL, func);
renameExpr (biabl->VALABL, func);
}
biabl = biabl->NEXT;
}
bus = bus->NEXT;
}
bux = beh->BEBUX;
while (bux)
{
bux->NAME = (*func) (bux->NAME);
biabl = bux->BIABL;
while (biabl)
{
if (biabl->CNDABL && biabl->VALABL)
{
renameExpr (biabl->CNDABL, func);
renameExpr (biabl->VALABL, func);
}
biabl = biabl->NEXT;
}
bux = bux->NEXT;
}
}
/*-------------------------------------------------------------------------
substPhyExprBeh : substitue une variable par une expression
---------------------------------------------------------------------------
retour : un void.
---------------------------------------------------------------------------*/
void
substPhyExprBeh (beh, name, expr)
befig_list *beh;
char *name;
chain_list *expr;
{
beout_list *out;
beaux_list *aux;
bebus_list *bus;
bebux_list *bux;
bereg_list *reg;
biabl_list *biabl;
out = beh->BEOUT;
while (out)
{
if (out->ABL)
{
if (searchExpr (out->ABL, name))
{
if (!ATOM (out->ABL))
substPhyExpr (out->ABL, name, expr);
else
out->ABL = copyExpr (expr);
}
}
out = out->NEXT;
}
aux = beh->BEAUX;
while (aux)
{
if (aux->ABL)
{
if (searchExpr (aux->ABL, name))
{
if (!ATOM (aux->ABL))
substPhyExpr (aux->ABL, name, expr);
else
aux->ABL = copyExpr (expr);
}
}
aux = aux->NEXT;
}
reg = beh->BEREG;
while (reg)
{
biabl = reg->BIABL;
while (biabl)
{
if (biabl->VALABL)
{
if (searchExpr (biabl->VALABL, name))
{
if (!ATOM (biabl->VALABL))
substPhyExpr (biabl->VALABL, name, expr);
else
biabl->VALABL = copyExpr (expr);
}
}
if (biabl->CNDABL)
{
if (searchExpr (biabl->CNDABL, name))
{
if (!ATOM (biabl->CNDABL))
substPhyExpr (biabl->CNDABL, name, expr);
else
biabl->CNDABL = copyExpr (expr);
}
}
biabl = biabl->NEXT;
}
reg = reg->NEXT;
}
bus = beh->BEBUS;
while (bus)
{
biabl = bus->BIABL;
while (biabl)
{
if (biabl->VALABL)
{
if (searchExpr (biabl->VALABL, name))
{
if (!ATOM (biabl->VALABL))
substPhyExpr (biabl->VALABL, name, expr);
else
biabl->VALABL = copyExpr (expr);
}
}
if (biabl->CNDABL)
{
if (searchExpr (biabl->CNDABL, name))
{
if (!ATOM (biabl->CNDABL))
substPhyExpr (biabl->CNDABL, name, expr);
else
biabl->CNDABL = copyExpr (expr);
}
}
biabl = biabl->NEXT;
}
bus = bus->NEXT;
}
bux = beh->BEBUX;
while (bux)
{
biabl = bux->BIABL;
while (biabl)
{
if (biabl->VALABL)
{
if (searchExpr (biabl->VALABL, name))
{
if (!ATOM (biabl->VALABL))
substPhyExpr (biabl->VALABL, name, expr);
else
biabl->VALABL = copyExpr (expr);
}
}
if (biabl->CNDABL)
{
if (searchExpr (biabl->CNDABL, name))
{
if (!ATOM (biabl->CNDABL))
substPhyExpr (biabl->CNDABL, name, expr);
else
biabl->CNDABL = copyExpr (expr);
}
}
biabl = biabl->NEXT;
}
bux = bux->NEXT;
}
}
/*----------------------------------------------------------------------------
compileVHDL : compile un vbe , cree eventuellement les BDD et verifie la
coherence de la description.
orderPI = permet d'imposer un ordonnancement initial
si sauveaux = 1 on conserve les variables intermediaires
si gcOk = 1 on peut effectuer un garbage collector.
si vhb_reorder > 1 on peut re-ordonnancer les bdds du circuit.
makeBdd = 1 : creation de BDD
-> Le systeme des BDD doit etre initialise auparavant.
trace : mode trace
func : fonction de renomage des signaux internes
beh : si <> NULL, la befig a deja ete compilee
------------------------------------------------------------------------------
retour : NULL si la compilation n'a pas fonctionne
l'ordonnancement des variables d'entrees sinon.
------------------------------------------------------------------------------*/
/*
compileVHDL(argv[argc-2],NULL,0,NULL,1,0,0,0,1,nameIntVect,NULL)
*/
chain_list *
compileVHDL (file, orderPI, order, par,
saveaux, gcOK, vhb_reorder, makeBdd, trace, func, beh)
char *file;
chain_list *orderPI;
int order;
void *par;
int saveaux;
int gcOK;
int vhb_reorder;
int makeBdd;
int trace;
char *(*func) ();
befig_list *beh;
{
befig_list *vhdlloadbefig ();
beaux_list *aux;
chain_list *ptChain;
biabl_list *biabl;
bereg_list *reg;
int coInter;
char *path;
int i;
int indice = 0;
char *filep;
chain_list *liste, *pAux = NULL;
/* si BEH est NULL, on appelle le compilateur */
if (beh == NULL)
{
filep = (char *) mbkalloc (strlen (file) + 2);
strcpy (filep, file);
file = filep;
for (i = 0; i < strlen (file); i++)
if (file[i] == '/')
indice = i;
if (indice == 0) /* pas de '/' dans file */
{
path = ".";
file[strlen (file) - 4] = '\0';
}
else
{
path = (char *) mbkalloc (indice + 1);
strncpy (path, file, indice);
path[indice] = '\0';
for (i = 0; i <= indice; i++)
file++;
file[strlen (file) - 4] = '\0';
}
/* compilation du VHDL */
if (trace)
printf ("Compiling '%s' ...\n", file);
beh = vhdlloadbefig (NULL, file, 0);
}
if (beh->ERRFLG != 0)
return NULL;
/* on empile sur VHB_HEDFIG */
beh->NEXT = VHB_HEDFIG;
VHB_HEDFIG = beh;
/* mise a NULL du champ USER pour les biabl des registres */
reg = beh->BEREG;
while (reg)
{
biabl = reg->BIABL;
while (biabl)
{
biabl->USER = NULL;
biabl = biabl->NEXT;
}
reg = reg->NEXT;
}
/* verification de la declaration correcte d'attribut 'stable
forme valide (l = '0') and not l'stable : front descendant
(and (not l) (not (stable l)))
ou (l = '1') and not l'stable : front montant
(and l (not (stable l)))
*/
if (beh->TYPE & BEH_STABLE)
{
reg = beh->BEREG;
while (reg)
{
biabl = reg->BIABL;
while (biabl)
{
chain_list *inter = biabl->CNDABL;
biabl->CNDABL = remegalExpr (biabl->CNDABL);
if (searchOperExpr (biabl->CNDABL, STABLE))
{
chain_list *pattern1, *pattern2;
chain_list *pattern3, *pattern4;
pattern1 = charToExpr ("(and (not x) (not (stable x)))");
pattern2 = charToExpr ("(and x (not (stable x)))");
pattern3 = charToExpr ("(and (not (stable x)) (not x))");
pattern4 = charToExpr ("(and (not (stable x)) x)");
if (!PMExpr (biabl->CNDABL, pattern1) &&
!PMExpr (biabl->CNDABL, pattern2) &&
!PMExpr (biabl->CNDABL, pattern3) &&
!PMExpr (biabl->CNDABL, pattern4))
{
printf ("VHDL : Error - bad usage of the 'stable' attribut\n");
return (NULL);
}
else
{
biabl->USER = addptype (NULL, 0, 0);
}
/* (and (not x) (not (stable x))) --> x */
/* (and x (not (stable x))) --> (not x) */
if (PMExpr (biabl->CNDABL, pattern1) ||
PMExpr (biabl->CNDABL, pattern2))
{
if (ATOM (CADR (biabl->CNDABL)))
biabl->CNDABL = notExpr (CADR (biabl->CNDABL));
else
biabl->CNDABL = CADR (CADR (biabl->CNDABL));
}
else
{
if (ATOM (CADR (CDR (biabl->CNDABL))))
biabl->CNDABL = notExpr (CADR (CDR (biabl->CNDABL)));
else
biabl->CNDABL = CADR (CADR (CDR (biabl->CNDABL)));
}
freeExpr (pattern1);
freeExpr (pattern2);
freeExpr (pattern3);
freeExpr (pattern4);
}
freeExpr (inter);
biabl = biabl->NEXT;
}
reg = reg->NEXT;
}
}
/* on renomme les variables de la befig pour les vecteurs */
if (func != NULL)
renameBeh (beh, func);
/* on de-vectorise les variables intermediaires */
aux = beh->BEAUX;
while (aux)
{
int i = 0;
char *name = (char *) mbkalloc (strlen (aux->NAME) + 1);
strcpy (name, aux->NAME);
/* detection signal vectorise */
while (name[i] != '\0' && name[i] != ' ')
{
i++;
}
/* substitution avec un souligne */
if (name[i] == ' ')
{
name[i] = '_';
substPhyExprBeh (beh, aux->NAME, createAtom (name));
aux->NAME = namealloc (name);
}
mbkfree (name); /* desa. de name */
aux = aux->NEXT;
}
return ((chain_list *) 1);
}

66
alliance/src/proof/src/proof_compile.h Normal file
View File

@ -0,0 +1,66 @@
/*------------------------------------------------------------\
| |
| This file is part of the Alliance CAD System Copyright |
| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie|
| |
| Home page : http://www-asim.lip6.fr/alliance/ |
| E-mail support : mailto:alliance-support@asim.lip6.fr |
| |
| This progam is free software; you can redistribute it |
| and/or modify it under the terms of the GNU Library General|
| Public License as published by the Free Software Foundation |
| either version 2 of the License, or (at your option) any |
| later version. |
| |
| Alliance VLSI CAD System is distributed in the hope that |
| it will be useful, but WITHOUT ANY WARRANTY; |
| without even the implied warranty of MERCHANTABILITY or |
| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General |
| Public License for more details. |
| |
| You should have received a copy of the GNU General Public |
| License along with the GNU C Library; see the file COPYING. |
| If not, write to the Free Software Foundation, Inc., |
| 675 Mass Ave, Cambridge, MA 02139, USA. |
| |
\------------------------------------------------------------*/
#ifndef __P
# if defined(__STDC__) || defined(__GNUC__)
# define __P(x) x
# else
# define __P(x) ()
# endif
#endif
# ifndef PROOF_COMPIL_H
# define PROOF_COMPIL_H
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern chain_list * compileVHDL __P(( char *file, chain_list *orderPI, int order, void *par, int saveaux, int gcOK, int vhb_reorder, int makeBdd, int trace, char *(*func) (), befig_list *beh ));
# endif

280
alliance/src/proof/src/proof_main.c Normal file
View File

@ -0,0 +1,280 @@
/*
* This file is part of the Alliance CAD System
* Copyright (C) Laboratoire LIP6 - Département ASIM
* Universite Pierre et Marie Curie
*
* Home page : http://www-asim.lip6.fr/alliance/
* E-mail support : mailto:alliance-support@asim.lip6.fr
*
* This progam is free software; you can redistribute it and/or modify it
* under the terms of the GNU General Public License as published by the
* Free Software Foundation; either version 2 of the License, or (at your
* option) any later version.
*
* Alliance VLSI CAD System is distributed in the hope that it will be
* useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
* Public License for more details.
*
* You should have received a copy of the GNU General Public License along
* with the GNU C Library; see the file COPYING. If not, write to the Free
* Software Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
*/
/*
* Tool : Logic Synthesis - formal proof
* Date : 1991,92
* Author : Luc Burgun
* Modified by Czo <Olivier.Sirol@lip6.fr> 1996,97
* Modified by Ludo 2002
*/
#include <stdio.h>
#include <stdlib.h>
#include "mut.h"
#include "log.h"
#include "beh.h"
# include "proof_compile.h"
char *GLOB_ABL_DC;
char *GLOB_ABL_ONE;
char *GLOB_ABL_ZERO;
extern befig_list *VHB_HEDFIG;
/*AFAC*/
char *nameIntVect (char *name);
/* on ne verifie pas si les fichiers existent ...*/
/*----------------------------------------------------------------------------
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[];
{
if (argc < 3 || argc > 6)
{
printf("\n");
printf("proof \nusage : proof -option");
printf(" <file_entity1> <file_entity2> \n");
printf("option : -d display the logical functions\n");
printf(" -a the common auxiliary signals are kept\n");
printf(" -p the polarity of the triggered edges is inversed \n");
printf(" within the first behavioural description\n");
return(0) ;
}
if (argc > 3)
{
if(strcmp(argv[1],"-d") && strcmp(argv[1],"-a") && strcmp(argv[1],"-p"))
{
printf("\nproof : 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 : 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 : unknown option '%s'\n\n",argv[2]) ;
return(0) ;
}
}
return(1);
}
/*======================================================================/
/ MAIN /
/======================================================================*/
int
main(argc,argv)
int argc ;
char *argv[];
{
char varaux;
befig_list *bef1,*bef2;
char *path;
char *auxpath;
int elimBusBef1,elimBusBef2;
/* verification de la validite des arguments */
mbkenv();
alliancebanner("Proof",VERSION,"Formal Proof","1990", ALLIANCE_VERSION);
GLOB_ABL_DC = namealloc ("'d'");
GLOB_ABL_ONE = namealloc ("'1'");
GLOB_ABL_ZERO = namealloc ("'0'");
path = (char *)mbkalloc(5);
auxpath = (char *) mbkalloc (5);
path = WORK_LIB;
if (!mbkgetenv("MBK_CATA_LIB"))
strcpy(auxpath,".");
else
auxpath = mbkstrdup(mbkgetenv("MBK_CATA_LIB"));
if (argc > 2)
{
char *auxFile1 = mbkalloc(strlen(argv[argc-2]) + 5);
char *auxFile2 = mbkalloc(strlen(argv[argc-1]) + 5);
sprintf(auxFile1, "%s.vbe",argv[argc-2]);
argv[argc-2] = auxFile1;
sprintf(auxFile2, "%s.vbe",argv[argc-1]);
argv[argc-1] = auxFile2;
}
if (!verifArgsProof(argc,argv))
exit(-1);
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 kept\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;
if(!strcmp(argv[1],"-a") || !strcmp(argv[2],"-a") ||
(argc > 4 && !strcmp(argv[3],"-a")))
varaux = 'A';
else
varaux = 'G';
/* 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,varaux);
/* re-ecriture des bus multiplex */
elimBusBef1 = elimBusMuxBeh(bef1);
elimBusBef2 = elimBusMuxBeh(bef2);
if (elimBusBef1 || elimBusBef2)
{
/* re-ordonnancement */
orderProofBeh(bef1,bef2,varaux);
}
/* renomage des befig */
{
char *auxBeh1 = mbkalloc(strlen(path) + strlen(bef1->NAME) + 2);
char *auxBeh2 = mbkalloc(strlen(path) + strlen(bef2->NAME) + 2);
sprintf(auxBeh1, "%s/%s",path,bef1->NAME);
bef1->NAME = auxBeh1;
sprintf(auxBeh2, "%s/%s",path,bef2->NAME);
bef2->NAME = auxBeh2;
}
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);
}

2679
alliance/src/proof/src/proof_util.c Normal file
View File

File diff suppressed because it is too large Load Diff

66
alliance/src/proof/src/proof_util.h Normal file
View File

@ -0,0 +1,66 @@
/*------------------------------------------------------------\
| |
| This file is part of the Alliance CAD System Copyright |
| (C) Laboratoire LIP6 - Département ASIM Universite P&M Curie|
| |
| Home page : http://www-asim.lip6.fr/alliance/ |
| E-mail support : mailto:alliance-support@asim.lip6.fr |
| |
| This progam is free software; you can redistribute it |
| and/or modify it under the terms of the GNU Library General|
| Public License as published by the Free Software Foundation |
| either version 2 of the License, or (at your option) any |
| later version. |
| |
| Alliance VLSI CAD System is distributed in the hope that |
| it will be useful, but WITHOUT ANY WARRANTY; |
| without even the implied warranty of MERCHANTABILITY or |
| FITNESS FOR A PARTICULAR PURPOSE. See the GNU General |
| Public License for more details. |
| |
| You should have received a copy of the GNU General Public |
| License along with the GNU C Library; see the file COPYING. |
| If not, write to the Free Software Foundation, Inc., |
| 675 Mass Ave, Cambridge, MA 02139, USA. |
| |
\------------------------------------------------------------*/
#ifndef __P
# if defined(__STDC__) || defined(__GNUC__)
# define __P(x) x
# else
# define __P(x) ()
# endif
#endif
# ifndef PROOF_UTIL_H
# define PROOF_UTIL_H
/*------------------------------------------------------------\
| |
| Constants |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Macro |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Types |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Variables |
| |
\------------------------------------------------------------*/
/*------------------------------------------------------------\
| |
| Functions |
| |
\------------------------------------------------------------*/
extern chain_list * berinToChain_list __P(( befig_list *beh ));
# endif