Inheritance diagram for hal::z3_utils::VerilogConverter:

Collaboration diagram for hal::z3_utils::VerilogConverter:

Public Member Functions
void	set_control_mapping (const std::map< std::string, bool > &control_mapping)

Public Member Functions inherited from hal::z3_utils::Converter
std::string	convert_z3_expr_to_func (const z3::expr &e) const

Additional Inherited Members
Public Types inherited from hal::z3_utils::Converter
enum	Operation { bvand , bvnot , bvor , bvxor , NONE }

Protected Member Functions inherited from hal::z3_utils::Converter
std::string	integer_with_leading_zeros (const u32 i, const u32 total_length) const

std::string	replace_all (const std::string &str, const std::string &from, const std::string &to) const

std::string	operation_to_string (const Operation &op) const

bool	does_line_contain_assignment (const std::string &l) const

std::string	extract_lhs (const std::string &l) const

std::map< u32, u32 >	extract_paranthesis_pairs (const std::string &l) const

bool	contains_one_operation (const std::string &l) const

std::map< std::string, std::string >	extract_sub_exrepssions (const std::string &l) const

Operation	extract_operation (const std::string &se) const

std::vector< std::string >	extract_operands (const std::string &se) const

std::map< std::string, std::string >	translate_sub_expressions (const std::map< std::string, std::string > &se) const

std::string	merge_sub_expressions (const std::map< std::string, std::string > &translated_sub_expressions) const

std::string	generate_function (const std::vector< std::string > &assignments, std::vector< std::string > &input_vars) const

Protected Attributes inherited from hal::z3_utils::Converter
std::vector< Operation >	m_operations = {Converter::bvand, Converter::bvnot, Converter::bvor, Converter::bvxor}

Detailed Description

Converts a Boolean function given in SMT-LIB notation into Verilog source code.

Definition at line 37 of file verilog_converter.h.

Member Function Documentation

void hal::z3_utils::VerilogConverter::set_control_mapping ( const std::map< std::string, bool > & control_mapping )

Set the values that the control signals are fixed to while the function is translated.

Parameters

[in] control_mapping - A map from the name of a control signal to the value it is fixed to.

Definition at line 9 of file verilog_converter.cpp.

The documentation for this class was generated from the following files: