Lava-arrows
From 31C3_Public_Wiki
| Description | Towards type-safety in asynchronous hardware description (s/VHDL/Arrows/g) |
|---|---|
| Slides | http://blog.the-leviathan.ch/wp-content/uploads/2014/12/presentation1.pdf |
| Website(s) | http://hackage.haskell.org/package/xilinx-lava |
| Tags | lava-arrows |
| Person organizing | Leviathan |
| Contact: | david.lanzendoerfer@o2s.ch |
| Language | 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
