Meta-model Based Automation of Properties for Pre-Silicon Verification
Keerthikumara Devarajegowda, Wolfgang Ecker · 2018
In the last decade, several hardware generation languages (HGLs: chisel, metartl, spinalhdl, coreir and more) that focus on generation of RTL code have been proposed. These languages rise the level of abstraction from RTL description to RTL generation and utilize high-level languages such as Python or Scala for describing the generation intent. As a result, they are guiding the overall productivity and chip complexity on the rising trend. On the other front, pre -silicon verification is an equally important aspect of the design process and consumes more than 50% of the overall development time. As a consequence of increased chip complexity, the existing verification gap becomes wider. Therefore it neutralizes the productivity gain achieved from RTL generation or other productivity improvement techniques. In this paper, we describe a Python based generation language and framework for hardware properties in order to increase formal verification productivity. The described approach follows the model driven architecture (MDA) vision of OMG. The MDA approach includes transformations, that make the approach platform independent: Different property languages as well as different simulation and formal verification tools are supported. Applied to formal hardware verification, the approach empowers comparable productivity increase as HGLs in RTL designs. In addition, it is an ideal partner for HGLs, since it enables to generate a property set for each HGL generated RTL. The applicability of our approach for real -life industrial designs is demonstrated by generating properties for a RiscV CPU core and also for peripheral devices of a CPU system. The correctness of the generated properties are validated by verifying these designs with a formal verification tool.