From 31C3_Public_Wiki
Jump to: navigation, search

Description Towards type-safety in asynchronous hardware description (s/VHDL/Arrows/g)
Tags lava-arrows
Person organizing Leviathan
Language en - English
en - English
Duration 3
Desired session Day 3
Desired timeframe begin, middle, end


Circuitry written in commonly used hardware description languages like VHDL are exceptionally hard to formally verify and remind us of assembler-type languages, lowest possible instructions/gates enriched with some artificial abstraction. I show a more natural abstraction, namely from circuits to categories 1 and use the purely-functional language Haskell to embed a domain specific language for digital hardware description. Through implementing LavaArrows in Haskell, we get an intuitive arrow notation for free as well as type declarations that may show proofs of your circuit’s formal correctness