CPA-CSA: Verification-Aware Microarchitecture
CPA-CSA: Verification-Aware Microarchitecture
批准号:
0811290
负责人:
Daniel Sorin
金额:
$22.0万
依托单位:
依托单位国家:
美国
项目类别:
Standard Grant
财政年份:
2008
资助国家:
美国
项目状态:
已结题
起止时间:
2008-09-01 至 2012-08-31
中文摘要
点击翻译按钮获取中文摘要
英文摘要
Microprocessor verification is a critical challenge for the computing industry. A design bug in a shipped processor chip can lead to failures and data corruptions, which can be catastrophic in many applications, such as medical equipment, avionics, and automotive control. Microprocessor design bugs can also be financially disastrous; the recall of Intel's Pentium, due to its notorious division bug, cost Intel approximately 420 million dollars. Society relies upon microprocessors, and thus the possibility of a flawedmicroprocessor is an enormous concern. Unfortunately, verifying a complex, modern microprocessor is extremely difficult. Due to both its difficulty and importance, verification consumes a large fraction (60-70%) of the resources--engineers, time, and money--devoted to the creation of a new microprocessor. Despite this effort, the most recent processors from Intel, AMD, and IBM have been shipped with dozens of documented design bugs.This research project addresses both society's need for correct microprocessor designs and industry's desire to improve product quality and shorten the design cycle, both of which can be achieved through a reduction in verification effort. The project's goal is to design microprocessors such that they can be more easily verified. To achieve this goal, this project will pursue three complementary research thrusts. The first thrust will analyze existing designs to identify features that require more verification effort than is merited by their benefits. The second thrust will re-design the waysin which microprocessor components interact, in order to reduce design complexity. The third thrust will develop sets of invariants that facilitate verification; there are often many ways to specify the correctness of a system, some of which are far easier to verify than others. The benefits of the proposed research are broader than its technical results, because of the importance of the verification problem to national infrastructure and industry. This project will also support training of undergraduate and minority students.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
SHF: Small: Transforming Computer Architecture Evaluation with Statistical Model Checking
-
批准号:2133160
-
项目类别:Standard Grant
-
资助金额:$50.0万
-
财政年份:2021
-
负责人:Daniel Sorin
-
依托单位:
SHF: Small: Automatic Generation of Cache Coherent Memory Systems for Multicore Processors
-
批准号:2002737
-
项目类别:Standard Grant
-
资助金额:$40.0万
-
财政年份:2020
-
负责人:Daniel Sorin
-
依托单位:
SHF: Small: Using Coding Theory to Optimize the Representation of Information in Computer Architecture
-
批准号:1421177
-
项目类别:Standard Grant
-
资助金额:$45.0万
-
财政年份:2014
-
负责人:Daniel Sorin
-
依托单位:
SHF:Small:Designing Architectures to be Formally Verifiable
-
批准号:1421167
-
项目类别:Standard Grant
-
资助金额:$34.0万
-
财政年份:2014
-
负责人:Daniel Sorin
-
依托单位:
SHF: Small: Shared Memory Architectures and Microarchitectures for Heterogeneous General-Purpose Chips
-
批准号:1216695
-
项目类别:Standard Grant
-
资助金额:$30.0万
-
财政年份:2012
-
负责人:Daniel Sorin
-
依托单位:
SHF: EAGER: FIESTA: A Sound Multi-Program Workload Methodology
-
批准号:1259028
-
项目类别:Standard Grant
-
资助金额:$13.45万
-
财政年份:2012
-
负责人:Daniel Sorin
-
依托单位:
SHF: Small: Commodity Processors with Mainframe Reliability
-
批准号:1115367
-
项目类别:Standard Grant
-
资助金额:$42.0万
-
财政年份:2011
-
负责人:Daniel Sorin
-
依托单位:
SHF: EAGER: FIESTA: A Sound Multi-Program Workload Methodology
-
批准号:1012008
-
项目类别:Standard Grant
-
资助金额:$18.85万
-
财政年份:2010
-
负责人:Daniel Sorin
-
依托单位:
CAREER: Improving Multiprocessor Availability with Dynamic Verification and Autonomic Operation
-
批准号:0444516
-
项目类别:Continuing Grant
-
资助金额:$40.0万
-
财政年份:2005
-
负责人:Daniel Sorin
-
依托单位:
FaultFinder: Improving the Availability of Multiprocessor Servers
-
批准号:0309164
-
项目类别:Standard Grant
-
资助金额:$11.44万
-
财政年份:2003
-
负责人:Daniel Sorin
-
依托单位:
国内基金
海外基金
登录
查看更多内容
活血定眩胶囊通过GSDMD-NT/ROS/NLRP3/Caspase-1轴调控线粒体损伤介导的细胞焦亡防治CSA的机制研究
-
批准号:
-
项目类别:地区科学基金项目
-
资助金额:34万元
-
批准年份:2024
-
负责人:宋敏
-
依托单位:
超声实时示踪巨噬细胞递送携带 CSA和 MTX 的靶向纳米颗
粒治疗肿瘤研究
-
批准号:2024JJ9321
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2024
-
负责人:龙湘党
-
依托单位:
严寒环境CaO@CaCO3“核壳”发热材料调控PC-CSA复合水泥体系热-力性能及稳定性研究
-
批准号:--
-
项目类别:青年科学基金项目
-
资助金额:30万元
-
批准年份:2022
-
负责人:张歌
-
依托单位:
Ag/PAAm-CSA水凝胶柔性电极用于胃黏膜消融和创面保护的机制研究
-
批准号:--
-
项目类别:青年科学基金项目
-
资助金额:30万元
-
批准年份:2022
-
负责人:任冯刚
-
依托单位:
CSA通过mTORC1和线粒体能量代谢途径调控肝组织再生的机制
-
批准号:
-
项目类别:省市级项目
-
资助金额:--
-
批准年份:2021
-
负责人:赵建军
-
依托单位:
CSA调控水稻光敏育性转换分子机制的研究
-
批准号:31970803
-
项目类别:面上项目
-
资助金额:57.0万元
-
批准年份:2019
-
负责人:张大兵
-
依托单位:
ABCB1甲基化水平调控T淋巴细胞内CsA浓度引起CsA药效学差异的研究
-
批准号:81803634
-
项目类别:青年科学基金项目
-
资助金额:21.0万元
-
批准年份:2018
-
负责人:李丹滢
-
依托单位:
“代谢-转运互作”介导槲皮素及其活性代谢物Q3GA调控CsA药动学的分子机制
-
批准号:81874326
-
项目类别:面上项目
-
资助金额:57.0万元
-
批准年份:2018
-
负责人:师少军
-
依托单位:
茶树叶片质膜H+-ATPase CsA1和CsA7在干旱胁迫与复水处理下调控钾稳态的功能研究
-
批准号:31800583
-
项目类别:青年科学基金项目
-
资助金额:27.0万元
-
批准年份:2018
-
负责人:张显晨
-
依托单位:
Bcl-2与PI3K/Akt/mTOR信号通路“串话”调控CSA血管内皮细胞自噬及活血定眩胶囊的干预机制研究
-
批准号:81760876
-
项目类别:地区科学基金项目
-
资助金额:38.0万元
-
批准年份:2017
-
负责人:宋敏
-
依托单位: