A Typing Discipline for Hardware Interfaces
A Typing Discipline for Hardware Interfaces
复制标题
硬件接口的打字规则
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
W. Vanderbauwhede
中科院分区：
文献类型：
--
作者：
Jan de Muijnck;W. Vanderbauwhede
现代片上系统（SoC）由IP（知识产权）核组成，这些IP核之间的通信由良好描述的交互协议管理。然而，在这些协议的机器可读规范与它们在已知硬件描述语言中的实现的验证之间存在脱节。虽然可以编写工具来解决这种关注点分离，但工具通常是手写的，用于事后检查硬件设计。我们已经开发了一个依赖的类型系统和概念验证建模语言的原因，硬件接口的物理结构，使用用户提供的描述。我们的类型系统提供了正确的构造保证，如果IP Core上的接口符合指定的标准，则它们将是良好类型的。
Modern Systems-on-a-Chip (SoC) are constructed by composition of IP (Intellectual Property) Cores with the communication between these IP Cores being governed by well described interaction protocols. However, there is a disconnect between the machine readable specification of these protocols and the verification of their implementation in known hardware description languages. Although tools can be written to address such separation of concerns, the tooling is often hand written and used to check hardware designs a posteriori. We have developed a dependent type-system and proof-of-concept modelling language to reason about the physical structure of hardware interfaces using user provided descriptions. Our type-system provides correct-by-construction guarantees that the interfaces on an IP Core will be well-typed if they adhere to a specified standard.