#include <BMCTrace.h>

Collaboration diagram for circt::bmc::BMCTrace:

[legend]

Classes
struct	Signal
	Metadata for a tracked signal in the trace. More...

Public Types
using	Handle = const void *
	Opaque per-signal value reference recorded for a specific cycle.
using	Evaluator
	Callback used to materialize a recorded handle into a concrete value when formatting a trace.
using	ModelEval
	Z3 API callbacks passed in by JIT-compiled code.
using	GetNumeralBinaryString = const char ()(Handle context, Handle value)

Public Member Functions
	BMCTrace (llvm::StringRef topName="bmc")
	Create an empty trace for the given top-level design/module name.
size_t	addSignal (llvm::StringRef name, unsigned width)
	Register a signal to be tracked and return its stable index.
void	record (size_t step, size_t signal, Handle handle)
	Record the value handle for a tracked signal at the given cycle.
void	record (size_t step, llvm::StringRef name, unsigned width, Handle handle)
	Register a signal by name if necessary and record its value handle at the given cycle.
llvm::StringRef	getTopName () const
llvm::ArrayRef< Signal >	getSignals () const
size_t	getNumSteps () const
std::optional< Handle >	lookup (size_t step, size_t signal) const
	Return the recorded handle for a signal at a given cycle, if present.
bool	printTextTrace (llvm::raw_ostream &os, Evaluator evaluate) const
	Render the trace as cycle-by-cycle text using the provided evaluator to materialize values from recorded handles.
bool	printTextTrace (llvm::raw_ostream &os, Handle context, Handle model, ModelEval modelEval, GetNumeralBinaryString getNumeralBinaryString) const
	Render the trace by evaluating its recorded Z3 ASTs in a satisfying model.

Private Types
using	Step = std::vector<std::optional<Handle>>
	Per-cycle storage for all tracked signals.

Private Member Functions
void	ensureStep (size_t step)

Private Attributes
std::string	topName
std::vector< Signal >	signals
llvm::StringMap< size_t >	signalIndices
std::vector< Step >	recorded

Detailed Description

Definition at line 30 of file BMCTrace.h.

Member Typedef Documentation

◆ Evaluator

using circt::bmc::BMCTrace::Evaluator

Initial value:

llvm::function_ref<std::optional<llvm::APInt>(Handle, unsigned width)>

circt::bmc::BMCTrace::Handle

const void * Handle

Opaque per-signal value reference recorded for a specific cycle.

Definition BMCTrace.h:33

Callback used to materialize a recorded handle into a concrete value when formatting a trace.

The provided width is the declared width of the signal, which may be zero for i0 values.

Definition at line 37 of file BMCTrace.h.

◆ GetNumeralBinaryString

using circt::bmc::BMCTrace::GetNumeralBinaryString = const char *(*)(Handle context, Handle value)

Definition at line 44 of file BMCTrace.h.

◆ Handle

using circt::bmc::BMCTrace::Handle = const void *

Opaque per-signal value reference recorded for a specific cycle.

Definition at line 33 of file BMCTrace.h.

◆ ModelEval

using circt::bmc::BMCTrace::ModelEval

Initial value:

bool (*)(Handle context, Handle model, Handle expression,

bool modelCompletion, Handle *value)

context

static std::unique_ptr< Context > context

Definition DpiEntryPoints.cpp:37

Z3 API callbacks passed in by JIT-compiled code.

Keeping these as opaque function pointers avoids making the runtime library depend on Z3 headers or a particular Z3 shared library at link time.

Definition at line 42 of file BMCTrace.h.

◆ Step

using circt::bmc::BMCTrace::Step = std::vector<std::optional<Handle>>

private

Per-cycle storage for all tracked signals.

Definition at line 81 of file BMCTrace.h.

Constructor & Destructor Documentation

◆ BMCTrace()

circt::bmc::BMCTrace::BMCTrace ( llvm::StringRef topName = "bmc" )

explicit

Create an empty trace for the given top-level design/module name.

Definition at line 15 of file BMCTrace.cpp.

References topName.

Member Function Documentation

◆ addSignal()

size_t circt::bmc::BMCTrace::addSignal	(	llvm::StringRef	name,
		unsigned	width )

Register a signal to be tracked and return its stable index.

Signals may have zero width to represent i0 values.

Definition at line 17 of file BMCTrace.cpp.

References assert(), recorded, signalIndices, and signals.

Referenced by record().

◆ ensureStep()

void circt::bmc::BMCTrace::ensureStep ( size_t step )

