EngineeringComputer EngineeringComputer ScienceComputer ArchitectureHardware Description LanguagesProgramming LanguagesAbstract InterpretationData TypesDigital Logic DesignFunctional ProgrammingHardware Modeling For Digital SystemsType SystemsFast Fourier TransformFast Fourier Transform Circuit DesignFormal Hardware VerificationFormal Specification Of Combinational CircuitsFormal VerificationHigher-order FunctionsMonadsType Classes
Lava is a Haskell‑based tool that aids circuit designers in specifying, designing, verifying, and implementing hardware. It leverages Haskell’s monads, type classes, polymorphism, and higher‑order functions to offer multiple interpretations of circuit descriptions, enabling simulation, formal verification, and code generation. Two Fast Fourier Transform circuit examples demonstrate the tool’s capabilities.
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.
6
Otter - The CADE-13 Competition Incarnations
William McCune, Larry Wos · Journal of Automated Reasoning · 1997 · 104 citations
Tanel Tammet · Journal of Automated Reasoning · 1997 · 48 citations