fsp - 云端在线

程序：

您的姓名

fsp - 两个 FSM 描述之间的正式证明

概要

FSP [-V] 格式1 格式2 file1 file2

商品描述

用于在 FSM 描述上运行， FSP 支持与 syf 相同的 VHDL 子集（为了进一步
关于这个子集的信息见 SYF（1）和 FSM（5））。 FSP 使用降序二进制
决策图表示并计算两个 FSM 描述的乘积。
在这一步之后，它探索得到的 FSM 产品并正式证明等价
在两个初始 FSM 描述之间。 这两个描述必须相同
接口（VHDL 实体）。

环境 变数

MBK_WORK_LIB 给出 FSM 描述的路径。 默认值为当前
目录。

MBK_CATA_LIB 给出了 FSM 描述的一些辅助路径。 默认值为
当前目录。

配置

-V 设置详细模式。 形式证明的每一步都显示在标准上
输出。

例

fsp fsm fsm 数字 digi2

使用 onworks.net 服务在线使用 fsp