Browse > Home / 信息中心 / SNUG / 2005论文集 / 龙芯-2系统芯片组的混合形式化验证

龙芯-2系统芯片组的混合形式化验证


Verifying the Chipset Design of Godson-2 with Hybrid Formal Method

张珩
中国科学院计算技术研究所系统结构研究室 北京　 100080
zhangheng@ict.ac.cn

Zhang Heng
Department of Computer Architecture, Institute of Computing Technology, CAS, Beijing, 100080

摘要：

目前基于断言的验证方法 ( Assertion Based Verification ), 尤其是基于断言的形 式化验证方法被越来越多地应用到大规模ASIC设计的功能验证中。形式化验证方法与传统的基于动态仿真的验证方法相比可以更加有效地发现系统设计中的错误，并且更加充分地验证系统设计。

本文介绍了在龙芯-2系统芯片组的设计验证过程中使用的形式化验证方法和流程。在该流程中我们使用了Synopsys公司的形式化验证工具Megallen对设计的模块级RTL进行了基于断言的功能验证，在较短的时间内完成了模块级的功能验证工作。

I. 引 言

随 着 集 成 电 路 技 术 的 不 断 发 展， 功 能 验 证 已 经 成 为 了 ASIC 设 计 流 程 的 瓶 颈， 这 是 因 为 验 证 的 复 杂 度 随 着 设 计 的 增 大 呈 指 数 增 长。 在 一 个 大 规 模 集 成 电 路 的 开 发 过 程 中， 使 用 单 一 的、 传 统 的 基 于 动 态 模 拟 仿 真 的 方 法 进 行 功 能 验 证 已 经 不 能 满 足 设 计 的 需 要。 使 用 新 的 验 证 方 法 和 流 程 成 为 高 效 解 决 验 证 问 题 的 关 键。 同 时 下 面 几 个 原 因 也 决 定 了 模 块 级 验 证 在 大 规 模 A S I C 验 证 流 程 中 也 起 着 越 来 越 重 要 的 作 用：
系 统 级 验 证 只 有 在 整 体 设 计 基 本 完 成 之 后 才 能 进 行。 模 块 级 验 证 可 以 和 设 计 并 行 进 行， 并 有 效 的 提 高 模 块 的 设 计 质 量。
● 设 计 工 程 师 对 设 计 模 块 有 比 较 透 彻 的 了 解， 可 以 很 快 分 析 和 定 位 设 计 缺 陷 (bug)。
● 当 模 块 级 的 设 计 缺 陷 带 入 到 系 统 级 后， 设 计 缺 陷 分 析 和 定 位 的 复 杂 性 大 大 增 加
● 高 质 量 的 设 计 模 块 可 以 更 容 易 地 在 其 他 设 计 中 进 行 重 用。
● 断 言 和 形 式 验 证（model check） 技 术 可 以 在 没 有 完 备 测 试 激 励 的 情 况 下 帮 助 模 块 设 计 工 程 师 发 现 潜 在 的 设 计 缺 陷。 形 式 验 证 技 术 在 短 期 内 还 难 以 应 用 到 超 大 规 模 SoC 系 统 验 证。

在 龙 芯 系 统 的 设 计 过 程 中， 实 际 的 经 验 已 经 使 我 们 充 分 认 识 到 高 效 率、 高 质 量 的 模 块 级 验 证 在 整 个 设 计、 验 证 流 程 中 的 重 要 性。

形 式 化 验 证 方 法 已 经 越 来 越 多 的 被 引 入 到 ASIC 开 发 项 目 中， 比 如 基 于 断 言 的 验 证， 等 价 性 检 验 和 模 型 检 验 等。 形 式 化 验 证 方 法 可 以 高 效、 完 备 地 验 证 设 计 的 功 能 正 确 性。 特 别 在 处 理 模 块 级 功 能 验 证 时 能 够 显 著 的 提 高 验 证 的 效 率 和 质 量。 Synopsys 公 司 的 混 合 形 式 化 验 证 工 具 Megallen 集 合 了 基 于 断 言 的 形 式 化 引 擎 以 及 内 建 的 测 试 激 励 产 生 和 RTL 仿 真 引 擎， 即 提 供 了 形 式 化 验 证 的 快 速 完 备， 同 时 也 增 大 了 处 理 问 题 的 规 模。 正 是 由 于 引 入 了 以 Megallen 为 主 要 工 具 的 混 合 形 式 化 验 证 方 法 才 使 龙 芯-2 系 统 芯 片 的 验 证 效 率 得 到 了 很 大 的 提 高。 本 文 主 要 介 绍 了 在 龙 芯 2 的 系 统 芯 片 的 开 发 验 证 流 程 中， 使 用 的 混 合 形 式 化 验 证 方 法 和 流 程。 第 二 部 分 主 要 介 绍 龙 芯 2 系 统 芯 片 的 主 要 结 构； 第 三 部 分 介 绍 混 合形 式 化 验 证的 流 程； 第 四 部 分 介 绍 基 于 断 言 的 通 讯 协 议 的 检 验 器 的 开 发 和 AIP（Assertion IP） 的 使 用； 第 五 部 分 介 绍 运 行 结 果 和 分 析 ； 最 后 给 出 结 论。

