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

CPA-DA：从非正式规范到总线协议的 RTL 断言

• 批准号: 0811067
• 负责人: Kathryn Fisler
• 金额: $ 30万
• 依托单位: Worcester Polytechnic Institute
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2008
• 资助国家: 美国
• 起止时间: 2008-08-01 至 2012-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0811067&HistoricalAwards=false
• 关键词: CPA; DA; Informal; Specifications; RTL

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.

提案编号：0811067 PI name：Fisler，Kathi Title：CPA-DA：From Informal Specifications to RTL Assertions for Bus ProtocolsInstitution：Worcester Polytechnic InstituteHardware-verification engineers regularly use informal specification documents to develop formal behavioral descriptions（such as RTL assertions）for validating designs.非正式规范文档通过使用图表、表格和精心编写的散文的组合的描述和示例来呈现协议。相比之下，验证工件由工具消耗，并且需要精确的行为细节。从非正式文档生成验证工件是一项费力的手工任务。然而，由于非正式和正式表示之间存在固有的差距，因此将其自动化具有挑战性。 该建议的目的是部分自动化的RTL断言从非正式的总线协议规范的提取。 PI将开发一种新的中间语言来描述这些协议，反映非正式规范的结构和符号。 所设想的软件工具将产生（1）一个部分但可执行的正式模型从一个非正式的规范和（2）一组细节，人类工程师需要检查或提供。 在工程师修改模型以澄清这些细节之后，工具将从精炼的正式模型生成验证工件。 这个过程将工程师的精力集中在缩小非正式规范和正式规范之间的差距上，这个任务实际上需要人工干预，而不是当前手动过程中更平凡的转录任务。如果这个项目成功，它将产生一个更轻量级的过程，用于从非正式规范创建所需的验证工件。 这反过来又会简化验证过程本身，这是硬件设计中越来越耗时但又至关重要的部分。 由于验证已成为硬件设计中的瓶颈，该项目有可能改善现代硬件开发实践。 此外，参与该项目的学生将获得在设计的非正式和正式表示之间的边界工作的技能。 随着信息技术用户的多样化，不再局限于那些受过该领域研究生培训的人，这种技能对研究人员越来越有价值。