hal::z3_utils Namespace Reference

Classes
class	Converter
class	Cpp_Converter
class	VerilogConverter

Functions
Result< bool >	compare_nets (const Netlist *netlist_a, const Netlist *netlist_b, const Net *net_a, const Net *net_b, const bool fail_on_unknown=true, const u32 solver_timeout=10)
	Compare two nets from two different netlists. More...
Result< bool >	compare_nets (const Netlist *netlist_a, const Netlist *netlist_b, const std::vector< std::pair< Net *, Net * >> &nets, const bool fail_on_unknown=true, const u32 solver_timeout=10)
	Compare pairs of nets from two different netlist. More...
Result< bool >	compare_netlists (const Netlist *netlist_a, const Netlist *netlist_b, const bool fail_on_unknown=true, const u32 solver_timeout=10)
	Compares two netlists on a functional level. More...
Result< z3::expr >	simplify_local (const z3::expr &e, std::unordered_map< u32, z3::expr > &cache, const bool check_correctness=false)
	Applies hand-crafted simplification rules iteratively until no further simplifications can be made. More...
Result< z3::expr >	simplify_local (const z3::expr &e, const bool check_correctness=false)
	Applies hand-crafted simplification rules iteratively until no further simplifications can be made. More...
Result< z3::expr >	get_subgraph_z3_function (const std::vector< Gate * > &subgraph_gates, const Net *subgraph_output, z3::context &ctx)
	Get the z3 expression representation of a combined Boolean function of a subgraph of combinational gates starting at the source of the provided subgraph output net. More...
Result< std::vector< z3::expr > >	get_subgraph_z3_functions (const std::vector< Gate * > &subgraph_gates, const std::vector< Net * > &subgraph_outputs, z3::context &ctx)
	Get the z3 expression representations of combined Boolean functions of a subgraph of combinational gates starting at the sources of the provided subgraph output nets. More...
z3::expr	from_bf (const BooleanFunction &bf, z3::context &ctx, const std::map< std::string, z3::expr > &var2expr={})
Result< z3::expr >	value_from_binary_string (z3::context &ctx, const std::string &bit_string)
Result< BooleanFunction >	to_bf (const z3::expr &e)
std::string	to_smt2 (const z3::expr &e)
std::string	to_cpp (const z3::expr &e)
std::string	to_verilog (const z3::expr &e, const std::map< std::string, bool > &control_mapping={})
	Translates a z3 expression into a verilog network representation. More...
std::set< std::string >	get_variable_names (const z3::expr &e)
	Extracts all variable names from a z3 expression. More...
std::set< u32 >	extract_net_ids (const z3::expr &e)
	Extracts all net IDs from the variables of a z3 expression. More...
std::set< u32 >	extract_net_ids (const std::set< std::string > &variable_names)
	Extracts all net IDs from a set of variables. More...
z3::expr	get_expr_in_ctx (const z3::expr &e, z3::context &ctx)
	Translates the expr to another context. More...

Detailed Description

Translates between HAL Boolean functions and z3 expressions and provides the analyses built on top of them.

Function Documentation

compare_netlists()

Result< bool > hal::z3_utils::compare_netlists	(	const Netlist *	netlist_a,
		const Netlist *	netlist_b,
		const bool	fail_on_unknown = true,
		const u32	solver_timeout = 10
	)

Compares two netlists on a functional level.

This is done by finding a corresponding partner for each sequential gate in the netlist and checking whether they are identical. This is done on a functional level by building the subgraph function of all their input nets considering all combinational gates of the netlist. In order for this to work the sequential gates of both netlists must have identical names and only the combinational gates may differ.

Parameters

[in]	netlist_a	- The first netlist.
[in]	netlist_b	- The second netlist.
[in]	fail_on_unknown	- Determines whether the function returns false or true in case the SAT solver returns unknown.
[in]	solver_timeout	- The timeout for each SAT solver query in seconds.

Returns

Ok and a Boolean indicating whether the two netlists are functionally equivalent, an error otherwise.

Definition at line 466 of file netlist_comparison.cpp.

