Chisel Verification Assertions.

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.