Title :
Assisting abstraction and verification of IP modules by control-data slicing
Author :
Muhammad, Waseem ; Coudert, Sophie ; Ameur-Boulifa, Rabéa ; Pacalet, Renaud
Author_Institution :
Syst.-on-Chip Lab. (LabSoC), Telecom Paristech, Sophia Antipolis, France
Abstract :
Functional verification of hardware modules is growing to be challenging due to strict timing requirements, power limitation and time-to-market pressure in design process. Removal of irrelevant information by abstraction of hardware computations has been used by the experts to speed up the verification process. We introduce a register transfer level (RTL) control-data slicing approach in intellectual property (IP) modules to assist formal verification and simulation based validation approaches by removing irrelevant information and reduce state space for model checking and save cycles for simulations. In this paper a control-data separation solution is presented based on slicing of RTL models. Slicing is helpful to identify and separate control state machine from data processing of the IP module to be used for static verification of the critical timing behaviors of the module. The data processing separated from critical control state machine is abstracted to improve verification by simulation without loss of timing information.
Keywords :
formal verification; logic design; optimising compilers; program slicing; IP module abstraction; IP module verification; control-data slicing approach; formal verification; intellectual property modules; model checking; register transfer level; simulation based validation; Computational modeling; Data processing; Formal verification; Hardware; Intellectual property; Process design; Registers; State-space methods; Time to market; Timing;
Conference_Titel :
TENCON 2009 - 2009 IEEE Region 10 Conference
Conference_Location :
Singapore
Print_ISBN :
978-1-4244-4546-2
Electronic_ISBN :
978-1-4244-4547-9
DOI :
10.1109/TENCON.2009.5395936