|
HAL
v4.5.0-124-g47ab54673
The Hardware Analyzer - a comprehensive reverse engineering and manipulation framework for gate-level netlists.
|
#include <hal_core/netlist/boolean_function.h>

Classes | |
| struct | Node |
| struct | NodeType |
Public Types | |
| enum | Value { ZERO = 0 , ONE = 1 , X = -1 , Z = -2 } |
| represents the type of the node More... | |
Public Member Functions | |
| BooleanFunction () | |
| BooleanFunction | operator& (const BooleanFunction &other) const |
| BooleanFunction & | operator&= (const BooleanFunction &other) |
| BooleanFunction | operator~ () const |
| BooleanFunction | operator| (const BooleanFunction &other) const |
| BooleanFunction & | operator|= (const BooleanFunction &other) |
| BooleanFunction | operator^ (const BooleanFunction &other) const |
| BooleanFunction & | operator^= (const BooleanFunction &other) |
| BooleanFunction | operator+ (const BooleanFunction &other) const |
| BooleanFunction & | operator+= (const BooleanFunction &other) |
| BooleanFunction | operator- (const BooleanFunction &other) const |
| BooleanFunction & | operator-= (const BooleanFunction &other) |
| BooleanFunction | operator* (const BooleanFunction &other) const |
| BooleanFunction & | operator*= (const BooleanFunction &other) |
| bool | operator== (const BooleanFunction &other) const |
| bool | operator!= (const BooleanFunction &other) const |
| bool | operator< (const BooleanFunction &other) const |
| bool | is_empty () const |
| BooleanFunction | clone () const |
| u16 | size () const |
| bool | is (u16 type) const |
| bool | is_variable () const |
| bool | has_variable_name (const std::string &variable_name) const |
| Result< std::string > | get_variable_name () const |
| bool | is_constant () const |
| bool | has_constant_value (const std::vector< Value > &value) const |
| bool | has_constant_value (u64 value) const |
| Result< std::vector< Value > > | get_constant_value () const |
| Result< u64 > | get_constant_value_u64 () const |
| bool | is_index () const |
| bool | has_index_value (u16 index) const |
| Result< u16 > | get_index_value () const |
| const BooleanFunction::Node & | get_top_level_node () const |
| u32 | length () const |
| const std::vector< BooleanFunction::Node > & | get_nodes () const |
| std::vector< BooleanFunction > | get_parameters () const |
| std::set< std::string > | get_variable_names () const |
| std::string | to_string (std::function< Result< std::string >(const BooleanFunction::Node &node, std::vector< std::string > &&operands)> &&printer=default_printer) const |
| BooleanFunction | simplify () const |
| BooleanFunction | simplify_local () const |
| BooleanFunction | substitute (const std::string &old_variable_name, const std::string &new_variable_name) const |
| Result< BooleanFunction > | substitute (const std::string &variable_name, const BooleanFunction &function) const |
| BooleanFunction | substitute (const std::map< std::string, std::string > &substitutions) const |
| Result< BooleanFunction > | substitute (const std::map< std::string, BooleanFunction > &substitutions) const |
| Result< Value > | evaluate (const std::unordered_map< std::string, Value > &inputs) const |
| Result< std::vector< Value > > | evaluate (const std::unordered_map< std::string, std::vector< Value >> &inputs) const |
| Result< std::vector< std::vector< Value > > > | compute_truth_table (const std::vector< std::string > &ordered_variables={}, bool remove_unknown_variables=false) const |
| Result< std::string > | get_truth_table_as_string (const std::vector< std::string > &ordered_variables={}, std::string function_name="", bool remove_unknown_variables=false) const |
| z3::expr | to_z3 (z3::context &context, const std::map< std::string, z3::expr > &var2expr={}) const |
Static Public Attributes | |
| static constexpr u32 | MAX_TRUTH_TABLE_VARIABLES = 20 |
Friends | |
| std::ostream & | operator<< (std::ostream &os, Value v) |
| std::ostream & | operator<< (std::ostream &os, const BooleanFunction &f) |
A BooleanFunction represents a symbolic expression (e.g., A & B) in order to abstract the (semantic) functionality of a single netlist gate (or even a complex subcircuit comprising multiple gates) in a formal manner. To this end, the BooleanFunction class is able to construct and display arbitrarily nested expressions, enable symbolic simplification (e.g., simplify A & 0 to 0), and translate Boolean functions to the SAT / SMT solver domain to use the solve constraint formulas.
Definition at line 54 of file boolean_function.h.
represents the type of the node
Represents the logic value that a Boolean function operates on.
| Enumerator | |
|---|---|
| ZERO | Represents a logical 0. |
| ONE | Represents a logical 1. |
| X | Represents an undefined value. |
| Z | Represents a high-impedance value. |
Definition at line 73 of file boolean_function.h.
|
explicit |
Constructs an empty / invalid Boolean function.
Definition at line 249 of file boolean_function.cpp.
Referenced by Add(), And(), Ashr(), build(), clone(), Concat(), Const(), Eq(), get_parameters(), Index(), Ite(), Lshr(), Mul(), Not(), Or(), Rol(), Ror(), Sdiv(), Sext(), Shl(), Sle(), Slice(), Slt(), Srem(), Sub(), substitute(), Udiv(), Ule(), Ult(), Urem(), Var(), Xor(), and Zext().
|
static |
Joins two Boolean functions by applying an ADD operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 340 of file boolean_function.cpp.
References hal::BooleanFunction::NodeType::Add, BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init(), hal::module_identification::check_addition(), hal::module_identification::check_addition_offset(), operator+(), and operator+=().
|
static |
Joins two Boolean functions by applying an AND operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 297 of file boolean_function.cpp.
References hal::BooleanFunction::NodeType::And, BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), operator&(), operator&=(), and hal::netlist_preprocessing::simplify_lut_inits().
|
static |
Arithmetically shifts a Boolean function to the right by the specified number of bits.
| [in] | p0 | - Boolean function to shift. |
| [in] | p1 | - Boolean function of type Index encoding the number of bits to shift. |
| [in] | size | - Bit-size of the shifted Boolean function. |
Definition at line 515 of file boolean_function.cpp.
References hal::BooleanFunction::NodeType::Ashr, BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init().
|
static |
Builds and validates a Boolean function from a vector of nodes.
| [in] | nodes | - Vector of Boolean function nodes. |
Definition at line 253 of file boolean_function.cpp.
References BooleanFunction(), and ERR_APPEND.
Referenced by hal::boolean_function_init(), hal::SMT::Model::evaluate(), and hal::BooleanFunctionParser::translate().
| BooleanFunction hal::BooleanFunction::clone | ( | ) | const |
Clones the Boolean function.
Definition at line 748 of file boolean_function.cpp.
References BooleanFunction().
Referenced by hal::GateType::add_boolean_function(), hal::boolean_function_init(), hal::GateTypeComponent::create_ff_component(), hal::GateTypeComponent::create_ram_port_component(), hal::FFComponent::get_async_reset_function(), hal::LatchComponent::get_async_reset_function(), hal::FFComponent::get_async_set_function(), hal::LatchComponent::get_async_set_function(), hal::BooleanFunctionDecorator::get_boolean_function_from(), hal::FFComponent::get_clock_function(), hal::LatchComponent::get_data_in_function(), hal::LatchComponent::get_enable_function(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), hal::FFComponent::get_next_state_function(), operator&(), operator&=(), operator*(), operator*=(), operator+(), operator+=(), operator-(), operator-=(), operator^(), operator^=(), operator|(), operator|=(), operator~(), hal::SMT::SymbolicState::set(), hal::FFComponent::set_async_reset_function(), hal::LatchComponent::set_async_reset_function(), hal::FFComponent::set_async_set_function(), hal::LatchComponent::set_async_set_function(), hal::FFComponent::set_clock_function(), hal::RAMPortComponent::set_clock_function(), hal::LatchComponent::set_data_in_function(), hal::LatchComponent::set_enable_function(), hal::RAMPortComponent::set_enable_function(), hal::FFComponent::set_next_state_function(), simplify(), simplify_local(), hal::solve_fsm::solve_fsm(), substitute(), hal::BooleanFunctionDecorator::substitute_module_pins(), hal::BooleanFunctionDecorator::substitute_power_ground_nets(), and hal::BooleanFunctionDecorator::substitute_power_ground_pins().
| Result< std::vector< std::vector< BooleanFunction::Value > > > hal::BooleanFunction::compute_truth_table | ( | const std::vector< std::string > & | ordered_variables = {}, |
| bool | remove_unknown_variables = false |
||
| ) | const |
Definition at line 1445 of file boolean_function.cpp.
References ERR, evaluate(), get_variable_names(), index, hal::input, MAX_TRUTH_TABLE_VARIABLES, OK, hal::output, size(), and to_string().
Referenced by hal::Gate::add_boolean_function(), get_truth_table_as_string(), hal::LUTTableModel::setBooleanFunction(), and hal::GateLibraryTabTruthTable::update().
|
static |
Concatenates two Boolean functions of bit-sizes n and m to form a single Boolean function of bit-size n + m.
| [in] | p0 | - First Boolean function (MSBs). |
| [in] | p1 | - Second Boolean function (LSBs). |
| [in] | size | - Bit-size of the concatenated Boolean function, i.e., n + m. |
Definition at line 440 of file boolean_function.cpp.
References BooleanFunction(), hal::BooleanFunction::NodeType::Concat, ERR, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init(), hal::module_identification::check_addition_offset(), hal::BooleanFunctionDecorator::get_boolean_function_from(), hal::solve_fsm::solve_fsm(), and hal::solve_fsm::solve_fsm_brute_force().
|
static |
Creates a constant single-bit Boolean function from a value.
| [in] | value | - The value. |
Definition at line 270 of file boolean_function.cpp.
References BooleanFunction(), and hal::BooleanFunction::Node::Constant().
Referenced by hal::BV_ConstantPropagation::Add(), hal::BV_ConstantPropagation::And(), hal::boolean_function_init(), hal::module_identification::check_addition_offset(), Const(), hal::SMT::Model::evaluate(), hal::SMT::SymbolicExecution::evaluate(), evaluate(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), hal::hawkeye::CipherCandidate::identify_sbox(), hal::BV_ConstantPropagation::Ite(), hal::BV_ConstantPropagation::Mul(), hal::BV_ConstantPropagation::Not(), hal::BV_ConstantPropagation::Or(), hal::netlist_utils::remove_buffers(), hal::BV_ConstantPropagation::Sle(), hal::BV_ConstantPropagation::Slt(), hal::solve_fsm::solve_fsm(), hal::solve_fsm::solve_fsm_brute_force(), hal::BV_ConstantPropagation::Sub(), hal::BooleanFunctionDecorator::substitute_power_ground_nets(), hal::BooleanFunctionDecorator::substitute_power_ground_pins(), hal::BV_ConstantPropagation::Ule(), hal::BV_ConstantPropagation::Ult(), and hal::BV_ConstantPropagation::Xor().
|
static |
Creates a constant multi-bit Boolean function from a vector of values.
| [in] | value | - The vector of values. |
Definition at line 275 of file boolean_function.cpp.
References BooleanFunction(), and hal::BooleanFunction::Node::Constant().
|
static |
Creates a constant multi-bit Boolean function of the given bit-size from an integer value.
| [in] | value | - The integer value. |
| [in] | size | - The bit-size. |
Definition at line 280 of file boolean_function.cpp.
|
static |
Joins two Boolean functions by an equality check that produces a single-bit result.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation (always =1). |
Definition at line 563 of file boolean_function.cpp.
References BooleanFunction(), hal::BooleanFunction::NodeType::Eq, ERR, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), and hal::solve_fsm::solve_fsm().
| Result< std::vector< BooleanFunction::Value > > hal::BooleanFunction::evaluate | ( | const std::unordered_map< std::string, std::vector< Value >> & | inputs | ) | const |
Evaluates a Boolean function comprising multi-bit variables using the given input values.
| [in] | inputs | - A map from variable name to a vector of input values. |
Definition at line 1257 of file boolean_function.cpp.
References Const(), ERR, name, OK, size(), to_string(), and Var().
| Result< BooleanFunction::Value > hal::BooleanFunction::evaluate | ( | const std::unordered_map< std::string, Value > & | inputs | ) | const |
Evaluates a Boolean function comprising only single-bit variables using the given input values.
| [in] | inputs | - A map from variable name to input value. |
Definition at line 1226 of file boolean_function.cpp.
References ERR, name, OK, size(), and to_string().
Referenced by compute_truth_table(), and hal::boolean_influence::get_boolean_influence_with_hal_boolean_function_class().
|
static |
Parses a Boolean function from a string expression.
| [in] | expression | - Boolean function string. |
Definition at line 1063 of file boolean_function.cpp.
References ERR, hal::BooleanFunctionParser::parse_with_liberty_grammar(), hal::BooleanFunctionParser::parse_with_standard_grammar(), hal::gate_library_manager::remove(), hal::BooleanFunctionParser::reverse_polish_notation(), and hal::BooleanFunctionParser::translate().
Referenced by hal::boolean_function_init(), hal::BoolWizardPage::getBoolFunctions(), hal::ActionAddBooleanFunction::readFromXml(), hal::GateLibraryWizard::setComponents(), and hal::WaveDataBoolean::WaveDataBoolean().
| Result< std::vector< BooleanFunction::Value > > hal::BooleanFunction::get_constant_value | ( | ) | const |
Get the value of the top-level node of the Boolean function of type Constant as a vector of BooleanFunction::Value.
Definition at line 806 of file boolean_function.cpp.
References ERR, hal::BooleanFunction::Node::get_constant_value(), get_top_level_node(), and is_empty().
Get the value of the top-level node of the Boolean function of type Constant as long as it has a size <= 64-bit.
Definition at line 816 of file boolean_function.cpp.
References ERR, hal::BooleanFunction::Node::get_constant_value_u64(), get_top_level_node(), and is_empty().
Get the index value of the top-level node of the Boolean function of type Index.
Definition at line 836 of file boolean_function.cpp.
References ERR, hal::BooleanFunction::Node::get_index_value(), get_top_level_node(), and is_empty().
| const std::vector< BooleanFunction::Node > & hal::BooleanFunction::get_nodes | ( | ) | const |
Returns the reverse polish notation list of the Boolean function nodes.
Definition at line 856 of file boolean_function.cpp.
Referenced by hal::boolean_function_init(), hal::SMT::Model::evaluate(), and hal::z3_utils::from_bf().
| std::vector< BooleanFunction > hal::BooleanFunction::get_parameters | ( | ) | const |
Returns the parameter list of the top-level node of the Boolean function.
Instead of iterating the whole Boolean function and decomposing the abstract syntax tree, we simple iterate the Boolean function once and compute the coverage, i.e. how many nodes are covered below the node in the tree, and based on these indices assemble the Boolean function node vector.
Definition at line 861 of file boolean_function.cpp.
References BooleanFunction(), get_top_level_node(), index, and length().
Referenced by hal::boolean_function_init().
| const BooleanFunction::Node & hal::BooleanFunction::get_top_level_node | ( | ) | const |
Returns the top-level node of the Boolean function.
Definition at line 846 of file boolean_function.cpp.
Referenced by hal::boolean_function_init(), get_constant_value(), get_constant_value_u64(), get_index_value(), get_parameters(), get_variable_name(), has_constant_value(), has_index_value(), has_variable_name(), is(), is_constant(), is_index(), is_variable(), and size().
| Result< std::string > hal::BooleanFunction::get_truth_table_as_string | ( | const std::vector< std::string > & | ordered_variables = {}, |
| std::string | function_name = "", |
||
| bool | remove_unknown_variables = false |
||
| ) | const |
Prints the truth table for a Boolean function that comprises <= 10 single-bit variables.
| [in] | ordered_variables | - A vector describing the order of input variables used to generate the truth table. Defaults to an empty vector. |
| [in] | function_name | - The name of the Boolean function to be printed as header of the output columns. |
| [in] | remove_unknown_variables | - Set true to remove variables from the truth table that are not present within the Boolean function, false otherwise. Defaults to false. |
Definition at line 1524 of file boolean_function.cpp.
References compute_truth_table(), ERR_APPEND, get_variable_names(), and OK.
| Result< std::string > hal::BooleanFunction::get_variable_name | ( | ) | const |
Get the variable name of the top-level node of the Boolean function of type Variable.
Definition at line 781 of file boolean_function.cpp.
References ERR, get_top_level_node(), hal::BooleanFunction::Node::get_variable_name(), and is_empty().
Referenced by hal::BooleanFunctionNetDecorator::get_net_from(), hal::BooleanFunctionNetDecorator::get_net_id_from(), hal::netlist_preprocessing::remove_buffers(), and substitute().
| std::set< std::string > hal::BooleanFunction::get_variable_names | ( | ) | const |
Returns the set of variable names used by the Boolean function.
Definition at line 901 of file boolean_function.cpp.
Referenced by hal::boolean_function_init(), hal::LogicEvaluatorDialog::compile(), compute_truth_table(), hal::boolean_influence::get_boolean_influence_with_hal_boolean_function_class(), hal::boolean_influence::get_boolean_influence_with_z3_expr(), hal::verilator::converter::get_function_for_combinational_gate(), hal::Gate::get_resolved_boolean_function(), get_truth_table_as_string(), hal::LUTTableModel::setBooleanFunction(), hal::BooleanFunctionDecorator::substitute_module_pins(), hal::BooleanFunctionDecorator::substitute_power_ground_nets(), and hal::BooleanFunctionDecorator::substitute_power_ground_pins().
| bool hal::BooleanFunction::has_constant_value | ( | const std::vector< Value > & | value | ) | const |
Checks whether the top-level node of the Boolean function is of type Constant and holds a specific value.
| [in] | value | - The constant value to check for. |
true if the Boolean function is of type Constant and holds the given value, false otherwise. Definition at line 796 of file boolean_function.cpp.
References get_top_level_node(), hal::BooleanFunction::Node::has_constant_value(), and is_empty().
Referenced by hal::boolean_function_init(), and hal::module_identification::has_constant_value().
| bool hal::BooleanFunction::has_constant_value | ( | u64 | value | ) | const |
Checks whether the top-level node of the Boolean function is of type Constant and holds a specific value.
| [in] | value | - The constant value to check for. |
true if the Boolean function is of type Constant and holds the given value, false otherwise. Definition at line 801 of file boolean_function.cpp.
References get_top_level_node(), hal::BooleanFunction::Node::has_constant_value(), and is_empty().
| bool hal::BooleanFunction::has_index_value | ( | u16 | index | ) | const |
Checks whether the top-level node of the Boolean function is of type Index and holds a specific value.
| [in] | index | - The index value to check for. |
true if the Boolean function is of type Index and holds the given value, false otherwise. Definition at line 831 of file boolean_function.cpp.
References get_top_level_node(), hal::BooleanFunction::Node::has_index_value(), and is_empty().
Referenced by hal::boolean_function_init().
| bool hal::BooleanFunction::has_variable_name | ( | const std::string & | variable_name | ) | const |
Checks whether the top-level node of the Boolean function is of type Variable and holds a specific variable name.
| variable_name | - The variable name to check for. |
true if the Boolean function is of type Variable and holds the given variable name, false otherwise. Definition at line 776 of file boolean_function.cpp.
References get_top_level_node(), hal::BooleanFunction::Node::has_variable_name(), and is_empty().
Referenced by hal::boolean_function_init(), and substitute().
|
static |
Creates an index for a Boolean function of the given bit-size from an integer value.
| [in] | index | - The integer value. |
| [in] | size | - The bit-size. |
Definition at line 292 of file boolean_function.cpp.
References BooleanFunction(), hal::BooleanFunction::Node::Index(), index, and size().
Referenced by hal::boolean_function_init(), hal::BooleanFunctionDecorator::get_boolean_function_from(), and hal::BooleanFunctionDecorator::substitute_module_pins().
| bool hal::BooleanFunction::is | ( | u16 | type | ) | const |
Checks whether the top-level node of the Boolean function is of a specific type.
| [in] | type | - The type to check for. |
true if the node is of the given type, false otherwise. Definition at line 766 of file boolean_function.cpp.
References get_top_level_node(), hal::BooleanFunction::Node::is(), and is_empty().
Referenced by hal::boolean_function_init(), hal::BooleanFunction::Node::is_constant(), hal::BooleanFunction::Node::is_index(), and hal::BooleanFunction::Node::is_variable().
| bool hal::BooleanFunction::is_constant | ( | ) | const |
Checks whether the top-level node of the Boolean function is of type Constant.
true if the top-level node of the Boolean function is of type Constant, false otherwise. Definition at line 791 of file boolean_function.cpp.
References get_top_level_node(), hal::BooleanFunction::Node::is_constant(), and is_empty().
Referenced by hal::boolean_function_init(), hal::BooleanFunction::Node::get_constant_value(), hal::BooleanFunction::Node::get_constant_value_u64(), hal::BooleanFunction::Node::has_constant_value(), and hal::BooleanFunction::Node::is_operand().
| bool hal::BooleanFunction::is_empty | ( | ) | const |
Checks whether the Boolean function is empty.
true if the Boolean function is empty, false otherwise. Definition at line 743 of file boolean_function.cpp.
Referenced by hal::boolean_function_init(), get_constant_value(), get_constant_value_u64(), hal::verilator::converter::get_function_for_ff(), get_index_value(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), get_variable_name(), has_constant_value(), has_index_value(), has_variable_name(), is(), is_constant(), is_index(), and is_variable().
| bool hal::BooleanFunction::is_index | ( | ) | const |
Checks whether the top-level node of the Boolean function is of type Index.
true if the top-level node of the Boolean function is of type Index, false otherwise. Definition at line 826 of file boolean_function.cpp.
References get_top_level_node(), is_empty(), and hal::BooleanFunction::Node::is_index().
Referenced by hal::boolean_function_init(), hal::BooleanFunction::Node::get_index_value(), hal::BooleanFunction::Node::has_index_value(), and hal::BooleanFunction::Node::is_operand().
| bool hal::BooleanFunction::is_variable | ( | ) | const |
Checks whether the top-level node of the Boolean function is of type Variable.
true if the top-level node of the Boolean function is of type Variable, false otherwise. Definition at line 771 of file boolean_function.cpp.
References get_top_level_node(), is_empty(), and hal::BooleanFunction::Node::is_variable().
Referenced by hal::boolean_function_init(), hal::BooleanFunction::Node::get_variable_name(), hal::BooleanFunction::Node::has_variable_name(), hal::BooleanFunction::Node::is_operand(), hal::netlist_preprocessing::remove_buffers(), and hal::SMT::SymbolicState::set().
|
static |
Joins three Boolean functions by an if-then-else operation with p0 as the condition, p1 as true-case, and p2 as false-case. Requires p1 to be of bit-size 1 and both Boolean functions p1 and p2 to be of the same bit-size. Produces a new Boolean function of the specified bit-size that must be equal to the size of p1 and p2.
| [in] | p0 | - Boolean function condition. |
| [in] | p1 | - Boolean function for true-case. |
| [in] | p2 | - Boolean function for false-case. |
| [in] | size | - Bit-size of the operation, i.e., size of p1 and p2. |
Definition at line 618 of file boolean_function.cpp.
References BooleanFunction(), ERR, hal::BooleanFunction::NodeType::Ite, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init(), and hal::module_identification::VerifiedCandidate::get_merged_word_level_operation().
| u32 hal::BooleanFunction::length | ( | ) | const |
Returns the number of nodes in the Boolean function.
Definition at line 851 of file boolean_function.cpp.
Referenced by hal::boolean_function_init(), and get_parameters().
|
static |
Logically shifts a Boolean function to the right by the specified number of bits.
| [in] | p0 | - Boolean function to shift. |
| [in] | p1 | - Boolean function of type Index encoding the number of bits to shift. |
| [in] | size | - Bit-size of the shifted Boolean function. |
Definition at line 499 of file boolean_function.cpp.
References BooleanFunction(), ERR, hal::BooleanFunction::NodeType::Lshr, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init().
|
static |
Joins two Boolean functions by applying an MUL operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 362 of file boolean_function.cpp.
References BooleanFunction(), ERR, hal::BooleanFunction::NodeType::Mul, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init(), operator*(), and operator*=().
|
static |
Negates the given Boolean function. Requires the Boolean function to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - The Boolean function to negate. |
| [in] | size | - Bit-size of the operation. |
Definition at line 319 of file boolean_function.cpp.
References BooleanFunction(), ERR, hal::BooleanFunction::NodeType::Not, OK, hal::BooleanFunction::Node::Operation(), and size().
Referenced by hal::boolean_function_init(), operator~(), and hal::solve_fsm::solve_fsm().
| bool hal::BooleanFunction::operator!= | ( | const BooleanFunction & | other | ) | const |
Checks whether two Boolean functions are unequal.
| [in] | other | - The other Boolean function. |
true if the Boolean functions are unequal, false otherwise. Definition at line 722 of file boolean_function.cpp.
| BooleanFunction hal::BooleanFunction::operator& | ( | const BooleanFunction & | other | ) | const |
Joins two Boolean functions by an AND operation. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 634 of file boolean_function.cpp.
| BooleanFunction & hal::BooleanFunction::operator&= | ( | const BooleanFunction & | other | ) |
Joins two Boolean functions by an AND operation in-place. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 639 of file boolean_function.cpp.
| BooleanFunction hal::BooleanFunction::operator* | ( | const BooleanFunction & | other | ) | const |
Joins two Boolean functions by an MUL operation. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 694 of file boolean_function.cpp.
| BooleanFunction & hal::BooleanFunction::operator*= | ( | const BooleanFunction & | other | ) |
Joins two Boolean functions by an MUL operation in-place. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 699 of file boolean_function.cpp.
| BooleanFunction hal::BooleanFunction::operator+ | ( | const BooleanFunction & | other | ) | const |
Joins two Boolean functions by an ADD operation. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 672 of file boolean_function.cpp.
| BooleanFunction & hal::BooleanFunction::operator+= | ( | const BooleanFunction & | other | ) |
Joins two Boolean functions by an ADD operation in-place. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 677 of file boolean_function.cpp.
| BooleanFunction hal::BooleanFunction::operator- | ( | const BooleanFunction & | other | ) | const |
Joins two Boolean functions by an SUB operation. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 683 of file boolean_function.cpp.
| BooleanFunction & hal::BooleanFunction::operator-= | ( | const BooleanFunction & | other | ) |
Joins two Boolean functions by an SUB operation in-place. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 688 of file boolean_function.cpp.
| bool hal::BooleanFunction::operator< | ( | const BooleanFunction & | other | ) | const |
Checks whether this Boolean function is 'smaller' than the other Boolean function.
| [in] | other | - The other Boolean function. |
true if this Boolean function is 'smaller', false otherwise. Definition at line 727 of file boolean_function.cpp.
| bool hal::BooleanFunction::operator== | ( | const BooleanFunction & | other | ) | const |
Checks whether two Boolean functions are equal.
| [in] | other | - The other Boolean function. |
true if the Boolean functions are equal, false otherwise. Definition at line 705 of file boolean_function.cpp.
| BooleanFunction hal::BooleanFunction::operator^ | ( | const BooleanFunction & | other | ) | const |
Joins two Boolean functions by an XOR operation. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 661 of file boolean_function.cpp.
| BooleanFunction & hal::BooleanFunction::operator^= | ( | const BooleanFunction & | other | ) |
Joins two Boolean functions by an XOR operation in-place. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 666 of file boolean_function.cpp.
| BooleanFunction hal::BooleanFunction::operator| | ( | const BooleanFunction & | other | ) | const |
Joins two Boolean functions by an OR operation. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 650 of file boolean_function.cpp.
| BooleanFunction & hal::BooleanFunction::operator|= | ( | const BooleanFunction & | other | ) |
Joins two Boolean functions by an OR operation in-place. Requires both Boolean functions to be of the same bit-size.
| [in] | other | - The other Boolean function. |
Definition at line 655 of file boolean_function.cpp.
| BooleanFunction hal::BooleanFunction::operator~ | ( | ) | const |
Negates the Boolean function.
Definition at line 645 of file boolean_function.cpp.
|
static |
Joins two Boolean functions by applying an OR operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 308 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Or, and size().
Referenced by hal::boolean_function_init(), operator|(), and operator|=().
|
static |
Rotates a Boolean function to the left by the specified number of bits.
| [in] | p0 | - Boolean function to rotate. |
| [in] | p1 | - Boolean function of type Index encoding the number of bits to rotate. |
| [in] | size | - Bit-size of the rotated Boolean function. |
Definition at line 531 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Rol, and size().
Referenced by hal::boolean_function_init().
|
static |
Rotates a Boolean function to the right by the specified number of bits.
| [in] | p0 | - Boolean function to rotate. |
| [in] | p1 | - Boolean function of type Index encoding the number of bits to rotate. |
| [in] | size | - Bit-size of the rotated Boolean function. |
Definition at line 547 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Ror, and size().
Referenced by hal::boolean_function_init().
|
static |
Joins two Boolean functions by applying an SDIV operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 373 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Sdiv, and size().
Referenced by hal::boolean_function_init().
|
static |
Sign-extends a Boolean function to the specified bit-size.
| [in] | p0 | - Boolean function to extend. |
| [in] | p1 | - Boolean function of type Index encoding the bit-size of the sign-extended result. |
| [in] | size | - Bit-size of the sign-extended Boolean function. |
Definition at line 467 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Sext, and size().
Referenced by hal::boolean_function_init(), and hal::BooleanFunctionDecorator::get_boolean_function_from().
|
static |
Shifts a Boolean function to the left by the specified number of bits.
| [in] | p0 | - Boolean function to shift. |
| [in] | p1 | - Boolean function of type Index encoding the number of bits to shift. |
| [in] | size | - Bit-size of the shifted Boolean function. |
Definition at line 483 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), hal::BooleanFunction::NodeType::Shl, and size().
Referenced by hal::boolean_function_init().
| BooleanFunction hal::BooleanFunction::simplify | ( | ) | const |
Simplifies the Boolean function.
Definition at line 1112 of file boolean_function.cpp.
References clone(), and hal::Simplification::local_simplification().
Referenced by hal::boolean_function_init(), and hal::netlist_utils::remove_buffers().
| BooleanFunction hal::BooleanFunction::simplify_local | ( | ) | const |
Simplifies the Boolean function using only the local simplification.
Definition at line 1121 of file boolean_function.cpp.
References clone(), and hal::Simplification::local_simplification().
Referenced by hal::boolean_function_init(), and hal::netlist_preprocessing::remove_buffers().
| u16 hal::BooleanFunction::size | ( | ) | const |
Returns the bit-size of the Boolean function.
Definition at line 761 of file boolean_function.cpp.
References get_top_level_node(), and hal::BooleanFunction::Node::size.
Referenced by Add(), And(), Ashr(), hal::boolean_function_init(), hal::BooleanFunction::Node::clone(), compute_truth_table(), Concat(), Const(), Eq(), evaluate(), hal::BooleanFunction::Node::get_constant_value_u64(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), hal::BooleanFunction::Node::has_constant_value(), Index(), Ite(), Lshr(), Mul(), Not(), operator&(), operator&=(), operator*(), operator*=(), operator+(), operator+=(), operator-(), operator-=(), hal::BooleanFunction::Node::operator<(), hal::BooleanFunction::Node::operator==(), operator^(), operator^=(), operator|(), operator|=(), operator~(), Or(), Rol(), Ror(), Sdiv(), Sext(), Shl(), Sle(), Slice(), Slt(), hal::solve_fsm::solve_fsm_brute_force(), Srem(), Sub(), substitute(), Udiv(), Ule(), Ult(), Urem(), Var(), Xor(), and Zext().
|
static |
Joins two Boolean functions by a signed less-than-equal check that produces a single-bit result.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation (always =1). |
Definition at line 574 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Sle.
Referenced by hal::boolean_function_init(), and hal::module_identification::check_leq().
|
static |
Returns the slice [i:j] of a Boolean function specified by a start index i and an end index j beginning at 0. Note that slice [i:j] includes positions i and j as well.
| [in] | p0 | - Boolean function to slice. |
| [in] | p1 | - Boolean function of type Index encoding start index i. |
| [in] | p2 | - Boolean function of type Index encoding end index j. |
| [in] | size | - Bit-size of the resulting Boolean function slice, i.e., j - i + 1. |
Definition at line 417 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Slice.
Referenced by hal::boolean_function_init(), and hal::BooleanFunctionDecorator::substitute_module_pins().
|
static |
Joins two Boolean functions by a signed less-than check that produces a single-bit result.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation (always =1). |
Definition at line 585 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Slt.
Referenced by hal::boolean_function_init(), and hal::module_identification::check_leq().
|
static |
Joins two Boolean functions by applying an SREM operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 395 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Srem.
Referenced by hal::boolean_function_init().
|
static |
Joins two Boolean functions by applying an SUB operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 351 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Sub.
Referenced by hal::boolean_function_init(), hal::module_identification::check_sub(), operator-(), and operator-=().
| Result< BooleanFunction > hal::BooleanFunction::substitute | ( | const std::map< std::string, BooleanFunction > & | substitutions | ) | const |
Substitute multiple variables with Boolean functions at once. The operation is applied to all instances of the variable in the function.
| [in] | substitutions | - A map from variable names to Boolean functions. |
Definition at line 1189 of file boolean_function.cpp.
References BooleanFunction(), clone(), ERR, and OK.
| BooleanFunction hal::BooleanFunction::substitute | ( | const std::map< std::string, std::string > & | substitutions | ) | const |
Substitute multiple variable names with different names at once, i.e., rename the variables. The operation is applied to all instances of the variable in the function.
| [in] | substitutions | - A map from old variable names to new variable names. |
Definition at line 1172 of file boolean_function.cpp.
References clone(), get_variable_name(), and hal::BooleanFunction::Node::Variable().
| BooleanFunction hal::BooleanFunction::substitute | ( | const std::string & | old_variable_name, |
| const std::string & | new_variable_name | ||
| ) | const |
Substitute a variable name with another one, i.e., renames the variable. The operation is applied to all instances of the variable in the function.
| [in] | old_variable_name | - The old variable name to substitute. |
| [in] | new_variable_name | - The new variable name. |
Definition at line 1128 of file boolean_function.cpp.
References clone(), has_variable_name(), size(), and hal::BooleanFunction::Node::Variable().
Referenced by hal::boolean_function_init(), hal::verilator::converter::get_function_for_combinational_gate(), hal::Gate::get_resolved_boolean_function(), hal::netlist_utils::remove_buffers(), hal::solve_fsm::solve_fsm_brute_force(), hal::BooleanFunctionDecorator::substitute_power_ground_nets(), and hal::BooleanFunctionDecorator::substitute_power_ground_pins().
| Result< BooleanFunction > hal::BooleanFunction::substitute | ( | const std::string & | variable_name, |
| const BooleanFunction & | function | ||
| ) | const |
Substitute a variable with another Boolean function. The operation is applied to all instances of the variable in the function.
| [in] | variable_name | - The variable to substitute. |
| [in] | function | - The function replace the variable with. |
Definition at line 1142 of file boolean_function.cpp.
References BooleanFunction(), clone(), ERR, name, OK, and to_string().
|
static |
Convert the given bit-vector to its string representation in the given base.
| [in] | value | - The value as a bit-vector. |
| [in] | base | - The base that the values should be converted to. Valid values are 2 (default), 8, 10, and 16. |
Definition at line 205 of file boolean_function.cpp.
References ERR.
| std::string hal::BooleanFunction::to_string | ( | std::function< Result< std::string >(const BooleanFunction::Node &node, std::vector< std::string > &&operands)> && | printer = default_printer | ) | const |
Translates the Boolean function into its string representation.
| [in] | printer | - A function a node and its operands as inputs and outputs their string representation. Allows for different grammers to be printed. Defaults to the 'default_printer'. |
Definition at line 1018 of file boolean_function.cpp.
References hal::BooleanFunction::Node::get_arity(), log_error, and hal::BooleanFunction::Node::to_string().
|
static |
Get the value as a string.
| [in] | value | - The value. |
Definition at line 26 of file boolean_function.cpp.
References ONE, X, Z, and ZERO.
Referenced by hal::Gate::add_boolean_function(), hal::ActionAddBooleanFunction::addToHash(), hal::boolean_function_init(), hal::BooleanFunctionEntry::BooleanFunctionEntry(), hal::LogicEvaluatorDialog::compile(), compute_truth_table(), evaluate(), hal::FFComponentEntry::FFComponentEntry(), hal::verilator::converter::get_function_for_combinational_gate(), hal::verilator::converter::get_function_for_ff(), hal::BooleanFunctionNetDecorator::get_net_from(), hal::BooleanFunctionNetDecorator::get_net_id_from(), hal::LatchComponentEntry::LatchComponentEntry(), hal::netlist_utils::remove_buffers(), substitute(), to_u64(), and hal::ActionAddBooleanFunction::writeToXml().
|
static |
Convert the given bit-vector to its unsigned 64-bit integer representation.
| [in] | value | - The value as a bit-vector. |
Definition at line 222 of file boolean_function.cpp.
References ERR, OK, and to_string().
Referenced by hal::SMT::ConstantPropagation::Add(), hal::boolean_function_init(), hal::solve_fsm::solve_fsm(), hal::solve_fsm::solve_fsm_brute_force(), and hal::SMT::ConstantPropagation::Sub().
| z3::expr hal::BooleanFunction::to_z3 | ( | z3::context & | context, |
| const std::map< std::string, z3::expr > & | var2expr = {} |
||
| ) | const |
| [in,out] | context | - Z3 context to generate expressions. |
| [in] | var2expr | - Maps input variables to expression. |
Definition at line 1611 of file boolean_function.cpp.
References hal::BooleanFunction::NodeType::And, hal::BooleanFunction::NodeType::Concat, hal::BooleanFunction::NodeType::Constant, hal::BooleanFunction::NodeType::Index, log_error, hal::BooleanFunction::NodeType::Not, hal::BooleanFunction::NodeType::Or, hal::BooleanFunction::NodeType::Sext, hal::BooleanFunction::NodeType::Slice, hal::BooleanFunction::NodeType::Variable, and hal::BooleanFunction::NodeType::Xor.
|
static |
Joins two Boolean functions by applying an UDIV operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 384 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Udiv.
Referenced by hal::boolean_function_init().
|
static |
Joins two Boolean functions by an unsigned less-than-equal check that produces a single-bit result.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation (always =1). |
Definition at line 596 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Ule.
Referenced by hal::boolean_function_init(), and hal::module_identification::check_leq().
|
static |
Joins two Boolean functions by an unsigned less-than check that produces a single-bit result.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation (always =1). |
Definition at line 607 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Ult.
Referenced by hal::boolean_function_init(), and hal::module_identification::check_leq().
|
static |
Joins two Boolean functions by applying an UREM operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 406 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Urem.
Referenced by hal::boolean_function_init().
|
static |
Creates a Boolean function of the given bit-size comprising only a variable of the specified name.
| [in] | name | - The name of the variable. |
| [in] | size | - The bit-size. Defaults to 1. |
Definition at line 265 of file boolean_function.cpp.
References BooleanFunction(), name, size(), and hal::BooleanFunction::Node::Variable().
Referenced by hal::boolean_function_init(), evaluate(), hal::BooleanFunctionDecorator::get_boolean_function_from(), hal::BooleanFunctionNetDecorator::get_boolean_variable(), hal::module_identification::VerifiedCandidate::get_merged_word_level_operation(), hal::netlist_preprocessing::simplify_lut_inits(), and hal::BooleanFunctionDecorator::substitute_module_pins().
|
static |
Joins two Boolean functions by applying an XOR operation. Requires both Boolean functions to be of the specified bit-size and produces a new Boolean function of the same bit-size.
| [in] | p0 | - First Boolean function. |
| [in] | p1 | - Second Boolean function. |
| [in] | size | - Bit-size of the operation. |
Definition at line 329 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Xor.
Referenced by hal::boolean_function_init(), operator^(), and operator^=().
|
static |
Zero-extends a Boolean function to the specified bit-size.
| [in] | p0 | - Boolean function to extend. |
| [in] | p1 | - Boolean function of type Index encoding the bit-size of the zero-extended result. |
| [in] | size | - Bit-size of the zero-extended Boolean function. |
Definition at line 451 of file boolean_function.cpp.
References BooleanFunction(), ERR, OK, hal::BooleanFunction::Node::Operation(), size(), and hal::BooleanFunction::NodeType::Zext.
Referenced by hal::boolean_function_init(), and hal::BooleanFunctionDecorator::get_boolean_function_from().
|
friend |
The ostream operator that forwards to_string of a boolean function.
| [in] | os | - the stream to write to. |
| [in] | f | - the function. |
Definition at line 629 of file boolean_function.cpp.
|
friend |
Output stream operator that forwards to_string of a value.
| [in] | os | - The stream to write to. |
| [in] | v | - The value. |
Definition at line 244 of file boolean_function.cpp.
|
staticconstexpr |
Computes the truth table outputs for a Boolean function that comprises <= 10 single-bit variables.
| [in] | ordered_variables | - A vector describing the order of input variables used to generate the truth table. Defaults to an empty vector. |
| [in] | remove_unknown_variables | - Set true to remove variables from the truth table that are not present within the Boolean function, false otherwise. Defaults to false. |
Definition at line 872 of file boolean_function.h.
Referenced by compute_truth_table().