II. 龙 芯 2 系 统 芯 片 的 基 本 结 构 和 验 证 特 征

龙 芯 2 的 系 统 芯 片 （也 称 为 北 桥 芯 片）。 北 桥 的 内 部 逻 辑 可 以 大 致 分 成 MIPS CPU 接 口 模 块、 PCI 接 口 模 块（Master/Slave）、 DDR SDRAM 接 口 模 块、 Local I/O 接 口 模 块、 寄 存 器 模 块、 中 断 控 制 模 块、 系 统 仲 裁 模 块 和 PCI 仲 裁 模 块 等 8 个 子 模 块。 其 中 包 括 3 个 主 设 备 和 4 个 从 设 备， 主 从 设 备 之 间 采 用 crossbar 交 叉 互 联 的 总 线 方 式 进 行 数 据 传 递， 做 到 最 大 限 度 的 提 高 北 桥 内 部 的 数 据 吞 吐 率。 整 个 北 桥 的 系 统 结 构 如 图 II 1 所 示：

图 II 1 系 统 芯 片 结 构 框 图

在 整 个 设 计 中， 多 种 接 口 的 协 议 验 证 是 工 作 的 关 键， 特 别 是 PCI 总 线 接 口 协 议、 DDR SDRAM 协 议、 交 叉 开 关 互 连（wishbone） 总 线 协 议 以 及 CPU 和 系 统 芯 片 接 口 协 议 的 验 证。 通 过 使 用 商 业 的 VIP（Verification IP）， 可 以 减 少 验 证 的 工 作 量。 例 如 synopsys 公 司 提 供 的 DesignWare Library 中 就 有 用 于 PCI 验 证 的 AIP 。 同 时 还 需 要 根 据 设 计 规 范 所 描 述 的 功 能 属 性 开 发 出 自 己 的 协 议 检 验 器（protocol checker）。 这 样 即 可 以 在 基 于 动 态 的 模 拟 仿 真 验 证 流 程 中 使 用 这 些 断 言 来 检 验 设 计， 也 可 以 使 用 Megallen 这 样 的 形 式 化 验 证 工 具 来 静 态 验 证 设 计 的 逻 辑 功 能 正 确 性。

III. 混 合 形 式 化 验 证 的 流 程

引 入 形 式 化 验 证 工 具 和 方 法， 并 不 能 完 全 替 代 传 统 的 基 于 模 拟 仿 真 的 验 证 方 法， 而 是 对 模 拟 仿 真 的 一 个 重 要 补 充 ， 特 别 是 对 于 使 用 传 统 仿 真 方 法 很 难 验 证 的 一 些 corner cases， 以 此 来 提 高 验 证 的 效 率 和 质 量。 在 龙 芯 2 系 统 芯 片 的 模 块 级 形 式 化 功 能 验 证 中 使 用 了 如 图 III 1 所 示 的 流 程。

图 III 1 混 合 形 式 化 验 证 基 本 流 程

首 先 根 据 设 计 规 范 撰 写 验 证 文 档。 描 述 清 晰 准 确 的 验 证 文 档 是 完 成 验 证 工 作 的 重 要 前 提。 通 常 的 设 计 规 范 是 使 用 自 然 语 言 来 描 述 设 计 属 性 的， 将 自 然 语 言 描 述 的 设 计 规 范 转 化 为 形 式 化 语 言 描 述 是 一 个 好 方 法。 使 用 assertion 定 义 设 计 规 范 中 设 计 属 性 是 使 用 Magellen 进 行 形 式 化 验 证 的 重 要 前 提。

