hal::sse Namespace Reference

Functions
Result< z3::expr >	get_value_at_z3 (Net *net, const u32 time_index, const std::vector< bool > &subgraph_gates_byte_map, const std::vector< std::map< u32, bool >> &known_inputs, const std::map< PinGroup< ModulePin > *, BooleanFunction > &word_level_calculations, const bool substitute_endpoints, z3::context &ctx)
	Get the Z3 expression representing the value of a net at a specific time index. More...
Result< std::vector< z3::expr > >	get_word_values_at_z3 (const std::vector< std::vector< Net * >> &words, const std::vector< u32 > &time_indices, const std::vector< bool > &subgraph_gates_byte_map, const std::vector< std::map< u32, bool >> &known_inputs, const std::map< PinGroup< ModulePin > *, BooleanFunction > &word_level_calculations, const bool substitute_endpoints, z3::context &ctx)
	Get the Z3 expressions representing the values of multiple nets as words at specific time indices. More...
Result< std::vector< z3::expr > >	get_word_values_at_z3 (const std::vector< std::pair< Module *, PinGroup< ModulePin > * >> &words, const std::vector< u32 > &time_indices, const std::vector< bool > &subgraph_gates_byte_map, const std::vector< std::map< u32, bool >> &known_inputs, const std::map< PinGroup< ModulePin > *, BooleanFunction > &word_level_calculations, const bool substitute_endpoints, z3::context &ctx)
	Get the Z3 expressions representing the values of pin groups as words at specific time indices. More...

Detailed Description

Symbolically executes the sequential part of a netlist over several clock cycles.

Function Documentation

get_value_at_z3()

Result< z3::expr > hal::sse::get_value_at_z3	(	Net *	net,
		const u32	time_index,
		const std::vector< bool > &	subgraph_gates_byte_map,
		const std::vector< std::map< u32, bool >> &	known_inputs,
		const std::map< PinGroup< ModulePin > *, BooleanFunction > &	word_level_calculations,
		const bool	substitute_endpoints,
		z3::context &	ctx
	)

Get the Z3 expression representing the value of a net at a specific time index.

This function computes the Z3 expression for the value of a given net at a specific time index. It considers the known input values, subgraph gates, and word-level calculations.

Parameters

[in]	net	- The target net.
[in]	time_index	- The time index to evaluate.
[in]	subgraph_gates_byte_map	- A byte map indicating the included gates in the subgraph.
[in]	known_inputs	- A vector of maps containing known input values for each time index.
[in]	word_level_calculations	- A map of pin groups to their corresponding Boolean functions.
[in]	substitute_endpoints	- Whether to substitute endpoints with pins of identified modules.
[in]	ctx	- The Z3 context.

Returns

OK() and the Z3 expression on success, an error otherwise.

Definition at line 751 of file sequential_symbolic_execution.cpp.

References net.

get_word_values_at_z3() [1/2]

Result< std::vector< z3::expr > > hal::sse::get_word_values_at_z3	(	const std::vector< std::pair< Module *, PinGroup< ModulePin > * >> &	words,
		const std::vector< u32 > &	time_indices,
		const std::vector< bool > &	subgraph_gates_byte_map,
		const std::vector< std::map< u32, bool >> &	known_inputs,
		const std::map< PinGroup< ModulePin > *, BooleanFunction > &	word_level_calculations,
		const bool	substitute_endpoints,
		z3::context &	ctx
	)

Get the Z3 expressions representing the values of pin groups as words at specific time indices.

This function computes the Z3 expressions for the values of pin groups at specific time indices, treating them as words. It considers the known input values, subgraph gates, and word-level calculations.

Parameters

[in]	words	- A vector of pairs of modules and pin groups representing words.
[in]	time_indices	- A vector of time indices for each word.
[in]	subgraph_gates_byte_map	- A byte map indicating the included gates in the subgraph.
[in]	known_inputs	- A vector of maps containing known input values for each time index.
[in]	word_level_calculations	- A map of pin groups to their corresponding Boolean functions.
[in]	substitute_endpoints	- Whether to substitute endpoints with pins of identified modules.
[in]	ctx	- The Z3 context.

Returns

OK() and a vector of Z3 expressions on success, an error otherwise.

Definition at line 829 of file sequential_symbolic_execution.cpp.

References get_word_values_at_z3().

get_word_values_at_z3() [2/2]

Result< std::vector< z3::expr > > hal::sse::get_word_values_at_z3	(	const std::vector< std::vector< Net * >> &	words,
		const std::vector< u32 > &	time_indices,
		const std::vector< bool > &	subgraph_gates_byte_map,
		const std::vector< std::map< u32, bool >> &	known_inputs,
		const std::map< PinGroup< ModulePin > *, BooleanFunction > &	word_level_calculations,
		const bool	substitute_endpoints,
		z3::context &	ctx
	)

Get the Z3 expressions representing the values of multiple nets as words at specific time indices.

This function computes the Z3 expressions for the values of multiple nets at specific time indices, treating them as words. It considers the known input values, subgraph gates, and word-level calculations.

Parameters

[in]	words	- A vector of vectors of nets representing words.
[in]	time_indices	- A vector of time indices for each word.
[in]	subgraph_gates_byte_map	- A byte map indicating the included gates in the subgraph.
[in]	known_inputs	- A vector of maps containing known input values for each time index.
[in]	word_level_calculations	- A map of pin groups to their corresponding Boolean functions.
[in]	substitute_endpoints	- Whether to substitute endpoints with pins of identified modules.
[in]	ctx	- The Z3 context.

Returns

OK() and a vector of Z3 expressions on success, an error otherwise.

Definition at line 767 of file sequential_symbolic_execution.cpp.

References ERR_APPEND, OK, and hal::z3_utils::simplify_local().

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