Specification and verification of SOC using PTL

Author

Zhang, Pengfei

Author_Institution

Sch. of Comput. Sci. & Technol., Huaibei Coal Ind. Teachers´´ Coll., Huaibei, China

Volume

2

fYear

2009

fDate

28-29 Nov. 2009

Firstpage

312

Lastpage

317

Abstract

PTL (projection temporal logic) is a kind of temporal logic which can handle both sequential and parallel computation. In this paper, we proposed a formal approach of specification and verification of SOC using PTL. With this approach, PTL is used in high level design and hardware/software co-design for the formal specification and verification of a SOC system or its hardware/software parts. A simple CPU is specified in different abstract levels as an application illustrative example.

Keywords

formal specification; formal verification; hardware-software codesign; system-on-chip; temporal logic; PTL; SOC specification; SOC verification; formal specification; formal verification; hardware-software codesign; high level design; projection temporal logic; system-on-chip; Application software; Computational intelligence; Computer industry; Computer science; Concurrent computing; Educational institutions; Formal specifications; Fuel processing industries; Hardware design languages; Logic design; SOC design; formal specification; projection temporal logic; simulation; verification;

fLanguage

English

Publisher

ieee

Conference_Titel

Computational Intelligence and Industrial Applications, 2009. PACIIA 2009. Asia-Pacific Conference on

Conference_Location

Wuhan

Print_ISBN

978-1-4244-4606-3

Type

conf

DOI

10.1109/PACIIA.2009.5406596

Filename

5406596