Assertion 大 致 可 以 分 为 两 类： 设 计 实 现 的 属 性， 它 和 设 计 的 实 现 描 述 紧 密 相 关； 设 计 接 口（例 如 接 口 protocol） 的 属 性， 他 和 设 计 要 满 足 的 接 口 功 能 紧 密 相 关。 通 常 由 设 计 工 程 师 描 述 第 一 类 属 性， 而 由 验 证 工 程 师 描 述 第 二 类 属 性。

在 描 述 设 计 规 范 的 同 时 还 要 选 定 进 行 验 证 的 模 块 边 界 以 及 该 模 块 边 界 上 输 入 激 励 的 约 束 条 件（对 于 Magellan 来 说， 也 可 以 由 assertion 定 义 约 束 条 件）。 Megallen 内 部 集 成 的 形 式 化 验 证 引 擎 会 证 明 在 设 定 的 输 入 约 束 下 设 计 属 性 是 否 可 被 满 足。 如 果 有 设 计 属 性 被 违 反 则 会 停 止 分 析 并 给 出 相 应 的 测 试 激 励。 设 计 和 验 证 人 员 可 以 根 据 Megallen 提 供 的 测 试 激 励 对 设 计 进 行 分 析 调 试， 以 确 定 发 现 的 不 满 足 属 性 是 由 什 么 样 的 设 计 缺 陷 造 成 的。 有 时 设 计 属 性 不 满 足 的 原 因 也 可 能 是 assertion 的 描 述 错 误 或 者 边 界 约 束 条 件 设 定 错 误 造 成。 这 就 需 要 重 新 修 改 assertion 的 描 述 或 者 重 新 确 定 模 块 边 界 和 相 应 的 输 入 约 束。

另 外 模 块 边 界 的 选 择 不 合 理， 输 入 约 束 的 不 准 确 都 可 以 导 致 Magellen 不 能 给 出 检 验 结 果。 比 如 模 块 规 模 选 择 的 过 大， 就 会 造 成 运 行 时 间 过 长， 或 者 无 法 证 明 设 计 属 性。 这 就 需 要 重 新 选 择 要 验 证 的 模 块 边 界， 以 及 重 新 确 定 约 束 条 件。

IV. 基 于 断 言 的 协 议 检 验 器 和 边 界 约 束

通 过 上 述 的 介 绍 可 以 看 出， 在 整 个 混 合 形 式 化 验 证 流 程 中 以 下 两 点 是 关 键： 对 于 设 计 而 言， 哪 些 属 性 是 需 要 重 点 关 注 的， 如 何 将 这 些 我 们 重 点 关 注 的 设 计 属 性 转 化 为 assertion 进 行 准 确 的 描 述； 另 一 个 问 题 是 我 们 如 何 确 定 进 行 检 验 的 模 块 边 界 以 及 相 应 的 正 确 的 边 界 约 束 条 件。

为 了 更 好 的 描 述 断 言 和 设 计 的 属 性， 使 用 类 似 Verilog、 Jeda 和 SystemC 特 点 的 伪 代 码 来 进 行 编 写 验 证 文 档 是 一 个 好 的 方 法。 这 些 伪 代 码 的 用 处 就 是 作 为 以 后 写 Assertion 和 各 种 属 性 的 参 考。 示 例 如 代码 IV 1（DDR SDRAM 控 制 器 的 REFRESH）：

代码 IV 1 设 计 属 性 的 伪 代 码 示 例

在 龙 芯 2 系 统 芯 片 的 验 证 中 使 用 了 四 个 主 要 协 议 检 验 器， 其 中 包 括 DesignWare 中 的 PCI VIP AIP， 还 有 定 制 的 三 个 协 议 监 测 器： CPU 接 口 协 议 检 验 器、 DDR SDRAM 协 议 检 验 器 和 内 部 交 叉 开 关 协 议 检 验 器。 在 确 定 模 块 边 界 时 需 要 考 虑 模 块 的 设 计 规 模 ， 边 界 上 输 入 信 号 的 复 杂 度 等 等 因 素。 例 如 在 龙 芯 2 系 统 芯 片 的 验 证 中 对 PCI target 的 验 证 中 我 们 采 用 的 模 块 分 割 如 图 IV 1。 正 是 由 于 良 好 的 模 块 划 分 使 得 验 证 过 程 进 行 比 较 顺 利 ，在 合 理 的 时 间 内 完 成 了 验 证 过 程。

图 IV 1PCI Slave 验 证 的 模 块 边 界 划 分

