Scholarlink

This study constructs Chisel Verification Assertions (CVA), a new assertion language and formal verification tool. CVA heavily relies on the ChiselTest framework and integrates the powerful expressive power of Propositional Projection Temporal Logic (PPTL). A temporal operator system that adapts to Chisel characteristics is designed independently in CVA, achieving a leapfrog improvement in the expressiveness of the Chisel assertion language. This operator system, following hardware validation logic, can accurately describe complex temporal and functional properties. Several typical cases of Chisel program verification are selected to validate CVA. The results show that CVA can effectively capture logic and temporal errors in design, verifying its technical effectiveness and practicality in hardware verification scenarios.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Chisel Verification Assertions

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Zhiwei Wan,
  • Nan Zhang

摘要

This study constructs Chisel Verification Assertions (CVA), a new assertion language and formal verification tool. CVA heavily relies on the ChiselTest framework and integrates the powerful expressive power of Propositional Projection Temporal Logic (PPTL). A temporal operator system that adapts to Chisel characteristics is designed independently in CVA, achieving a leapfrog improvement in the expressiveness of the Chisel assertion language. This operator system, following hardware validation logic, can accurately describe complex temporal and functional properties. Several typical cases of Chisel program verification are selected to validate CVA. The results show that CVA can effectively capture logic and temporal errors in design, verifying its technical effectiveness and practicality in hardware verification scenarios.