4
rsta.royalsocietypublishing.org Phil.Trans.R.Soc.A375:20150399
.........................................................
CLI similarly tested the FM9001 microprocessor model against the fabricated gate array and
tested the MC68020 model against a Sun 3 workstation. Since all of these models were moderately
large Lisp systems, execution efficiency was very important. To quote again from [5,p.9]:
Note that the post-fabrication testing of verified devices changes the role of model
execution. Heretofore execution was merely an efficient way to avoid ‘premature’
proof attempts. ... But the post-fabrication testing of a verified device is not a purely
mathematical question. On the one hand one has a physical object. On the other one
has a mathematical expression. The question is whether the behavior of the object is
accurately predicted by the mathematical expression. The behavior of the object can only
be manifested by giving it concrete data and observing its concrete output. Thus, one is
forced to give concrete data to the mathematical expression and derive its concrete output.
... Often, at least for devices for which verification is needed, the required computations
are so large and the test cases so numerous that we expect the efficiency with which the
model can be executed becomes an important issue.
The performance challenges raised by the use of Nqthm in the CLI Stack and MC68020
projects prompted Boyer, Moore and (soon thereafter) Kaufmann to begin creating ACL2 in the
late 1980s. Performance was a key driver in our attempts to connect this work to commercial
efforts, and it was a tremendous asset to define ACL2 as a superset of a substantial subset of the
widely supported Common Lisp language. This design decision enables all ACL2 functions to
be compiled by off-the-shelf Common Lisp compilers, so that ACL2 programs can be run with
commercial-class speed and capacity.
This speed and capacity has been a tremendous advantage for our work on commercial-size
models. A key development was the ‘deep embedding’ of our hardware description language
(HDL) into the logic of NQTHM and later, ACL2, which we first used in the NQTHM-based
verification of the FM9001 [6] gate-level design. Our HDL was sufficiently similar to commercial
HDLs (e.g. LSI Logic’s NDL and Verilog) to permit automatic translation of (subsets of)
commercial HDLs into our ACL2-based HDL. The resulting ACL2-based representation enabled
not only efficient simulation of the design (as is done with commercial simulators), but also
reasoning about the design using the ACL2 prover. Today, Centaur and Oracle represent designs
of interest by translating them from vendor-specific implementation formats into an ACL2-based
HDL, and then use ACL2 to specify and prove properties about their designs.
The process just described is used by companies to analyse very large systems. For instance,
at Centaur Technology the Verilog specification of one of their products is more than 700 000 lines
in length; this design can be translated (by our ACL2-based Verilog-to-ACL2 translator) into our
ACL2-specified HDL in just a few minutes. Once translated, Centaur runs thousands of proof
scripts daily to check tens of thousands of properties of Centaur’s evolving design. Later (in §6)
we elaborate on the use of this approach by engineers at Centaur.
3. Initial industrial demonstrations
By 1993, CLI was ready to try ACL2 on industrial verification projects. Finding suitable projects
was primarily the responsibility of Warren Hunt, CLI’s Vice President for Hardware Engineering.
The first project was the modelling and verification of a Motorola digital signal processor, the
Motorola Complex Arithmetic Processor (CAP) DSP. CLI’s involvement in the project started in
late 1993, with Bishop Brock relocating from CLI’s home in Austin, TX, to Phoenix, AZ, to work
with the Motorola Government Systems’ DSP design team. The formal methods project lasted 31
months. In the end, ACL2 was used to model the processor and its microcode and to verify that
the microcode semantics was correctly implemented. The most significant contribution was the
identification of over 50 ‘pipeline hazards’, the coding of a Lisp (ACL2) function for recognizing
those hazards, and the proof that the absence of those recognized hazards implied accurate
execution of the microcode. The compiled hazard detection predicate was used to identify hazards
Downloaded from https://royalsocietypublishing.org/ on 23 August 2021
剩余19页未读，继续阅读
jiankangshiye
- 粉丝: 72
- 资源: 109
我的内容管理
展开
最新资源
- 最优条件下三次B样条小波边缘检测算子研究
- 深入解析：wav文件格式结构
- JIRA系统配置指南：代理与SSL设置
- 入门必备：电阻电容识别全解析
- U盘制作启动盘：详细教程解决无光驱装系统难题
- Eclipse快捷键大全：提升开发效率的必备秘籍
- C++ Primer Plus中文版：深入学习C++编程必备
- Eclipse常用快捷键汇总与操作指南
- JavaScript作用域解析与面向对象基础
- 软通动力Java笔试题解析
- 自定义标签配置与使用指南
- Android Intent深度解析：组件通信与广播机制
- 增强MyEclipse代码提示功能设置教程
- x86下VMware环境中Openwrt编译与LuCI集成指南
- S3C2440A嵌入式终端电源管理系统设计探讨
- Intel DTCP-IP技术在数字家庭中的内容保护
资源上传下载、课程学习等过程中有任何疑问或建议，欢迎提出宝贵意见哦~我们会及时处理！
点击此处反馈
