scalableautomatedverificationviaexpert-systemguided可扩展的自动验证通过专家系统指导
26页1、Summer Formal 2011,Jason Baumgartner IBM Corporation,Hardware Verification,Homework and Lab,Homework 1: Netlist Modeling Exercises,1.1) Properties are specially annotated as “outputs“ in the AIGER format. However, there are no special ways to annotate “constraints“. How may the netlist be manipulated to allow constraints be reflected in an AIGER netlist?,assume (busy not req_valid),Homework 1: Netlist Modeling Exercises,1.2) Latches are assumed to have constant-0 initial value in the AIGER form
2、at. Assume you wish to initialize a set of latches to an arbitrary one-hot state: i.e., exactly one of them will be active at any point in time. How may this be represented in the netlist?,0 0 0,assertable?,Homework 1: Netlist Modeling Exercises,1.3) Certain types of logic functions such as multipliers are very difficult to reason about using bit-level algorithms. “Uninterpreted functions“ are sometimes used to facilitate the verification of designs with such functions, wherein two instances of
3、a particular function (e.g., one in the implementation and one in a reference model) are replaced with nondeterministic behavior. In particular, these two instances are each replaced by a multiplexor: if the arguments to the abstracted functions are identical, the same nondeterminstic values are sensitized through both multiplexors. Otherwise, different nondeterminstic values are sensisized through. Uninterpreted functions are useful when the correctness of the verification task is not dependent
4、 upon the precise values produced from the abstracted functions; only the *consistency* of identical results being produced under identical arguments is relevant. When verifying sequential netlists, a challenge with using uninterpreted functions is that the function pairs to be abstracted may be receive their arguments at different points in time. I.e., the implementation may be pipelined hence the timing with which it receives relevant arguments may not match the un-pipelined reference model. H
《scalableautomatedverificationviaexpert-systemguided可扩展的自动验证通过专家系统指导》由会员tian****1990分享,可在线阅读,更多相关《scalableautomatedverificationviaexpert-systemguided可扩展的自动验证通过专家系统指导》请在金锄头文库上搜索。
2018-2019学年八年级历史上册 第3单元 新民主主义革命的兴起 第12课 国民革命导学案北师大版
2018-2019学年八年级历史上册 第六单元 中华民族的抗日战争 第21课 敌后战场的抗战导学案(新人教版
2018-2019学年八年级历史上册 第1单元 民族危机与晚晴时期的救亡运动 第1课 鸦片战争导学案2北师大版
2018-2019学年八年级历史上册 第2单元 辛亥革命与中华民国的建立 第8课 辛亥革命导学案北师大版
2018-2019学年八年级历史上册 第六单元 中华民族的抗日战争 第20课 正面战场的抗战导学案(新人教版
2018-2019学年八年级历史上册 第2单元 辛亥革命与民族觉醒 第10课 新文化运动导学案华东师大版
2018-2019学年八年级历史上册 第2单元 辛亥革命与民族觉醒 第8课 袁世凯称帝与军阀混战导学案2华东师大版
2018-2019学年八年级历史上册 第4单元 中华民族的抗日战争 第14课 民族危机的空前严重导学案华东师大版
2018-2019学年八年级历史上册 第五单元 从国共合作到国共对峙 第17课 中国工农红军长征导学案(新人教版
2018-2019学年八年级历史上册 第1单元 民族危机与晚晴时期的救亡运动 第5课 中日甲午战争导学案1北师大版
2018-2019学年八年级历史上册 第2单元 辛亥革命与民族觉醒 第8课 袁世凯称帝与军阀混战导学案1华东师大版
2018-2019学年八年级历史上册 第1单元 民族危机与晚晴时期的救亡运动 第5课 中日甲午战争导学案2北师大版
2018-2019学年八年级历史上册 第1单元 民族危机与晚晴时期的救亡运动 第1课 鸦片战争导学案1北师大版
2018-2019学年八年级历史上册 第2单元 辛亥革命与中华民国的建立 第10课 新文化运动导学案北师大版
2018-2019学年八年级历史上册 第1单元 民族危机与晚晴时期的救亡运动导学案北师大版
2018-2019学年八年级物理上册 第二章 第1节 声音的产生与传播导学案 (新版)新人教版
2018-2019学年八年级地理上册 第四章 第三节 工业的分布与发展(第1课时)学案(新版)新人教版
2018-2019学年八年级物理上册 第二章 第2节 声音的特性导学案 (新版)新人教版
2018-2019学年八年级地理上册 3.3 中国的水资源教学案(新版)湘教版
2018-2019学年八年级物理上册 第三章 第3节 汽化和液化(第1课时 汽化)导学案 (新版)新人教版
2024-04-11 25页
2024-04-11 37页
2024-04-11 28页
2024-04-11 31页
2024-04-11 36页
2024-04-11 29页
2024-04-11 22页
2024-04-11 27页
2024-04-11 34页
2024-04-11 32页