抽象 stobj 及其在 ISA 建模中的应用
计算机科学中的逻辑
2013-05-01 v1 硬件体系结构
符号计算
摘要
我们介绍了一项新的 ACL2 特性——抽象 stobj（abstract stobj），并展示了如何将其应用于微处理器指令集架构（ISA）的建模。与传统（“具体”）stobj 相比，抽象 stobj 的优势包括更快的执行速度、对符号模拟的支持、更高效的推理能力，以及在建模优化下证明开发过程的鲁棒性。
引用
@article{arxiv.1304.7858,
title = {Abstract Stobjs and Their Application to ISA Modeling},
author = {Shilpi Goel and Warren A Hunt, and Matt Kaufmann},
journal= {arXiv preprint arXiv:1304.7858},
year = {2013}
}
备注
In Proceedings ACL2 2013, arXiv:1304.7123