Mechanised Wire-wise Verification of Handel-C Synthesis | Zendy

Juan Ignacio Perna | Zendy; Jim Woodcock | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Mechanised Wire-wise Verification of Handel-C Synthesis

Author(s) -

Juan Ignacio Perna,

Jim Woodcock

Publication year - 2009

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2009.05.053

Subject(s) - correctness , hol , computer science , mathematical proof , programming language , automated theorem proving , schema (genetic algorithms) , gas meter prover , theoretical computer science , mathematics , geometry , machine learning

The compilation of Handel-C programs into net-list descriptions of hardware components has been extensively used in commercial tools but never formally verified. In this paper, we first introduce a variation of the existing semantic model for Handel-C compilation that is amenable for mechanical proofs and detailed enough to analyse properties about the generated hardware. We use this model to prove the correctness of the wiring schema used to interconnect the components at the hardware level and propagate control signals among them. Finally, we present the most interesting aspects of the mechanisation of the model and the correctness proofs in the HOL theorem prover

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research