FSP(1)

📦 version 5.1.1, in fedora 43, fedora 44

💖 FSP(1) — like, the CAO-VLSI Reference Manual era, but make it make sense 💖

okay bestie, sit down, hydrate, and let me tell you about fsp from the CAO-VLSI Reference Manual 🎀 (yes that's the manual name, we're keeping it, it's iconic).

✨ NAME ✨

fsp — Formal proof between two FSM descriptions. that's it. that's the whole vibe. 💅

🌸 ORIGIN 🌸

So this software is part of the ALLIANCE CAD SYSTEM, developed by the ASIM team at the LIP6 laboratory of Université Pierre et Marie CURIE, in Paris, France. 🇫🇷✨

like, they literally built this in Paris. main character energy fr. 🥐

🦋 SYNOPSIS 🦋

fsp [-V] format1 format2 file1  file2

(yes there are two spaces between file1 and file2, we do not touch it, we respect it 🫶)

💜 DESCRIPTION 💜

Made to run on FSM descriptions, fsp supports the same subset of VHDL as syf (for further information about this subset, go look at SYF(1) and FSM(5) — the receipts are there, iykyk 📚).

fsp uses a Reduced Ordered Binary Decision Diagrams representation and computes the product of the two FSM descriptions. Then, after that step, it explores the resulting FSM product and formally proves the equivalence between the two initial FSM descriptions. ✨

lowkey important: those two descriptions must have the same interface (VHDL entity). no matching interface, no proof, no slay. 💀

🌈 ENVIRONMENT VARIABLES 🌈

  • MBK_WORK_LIB — gives the path for the FSM descriptions. The default value is the current directory. 📁
  • MBK_CATA_LIB — gives some auxiliary paths for the FSM descriptions. The default value is the current directory. 🗂️

💅 OPTIONS 💅

  • -V — Sets verbose mode on. Each step of the formal proof is displayed on the standard output. it's giving commentary track, it's giving director's cut, we're obsessed. 👑

🍓 EXAMPLE 🍓

fsp fsm fsm digi digi2

look at her go. ✨

🧚 SEE ALSO 🧚

syf (1), fmi (1), fsm (5), xfsm (1).

(the whole friend group. go say hi. 🫶)

⭐ BUG REPORT ⭐

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

We need your feedback to improve documentation and tools. 🥺 like genuinely, pls tell them things, they're asking so nicely.

ASIM/LIP6 · October 1, 1997 · FSP(1) — yeah the date is giving vintage, the tool is giving timeless, periodt. 💖✨

📦 where this page comes from