References hal::combinational, compare_nets(), ERR_APPEND, hal::Gate::get_fan_in_net(), hal::Netlist::get_gates(), hal::Gate::get_id(), hal::Netlist::get_id(), hal::Gate::get_name(), hal::GateType::get_name(), hal::ModulePin::get_net(), hal::Module::get_output_pin_names(), hal::Module::get_pin_by_name(), hal::Netlist::get_top_module(), hal::Gate::get_type(), hal::BasePin< T >::get_type(), log_debug, log_info, log_warning, OK, hal::sequential, and hal::utils::to_vector().

Referenced by hal::PYBIND11_PLUGIN().

compare_nets() [1/2]

Result< bool > hal::z3_utils::compare_nets	(	const Netlist *	netlist_a,
		const Netlist *	netlist_b,
		const Net *	net_a,
		const Net *	net_b,
		const bool	fail_on_unknown = true,
		const u32	solver_timeout = 10
	)

Compare two nets from two different netlists.

This is done on a functional level by building the subgraph function of each net considering all combinational gates of the netlist. In order for this to work the sequential gates of both netlists must have identical names and only the combinational gates may differ.

Parameters

[in]	netlist_a	- The first netlist.
[in]	netlist_b	- The second netlist.
[in]	net_a	- First net, from netlist_a.
[in]	net_b	- Second net, from netlist_b.
[in]	fail_on_unknown	- Determines whether the function returns false or true in case the SAT solver returns unknown.
[in]	solver_timeout	- The timeout for the SAT solver query in seconds.

Returns

Ok and a Boolean indicating whether the two nets are functionally equivalent, an error otherwise.

Definition at line 363 of file netlist_comparison.cpp.

References hal::combinational, ERR, ERR_APPEND, hal::Netlist::get_gates(), hal::Netlist::get_id(), and hal::Gate::get_type().

Referenced by compare_netlists(), and hal::PYBIND11_PLUGIN().

compare_nets() [2/2]

Result< bool > hal::z3_utils::compare_nets	(	const Netlist *	netlist_a,
		const Netlist *	netlist_b,
		const std::vector< std::pair< Net *, Net * >> &	nets,
		const bool	fail_on_unknown = true,
		const u32	solver_timeout = 10
	)

Compare pairs of nets from two different netlist.

This is done on a functional level by building the subgraph function of each net considering all combinational gates of the netlist. In order for this to work the sequential gates of both netlists must have identical names and only the combinational gates may differ.

Parameters

[in]	netlist_a	- The first netlist.
[in]	netlist_b	- The second netlist.
[in]	nets	- The pairs of nets to compare against each other.
[in]	fail_on_unknown	- Determines whether the function returns false or true in case the SAT solver returns unknown.
[in]	solver_timeout	- The timeout for each SAT solver query in seconds.

Returns

Ok and a Boolean indicating whether the two nets are functionally equivalent, an error otherwise.

Definition at line 404 of file netlist_comparison.cpp.

References hal::combinational, ERR, ERR_APPEND, hal::Netlist::get_gates(), hal::Netlist::get_id(), hal::Gate::get_type(), log_warning, and OK.

extract_net_ids() [1/2]

std::set< u32 > hal::z3_utils::extract_net_ids

(

const std::set< std::string > &

variable_names

)

Extracts all net IDs from a set of variables.

Parameters

[in]

variable_names

- The set of variable names.

Returns

A set containing all the net IDs.

Definition at line 525 of file z3_utils.cpp.

References hal::BooleanFunctionNetDecorator::get_net_id_from(), and log_error.

extract_net_ids() [2/2]

std::set< u32 > hal::z3_utils::extract_net_ids

(

const z3::expr &

e

)

Extracts all net IDs from the variables of a z3 expression.

Parameters

[in]

e

- The expression to extract the net IDs from.

Returns

A set containing all the net IDs.

Definition at line 519 of file z3_utils.cpp.

References get_variable_names().

from_bf()

z3::expr hal::z3_utils::from_bf	(	const BooleanFunction &	bf,
		z3::context &	ctx,
		const std::map< std::string, z3::expr > &	var2expr = {}
	)