private

Definition at line 26 of file BMCTrace.cpp.

References recorded, and signals.

Referenced by record().

◆ getNumSteps()

size_t circt::bmc::BMCTrace::getNumSteps ( ) const

inline

Definition at line 66 of file BMCTrace.h.

References recorded.

◆ getSignals()

llvm::ArrayRef< Signal > circt::bmc::BMCTrace::getSignals ( ) const

inline

Definition at line 65 of file BMCTrace.h.

References signals.

◆ getTopName()

llvm::StringRef circt::bmc::BMCTrace::getTopName ( ) const

inline

Definition at line 64 of file BMCTrace.h.

References topName.

◆ lookup()

std::optional< circt::bmc::BMCTrace::Handle > circt::bmc::BMCTrace::lookup	(	size_t	step,
		size_t	signal ) const

Return the recorded handle for a signal at a given cycle, if present.

Definition at line 51 of file BMCTrace.cpp.

References recorded, and signals.

◆ printTextTrace() [1/2]

bool circt::bmc::BMCTrace::printTextTrace	(	llvm::raw_ostream &	os,
		Evaluator	evaluate ) const

Render the trace as cycle-by-cycle text using the provided evaluator to materialize values from recorded handles.

Definition at line 57 of file BMCTrace.cpp.

References recorded, signals, and topName.

Referenced by circt::bmc::circt_bmc_print_trace(), and printTextTrace().

◆ printTextTrace() [2/2]

bool circt::bmc::BMCTrace::printTextTrace	(	llvm::raw_ostream &	os,
		Handle	context,
		Handle	model,
		ModelEval	modelEval,
		GetNumeralBinaryString	getNumeralBinaryString ) const

Render the trace by evaluating its recorded Z3 ASTs in a satisfying model.

This must run before the owning Z3 context is destroyed.

Definition at line 79 of file BMCTrace.cpp.

References context, and printTextTrace().

◆ record() [1/2]

void circt::bmc::BMCTrace::record	(	size_t	step,
		llvm::StringRef	name,
		unsigned	width,
		Handle	handle )

Register a signal by name if necessary and record its value handle at the given cycle.

Definition at line 37 of file BMCTrace.cpp.

References addSignal(), assert(), record(), signalIndices, and signals.

◆ record() [2/2]

void circt::bmc::BMCTrace::record	(	size_t	step,
		size_t	signal,
		Handle	handle )

Record the value handle for a tracked signal at the given cycle.

Definition at line 31 of file BMCTrace.cpp.

References assert(), ensureStep(), recorded, and signals.

Referenced by circt::bmc::circt_bmc_record_trace(), and record().

Member Data Documentation

◆ recorded

std::vector<Step> circt::bmc::BMCTrace::recorded

private

Definition at line 88 of file BMCTrace.h.

Referenced by addSignal(), ensureStep(), getNumSteps(), lookup(), printTextTrace(), and record().

◆ signalIndices

llvm::StringMap<size_t> circt::bmc::BMCTrace::signalIndices

private

Definition at line 87 of file BMCTrace.h.

Referenced by addSignal(), and record().

◆ signals

std::vector<Signal> circt::bmc::BMCTrace::signals

private

Definition at line 86 of file BMCTrace.h.

Referenced by addSignal(), ensureStep(), getSignals(), lookup(), printTextTrace(), record(), and record().

◆ topName

std::string circt::bmc::BMCTrace::topName

private

Definition at line 85 of file BMCTrace.h.

Referenced by BMCTrace(), getTopName(), and printTextTrace().

The documentation for this class was generated from the following files:

/home/runner/work/circt-www/circt-www/circt_src/include/circt/Tools/circt-bmc/BMCTrace.h
/home/runner/work/circt-www/circt-www/circt_src/lib/Tools/circt-bmc/Runtime/BMCTrace.cpp

Classes

Public Types

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Detailed Description

Member Typedef Documentation

◆ Evaluator

◆ GetNumeralBinaryString

◆ Handle

◆ ModelEval

◆ Step

Constructor & Destructor Documentation

◆ BMCTrace()

Member Function Documentation

◆ addSignal()

◆ ensureStep()

◆ getNumSteps()

◆ getSignals()

◆ getTopName()

◆ lookup()

◆ printTextTrace() [1/2]

◆ printTextTrace() [2/2]

◆ record() [1/2]

◆ record() [2/2]

Member Data Documentation

◆ recorded

◆ signalIndices

◆ signals

◆ topName