This is the command proof that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
PROGRAM:
NAME
proof - Formal proof between two behavioural descriptions
SYNOPSIS
proof [-a] [-d] file1 file2
DESCRIPTION
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
descriptions. 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 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 .inf file in yagle (see
further 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 directory.
ENVIRONMENT VARIABLES
MBK_WORK_LIB gives the path for the behavioral descriptions. The default value is the
current directory.
MBK_CATA_LIB gives some auxiliary pathes for the behavioral descriptions. The default
value is the current directory.
OPTIONS
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 descriptions 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.
EXAMPLE
proof -a -d adder1 adder2
YAGLE
YAGLE (Functional abstraction) is now comercially distributed by Avertec
(http://www.avertec.com/). More information can be obtained at their web site. Binaries
of this tool can also be downloaded for non-commercial university research.
Use proof online using onworks.net services
