OneSpin360图形界面

一致性检查举例

等价性检查举例

Onespin是领先的EDA解决方案提供商，其360系列产品为FPGA形式化验证工具。它以强大、高性能的形式化验证引擎为基础，能够覆盖自动设计分析到高级属性检查以及逻辑等效性验证，帮助构建功能正确，安全，可靠、可信赖的系统。

本文基于OneSpin 360版本 2020的学习笔记

OneSpin360图形界面

OneSpin360读入了设计后，它的图形界面如图1所示。图中三个数字标红的圈圈是OneSpin360提供给用户的主要功能。用户可以方便的通过这些按钮去实现其功能。其中标红圈圈1中，主要是用于用户执行设计设置 (Design Setup)：

读入设计(Reading in the design :VHDL button for VHDL files, V button for Verilog files)
详细阐述设计(Elaborate the design : E button)
编译设计(Compile the design : C button)
指定时钟信号和复位时序(Specify clock pins and reset sequence)

图1 OneSpin360 图形界面

在design setup 结束后，用户可以切换到三种模式，CC、MV和EC. 此后，先前组成setup模式的按钮将会被隐藏并显示当前模式的按钮。如图2中显示的是setup模式，从左到右的按钮的功能依次是读入VHDL文件、读入Verilog文件、设计详细阐述(elaborating the design)、编译(Compiling)、设计和端口(pin the port ,only EC mode)。右边三个是模式选择。

图2 setup 模式

红色圈圈2是shell/message/progress 窗口,每个功能的输出信息都会显示在这里。命令在shell 窗口输入红色圈圈3功能如下：

Hiding the shell -隐藏shell 窗口，进入GUI 模式
Hid the GUI – 隐藏GUI, 进入shell 交互界面
Interrupting the execution of a running command - 中断操作命令
Calling the help browser – 调用帮助手册

OneSpin 提供了非常强大的帮助命令，这很方便用户很快的查找命令和掌握该工具，很大的方便了验证师，节省了验证时间。那么如何获得帮助呢? 除了在GUI界面下直接点击help-browser外，用户可直接在OneSpin shell区中输入命令“help”。Help命令可以获得对一个命令的详细语法描述。例如，以下命令都可以获得read_verilog命令的语法描述：

Setup> help read_verilog

Setup> help *verilog*

除help命令以外，OneSpin shell也支持使用Tab键自动匹配(Tab-completion)命令。当用户输入了命令的前几个字母，再按下Tab键，如果输入的前几个字母在命令中是唯一的，shell就可以自动输入该命令；如果不唯一，shell就会列出所有匹配的命令，用户可以通过上下键自由选择，例如（图3）：

setup>read_

Tab-completion的功能不光适合于命令匹配，在命令的选项(option)和文件名的匹配上同样适用。

用户要退出OneSpin时，可以在shell中输入：exit．如果用户没有保存数据库(database)，oneSpin就会弹出对话框，提示是否保存数据库。

图3 Tab 键自动匹配命令

一致性检查举例

在这里用一个小例子来说明如何用OneSpin来执行一致性检查（consistency checking）.

步骤1：随便找一个vhdl 或者verilog 文件，我这里是这一个VHDL文件包含了整个设计文件。
步骤2：Read the Design

在shell 窗口使用以下命令读入设计文件,-version 93是指定VHDL标准

Setup > read_vhdl -cell -version 93 arbiter.vhd

也可以在GUI界面，点击setup 目录下的VHDL,其中version可以选择VHDL的标准。点击文件后Read & close 就可以，会在shell 窗口提示读成功

步骤3：Elaboration and Compilation

在读入全部的VHDL 和Verilog 文件之后，必须对设计座elaboration,在shell 窗口输入：

Setup > elaborate

对于时钟，复位以及一些黑盒或者其他不关心的设计，用户可能通过一些特别说明来阐述。这个后面再讲。详细设计阐述后就可以compile 了，这个命令会产生一些单元的内部描述，见图4。

Setup > compile

图4完成编译后的OneSpin界面

步骤4：set mode to CC

OneSpin有三种可选的模式，在CC(consistency checking)模式和 MV (module Verification)模式下都可实现一致性检查(consistency checking)。这种重复是因为一致性检查是非常有用的。而且便于用户集中注意力在等价性检查(equivalence checking)，而不需要360MV许可证(License)。所以非常值得推荐。

为了进入一致性检查，可在shell窗口中输入下面的命令：

Setup > set_mode cc

Tips: 该命令会将命令提示符从” setup”转变到”cc”，如图5所示。

图5 CC 工作模式

步骤5：一致性检查 consistency checking with model building assertions,在CC模式，执行命令check_consistency：

CC > check_consistency

许多的基本检查会被自动执行。这些检查都是基于设计中插入的一些断言实现的。在工程应用中，该功能一般很少用到。所以这里不做详述。执行完一致性检查后，便可以开始执行模块验证(module verification)或者特征检查(property checking)。这个后面再说。一致性检查结果会再shell 窗口打印如图6

图6 一致性检查打印结果

一致性检查包含了signal domain checks 、init checks、fsm checks、dead code checks、stick checks; 如果只需要对其中某一项进行检查可以使用命令（如init checks）：check_consistency -category { init } 除此之外，还可以再GUI界面操作，如图7所示，check ALL Visible 就是检查所有可见的条目，另外通过explain Check可以查看本条检查的规则。Explore Selected Auto Check 可以定位到这条检查在设计中的位置。

