| Copyright | (c) Matthew Naylor 2020 (c) Alexandre Joannou 2020-2021 |
|---|---|
| License | MIT |
| Maintainer | mattfn@gmail.com |
| Stability | experimental |
| Safe Haskell | Safe-Inferred |
| Language | GHC2021 |
Blarney.Backend
Description
Synopsis
- module Blarney.Backend.Verilog
- writeVerilog :: Modular a => String -> a -> IO ()
- writeVerilogModule :: Modular a => a -> String -> String -> IO ()
- writeVerilogTop :: Module () -> String -> String -> IO ()
- module Blarney.Backend.SMT
- writeSMTScript :: Modular a => VerifyConf -> a -> String -> String -> IO ()
- verifyWith :: Modular a => VerifyConf -> a -> IO ()
- verifyToDepth :: Modular a => Int -> a -> IO ()
- module Blarney.Backend.Simulation
- simulate :: Module () -> IO ()
- simulateCapture :: Module () -> IO String
- view :: FShow a => a -> IO ()
- viewFor :: FShow a => Int -> a -> IO ()
Verilog backend
module Blarney.Backend.Verilog
writeVerilog :: Modular a => String -> a -> IO () Source #
Shorthand for writeVerilogModule, with output directory set to
current directory.
This function generates Verilog for the mod Blarney 'Modular a' function.
The name of the generated Verilog module is specified with modName and
the generated Verilog file is `dirName/modName.v`.
This function is similar to writeVerilogModule but also generates
a verilator wrapper and Makefile.
This is useful for simple examples. Major projects will
probably require a more customised verilator wrapper;
in that case, just use writeVerilogModule, even for the top-level
module, and write a custom verilator driver, perhaps using the
Blarney-generated one as a starting point.
SMT backend
module Blarney.Backend.SMT
Arguments
| :: Modular a | |
| => VerifyConf | Verification configuration setup |
| -> a | Blarney circuit |
| -> String | Script name |
| -> String | Output directory |
| -> IO () |
This function generates an SMT script to verify each assertion present in
circuit, introduced by calls to the assert function.
The name of the generated SMT script is specified with scriptName and
the generated file is `dirName/scriptName.smt2`.
Arguments
| :: Modular a | |
| => VerifyConf | Verification configuration setup |
| -> a | Blarney circuit |
| -> IO () |
This function interacts with an SMT solver to verify each assertion present
in circuit, introduced by calls to the assert function.
New, improved SMT backend
Simulation backend
module Blarney.Backend.Simulation