V. 运 行 结 果 与 分 析

Magellen 提 供 了 良 好 的 图 形 界 面 ， 可 以 方 便 的 进 行 操 作 和 维 护。 在 四 天 的 时 间 内 对 P C I 模 块 的 21 项 设 计 属 性 进 行 了 验 证， 证 明 了 20 项 设 计 属 性， 并 发 现 一 个 属 性 没 有 满 足。 Magellen 在 发 现 不 满 足 的 设 计 属 性 时 会 自 动 给 出 testbench 和 相 应 的 测 试 激 励， 用 来 生 成 反 例， 这 极 大 的 方 便 了 RTL 设 计 代 码 的 调 试 工 作。图 V 1 是 Magellan 给 出 的 违 反 该 属 性 的 一 个 反 例 的 波 形 图。

该 属 性 的 描 述 是： 一 旦 目 标 设 备 将 TRDY# 信 号 置 位， 直 至 数 据 周 期 结 束 不 能 改 变 TRDY# 信 号。（Neither the master nor the target can change its mind once it has committed to the current data transfer until the current data phase completes. (A data phase completes when IRDY# and [TRDY# or STOP#] are asserted.)，Section3.2.1，PCI Local BUS Specification）。 该 属 性 的 OpenVera Assertion 描 述 如 代码 V 1：

代码 V 1 Assertion 代 码 的 一 个 例 子

通 过 波 形 图 我 们 可 以 发 现 在 数 据 周 期 没 有 结 束 时 目 标 设 备 改 变 了 TRDY# 信 号 的 值， 设 计 者 可 以 快 速 的 定 位 错 误 的 原 因， 从 而 改 正 设 计 的 逻 辑 错 误。 而 该 错 误 在 使 用 基 于 动 态 模 拟 仿 真 的 验 证 方 法 时 并 没 有 发 现。 如 果 希 望 在 模 拟 仿 真 时 重 现 该 错 误， 则 需 要 花 费 更 多 的 时 间 和 人 力。

VI. 结 论 和 未 来 工 作

使 用 断 言 描 述 设 计 的 功 能 属 性 同 时 使 用 Megallen 进 行 形 式 化 验 证 ， 是 龙 芯 2 系 统 芯 片 设 计 验 证 采 用 的 新 流 程， 事 实 证 明 该 流 程 减 少 了 验 证 工 作 量， 提 高 了 验 证 质 量 。 对 于 使 用 传 统 的 基 于 动 态 模 拟 仿 真 的 验 证 方 法 提 供 很 好 的 互 补。

可 验 证 性 设 计 (Design For Verification: DFV) 是 当 今 的 设 计 验 证 领 域 的 一 个 重 要 方 展 方 向， 而 在 设 计 初 期 就 加 入 assertion 描 述 设 计 属 性 是 可 验 证 性 设 计 的 一 个 重 要 方 法。 使 用 Megallen 进 行 基 于 断 言 的 形 式 化 验 证 也 将 成 为 主 要 的 ASIC 功 能 验 证 方 法 之 一，从 而 被 广 大 的 验 证 工 程 师 接 受。

附 录 1 PCI Target 形 式 验 证 的 Magellan 工 程 文 件

##

## Magellan Project: project1

##

define_project project1\

-simulator vcs\

-format verilog

## Design ############################################################

define_design mytop\

-topModule mytop

set_design_info -vcs {

+incdir+../verilog -y ../verilog +libext+.v ../dummy/mytop.v

../dummy/wbdummy.v

}

## Environment(s) ####################################################

## Environment: env1

define_env env1

set_env_reset env1\

-xOverride 1\

-taskFormat verilog

add_env_info env1\

-simOptions {

-ova_quiet

}

add_env_port env1 -name clk_in -clock 100

add_env_port env1 -name reset_in -reset 0

add_env_port env1 -name reset_in -constant 1

add_env_block env1 -name SnpsPciCommonExpressions\

-files {

/home/whan/magellan/ict/pci/mg/ova/SnpsPciCommonExpressions.ova

/home/whan/magellan/ict/pci/mg/ova/SnpsPciCoverage.ova

/home/whan/magellan/ict/pci/mg/ova/SnpsPciMasterChecker.ova

/home/whan/magellan/ict/pci/mg/ova/SnpsPciTargetChecker.ova

} -format ova -simAlways

add_env_block env1 -name masterbind\

-files {

/home/whan/magellan/ict/pci/mg/bind/masterbind.ova

/home/whan/magellan/ict/pci/mg/bind/targetbind.ova

} -format ova -simAlways

## Coverage Module(s) ################################################

## Coverage: target_cov

define_coverage target_cov

add_coverage_info target_cov\

-scope {

mytop.TC1.SnpsPciCov*

}

## Property Module(s) ################################################

## Property: trial1_constraint

define_property trial1_constraint

add_property_info trial1_constraint -constraint -scope { mytop.MC1.c_SnpsPciMP54_GRANTED_MASTER_CAN_START_THE_TRANSFER \

mytop.MC1.c_SnpsPciMP18_NO_MASTER_ABORT_BEFORE_FIVE_CLKS_FROM_FRAME \

mytop.MC1.c_SnpsPciMP09_NO_RESERVED_BURST_ORDERING_AD_1_1 \

mytop.MC1.c_SnpsPciMP02_ALL_BE_ASSERTED_FOR_MEM_WR_INV \

mytop.MC1.c_SnpsPciMP36_DEASSERT_FRAME_ONCE_STOP_ASSERTED \

mytop.MC1.c_SnpsPciMP13b_NO_BE_CHANGE_UNTIL_DP_COMPLETE \

mytop.MC1.c_SnpsPciMP08_NO_RESERVED_BURST_ORDERING_AD_0_1 \

mytop.MC1.c_SnpsPciMP55_IDSEL_CAN_BE_ASSERTED_FOR_CFG_TRANSFER \

mytop.MC1.c_SnpsPciMP18_END_THE_TRANSFER_AFTER_FIVE_CLKS \

mytop.MC1.c_SnpsPciMP33_NO_DAC_IF_UPPER_ADDR_IS_ZERO \

mytop.MC1.c_SnpsPciMP11a_VALID_ADDR_DURING_ADDR_PHASE \

mytop.MC1.c_SnpsPciMP35a_VALID_CMD_DURING_ADDR_PHASE \

mytop.MC1.c_SnpsPciMP06_IRDY_0_NO_CHANGE_FRAME_TILL_DP_END \

mytop.MC1.c_SnpsPciMP32_FRAME_ASSERTED_DURING_2ND_ADDR_PHASE_OF_DAC \

mytop.MC1.c_SnpsPciMP14_FRAME_DEASSERT_ONLY_WITH_IRDY \

mytop.MC1.c_SnpsPciMP52_KEEP_IRDY_FRAME_1_AT_POSEDGE_RST \

mytop.MC1.c_SnpsPciMP37_DEASSERT_IRDY_AFTER_COMPLETION \

mytop.MC1.c_SnpsPciMP19_REPEAT_TRANSFER_AFTER_RETRY \

mytop.MC1.c_SnpsPciMP13a_VALID_AD_1_0_C_BE_COMB_FOR_IO \

mytop.MC1.c_SnpsPciMP07_IRDY_0_NO_CHANGE_IRDY_TILL_DP_END \

mytop.MC1.c_SnpsPciMP46_NO_DAC_JUST_AFTER_DAC \

mytop.MC1.c_SnpsPciMP23_MASTER_LATENCY_8_CLKS \

mytop.MC1.c_SnpsPciMP17_NO_MASTER_ABORT_IF_DEVSEL_ASSERTED \

mytop.MC1.c_SnpsPciMP34_DEASSERT_REQ_FOR_2_CLK_AFTER_RETRY_OR_DISCON \

mytop.MC1.c_SnpsPciMP03_LINEAR_INCR_BURST_MODE_FOR_MEM_WR_INV \

mytop.MC1.c_SnpsPciMP49_64_BIT_ADDR_ONLY_FOR_MEM_TRANSFER \

mytop.MC1.c_SnpsPciMP35b_VALID_CMD_DURING_ADDR_PHASE \

mytop.MC1.c_SnpsPciMP53_NO_IRDY_WITHOUT_START_OF_TRANSFER \

mytop.MC1.c_SnpsPciMP47_NO_IRDY_DURING_ADDR_PHASE \

mytop.MC1.c_SnpsPciMP05_DATA_TRANSFER_ONLY_WHEN_BOTH_TRDY_AND_IRDY \

mytop.MC1.c_SnpsPciMP29_DRIVE_VALID_PAR \

}

## Property: tp05

define_property tp05

add_property_info tp05 -checker -scope { mytop.TC1.c_SnpsPciTP05_ONCE_TRDY_0_NO_CHANGE_ON_TRDY_TILL_DP_END \

}