Translates a HAL Boolean function into an equivalent z3 expression in the given context. Replacement expressions for variables can be specified.

Parameters

[in]	bf	- The Boolean function to translate.
[in]	ctx	- The context where the new expression is created in.
[in]	var2expr	- Optional replacements for variables.

Returns

A z3 expression equivalent to the Boolean function.

Definition at line 15 of file z3_utils.cpp.

References hal::BooleanFunction::NodeType::Add, hal::BooleanFunction::NodeType::And, hal::BooleanFunction::NodeType::Ashr, hal::BooleanFunction::NodeType::Concat, hal::BooleanFunction::NodeType::Constant, hal::BooleanFunction::NodeType::Eq, hal::BooleanFunction::get_nodes(), hal::BooleanFunction::NodeType::Index, hal::BooleanFunction::NodeType::Ite, log_error, hal::BooleanFunction::NodeType::Lshr, hal::BooleanFunction::NodeType::Mul, hal::BooleanFunction::NodeType::Not, hal::BooleanFunction::NodeType::Or, hal::BooleanFunction::NodeType::Rol, hal::BooleanFunction::NodeType::Ror, hal::BooleanFunction::NodeType::Sdiv, hal::BooleanFunction::NodeType::Sext, hal::BooleanFunction::NodeType::Shl, hal::BooleanFunction::NodeType::Sle, hal::BooleanFunction::NodeType::Slice, hal::BooleanFunction::NodeType::Slt, hal::BooleanFunction::NodeType::Srem, hal::BooleanFunction::NodeType::Sub, hal::BooleanFunction::NodeType::Udiv, hal::BooleanFunction::NodeType::Ule, hal::BooleanFunction::NodeType::Ult, hal::BooleanFunction::NodeType::Urem, hal::BooleanFunction::NodeType::Variable, hal::BooleanFunction::NodeType::Xor, and hal::BooleanFunction::NodeType::Zext.

Referenced by hal::boolean_influence::get_boolean_influence(), hal::boolean_influence::get_boolean_influence_deterministic(), hal::boolean_influence::get_boolean_influence_with_z3_expr(), and hal::PYBIND11_PLUGIN().

get_expr_in_ctx()

z3::expr hal::z3_utils::get_expr_in_ctx	(	const z3::expr &	e,
		z3::context &	ctx
	)

Translates the expr to another context.

Parameters

[in]	e	- The expression to be translated.
[in]	ctx	- Context that the expression is translated into.

Returns

A copy of the expression inside the new context.

Definition at line 542 of file z3_utils.cpp.

References to_smt2().

get_subgraph_z3_function()

Result< z3::expr > hal::z3_utils::get_subgraph_z3_function	(	const std::vector< Gate * > &	subgraph_gates,
		const Net *	subgraph_output,
		z3::context &	ctx
	)

Get the z3 expression representation of a combined Boolean function of a subgraph of combinational gates starting at the source of the provided subgraph output net.

The variables of the resulting Boolean function are created from the subgraph input nets using BooleanFunctionNetDecorator::get_boolean_variable.

Parameters

[in]	subgraph_gates	- The gates making up the subgraph to consider.
[in]	subgraph_output	- The subgraph output net for which to generate the Boolean function.
[in]	ctx	- The context where the new expression is created in.

Returns

The z3 expression representation of the combined Boolean function of the subgraph on success, an error otherwise.

Definition at line 148 of file subgraph_function_generation.cpp.

Referenced by hal::PYBIND11_PLUGIN().

get_subgraph_z3_functions()

Result< std::vector< z3::expr > > hal::z3_utils::get_subgraph_z3_functions	(	const std::vector< Gate * > &	subgraph_gates,
		const std::vector< Net * > &	subgraph_outputs,
		z3::context &	ctx
	)

Get the z3 expression representations of combined Boolean functions of a subgraph of combinational gates starting at the sources of the provided subgraph output nets.

The variables of the resulting Boolean functions are created from the subgraph input nets using BooleanFunctionNetDecorator::get_boolean_variable.

Parameters

[in]	subgraph_gates	- The gates making up the subgraph to consider.
[in]	subgraph_outputs	- The subgraph output nets for which to generate the Boolean functions.
[in]	ctx	- The context where the new expression is created in.

