![]() |
HAL
|
#include <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 |
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 234 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 325 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(), 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 282 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(), operator&(), and operator&=().
|
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 500 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 238 of file boolean_function.cpp.
References BooleanFunction(), and ERR_APPEND.
Referenced by hal::SMT::Model::evaluate(), and hal::BooleanFunctionParser::translate().
BooleanFunction hal::BooleanFunction::clone | ( | ) | const |
Clones the Boolean function.
Definition at line 731 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::FFComponent::get_clock_function(), hal::LatchComponent::get_data_in_function(), hal::LatchComponent::get_enable_function(), hal::FFComponent::get_next_state_function(), operator&(), operator&=(), operator*(), operator*=(), operator+(), operator+=(), operator-(), operator-=(), operator^(), operator^=(), operator|(), operator|=(), operator~(), 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 |
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 1270 of file boolean_function.cpp.
References ERR, evaluate(), get_variable_names(), hal::input, 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 425 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::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 255 of file boolean_function.cpp.
References BooleanFunction(), and hal::BooleanFunction::Node::Constant().
Referenced by hal::SMT::ConstantPropagation::Add(), hal::SMT::ConstantPropagation::And(), hal::boolean_function_init(), Const(), hal::SMT::Model::evaluate(), evaluate(), hal::SMT::ConstantPropagation::Ite(), hal::SMT::ConstantPropagation::Mul(), hal::SMT::ConstantPropagation::Not(), hal::SMT::ConstantPropagation::Or(), hal::netlist_utils::remove_buffers(), hal::SMT::ConstantPropagation::Sle(), hal::SMT::ConstantPropagation::Slt(), hal::solve_fsm::solve_fsm(), hal::solve_fsm::solve_fsm_brute_force(), hal::SMT::ConstantPropagation::Sub(), hal::BooleanFunctionDecorator::substitute_power_ground_nets(), hal::BooleanFunctionDecorator::substitute_power_ground_pins(), hal::SMT::ConstantPropagation::Ule(), hal::SMT::ConstantPropagation::Ult(), and hal::SMT::ConstantPropagation::Xor().
|
static |
Creates a constant multi-bit Boolean function from a vector of values.
[in] | value | - The vector of values. |
Definition at line 260 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 265 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 548 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(), 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 1227 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 1196 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 1046 of file boolean_function.cpp.
References ERR, hal::BooleanFunctionParser::parse_with_liberty_grammar(), hal::BooleanFunctionParser::parse_with_standard_grammar(), control::parser, 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::TEST_F().
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 789 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 799 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 819 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 839 of file boolean_function.cpp.
Referenced by hal::boolean_function_init(), and hal::SMT::Model::evaluate().
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 844 of file boolean_function.cpp.
References BooleanFunction(), get_top_level_node(), 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 829 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 1339 of file boolean_function.cpp.
References compute_truth_table(), ERR_APPEND, get_variable_names(), OK, and control::str.
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 764 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(), 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 884 of file boolean_function.cpp.
Referenced by hal::boolean_function_init(), compute_truth_table(), hal::boolean_influence::get_boolean_influence_with_hal_boolean_function_class(), hal::boolean_influence::get_boolean_influence_with_z3_expr(), 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 779 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().
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 784 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 814 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 759 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 277 of file boolean_function.cpp.
References BooleanFunction(), hal::BooleanFunction::Node::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 749 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 774 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 726 of file boolean_function.cpp.
Referenced by hal::boolean_function_init(), get_constant_value(), get_constant_value_u64(), get_index_value(), 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 809 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 754 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(), 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 603 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().
u32 hal::BooleanFunction::length | ( | ) | const |
Returns the number of nodes in the Boolean function.
Definition at line 834 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 484 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 347 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 304 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 707 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 619 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 624 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 679 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 684 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 657 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 662 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 668 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 673 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 712 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 690 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 646 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 651 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 635 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 640 of file boolean_function.cpp.
BooleanFunction hal::BooleanFunction::operator~ | ( | ) | const |
Negates the Boolean function.
Definition at line 630 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 293 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 516 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 532 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 358 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 452 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 468 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 1082 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 1091 of file boolean_function.cpp.
References clone(), and hal::Simplification::local_simplification().
u16 hal::BooleanFunction::size | ( | ) | const |
Returns the bit-size of the Boolean function.
Definition at line 744 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::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 559 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().
|
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 402 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 570 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().
|
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 380 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 336 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(), 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. |
Helper function to find the replacement for a variable and substitute it with a Boolean function.
[in] | node | - Node. |
[in] | operands | - Operands of node. |
Definition at line 1159 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 1142 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 1098 of file boolean_function.cpp.
References clone(), has_variable_name(), size(), and hal::BooleanFunction::Node::Variable().
Referenced by hal::boolean_function_init(), 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 1112 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 190 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 1001 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 23 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(), compute_truth_table(), evaluate(), hal::FFComponentEntry::FFComponentEntry(), 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 207 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. |
Helper function to reduce a abstract syntax subtree to z3 expressions
[in] | node | - Boolean function node. |
[in] | p | - Boolean function node parameters. |
Definition at line 1426 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 369 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 581 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().
|
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 592 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().
|
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 391 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 250 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::BooleanFunctionDecorator::substitute_module_pins(), and hal::TEST_F().
|
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 314 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 436 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 614 of file boolean_function.cpp.
|
friend |
Output stream operator that forwards to_string
of a value.
[in] | os | - The stream to write to. |
[in] | value | - The value. |
Definition at line 229 of file boolean_function.cpp.