## Property: tp20

define_property tp20

add_property_info tp20 -checker -scope { mytop.TC1.c_SnpsPciTP20_NO_TRDY_STOP_DEVSEL_ACK64_AFTER_COMPLETION \

}

## Property: tp_all_22v

define_property tp_all_22v

add_property_info tp_all_22v -checker -scope { mytop.TC1.c_SnpsPciTP21_DISCONNECT_WHEN_BURST_CROSSES_RESOURCE_BOUNDARY \

mytop.TC1.c_SnpsPciTP16_DISCONNECT_IF_RESERVED_BURST_MODE \

mytop.TC1.c_SnpsPciTP03_NO_ALIAS_FOR_RESERVED_CMDS \

mytop.TC1.c_SnpsPciTP29_DEVSEL_REMAIN_ASSERTED_TILL_END \

mytop.TC1.c_SnpsPciTP07_ONCE_TRDY_0_NO_CHANGE_ON_STOP_TILL_DP_END \

mytop.TC1.c_SnpsPciTP20_NO_TRDY_STOP_DEVSEL_ACK64_AFTER_COMPLETION \

mytop.TC1.c_SnpsPciTP11_DATA_TRANSFER_ONLY_WHEN_BOTH_TRDY_AND_IRDY \

mytop.TC1.c_SnpsPciTP32_DRIVE_VALID_PAR \

mytop.TC1.c_SnpsPciTP24_DEASSERT_TRDY_BEFORE_TARGET_ABORT \

mytop.TC1.c_SnpsPciTP08_ONCE_STOP_0_NO_CHANGE_ON_STOP_TILL_DP_END \

mytop.TC1.c_SnpsPciTP10_ONCE_STOP_0_NO_CHANGE_ON_DEVSEL_TILL_DP_END \

mytop.TC1.c_SnpsPciTP23_ONCE_ASSERTED_STOP_REMAINS_TILL_END \

mytop.TC1.c_SnpsPciTP05_ONCE_TRDY_0_NO_CHANGE_ON_TRDY_TILL_DP_END \

mytop.TC1.c_SnpsPciTP19_NO_TRDY_DURING_TURN_AROUND_OF_READ \

mytop.TC1.c_SnpsPciTP28_DEVSEL_BEFORE_ANY_OTHER_RESPONSE \

mytop.TC1.c_SnpsPciTP25_DEASSERTED_STOP_THEN_NO_CONTINUE \

mytop.TC1.c_SnpsPciTP06_ONCE_TRDY_0_NO_CHANGE_ON_DEVSEL_TILL_DP_END \

mytop.TC1.c_SnpsPciTP30_NO_RESPONSE_TO_SPECIAL_CYCLES \

mytop.TC1.c_SnpsPciTP09_ONCE_STOP_0_NO_CHANGE_ON_TRDY_TILL_DP_END \

mytop.TC1.c_SnpsPciTP26_INITIAL_TGT_LATENCY_16_CLOCK_CYCLES \

}

## Session Module(s) ################################################

## Session: s_tp05

define_session s_tp05\

-env env1

set_session_info s_tp05 \

-debugLog 1

add_session_info s_tp05\

-property {

trial1_constraint

tp05

}

## Session: s_tp20

define_session s_tp20\

-env env1

add_session_info s_tp20\

-property {

tp20

trial1_constraint

}

## Session: s_tpall

define_session s_tpall\

-env env1

add_session_info s_tpall\

-property {

trial1_constraint

tp_all_22v

}

## Session: s_target_cov

define_session s_target_cov\

-env env1

add_session_info s_target_cov\

-coverage {

target_cov

}\

-property {

trial1_constraint

}

附 录 2 20 个 被 Magellan 验 证 的 属 性 报 告

Magellan 在 验 证 结 束 之 后 可 以 给 出 一 个 HTML 格 式 的 报 告，下 图 是 其 中 的 一 页，显 示 在 这 次 验 证 中， 有 31 个 属 性 作 为 Constraints, 20 个 属 性 被 证 明 是 正 确 的。

单 击 链 接 可 以 得 到 更 详 细 的 信 息， 例 如 单 击 被 证 明 的 20 个 属 性， 则 可 以 得 到 如 下 图 所 示 的 结 果：

单 击 Browse 还 可 以 通 过 Virsim 或 者 Debussy 看 到 相 应 的 源 代 码。