PROOF(1)

📦 version 5.1.1, in fedora 43, fedora 44

💖 PROOF(1) — the CAO-VLSI Reference Manual, but make it cute 💖

okay bestie, sit down, we're learning proof today and honestly? it's giving genius. 🧚✨

✨ NAME ✨

proof — formal proof between two behavioural descriptions. yes really, it proves two things are the same. slay.

🌸 ORIGIN 🌸

This software belongs to the ALLIANCE CAD SYSTEM, developed by the ASIM team at the LIP6 laboratory of Université Pierre et Marie CURIE, in Paris, France. 🇫🇷 iconic behaviour honestly.

⭐ SYNOPSIS ⭐

proof [-a] [-d] file1 file2

🦋 DESCRIPTION 🦋

So. proof was made to run on a data-flow description, and it supports the exact same subset of VHDL as asimut and boom and boog do. wanna know more about that subset? go call the VHDL manual, it's right there, it's not shy. 📞

proof uses a Reduced Ordered Binary Decision Diagrams representation, which is a whole vibe, and it lets you prove easily the functionnal equivalence between two behavioral descriptions. like, no cap, you just... prove they do the same thing. 🔥

proof is generally used in order to compare a behavioural specification with an extracted behaviour obtained by yagle. that's the classic use case, that's the moment. 💅

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. basically it's decluttering. main character energy. ✨

The two descriptions must contain the same ressources (signals register with the same name). no exceptions bestie.

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. yes, separatly. both of them. 💀

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. periodt. 🛑

proof only uses two system environment variables related to the work directory. just two. low maintenance queen. 👑

🌈 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. flexible queen.

  • -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. so you actually see what went wrong. obsessed. 😭

🍓 EXAMPLE 🍓

proof -a -d adder1 adder2

look at her go. 🫶

🧚 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. 📚

👑 SEE ALSO 👑

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

the whole friend group. the squad. 💜

💀 BUG REPORT 💀

This tool is under development at the ASIM department of the LIP6 laboratory.

We need your feedback to improve documentation and tools. fr fr, tell them what's broken, they wanna know. 🙈

ok that's the whole page bestie, you're officially certified in proof now 💖

and a lil sign-off for the vibes: this page comes from ASIM/LIP6, dated October 1, 1997 — yeah it's vintage, it's archival, it's iconic, and it still ate. 🌟💅✨

📦 where this page comes from