首页> 外文OA文献 >Formal models of cache coherent communication fabrics: from micro-architectures to RTL designs
【2h】

Formal models of cache coherent communication fabrics: from micro-architectures to RTL designs

机译:缓存一致性通信结构的正式模型:从微体系结构到RTL设计

代理获取
本网站仅为用户提供外文OA文献查询和代理获取服务,本网站没有原文。下单后我们将采用程序或人工为您竭诚获取高质量的原文,但由于OA文献来源多样且变更频繁,仍可能出现获取不到、文献不完整或与标题不符等情况,如果获取不到我们将提供退款服务。请知悉。

摘要

The xMAS primitives form a suitable basis for modelling interconnection networks, even nontrivial structures such as the Spidergon network. By implementing iterative and/or recursive modelling features in the supporting toolset (WickedXmas), a network can be constructed that remains generic in the number of nodes. Using a formally specified syntax for the equations in source, switch, function et cetera, the necessary packet routing decisions can be defined unambiguously. There remains a small amount of ambiguity in the expression language that should be addressed. Assumptions about the tacit resolution of identical data fields for multi-input primitives should be formalized in order to avoid different interpretations across toolchains. In conjuction with the generation of a flattened netlist and an automated translation to a simulation-capable language such as Verilog, the network can be verified. The generalisation of xMAS primitives to their n-input or -output equivalents is straightforward, with only minor remarks for the arbitration of n-input merges. A particular area where xMAS is lacking expressivity is pipelining. Using the k >= 2-deep queue primitives, data processing stages can be formed that are locally decoupled from each other using elastic buffers (FIFOs). When extending the notion of a queue to k = 1, however, pipelining becomes severely limited in bandwidth and cannot be used to model the typical register stages used in manually crafted digital logic. Combining the xMAS formalism with the SELF protocol used by Cortadella et al. could address this shortcoming. The xMAS primitives are not semantically complete and are lacking some expressivity that would be available when modelling directly in an underlying hardware description language. Shortcomings in expressivity that presented themselves during the design of the Write- Once example algorithm were addressed by the introduction of new primitives (ctrljoin, forkany, joitch, peek). Although not all of these will adhere to the persistence assumption, their existence is indicative that a more rigorous exploration of possible Boolean equations for control and data flow will give rise to additional useful primitives.
机译:xMAS原语为建模互连网络,甚至是诸如Spidergon网络之类的非平凡结构提供了合适的基础。通过在支持工具集(WickedXmas)中实现迭代和/或递归建模功能,可以构建在节点数量上保持通用的网络。对源,交换,功能等中的方程式使用正式指定的语法,可以明确定义必要的数据包路由决策。在表达语言中仍然存在少量歧义,应该解决。对于多输入基元,相同数据字段的默认解析的假设应形式化,以避免在整个工具链中出现不同的解释。结合生成扁平化的网表和自动转换为具有仿真功能的语言(例如Verilog),可以验证网络。 xMAS原语到其n输入或-output等价物的一般化很简单,仅对n输入合并的仲裁作了少量说明。 xMAS缺乏表达能力的特定领域是流水线。使用k> = 2的深队列原语,可以形成使用弹性缓冲区(FIFO)在本地彼此解耦的数据处理阶段。但是,当将队列的概念扩展到k = 1时,流水线将严重限制带宽,并且不能用于对手工制作的数字逻辑中使用的典型寄存器级进行建模。将xMAS形式主义与Cortadella等人使用的SELF协议结合起来。可以解决这个缺点。 xMAS原语在语义上并不完整,并且缺少某些表达能力,这些表达能力直接在底层硬件描述语言中进行建模时可用。通过编写新原语(ctrljoin,forkany,joitch,peek)解决了一次编写一次示例算法设计过程中表现出来的表现性缺陷。尽管并非所有这些方法都遵循持久性假设,但它们的存在表明对控制和数据流可能的布尔方程的更严格的探索将产生其他有用的原语。

著录项

  • 作者

    Vloed Hendrik De;

  • 作者单位
  • 年度 2016
  • 总页数
  • 原文格式 PDF
  • 正文语种 en
  • 中图分类

相似文献

  • 外文文献
  • 中文文献
  • 专利

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号