Title :
Verification of a production cell using an automatic verification environment for VHDL
Author :
Herrmann, Ronald ; Reielts, Thomas
Author_Institution :
Corp. Res. & Dev., Siemens AG, Munich, Germany
Abstract :
This paper presents from the users point of view the automatic verification of nontrivial liveness properties for a reactive system implemented using VHDL. The aim is to make clear the simplicity, power and practical relevance of tools developed within the ESPRIT project FORMAT. For the specialist this paper provides a run through assumption commitment style verification and an overview of relevant publications
Keywords :
formal verification; hardware description languages; programming environments; ESPRIT project FORMAT; VHDL; assumption commitment style verification; automatic verification environment; nontrivial liveness properties; production cell verification; Automatic control; Belts; Control systems; Cranes; Design automation; Feeds; Production; Robots; Safety; Sliding mode control;
Conference_Titel :
Design Automation Conference, 1995, with EURO-VHDL, Proceedings EURO-DAC '95., European
Conference_Location :
Brighton
Print_ISBN :
0-8186-7156-4
DOI :
10.1109/EURDAC.1995.527457
