基于SMT求解器的微处理器指令验证数据约束生成技术.pdf
免费下载
计 算 机 研 究 与 发 展
DOI
:
１０．７５４４∕issn１０００Ｇ１２３９．２０２０．２０１９０７１８
JournalofCom
p
uterResearchandDevelo
p
ment ５７
(
１２
):
２６９４ ２７０２
,
２０２０
收稿日期
:
２０１９
－
１０
－
１１
;
修回日期
:
２０２０
－
０２
－
１３
基金项目
:
国家重点研发计划项目
(
２０１７YFB０２０２７０３
)
Thisworkwassu
pp
ortedb
y
theNationalKe
y
ResearchandDevelo
p
mentPro
g
ramofChina
(
２０１７YFB０２０２７０３
)
．
基于
SMT
求解器的微处理器指令验证数据约束生成技术
谭
坚
罗 巧 玲
王 丽 一
胡 夏 晖
范
昊
徐
占
(
江南计算技术研究所
江苏无锡
２１４０８３
)
(
tan
j
ian１３１＠１６３．com
)
DataConstraintGenerationTechnolo
gy
forMicro
p
rocessorInstruction
VerificationBasedonSMTSolver
TanJian
,
LuoQiaolin
g
,
Wan
g
Li
y
i
,
HuXiahui
,
FanHao
,
andXuZhan
(
Jian
g
nanInstituteo
f
Com
p
utin
g
Technolo
gy
,
Wuxi
,
Jian
g
su
２１４０８３
)
Abstract Durin
g
thedevelo
p
mentofthe
p
rocessor
,
itisnecessar
y
tofull
y
verif
y
theinstructions
data
p
aths．Theexistin
g
simulationverificationmethodshaveinsufficientfunctionalcovera
g
einterms
ofinstructionresulto
p
erandsconstraints
,
relationshi
p
constraintsbetweeno
p
erands
,
andinternal
constraintsofinstructions
,
etc．This
p
a
p
er
p
ro
p
osesaninstructionconstraintsolvin
g
methodbasedon
satisfiabilit
y
modulotheor
y
(
SMT
)
solver．TheSMTsolverisintroducedtoconverttheinstruction
function verification tasksinto constraintsatisfaction
p
roblems．Constraintsatisfaction
p
roblem
techni
q
uesareusedto
g
eneratevalidationtu
p
ledata
,
whichcan beusedtoverif
y
thefunctional
correctnessoftheinstructionsset．Themodelin
gp
rocessesandexam
p
lesare
g
iveninfouras
p
ects
:
the
instructionresulto
p
erandconstraints
,
theinstructiono
p
erandconstraints
,
theinstructioninternal
constraints
,
andfloatＧ
p
ointin
g
instructionso
p
erandconstraints．Inordertoim
p
rovethe modelin
g
efficienc
y
,
we
p
ro
p
osetwostrate
g
ies．First
,
oncethetimethresholdisreached
,
thecurrent
p
rocessis
terminated
;
second
,
usin
g p
rocess mana
g
ementand thread mana
g
ementtechnolo
gy
,
a
p
arallel
solutionframeworkforinstructionfunctionconstraintsisim
p
lemented
,
andaseriesofserialsolvin
g
tasksareassi
g
nedto multi
p
lethreadsthatcanbeexecutedin
p
arallel
,
andthes
p
eedofsolutionis
acceleratedundertheconditionsofthesameconstraintscovera
g
e．Ourex
p
eriencesshowthatunder
theri
g
htcircumstances
,
instructionconstraintsolvin
g
technolo
gy
basedonSMT
p
rovidestechnical
su
pp
ortfors
y
stemＧlevelfunctionalverificationtoachievetestcovera
g
eofcom
p
lexscenarios．
Ke
y
words instructionfunction
;
data
p
aths
;
constraintsolvin
g
;
SMTsolver
;
verificationdata
;
p
arallel
acceleration
摘
要
处理器研制过程中 需 要对 指 令算 术 数据 路 径进 行 覆盖 验 证
．
针对 现 有模 拟 验 证 方 法 存 在 的 不
足
,
提出了一种基于可满足模理论
(
satisfiabilit
y
modulotheor
y
,
SMT
)
的指令约束求解方法
:
利用可满
足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题
．
在结果操作数约束
、
操作数间约
束
、
指令内部约束以及浮点操作数约束
４
个方面分别给出示例
,
并分别给出了利用
SMT
求解器进行约
束建模的关键过程以及可以用于指令级功能验证的元组数据
．
为提高求解模型效率
,
提出了
２
种解决方
法
:
首先利用时间阈值实现问题求解超时即终止的策略
;
其次是结合进程管 理与线 程管理 技术
,
实现了
指令功能约束并行求解框架
,
将串行求解任务分 派给可 并行执 行的多 个线程
,
提高了 求解速 度
．
该技术
已成功应用于系统级验证中
,
有效提升了测试覆盖与质量
,
取得了很好的效益
．
关键词
指令功能
;
数据路径
;
约束求解
;
SMT
求解器
;
验证数据
;
并行加速
中图法 分类号
TP３１１
随着计算机体 系结 构 理论 与 技术 的 迅速 发 展
、
制造工艺水 平不 断提 升以 及集 成 电 路 设 计 日 趋 复
杂
,
行业内科研人员 设 计实 现 的处 理 器逻 辑 功能 变
得越来越复杂
,
对处理 器 测试 验 证质 量 的要 求 越来
越高
．
为保证 处 理 器 功 能 正 确 性
,
硬 件 设 计 人 员
、
验
证人员
、
系统软件测试 人 员甚 至 用户 都 或多 或 少会
承担着处理器 功 能 与 性 能 的 测 试 验 证 任 务
．
指 令 级
功能测试是处理器 正 确性 验 证的 重 要组 成 部分
,
贯
穿处理器研制过程 中 的各 个 阶段
,
在软 件 模拟 指 令
验证
、
FPGA
(
field
p
ro
g
rammable
g
atearra
y
)
实 物
验证
、
硬件模拟仿真验证以及
SoC
(
s
y
stemonchi
p
)
硅后验证等阶段都 需 要进 行 充分 验 证
;
指令 级 测试
方法具有通用性的特点
,
与具体的处理器类型无关
,
在专用处理 器与 通用 处理 器研 制 过 程 中 都 需 要 用
到
,
其实现方法依赖于指令语义
、
内部规范以及指令
上下文等
．
在开展指 令级功 能测试 的过程 中
,
我们发 现对
于测试方案所要求 覆 盖的 部 分特 殊 场景
,
采用 现 有
模拟验证方法较难达到目的
．
例如
,
当需要对单指令
的结果进行各种数 据 类型 的 遍历 验 证时
、
在约 定 浮
点操作数的中间结果 为 某特 定 数值 时
、
在约 定
２
个
操作数之间满足特定关系时尤其是约定输入操作数
与输出操作数之间 满 足特 定 的约 束 关系 时
,
采用 现
有主流的模拟验证方法
[
１
]
通常显得比较低效
．
此外
,
很多的指令功能是 隐 含一 些 特定 的 约束 关 系
,
如加
减法
、
乘法指 令运 算 时 存 在 进
、
借 位 情 况 发 生 的 可
能
．
这些内部关系对于测试人员来说不直接
,
部分约
束甚至需要处 理 器 设 计 人 员 协 助 制 定
．
采 用 现 有 模
拟方法
,
在制定测试验 证 计划 或 者生 成 测试 程 序的
时候很难全面覆盖
,
即使能够实现代价也比较大
．
以
上提及的场景都是 比 较常 见 的验 证 功能 点
,
要求 测
试人员必须覆盖
．
面对结果操作数与指令内部关系进行约束的验
证场景
,
如果采用功能模拟测试方法
,
通常需要测试
人员根据指令的语 义 模拟 出 该指 令 的相 反 语义
,
将
输出转换成模拟程 序 的输 入
,
反推 出 指令 的 输入 操
作数
,
形成验证元组数据
,
再根据验证数据生成相应
的指令测试激励
,
验证指令功能正确性
．
部分指令其
实是没有严格意义 对 应的 求 反过 程 的
,
例如 浮 点指
令
,
假若存在浮点操作 数
A
×
B
＝
C
,
但是 由 于舍 入
模式等原因
,
导致数据元组
A
,
B
,
C
在很多时候并
不满足
C
∕
B
＝
A
的关系
．
因此
,
对于系统测试人员而言
,
很多的待验证场
景采用现有的功能模 拟 等手 段 是比 较 难以 实 现的
;
即使采用算法模拟 成 功实 现
,
得到 验 证数 据 的运 行
时间通常较长
,
生成的数据量也比较有限
．
国内外处理器设计研发机构如
Intel
,
IBM
等公
司
,
为满足处理器特殊约束场景的验证需求
,
组织了
大量的科学家专门设计了满足各自处理器约束建模
需求的求解器
[
２Ｇ３
]
．
根据
IBM
公司官 网显示
,
以色 列
海法实验室 研 究 开发 出了
GEC
(
g
enerationcore
),
Stocs
,
Ma
g
e
等专用求解器
[
４
]
,
并在此基础上开发出
了
Genes
y
sＧPro
[
５
]
,
FP
g
en
[
６
]
等 一 系 列 系 统
,
很 好 地
满足了处理 器验 证过 程中 面临 的 各 种 功 能 验 证 需
求
．
由于这些求 解 器 的 实 现 与 处 理 器 内 部 设 计 细 节
紧密相关
,
因此这些 专 用求 解 器仅 限 在公 司 内部 以
及合作单位进行应用
．
由于与设计紧密关联并且需要参考模型等底层
环境和技术的支撑 配 合
,
目前 现 有以 功 能模 拟 为基
础的系统级测 试 很 难 全 面 覆 盖 带 约 束 的 待 测 场 景
．
很多带约束的待测场景对系统级测试人员来说是可
见的
,
因此将会使系 统测 试 在功 能 覆盖 方 面存 在 不
足
．
如果不加以覆盖
,
将会导致经过系统测试的目 标
处理器仍然存在设 计 错误 的 隐患
,
这对 处 理器 研 制
来说是不能容忍的
．
随着形式化技术的快速发展
,
我
们可以在系统级测 试 过程 中 引入 形 式化 方 法
,
对指
令约束关系描 述 并 建 模 求 解
．
在 验 证 场 景 与 处 理 器
功能测试覆盖任务 之 间建 立 可靠 的 技术 桥 梁
,
满足
工程实际需要
,
提升处理器验证测试质量
．
本文首先对一种形式化技术方法
———
可满足模
理论
(
satisfiabilit
y
modulotheor
y
,
SMT
)
[
７
]
进行简
要介绍
;
然后 提出 了一 种基 于
SMT
求 解 器 的关 系
约束求解技术
,
分别从指令结果操作数约束
、
操作数
相互关系约束
、
指令内 部 关系 约 束以 及 浮点 操 作数
５９６２
谭
坚等
:
基于
SMT
求解器的微处理器指令验证数据约束生成技术
of 9
免费下载
【版权声明】本文为墨天轮用户原创内容，转载时必须标注文档的来源（墨天轮），文档链接，文档作者等基本信息，否则作者和墨天轮有权追究责任。如果您发现墨天轮中有涉嫌抄袭或者侵权的内容，欢迎发送邮件至：contact@modb.pro进行举报，并提供相关证据，一经查实，墨天轮将立刻删除相关内容。
下载排行榜
评论