Automatic Refinement of Requirements for Verification throughout the SoC Design Flow

International audienceThis paper focuses on the veri cation of requirements for hardware/software systems on chip (SoC's) along the design ow. In the early stages of this ow, the Electronic System Level (ESL) description style, and languages such as SystemC TLM, enable high-level debugging of the SoC functionality. In the last stages, hardware blocks become RTL or gate level (VHDL or Verilog) descriptions. We have developed two autonomous Assertion-Based Veri cation (ABV) solutions, for SystemC TLM platforms and for VHDL/Verilog IP blocks: designs are automatically instrumented with ad hoc property checkers produced from requirements formalized as PSL assertions. Furthermore, for a comprehensive and seamless veri cation ow, analogous requirements should be veri able before and after ESL-to- RTL hardware re nement. This requires the transformation of ESL assertions into their counterparts at the RT level. This paper discusses this issue and proposes a rst set of transformation rules for the automatic re nement of PSL assertions from the system level to the signal level. Properties of an industrial case study are used as illustrative examples