Collaborative Research: SHF: Small: Integrating Synthesis and Optimization in Satisfiability Modulo Theories

合作研究：SHF：小型：在可满足性模理论中集成综合和优化

基本信息

批准号：
2006542
负责人：
Timothy Sherwood
金额：
$ 21万
依托单位：
University of California-Santa Barbara
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-06-01 至 2023-05-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2006542&HistoricalAwards=false
关键词：
Collaborative Research SHF Small Integrating

项目摘要

The ever-increasing demand for optimized large-scale computing systems puts pressure on attaining significant improvements in automated design optimization and synthesis tools. This project aims to overcome the limitations of prior approaches through a tighter integration of optimization and synthesis algorithms leveraging advances in modern automated reasoning systems. The project demonstrates the power of Satisfiability Modulo Theories (SMT)-based synthesis combined with emerging research in Optimization Modulo Theories (OMT). The project explores advances in both theory and practice, with research demonstrations integrated into CVC4, the only SMT solver today providing synthesis features. In particular, CVC4 is being extended with optimization capabilities, making it the first automated reasoning tool capable of performing synthesis and optimization together. The resulting extensible framework enables system design for emerging technologies which often require reasoning over non Boolean (and mixed) primitives. The extensibility and generality of the approach charts a new direction of research at the intersection of synthesis and optimization, leads towards more scalable and complex system design, and allows optimization over a broader class of objectives including security and safety.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

对优化的大规模计算系统不断增长的需求给自动化设计优化和综合工具的显着改进带来了压力。该项目旨在利用现代自动推理系统的进步，通过优化和合成算法的更紧密集成来克服现有方法的局限性。该项目展示了基于可满足性模理论 (SMT) 的综合与优化模理论 (OMT) 新兴研究相结合的力量。该项目探索理论和实践方面的进步，并将研究演示集成到 CVC4 中，CVC4 是当今唯一提供综合功能的 SMT 求解器。特别是，CVC4 正在扩展优化功能，使其成为第一个能够同时执行综合和优化的自动推理工具。由此产生的可扩展框架支持新兴技术的系统设计，这些技术通常需要对非布尔（和混合）原语进行推理。该方法的可扩展性和通用性在综合和优化的交叉点上描绘了一个新的研究方向，导致更具可扩展性和复杂性的系统设计，并允许对更广泛的目标（包括安全和保障）进行优化。该奖项反映了 NSF 的法定使命通过使用基金会的智力优点和更广泛的影响审查标准进行评估，并被认为值得支持。

项目成果

期刊论文数量（5）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Low-Cost Superconducting Fan-Out With Cell $\text{I}_\text{C}$ Ranking

带单元的低成本超导扇出 $ ext{I}_ ext{C}$ 排名

DOI：
10.1109/tasc.2023.3256797
发表时间：
2023
期刊：
IEEE Transactions on Applied Superconductivity
影响因子：
1.8
作者：
Volk, Jennifer;Tzimpragos, Georgios;Wynn, Alex;Golden, Evan;Sherwood, Timothy
通讯作者：
Sherwood, Timothy

Temporal Computing With Superconductors

DOI：
10.1109/mm.2021.3066377
发表时间：
2021-05-01
期刊：
IEEE MICRO
影响因子：
3.6
作者：
Tzimpragos, Georgios;Volk, Jennifer;Sherwood, Timothy
通讯作者：
Sherwood, Timothy

PyLSE: a pulse-transfer level language for superconductor electronics

PyLSE：超导电子学的脉冲传输级语言

DOI：
10.1145/3519939.3523438
发表时间：
2022
期刊：
ACM
影响因子：
0
作者：
Christensen, Michael;Tzimpragos, Georgios;Kringen, Harlan;Volk, Jennifer;Sherwood, Timothy;Hardekopf, Ben
通讯作者：
Hardekopf, Ben

Superconducting Computing with Alternating Logic Elements

DOI：
10.1109/isca52012.2021.00057
发表时间：
2021-06
期刊：
2021 ACM/IEEE 48th Annual International Symposium on Computer Architecture (ISCA)
影响因子：
0
作者：
Georgios Tzimpragos;Jennifer Volk;A. Wynn;James E. Smith;T. Sherwood
通讯作者：
Georgios Tzimpragos;Jennifer Volk;A. Wynn;James E. Smith;T. Sherwood

In-sensor classification with boosted race trees

具有增强竞赛树的传感器内分类

DOI：
10.1145/3460223
发表时间：
2021
期刊：
Communications of the ACM
影响因子：
22.7
作者：
Tzimpragos, Georgios;Madhavan, Advait;Vasudevan, Dilip;Strukov, Dmitri;Sherwood, Timothy
通讯作者：
Sherwood, Timothy