Lava

Lava: hardware design in Haskell. Lava is a tool to assist circuit designers in specifying, designing, verifying and implementing hardware. It is a collection of Haskell modules. The system design exploits functional programming language features, such as monads and type classes, to provide multiple interpretations of circuit descriptions. These interpretations implement standard circuit analyses such as simulation, formal verification and the generation of code for the production of real circuits.Lava also uses polymorphism and higher order functions to provide more abstract and general descriptions than are possible in traditional hardware description languages. Two Fast Fourier Transform circuit examples illustrate this.


References in zbMATH (referenced in 13 articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Pizani, Flor João Paulo; Swierstra, Wouter; Sijsling, Yorick: (\Pi)-Ware: hardware description and verification in Agda (2018)
  2. Rizkallah, Christine; Garbuzov, Dmitri; Zdancewic, Steve: A formal equational theory for call-by-push-value (2018)
  3. Svensson, Bo Joel; Newton, Ryan R.; Sheeran, Mary: A language for hierarchical data parallel design-space exploration on GPUs (2016)
  4. Svenningsson, Josef; Axelsson, Emil: Combining deep and shallow embedding of domain-specific languages (2015)
  5. Liang, Yun; Rupnow, Kyle; Li, Yinan; Min, Dongbo; Do, Minh N.; Chen, Deming: High-level synthesis: productivity, performance, and software constraints (2012) ioport
  6. Megacz, Adam: Hardware design with generalized arrows (2012) ioport
  7. Braibant, Thomas: Coquet: a Coq library for verifying hardware (2011)
  8. Li, Yongjian; Hung, William N. N.; Song, Xiaoyu: A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL (2011)
  9. Burrows, Eva; Haveraaen, Magne: A hardware independent parallel programming model (2009)
  10. Slind, Konrad; Owens, Scott; Iyoda, Juliano; Gordon, Mike: Proof producing synthesis of arithmetic and cryptographic hardware (2007)
  11. Pell, Oliver: Verification of FPGA layout generators in higher-order logic (2006)
  12. Benton, Nick; Hyland, Martin: Traced premonoidal categories (2003)
  13. Erkök, Levent; Launchbury, John; Moran, Andrew: Semantics of value recursion for monadic input/output (2002)