Returns

The z3 expression representations of the combined Boolean functions of the subgraph on success, an error otherwise.

Definition at line 156 of file subgraph_function_generation.cpp.

References ERR_APPEND, net, and OK.

get_variable_names()

std::set< std::string > hal::z3_utils::get_variable_names

(

const z3::expr &

e

)

Extracts all variable names from a z3 expression.

Parameters

[in]

e

- The expression to extract the variable names from.

Returns

A set containing all the variable names

Definition at line 481 of file z3_utils.cpp.

Referenced by hal::Simplification::abc_simplification(), hal::z3_utils::Converter::convert_z3_expr_to_func(), and extract_net_ids().

simplify_local() [1/2]

Result< z3::expr > hal::z3_utils::simplify_local	(	const z3::expr &	e,
		const bool	check_correctness = false
	)

Applies hand-crafted simplification rules iteratively until no further simplifications can be made.

Parameters

[in]	e	The Z3 expression to be simplified.
[in]	check_correctness	A flag to check the correctness of each simplification step. Default is false.

Returns

OK() and the simplified Z3 expression in case of success, an error otherwise.

Definition at line 2054 of file simplification.cpp.

References simplify_local().

simplify_local() [2/2]

Result< z3::expr > hal::z3_utils::simplify_local	(	const z3::expr &	e,
		std::unordered_map< u32, z3::expr > &	cache,
		const bool	check_correctness = false
	)

Applies hand-crafted simplification rules iteratively until no further simplifications can be made.

Parameters

[in]	e	The Z3 expression to be simplified.
[in]	cache	A cache to store simplified (sub)expressions.
[in]	check_correctness	A flag to check the correctness of each simplification step. Default is false.

Returns

OK() and the simplified Z3 expression in case of success, an error otherwise.

Definition at line 2020 of file simplification.cpp.

References ERR, and OK.

Referenced by hal::sse::get_word_values_at_z3(), hal::PYBIND11_PLUGIN(), and simplify_local().

to_bf()

Result< BooleanFunction > hal::z3_utils::to_bf

(

const z3::expr &

e

)

Translates a z3 expression into an equivalent HAL Boolean function.

Parameters

[in]

e

- The expression to translate.

Returns

A Boolean function equivalent to the z3 expression.

Definition at line 443 of file z3_utils.cpp.

Referenced by hal::PYBIND11_PLUGIN().

to_cpp()

std::string hal::z3_utils::to_cpp

(

const z3::expr &

e

)

Translates a z3 expression into a C++ representation that can be used to evaluate the function fast and track the influence of the variables.

Parameters

[in]

e

- The expression to translate.

Returns

A string containing the c++ representation.

Definition at line 463 of file z3_utils.cpp.

to_smt2()

std::string hal::z3_utils::to_smt2

(

const z3::expr &

e

)

Translates a z3 expression into an equivalent SMT2 representation.

Parameters

[in]

e

- The expression to translate.

Returns

A string containing the SMT2 representation.

Definition at line 449 of file z3_utils.cpp.

Referenced by hal::z3_utils::Converter::convert_z3_expr_to_func(), and get_expr_in_ctx().

to_verilog()

std::string hal::z3_utils::to_verilog	(	const z3::expr &	e,
		const std::map< std::string, bool > &	control_mapping = {}
	)

Translates a z3 expression into a verilog network representation.

Parameters

[in]	e	- The expression to translate.
[in]	control_mapping	- A control mapping that can be applied.

Returns

A string containing the verilog representation.

Definition at line 471 of file z3_utils.cpp.

value_from_binary_string()

Result< z3::expr > hal::z3_utils::value_from_binary_string	(	z3::context &	ctx,
		const std::string &	bit_string
	)

Creates a z3 expression from a binary representation of a value of arbitrary size.

Parameters

[in]	ctx	- The context where the new expression is created in.
[in]	bit_string	- The binary string.

Returns

A z3 expression equivalent to the Boolean function.

Definition at line 145 of file z3_utils.cpp.

References ERR, and OK.