what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Safe Haskell | Safe-Inferred
Language | Haskell2010

What4.Protocol.VerilogWriter

Synopsis

- data Module sym n
- exprsVerilog :: (IsExprBuilder sym, SymExpr sym ~ Expr n) => sym -> [(Some (Expr n), Text)] -> [Some (Expr n)] -> Doc () -> ExceptT String IO (Doc ())
- exprsToModule :: (IsExprBuilder sym, SymExpr sym ~ Expr n) => sym -> [(Some (Expr n), Text)] -> [Some (Expr n)] -> ExceptT String IO (Module sym n)

# Documentation

data Module sym n Source #

exprsVerilog :: (IsExprBuilder sym, SymExpr sym ~ Expr n) => sym -> [(Some (Expr n), Text)] -> [Some (Expr n)] -> Doc () -> ExceptT String IO (Doc ()) Source #

Convert the given What4 expressions, representing the outputs of a circuit, into a textual representation of a Verilog module of the given name.

exprsToModule :: (IsExprBuilder sym, SymExpr sym ~ Expr n) => sym -> [(Some (Expr n), Text)] -> [Some (Expr n)] -> ExceptT String IO (Module sym n) Source #

Convert the given What4 expressions, representing the outputs of a circuit, into a Verilog module of the given name.