图7 GUI界面手动检查

等价性检查举例

这部分主要举例说明如何用OneSpin执行等价性检查(equivalence checking)。等价性检查主要是检查两个门级网表(gate-level netlist)之间是否一致或者RTL级与门级网表级是否一致以及两个RTL描述是否一致。在此，将以前一部分提及例子的VHDL设计作为对比举例。

1.Read the two design

在OneSpin中，被比较的两部分设计被冠以象征性的名字‘‘golden”和“revised”。通常，假设gold design是正确的，把revised design 和golden design 进行对比。为了强制某一命令工作在golden design 或者revised design上，必须指定相应的选项-golden或者-revised。如果投有指定这些选项，系统将默认当前的设计是golden design, 命令也将会工作在当前的设计。通过命令读入两个VHDL 文件

Setup > read_vhdl -golden arbiter.vhd

Setup > read_vhdl -revised arbiter_new.vhd

读如上述两个文件后的OneSpin界面如图8所示：

图8 读入两个文件后的OneSpin界面

2.Elaboration and Compilation

在读入设计文件之后，必须要做elaboration和compile.

Setup > elaborate -both

Setup > compile -both

编译成功后，OneSpin 会产生两个设计（golden 和 revised）的内部描述（internal representation : unit model）

图 9 Elaborate 和Compile之后界面

3.Set Mode to cc

成功编译后，就可以进行等价性检查了（equivalence checking）,在shell 窗口输入命令:

Setup > set_mode ec

4. Map Pins and States

设计的对比以golden design 和 revised design 的输入、输出和状态的映射（mapping）为基础。它们的映射关系通过map 命令建立起来，完成映射后的OneSpin界面如图10所示：

ec > map

图10 EC 模式下map 之后的OneSpin 界面

5. Compare the two design

在建立了映射（mapping）之后就可以对两个设计进行对比了，在ec 模式下上输入命令

ec > compare

该命令会将所有的映射的输入和状态(compare point)，并且输出的结果概述。对于那些行为不同的对比点，将会产生一个反例。图11为OneSpin 完成对比之后的界面。

图11 完成比较之后输出信息

6．Debug Differences

对于每一个失败的状态，都可以通过GUI中双击各自的状态得到一个反例，此外，GUI还会显示失败的fanin view.这些信息有利于调试。

7.Fix bugs

可以通过edit_file 命令还编辑有bug的文件，需要注意的是在文件修改之后，revised design 必须要重新读入，编译，映射对比。

FPGA形式化验证工具OneSpin360学习笔记（一）相关推荐

成都链安重磅出品 | 基于VS Code插件的智能合约自动形式化验证工具Beosin—VaaS『离线免费版』...
11月4日,成都链安重磅推出『离线免费版』智能合约自动形式化验证工具Beosin-VaaS,该版本基于流行的开发工具VS Code插件,供广大开发者免费使用.获得方式如下,欢迎体验使用: https: ...
Telerik移动应用开发工具AppBuilder学习笔记(二)--IDEs
Telerik移动应用开发工具AppBuilder学习笔记之 IDEs Telerik AppBuilder的IDE有四种: 1,在线IDE,地址:https://platform.telerik. ...
VHDL编写多功能数字钟，spartan3 FPGA开发板硬件实现-学习笔记
VHDL编写多功能数字钟,spartan3 FPGA开发板硬件实现-学习笔记多功能数字钟硬件测试视频: https://www.bilibili.com/video/av62501230 1.数字钟 ...
形式化验证工具TLA+：程序员视角的入门之道
简介: 女娲是飞天分布式系统中提供分布式协同的基础服务,支撑着阿里云的计算.网络.存储等几乎所有云产品.在女娲分布式协同服务中,一致性引擎是核心基础模块,支持了Paxos,Raft,EPaxos等多种 ...
元数据管理工具Atlas学习笔记之集成
文章目录背景环境 Atlas安装 solr Atlas Atlas启动启动Hadoop.ZooKeeper.HBase.Kafka.Hive和MySQL Hadoop 启动ZooKeeper 启 ...
Scyther形式化验证工具简单教程
Scyther形式化验证工具 Scyther是一种自动化的安全协议验证工具.在协议的安全性验证方面有着广泛的应用. 下面介绍其安装方法以及使用教程. 安装方法 Scyther工具在Windows 10 ...
golang实现将数据库表自动转为结构体的小工具（学习笔记）
golang实现将数据库表自动转为结构体的小工具必备条件代码结构如下代码详情 config.go init.go tool.go main.go config.json[运行man.go文件的时 ...
jquery 绘图工具 flot 学习笔记
原文地址为: jquery 绘图工具 flot 学习笔记今天想做一个统计图表,像163博客的流量统计一样的,借助 flot 实现了,而且很简单. flot网址:http://code.google. ...
软件缺陷报告与JIRA工具使用学习笔记
开发转自动化测试五六年了.工作当中做的最多的就是写自动化脚本.对于测试理论的知识有所欠缺,所以我打算抽空把理论知识补上.感谢黑马的这套软件缺陷报告与jiar工具使用的学习教程.以下是我学习笔记. 第一 ...

FPGA形式化验证工具OneSpin360学习笔记（一）

OneSpin360图形界面

一致性检查举例

等价性检查举例

FPGA形式化验证工具OneSpin360学习笔记（一）相关推荐

最新文章

热门文章