CPA-DA: From Informal Specifications to RTL Assertions for Bus Protocols

提案号：0811067PI名称：Fisler， kathittitle: CPA-DA：从总线协议的非正式规范到RTL断言机构：伍斯特理工学院硬件验证工程师通常使用非正式规范文档来开发用于验证设计的正式行为描述（如RTL断言）。非正式的规范文档通过使用图表、表格和精心编写的散文组合的描述和示例来呈现协议。相反，验证工件由工具消耗，并且需要精确的行为细节。从非正式文档生成验证工件是一项费力的手工任务。然而，考虑到非正式和正式表示之间的固有差距，将其自动化是具有挑战性的。该建议旨在部分自动化从非正式总线协议规范中提取RTL断言。PI将开发一种新的中间语言来描述这些反映非正式规范的结构和符号的协议。所设想的软件工具将产生(1)从非正式规范中生成部分但可执行的正式模型，以及(2)人类工程师需要检查或提供的一组细节。在工程师修改模型以澄清这些细节之后，工具将从精炼的正式模型中生成验证工件。这个过程将工程师的工作重点放在缩小非正式和正式规范之间的差距上，即实际需要人工干预的任务，而不是当前手动过程中更平凡的转录任务。如果这个项目是成功的，它将产生一个轻量级的过程，用于从非正式规范中创建所需的验证工件。这反过来将简化验证过程本身，这是硬件设计中越来越耗时但又至关重要的一部分。由于验证已成为硬件设计中的瓶颈，因此该项目具有改进现代硬件开发实践的潜力。此外，参与这个项目的学生将获得在设计的非正式和正式表示之间的边界工作的技能。随着信息技术用户的多样化，这些技能对研究人员来说越来越有价值，而不仅仅是那些在该领域受过研究生培训的人。

Proposal No: 0811067PI name: Fisler, KathiTitle: CPA-DA: From Informal Specifications to RTL Assertions for Bus ProtocolsInstitution: Worcester Polytechnic InstituteHardware-verification engineers routinely use informal specification documents to develop formal behavioral descriptions (such as RTL assertions) for validating designs. Informal specification documents present protocols through both descriptions and examples using a combination of diagrams, tables and carefully-written prose. Validation artifacts, in contrast, are consumed by tools and require precise behavioral details. Generating validation artifacts from informal documentation is a laborious manual task. Automating it, however, is challenging given the inherent gap between the informal and formal representations. This proposal aims to partially automate the extraction of RTL assertions from informal bus protocol specifications. The PI will develop a novel intermediate language for describing these protocols that reflects the structure and notations of informal specifications. The software tools envisioned will produce (1) a partial yet executable formal model from an informal specification and (2) a set of details that a human engineer needs to check or provide. After the engineer modifies the model to clarify these details, the tools will generate validation artifacts from the refined formal model. This process focuses the engineer's effort on closing the gap between the informal and formal specification, the task that actually requires human intervention, rather than on the more mundane transcription tasks in the current manual process.If this project is successful, it will yield a much lighter-weight process for creating needed validation artifacts from informal specifications. This in turn will simplify the validation process itself, an increasingly time-consuming yet critical part of hardware design. As validation has become a bottleneck in hardware design, the project has the potential to improve modern hardware development practice. Additionally, the students involved in this project will gain skills in working at the boundary between informal and formal representations of designs. Such skills are increasingly valuable for researchers as users of information technologies diversify beyond those with graduate training in the field.