sequential_symbolic_execution.cpp File Reference

#include "hal_core/netlist/boolean_function/simplification.h"
#include "hal_core/netlist/decorators/boolean_function_net_decorator.h"
#include "hal_core/netlist/gate.h"
#include "hal_core/netlist/gate_library/gate_type_component/ff_component.h"
#include "hal_core/netlist/module.h"
#include "hal_core/netlist/net.h"
#include "hal_core/netlist/netlist.h"
#include "hal_core/utilities/utils.h"
#include "z3_utils/simplification.h"
#include "z3_utils/z3_utils.h"
#include <sys/resource.h>

Include dependency graph for sequential_symbolic_execution.cpp:

Go to the source code of this file.

Namespaces
	hal
	hal::sse

Functions
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. More...
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. More...
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. More...