Back to University of Twente portal
| author: | Pieter Bos |
| title: | Logic for Hardware Description Languages |
| keywords: | |
| topics: | Logics and semantics |
| committee: |
Marieke Huisman
, Saeed Darabi |
| started: | September 2015 |
| end: | July 2016 |
Description
A Field-Programmable Gate Array (FPGA) [FPGA]is an integrated circuit designed to be configured by a customer or a designer after manufacturing. An application-specific integrated circuit (ASIC) is an integrated circuit (IC) customized for a particular use, rather than intended for general-purpose use [ASIC]. For both ASIC design and FPGA configuration, designers generally uses a hardware description language (HDL). Verilog [Veri] and VHDL [VH] are known as two popular HDLs.
We developed verification techniques for reasoning about SPMD (Single Program Multiple Data) programming model. Based on our verification technique we are able to reason about parallelization constructs such as parallel loops [OpenMP, PENCIL], GPGPU kernels [OpenCL], and generally data parallelism [SCP, FASE, CARP, Vercors].
There are similarities and differences between the semantics of SPMD programming model and HDLs. In this project we want to look into these similarities and differences. Our goal is to find possible extensions to our SPMD verification technique which enables us to reason about the correctness of HDL programs.
[Veri] http://www.verilogtutorial.info/
[VH]http://www.seas.upenn.edu/~ese171/vhdl/vhdl_primer.html
[FASE] S. Blom, S. Darabi, M. Huisman, Verification of Loop Parallelisations, 18th International Conference, FASE 2015
[SCP] S. Blom, M. Huisman, and M. Mihelcic. Specification and verification of GPGPU programs. Science of Computer Programming, 2014.
[CARP] http://carp.doc.ic.ac.uk/external/
[vercors] The VerCors toolset. https://fmt.ewi.utwente. nl/redmine/projects/vercors-verifier/wiki. Accessed: 14 March 2015
[OpenMP] L. Dagum and R. Menon. OpenMP: an industry standard API for shared-memory programming. Computational Science & Engineering, IEEE, 5(1):46{55, 1998.
[PENCIL] R. Baghdadi, A. Cohen, S. Guelton, S. Verdoolaege, J. Inoue, T. Grosser, G. Kouveli,A. Kravets, A. Lokhmotov, C. Nugteren, F. Waters, and A. F. Donaldson.PENCIL: Towards a Platform-Neutral Compute Intermediate Language for DSLs. CoRR, abs/1302.5586, 2013.
[OpenCL] OpenCL the open standard for parallel programming of heterogeneous systems.https://www.khronos.org/opencl/. Accessed: 13 March 2015.