KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design
KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive Design
复制标题
DOI：
10.23919/fmcad.2019.8894295
复制
发表时间：
2019-10
期刊：
影响因子：
--
通讯作者：
Luca Piccolboni;G. D. Guglielmo;L. Carloni
中科院分区：
文献类型：
--
作者：
Luca Piccolboni;G. D. Guglielmo;L. Carloni
高级综合(HLS)通过用不定时或基于事务的规范取代周期精确的规范来提高设计生产率。获得高质量的RTL实现需要设计人员的大量手动工作，他们必须操作代码并评估不同的HLS旋钮设置。这些修改可能会在RTL实现中引入错误。本文提出了一种用于HLS中增量形式验证的方法Kairos。Kairos通过应用代码操作和旋钮来验证设计者随后从相同规范派生的RTL实现的等价性。
High-level synthesis (HLS) improves design productivity by replacing cycle-accurate specifications with untimed or transaction-based specifications. Obtaining high-quality RTL implementations requires significant manual effort from designers, who must manipulate the code and evaluate different HLS-knob settings. These modifications can introduce bugs in the RTL implementations. We present KAIROS, a methodology for incremental formal verification in HLS. KAIROS verifies the equivalence of the RTL implementations the designer subsequently derives from the same specification by applying code manipulations and knobs.