第五章Expert System 专家系统

概述

JasperGold Expert System 是一个基于知识库（Knowledgebase）的智能辅助系统，分析设计和证明状态，提供优化建议。

启用/禁用 Knowledgebase

从 2016.12 版本开始，调用 JasperGold 时 JGES Knowledgebase System 默认就是启用的。要禁用它，可用以下任一方式：

点击 Expert System 状态栏上的电源按钮
用 -no_jges 命令行选项启动 JasperGold（jg -no_jges）
把 expert_system_status 变量设为 off

# 禁用 / 启用 JasperGold Expert System（on 为默认值）
set_expert_system_status off
set_expert_system_status on

# 查询当前是 on 还是 off
get_expert_system_status

禁用/启用单条建议或整类建议没有对应的 Tcl 命令，需要在 Knowledgebase Configuration 对话框中操作：在其中取消勾选你想禁用的建议或建议类别即可。

Expert System User Profile

首次启用 Knowledgebase System 时，JGES 会请你填写一份用户档案（user profile）。这份档案确保 Knowledgebase System 呈现的建议与你当前的专业水平相关、避免显示重复建议，并记住你通常会采纳哪些规则、忽略哪些规则。随着你在形式方法和 JasperGold Apps 上经验的积累，可以随时更新这份档案。

User Profile 是一个图形界面对话框（分 Server Mode 与 Server-less Mode 两种形态），通过界面中的 "Editing the User Profile and Preferences" 流程修改，没有对应的 Tcl 命令。

JGES Knowledgebase System 界面。三个标签页分别是 **System Recommendations**、**Knowledgebase Search** 和 **Recommendation History**。图中这条建议带着绿色的 **Proof Convergence** 类别标签，规则 ID 为 `PFC101: Abstract counters`——正好对应下文类别表中 `PFC` 前缀；右侧有 Show me… 链接、展开按钮和三点菜单，下方绿色按钮即该建议的 action

Information System 安装配置

系统要求

要安装 JGES Information System 服务器，系统需满足以下最低要求（安装过程中会检查）：

Intel Xeon E5500 系列 2.0GHz 或更好
操作系统（均为 64 位）：Red Hat Enterprise Linux 6.x 及以上、SUSE Linux Enterprise Server 11 及以上、CentOS 6.x 及以上、Ubuntu 14.04 及以上
至少 32GB 内存
至少 20GB 可用空间

Information System 不是必需的：你可以在启用或不启用 Information System 数据跟踪的情况下使用 JGES Knowledgebase System。若选择启用数据跟踪，运行的完整数据会存储在服务器上；若选择不启用，工具只在本地 ~/.config/jasper/jges.conf 存放极少量数据。

Expert System 建议的分类

Knowledgebase System 基于用户档案、task 和工具状态推荐具体的动作。这些建议是上下文感知的，范围从纠正 setup 错误的指示，到提升证明收敛性的建议。建议按类别和 ID 编号组织，类别包括：

类别	ID 前缀
Flow Guidance（流程指导）	`FLG`
Analyze（分析）	`ANA`
Elaborate（展开）	`ELA`
Clock（时钟）	`CLK`
Reset（复位）	`RST`
Environment（环境）	`ENV`
Proof Convergence（证明收敛）	`PFC`
Debug（调试）	`DBG`
Verification Signoff（验证签核）	`VSO`

Appendix A: Custom Rule Implementation

Expert System 支持自定义规则，用户可以编写自己的检查规则。

Appendix B: Web Client Report Attributes

Expert System 可以生成 Web 格式的报告，包含各种属性和统计信息。

Expert System 界面

Expert System Show-Me 对话框 — Expert System **Show-Me** 对话框：点击建议里的 "Show me…" 链接后弹出，列出该建议针对的 Task、Property（`dl.ack nak check i.AST no unexpected ack`）、Bound（40），以及涉及的 Counter 与位宽（`ctrl timeout cnt` 16 位、`phy out data seqnum` 6 位、`replay timeout cnt` 16 位）——正是 `PFC101: Abstract counters` 建议要抽象掉的那几个计数器

Expert System User Query 对话框：采纳建议前询问把 stopat 加到现有 task 还是新建 task，可直接 Apply 或加入 Action Plan

Information System Web Client 管理页 — Information System Web Client 的 Admin page（Administrator Options）：Configuration、User Management、Company Sites、User Roles、Website Settings、Aliases、Health Status、Logs 等标签，以及 LDAP 设置——可见它是一个带用户管理的服务端 Web 应用

Web Client 的 Usage Summary 报表，列正是 Appendix B 的属性：Project、App、Design、User、Usage Start/End Time、Total Runs、Total Run Time、Total Interactive Time、Total Engine Time——记录的是工具使用情况而非证明状态

正确认识 Expert System

Expert System 不是"黑盒魔法"，而是积累了大量形式验证工程师经验的知识库系统。它分析你的设计特征和证明结果，从知识库中匹配相似案例给出建议。

它能帮你做什么

官方对建议范围的描述是：从纠正 setup 错误的指示，到提升证明收敛性的建议。对照上面的类别表，可以看出它覆盖了从 analyze/elaborate、时钟复位设置、环境约束，一直到证明收敛、调试和验证签核的整条流程。

在 System Recommendations 标签页中，每条匹配的建议会给出简短描述，并带有：

Show me 链接：跳转到更多说明信息
action 链接：让你在采纳建议前先预览或编辑将要执行的命令
彩色标签：标明该规则属于哪个建议类别，并标识出 path recommendation（例如 Deep Bug Hunting）
展开/折叠按钮与右侧的三点菜单：展开描述、访问更多资源，或隐藏该建议、查看相关建议

Knowledgebase System 工具栏还支持：一次性展开/折叠所有建议的细节、实施 action plan（同时采纳多条建议）、打开 Knowledgebase Configuration 对话框、启用所有建议、设置 verbosity（默认为 low），以及按类别过滤建议。

Information System Web Client

JGES Information System 通过汇总来自各客户端的工具使用信息提供可见性，供 formal champion、工程经理和其他相关方做实时分析。

注意：Web Client 是一个需要登录的 Web 应用（属于 Information System 组件），而不是工具在本地生成的报告文件。它提供 Activity Dashboard 以及各种报表和图表——点击 Activity Dashboard 标签或图标可查看按天分组的主要活动，该 dashboard 左侧包含四个表格、右侧包含四个图表。

官方文档中的 "Web Client Report" 指的就是这些在 Web Client 中呈现的报表。它们记录的是工具使用情况，而不是证明状态统计。Appendix B 列出了报表的通用属性：

属性	含义
Project	在 `JASPERGOLD_UXDB_ARGS` 中指定的保留 tag
App	调用的 App
Design	本次 JasperGold 运行的顶层设计名
User	发起该 job 的用户
Country / Site Name	该 job 用户当前的国家（可修改）与站点名
Start Time / End Time	job、属性证明或 license checkout 的起止时间
Runs	相同 project、app、design 和 user 组合的调用次数（任一字段不同都会在报表中产生新条目）
Run Time	最后一次调用的运行时间（多次运行的情况下）
Interactive Time	测得的用户与工具交互的时间
Engine Time	最后一次调用的累计引擎时间
Regression	在 `JASPERGOLD_UXDB_ARGS` 中指定的保留 tag

别把两个组件搞混：Recommendations（建议）和 History（历史与反馈）属于 Knowledgebase System 的图形界面，而不是 Web Client 的组成部分。Web Client 侧的内容是 Login、Environment Variables、Administrator Options、Main Page Overview、Reports and Charts 和 Troubleshooting。

使用建议：Expert System 的建议应该作为参考而非绝对真理。它基于历史案例匹配，对你的特定设计可能不适用。理解每条建议背后的原理再决定是否采纳。

来源文档

jaspergold_expert_system.pdf