形式化验证 WARP-V：一个开源 TL-Verilog RISC-V 核心生成器
硬件体系结构
2018-12-03 v1
摘要
使用时序抽象和事务级设计的 TL-Verilog 在逻辑设计方面已显示出显著的生产力提升。在这项工作中，我们探索了将事务级设计方法自然扩展到形式化验证中。WARP-V 是一个用 TL-Verilog 编写的 CPU 核心生成器。我们针对 WARP-V 的主要验证工具是一个称为 riscv-formal 的 RISC-V 形式化验证框架。TL-Verilog 的时序抽象和事务级逻辑建模技术极大地简化了创建将 WARP-V 模型连接到 riscv-formal 验证接口的测试平台（harness）的任务。此外，同一个测试平台适用于 WARP-V 的所有 RISC-V 配置。
引用
@article{arxiv.1811.12474,
title = {Formally Verifying WARP-V, an Open-Source TL-Verilog RISC-V Core Generator},
author = {Steven Hoover and Ákos Hadnagy},
journal= {arXiv preprint arXiv:1811.12474},
year = {2018}
}
备注
4-pages. Presented by \'Akos Hadnagy at open-source hardware conferences: ORConf 2018 and VSDOpen 2018