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.