Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages


home | help
PROOF(1)		   CAO-VLSI Reference Manual		      PROOF(1)

       proof  -	Formal proof between two behavioural descriptions

       proof [-a] [-d]	file1  file2

       Made  to	run on a data-flow description,	proof supports the same	subset
       of VHDL as asimut and boom and boog  (for  further  informations	 about
       this subset, please call	the VHDL manual). proof	uses a Reduced Ordered
       Binary Decision Diagrams	representation that permits  the  designer  to
       prove  easily  the  functionnal	equivalence between two	behavioral de-
       scriptions.  proof is generally used in order to	compare	a  behavioural
       specification with an extracted behaviour obtained by yagle.
       In  default  mode, a collapsing phase is	done on	the description	by re-
       moving 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 .inf file in yagle (see fur-
       ther remark about YAGLE in this document) to rename  the	 registers  in
       the  extracted  behavioural  description	(see man yagle). 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
       proof is	stopped.
       proof only uses two system environment variables	related	 to  the  work


       MBK_WORK_LIB  gives  the	 path for the behavioral descriptions. The de-
	      fault value is the current directory.

       MBK_CATA_LIB gives some auxiliary pathes	for  the  behavioral  descrip-
	      tions. The default value is the current directory.

       Options may be given in any order before	the filenames.

       -a  This	 option	asks proof to keep the common auxiliary	signals. proof
	      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  de-
	      scriptions containing large equations. It	may be used when proof
	      has failed or if you want	to debug in step by step mode the  two
	      different	descriptions.

       -d  The	program	 displays  errors when the behavioral descriptions are
	      different. Equations are displayed when it's possible.

	    proof -a -d	adder1 adder2

       YAGLE  (Functional  abstraction)	 is  now  comercially  distributed  by
       Avertec (  More	information can	be obtained at
       their web site. Binaries	of this	tool can also be downloaded  for  non-
       commercial university research.

	boom (1), boog (1), loon (1), asimut(1), vhdl(5), vbe(5).

ASIM/LIP6			October	1, 1997			      PROOF(1)


Want to link to this manual page? Use this URL:

home | help