• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Formal Methods in Computer-Aided Design, 2009. FMCAD 2009 >Formal verification of correctness and performance of random priority-based arbiters
【24h】

Formal verification of correctness and performance of random priority-based arbiters

机译：正式验证基于随机优先级的仲裁器的正确性和性能

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Arbiters play a critical role in the performance of electronic systems. In this paper, we describe a novel method to formally verify correctness and performance of random priority-based arbiters. We define a property of random number sequences, called Complete Random Sequence (CRS), to characterize bounded fairness properties of random number generators and random priority-based arbiters. We propose a three step verification method utilizing the notion of CRS to establish deadlock-free operation of the arbiters, and to accurately quantify the request-to-grant delays. The proposed verification method may additionally be leveraged to tune systems composed of random priority-based arbiters and pseudo-random number generators, such as linear feedback shift registers (LFSRs), for optimal performance. We have successfully applied the approach to verify a host of cache arbiters and interconnection network controllers of commercial microprocessors.
机译：仲裁员在电子系统的性能中起着至关重要的作用。在本文中，我们描述了一种新方法来正式验证基于随机优先级的仲裁器的正确性和性能。我们定义了一个随机数序列的属性，称为完全随机序列（CRS），以表征随机数生成器和基于随机优先级的仲裁器的有界公平性。我们提出了一种利用CRS概念的三步验证方法，以建立仲裁器的无死锁操作，并准确地量化请求授予的延迟。所提出的验证方法还可以用于优化由基于随机优先级的仲裁器和伪随机数生成器（例如线性反馈移位寄存器（LFSR））组成的系统，以实现最佳性能。我们已经成功地将该方法应用于验证商用微处理器的大量缓存仲裁器和互连网络控制器。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号