题名 基于断言的验证方法在UART模块中的应用研究
被引量：7
1
作者
李洋洋 吴武臣 王龙伟 王宁 侯立刚
机构
北京工业大学集成电路与系统实验室
出处
《微电子学与计算机》
CSCD
北大核心
2010年第1期151-153,157,共4页
文摘
介绍了一种易于实现的基于断言的验证(ABV)方法,即经过5个步骤在设计文件中插入断言,使仿真器在仿真过程中监视设计中的关键功能点.该方法在UART的寄存器传输级(RTL)模型功能验证中的应用,实验中使用SVA描述设计属性.实验证明,这一方法提高了设计的可观察性,适用于数字集成电路功能验证.
关键词
可观察性 基于断言的验证 SVA UART
Keywords
observability assertion -based verification system verilog assertion （SVA） UART
分类号
TN4
[电子电信—微电子学与固体电子学]
题名 面向SOC芯片的跨时钟域设计和验证
被引量：5
2
作者
罗莉 何鸿君 徐炜遐 窦强
机构
国防科技大学计算机学院
出处
《计算机科学》
CSCD
北大核心
2011年第9期279-281,297,共4页
基金
863国家专项基金项目(2008AA01A202) 核高基重大专项(2009ZX01028-002-002)资助
文摘
随着高性能、低功耗芯片的发展,多时钟域和跨时钟域(Clock Domain Crossing,CDC)设计越来越多,CDC设计和验证越来越重要。阐述了5种常用的同步器设计模板。验证方法提出了层次化的验证流程:结构化检查,基于断言的验证(assertion-based verification,ABV),对关键模块进行形式化验证。CDC设计应用于研发的一款65nm工艺SOC芯片(最高主频1GHz、10个时钟域设计、多种工作模式),该芯片已流片回来。经测试,芯片的功能正确,说明设计和验证方法是完备的。
关键词
跨时钟域设计 基于断言的验证 PSL属性说明语言 符号模型检查 LTL线性时序逻辑
Keywords
Clock domain crossing design assertion -based verification PSL（Property Specification Language） Symbo-lic model checking LTL logic
分类号
TN402
[电子电信—微电子学与固体电子学]
题名 采用PSL的基于断言的验证
被引量：3
3
作者
马博 韩俊刚
机构
西安邮电学院计算机系
出处
《计算机工程》
CAS
CSCD
北大核心
2007年第2期217-219,共3页
基金
国家自然科学基金资助项目(90207015)
文摘
基于断言的验证方法被认为是在硬件设计验证方面的一次重大的方法学的变革。它能有效地提高验证工作的质量和效率。而性质描述语言(PSL)就是使用断言来表达要验证的性质,并且该语言已经被批准为IEEE标准。在简要介绍性质描述语言PSL的基础上,结合数字交叉连接芯片的实际设计验证工作,采用在Mentor Graphics公司出品的仿真软件ModelSim6.0,用PSL语言表述断言和验证命令,说明在设计中嵌入用断言表述的设计特性,通过这些特性来进行验证仿真工作。实验结果表明,用性质描述语言来辅助验证工作,是一个有效可行的方法。
关键词
基于断言的验证 性质描述语言 同步数字系列
Keywords
assertion -based verification Property specification language Synchronous digital hierarchy
分类号
TP391.9
[自动化与计算机技术—计算机应用技术]
题名 一种数字量的安全输入/输出模块的设计与实现
被引量：3
4
作者
陈海燕 穆建成 马连川
机构
北京交通大学轨道交通控制与安全国家重点实验室 铁道部科技司
出处
《铁路计算机应用》
2011年第8期54-56,共3页
基金
国家科技支撑计划项目:北京轨道交通核心技术CBTC研发及示范工程(2009BAG14B01)
文摘
本文在分析可扩展安全计算机平台实时性和安全性要求的基础上,提出基于可编程逻辑器件(FPGA)和时钟级同步2取2结构的安全输入/输出(安全I/O)模块的设计方法。深入阐述了安全I/O模块的硬件设计原理和基于PSL语言的断言验证方案。功能仿真和形式化验证结果说明了设计的正确性,同时在EDA开发平台上长时间稳定性的测试结果也证明了安全I/O模块的正确性和安全性。
关键词
轨道交通 信号设备 安全计算机平台 I/O模块 断言验证 超高速集成电
Keywords
rail transit signaling equipment safety computer platforms I/O assertion -based verification very-high-speed integrated circuit hardware description language（VHDL）
分类号
TP301.1
[自动化与计算机技术—计算机系统结构]
TP319
[自动化与计算机技术—计算机科学与技术]
题名 高性能DSP软核中DMA控制器的设计与验证
被引量：2
5
作者
郑挺 李勇
机构
国防科学技术大学计算机学院
出处
《计算机工程与设计》
CSCD
北大核心
2014年第1期112-118,共7页
基金
国家"核高基"重大专项(集成电路类)基金项目(2009ZX01034-001-001-006)
文摘
为解决数字信号处理器(digital signal processor,DSP)的数据供给问题,设计了一个可高效搬运数据的部件———直接存储器访问控制器(direct memory access controller,DMAC)。采用了模拟验证方法和基于断言的验证方法对设计进行了功能验证。传统的模拟验证方法目前仍是主流的功能验证方法,但基于断言的验证方法是今后集成电路验证的发展方向。模拟验证方法虽具有使用简单,不受设计规模影响的优点,却不能证明设计的完备性,而基于断言的验证方法虽具有验证完备性,但能够验证的设计规模有限。把两者结合起来,就能够发挥各自的优点。实验结果表明,把两者结合起来进行验证,确实能够提高验证质量。
关键词
数字信号处理器 直接存储器访问控制器 功能验证 模拟验证 基于断言的验证
Keywords
digital signal processor direct memory access controller functional verification simulation verification assertion -based verification
分类号
TP39
[自动化与计算机技术—计算机应用技术]
题名 基于PSL断言的宽带电路交换芯片验证
被引量：3
6
作者
张华 郭建 韩俊刚
机构
西安邮电学院ASIC设计中心
出处
《计算机工程》
CAS
CSCD
北大核心
2007年第14期216-218,235,共4页
基金
国家自然科学基金资助重大项目(90207015) 国家"863"计划基金资助重大专项课题"超大规模集成电路设计"(2003AA1Z1190)
文摘
利用基于PSL断言的验证方法验证了宽带电路交换芯片XYDXC160的设计。该芯片单片支持64路2.488Gb/s STM-16帧结构的SDH码流的输入/输出,实现1 024×1 024 STM-1流的无阻塞电路交换。断言技术的引入,降低了验证工作的复杂度,提高了验证的速度和效率,确保了验证工作的质量。
关键词
基于断言的验证 同步数字系列 性质描述语言
Keywords
assertion -based verification synchronous digital hierarchy（SDH） property specification language（PSL）
分类号
TN47
[电子电信—微电子学与固体电子学]
题名 DSP中存储保护单元的设计与断言验证
被引量：1
7
作者
肖海鹏 谢海情 汪东
机构
长沙理工大学物理与电子科学学院 湖南毂梁微电子有限公司
出处
《智能计算机与应用》
2020年第6期113-115,119,共4页
基金
湖南省教育厅基金资助科研项目(17B007) 长沙市科技计划重点项目(kq1901102)。
文摘
针对X-DSP存储空间的访问安全问题,本文采用硬件保护原理设计了一个存储保护单元,通过检查访问请求属性是否安全来决定是否允许未授权用户访问存储保护区域,从而实现存储空间的数据保护功能。采用System Verilog Assertions编写存储保护单元的功能属性描述,并采用断言验证方法完成存储保护单元的形式化验证。在X-DSP芯片验证环境下,采用FPGA原型验证,完成存储保护单元的功能测试。结果表明,存储保护单元实现了X-DSP存储空间的数据保护,防止非法程序破坏安全空间,阻止未经授权的用户访问存储空间。另外,断言验证方法保证了功能验证的完备性,从而缩短了产品开发周期。
关键词
存储保护单元 断言验证 DSP 功能验证
Keywords
memory protection unit assertion -based verification digital signal processor formal verification
分类号
TP39
[自动化与计算机技术—计算机应用技术]
题名 芯片设计形式验证
被引量：3
8
作者
詹博华 吴志林
机构
中国科学院软件研究所计算机科学国家重点实验室
出处
《前瞻科技》
2023年第1期23-32,共10页
基金
国家重点研发计划(2021ZD0113300)。
文摘
芯片设计验证是对芯片设计是否正确与安全进行检查,在芯片设计流程中具有非常重要的地位,占其将近1/2的成本和时间。形式验证是保证计算机软硬件系统正确性与安全性的非常重要的手段,已经成功用于芯片设计验证。全世界三大电子设计自动化(EDA)软件厂商Cadence、Synopsis、Siemens的EDA软件均包含成熟的芯片设计形式验证工具。文章总结了芯片设计形式验证发展现状,分析了面临的挑战,展望了发展趋势,并对其在中国的发展提出建议。
关键词
芯片设计 正确性与安全性 电子设计自动化 等价性验证 基于断言的形式验证 命题逻辑可满足性(SAT)求解 模型检测
Keywords
circuit design correctness and safety electronic design automation equivalence checking assertion -based formal verification satisfiability problem(SAT)solving model checking
分类号
TN402
[电子电信—微电子学与固体电子学]
题名 存储系统功能验证方法浅析
9
作者
刘洪锦 姚荣
机构
上海交通大学计算机科学与工程系 江南计算技术研究所
出处
《计算机工程》
CAS
CSCD
北大核心
2004年第B12期457-459,462,共4页
文摘
IC日益增长的设计复杂性和在时间、代价方面的需求,使得验证工作很重要却又困难重重。传统的简单验证方法和手段已不能满足 要求,采用新的验证方法势在必行。以存储系统功能性的验证为例,介绍了目前流行的先进的验证方法.包括ABV(Assertion-based verification)和TBV(Transaction-based verification)。对ASIC芯片的一般功能验证流程也作了较为详尽的分析。
关键词
存储系统 功能验证 ABV TBV
Keywords
Memory system Functional verification assertion -based verification (ABV) Transaction-based verification (TBV)
分类号
TP333
[自动化与计算机技术—计算机系统结构]
题名 基于断言的WISHBONE到AHB转换桥验证
被引量：1
10
作者
张挺 陈岚 冯燕
机构
中国科学院微电子研究所
出处
《微电子学与计算机》
CSCD
北大核心
2012年第6期150-152,157,共4页
文摘
随着集成电路设计复杂程度的不断提高.功能验证越来越受到重视.一种新兴的验证方法,基于断言的验证,得到越来越广泛的应用.介绍了基于断言的验证方法.及其在WISHBONE到AHB转换接口验证中的应用,总结了断言验证在功能验证中的优势和特点.
关键词
WISHBONE AHB 总线时序 SystemVerilog断言 基于断言的验证
Keywords
WISHBONE AHB bus timing SystemVerilog assert iom assertion -based verification
分类号
TN47
[电子电信—微电子学与固体电子学]
题名 属性说明语言在基于断言的硬件验证中的应用
被引量：4
11
作者
刘有耀 韩俊刚
机构
西安邮电学院ASIC设计中心
出处
《微电子学与计算机》
CSCD
北大核心
2006年第5期109-111,114,共4页
基金
国家自然科学基金项目(90207015)
文摘
EDA界的标准化组织Accellera最近确定IBM的sugar语言为标准的属性说明语言,可以用于基于断言验证技术的设计属性说明。文章首先介绍了基于断言验证的基本概念和属性说明语言PSL的用途和属性定义。然后给出了用PSL实现基于断言的硬件验证方法。用一个实例说明了怎样用PSL语言实现基于断言的验证。
关键词
硬件电路 属性说明语言 基于断言验证
Keywords
Hardware circuit, Property specification language, assertion based verification
分类号
TP302
[自动化与计算机技术—计算机系统结构]
题名 PSL逻辑及验证技术研究进展与展望
被引量：3
12
作者
虞蕾 赵宗涛
机构
国防科学技术大学计算机学院 第二炮兵工程学院计算机系
出处
《计算机应用研究》
CSCD
北大核心
2010年第7期2414-2420,共7页
基金
国家"863"计划资助项目(2007AA010301) 中国博士后科学基金资助项目(20080431401)
文摘
在简要介绍PSL的分层结构和语法与语义基础上,综述了PSL验证技术的应用研究现状,分析了各种方法、技术的优缺点,最后指出了PSL验证技术的未来研究展望。
关键词
属性规约语言 基于断言的验证 形式化验证 运行时验证
Keywords
PSL（property specification language） ABV（assertion based verification ） formal verification run-time verification
分类号
TP301
[自动化与计算机技术—计算机系统结构]
题名 硬件电路的属性说明语言
13
作者
刘有耀
机构
西安邮电学院ASIC设计中心 陕西西安
出处
《现代电子技术》
2005年第20期35-37,共3页
基金
国家自然科学基金(90207015)
文摘
传统的对系统功能规范说明都是采用自然语言,这种说明形式一般都是比较含糊的,并且由于缺乏标准的机器可执行代码而无法进行验证。本文介绍的属性说明语言(PSL)是一种易于读写、语法精简、语义严格清晰、表达能力强大、机器可执行的标准硬件设计属性说明语言。并对他在M ode ls im SE 6.0仿真工具中的使用做了具体的介绍。
关键词
硬件电路 属性说明语言 基于断言验证 自然语言
Keywords
hardware circuit property specification language assertion based verification natural language
分类号
TP312
[自动化与计算机技术—计算机软件与理论]
题名 基于性质描述语言的硬件验证
14
作者
纪小辉 郭建
机构
西安工业大学光电工程学院 西安邮电学院计算机科学系
出处
《科学技术与工程》
2010年第23期5652-5656,共5页
文摘
性质描述语言（Property Specification Language）为描述硬件设计的属性提供了一种标准语言,基于断言的验证方法为硬件的设计和验证提出了一种新的很具有优势的验证方法。用性质描述语言作为断言的验证方法中描述断言的语言,使得断言能够被语法精简、语义严格清晰地描述出来。通过对先进先出队列存储器的设计和断言的描述,以及对断言的验证结果的描述,给出了如何利用性质描述语言写断言的一般方法,然后再进行模拟仿真,找出使断言失败的原因,以便找出设计的错误,并验证了本方法在硬件验证中的有效性。
关键词
性质描述语言 断言的验证 先进先出队列存储器
Keywords
property specification language assertion based verification first in first out
分类号
TP317.2
[自动化与计算机技术—计算机软件与理论]
