Research On Specification-Driven Conformance Checking For System-on-Chips

System-on-Chips(SoCs)typically adopts a top-down design flow.After design space exploration based on the high-level design specifications,the design goes through virtual prototyping.Meanwhile,the hardware implementation of the design is refined and syn-thesized layer by layer from RTL description to the final tape-out.If the implementation of silicon device is inconsistent with the design specification,the system software such as device driver developed on the virtual prototype will be difficult to work with the silicon device,which may directly cause catastrophic failures of the system.Moreover,if the sili-con device is found to have defects that are inconsistent with the design specification after tape-out,it will cause huge cost to the enterprise.Therefore,how to ensure that design implementations conform to their high-level specifications is becoming a major research issue.To address this problem,with the detection of consistencies between the high-level design specification and low-level implementations of SoC as the research objective,this paper designs a framework of specification-driven conformance checking for System-on-Chips.To be specific,the main research content and contributions of this paper are as follows:(1).Based on the SystemRDL language,an automatic generation method for For-mal Device Model is proposed.To enable the behavior description of registers,this paper extends the syntax and semantics of the hardware register description language SystemRDL.Moreover,the transformation rules is proposed in this paper to convert the extended SystemRDL specification to its executable Formal Device Model(FDM)automatically.In this way,a non-executable high-level design speci-fication can be automatically converted into an executable FDM for automated con-formance checking.(2).Based on symbolic execution,a framework of specification-driven conformance checking for System-on-Chips.By using the Kernel analysis framework Kprobes,this paper realizes the collection of driver requests and device states from virtual prototypes or silicon devices.With an FDM acting as the golden reference model of a design,this paper symbolically execute FDM with the collected driver requests,and check the conformance between the FDM and low-level implementations(such as virtual prototypes and silicon devices)via comparing the FDM states and device states triggered by the same driver requests.(3).Based on mutation testing,a method for test generation and adequacy evalu-ation of conformance checking is designed.To optimize and improve the suffi-ciency and efficiency of conformance checking,this paper designs mutation opera-tors with hardware characteristics and the generation rules of Mutant-Killing Con-straints,and adopts Mutant-Killing Constraints to model the potential defects in low-level implementations of device.The Mutant-Killing Constraints are automatically instrumented in the FDM and guides the automated generation of device requests.This paper proposes a cooperative symbolic execution mechanism,which stimulates the devices using the generated device requests and collects the device states.With symbolically executing the instrumented FDM,the conformance between FDM and low-level implementations is checked.Meanwhile,the adequacy of conformance checking for SoCs is evaluated using test coverage criteria.This paper experiments on the virtual prototypes and silicon devices of two industrial network adapters.The experimental results demonstrate that,based on the automatically generated FDM,the proposed approach of specification-driven conformance checking for SoCs can not only detect defects in virtual prototypes and silicon devices more effectively,but also evaluate the adequacy of conformance checking.