Blogs (1) >>
ICSE 2019
Sat 25 - Fri 31 May 2019 Montreal, QC, Canada
Mon 27 May 2019 16:40 - 17:05 at Sainte-Catherine - Session 4 Chair(s): Stéphanie Challita

We present an automatic proof-producing translator targeting the hardware description language Verilog. The tool takes a circuit represented as a HOL function as input, translates the input function to a Verilog program and automatically proves a correspondence theorem between the input function and the output Verilog program ensuring that the translation is correct. As illustrated in the paper, the generated correspondence theorems furthermore enable transporting circuit reasoning from the HOL level to the Verilog level. We also present a formal semantics for the subset of Verilog targeted by the translator, which we have developed in parallel with the translator. The semantics is based on the official Verilog standard and is, unlike previous formalization efforts, designed to be usable for automated and interactive reasoning without sacrificing a clear correspondence to the standard. To illustrate the translator’s applicability, we present case studies of a simple verified processor and verified regexp matchers and synthesize them for our FPGA boards. The development has been carried out in the HOL4 theorem prover.

Mon 27 May
Times are displayed in time zone: (GMT-04:00) Eastern Time (US & Canada) change

Formalise-2019-papers
16:00 - 18:00: FormaliSE 2019 - Session 4 at Sainte-Catherine
Chair(s): Stéphanie ChallitaInria, France
Formalise-2019-papers16:00 - 16:25
Full-paper
Milad K. GhaleThe Australian National University, Dirk PattinsonAustralian National University, Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia
Formalise-2019-papers16:25 - 16:40
Short-paper
Erick RaelijohnUniversity of Montreal, Michalis FamelisUniversité de Montréal, Houari SahraouiUniversité de Montréal
Formalise-2019-papers16:40 - 17:05
Full-paper
Andreas LööwChalmers University of Technology, Magnus O. MyreenChalmers University of Technology, Sweden
Formalise-2019-papers17:05 - 17:30
Full-paper
Waqar AhmadCarnegie Mellon University, Shahid Ali MurtzaNational University of Sciences and Technology, Osman HasanConcordia University, Canada, Sofiene TaharConcordia University
Formalise-2019-papers17:30 - 18:00
Day closing
Nico PlatThanos