Formal verification of full-wave rectifier: A case study

Author

Lata, Kusum ; Jamadagni, H.S.

Author_Institution

Center for Electron. Design & Technol., Indian Inst. of Sci., Bangalore, India

fYear

2009

fDate

20-23 Oct. 2009

Firstpage

1306

Lastpage

1309

Abstract

We present a case study of formal verification of full-wave rectifier for analog and mixed signal designs. We have used the Checkmate tool from CMU [1], which is a public domain formal verification tool for hybrid systems. Due to the restriction imposed by Checkmate it necessitates to make the changes in the Checkmate implementation to implement the complex and non-linear system. Full-wave rectifier has been implemented by using the Checkmate custom blocks and the Simulink blocks from MATLAB from Math works. After establishing the required changes in the Checkmate implementation we are able to efficiently verify the safety properties of the full-wave rectifier.

Keywords

circuit simulation; formal verification; mixed analogue-digital integrated circuits; rectifying circuits; Checkmate custom blocks; Checkmate tool; MATLAB; Simulink blocks; formal verification; full-wave rectifier; mixed signal design; Analytical models; Automata; Circuits; Differential equations; Formal verification; Mathematical model; Nonlinear equations; Rectifiers; Safety; Signal design; Analog and Mixed Signal Design; Formal Verification; Hybrid systems; Simulation;

fLanguage

English

Publisher

ieee

Conference_Titel

ASIC, 2009. ASICON '09. IEEE 8th International Conference on

Conference_Location

Changsha, Hunan

Print_ISBN

978-1-4244-3868-6

Electronic_ISBN

978-1-4244-3870-9

Type

conf

DOI

10.1109/ASICON.2009.5351239

Filename

5351239