circt::bmc::BMCTrace Class Reference

#include <BMCTrace.h>

Collaboration diagram for circt::bmc::BMCTrace:

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 = llvm::function_ref< std::optional< llvm::APInt >(Handle, unsigned width)>
	Callback used to materialize a recorded handle into a concrete value when formatting a trace.

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

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
std::vector< Step >	recorded

Detailed Description

Definition at line 28 of file BMCTrace.h.

Member Typedef Documentation

Evaluator

using circt::bmc::BMCTrace::Evaluator = llvm::function_ref<std::optional<llvm::APInt>(Handle, unsigned width)>

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 35 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 31 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 65 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.

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.

ensureStep()

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

private

Definition at line 24 of file BMCTrace.cpp.

getNumSteps()

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

inline

Definition at line 55 of file BMCTrace.h.

References recorded.

getSignals()

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

inline

Definition at line 54 of file BMCTrace.h.

References signals.

getTopName()

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

inline

Definition at line 53 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 36 of file BMCTrace.cpp.

printTextTrace()

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 42 of file BMCTrace.cpp.

record()

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 29 of file BMCTrace.cpp.

References assert().

Member Data Documentation

recorded

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

private

Definition at line 71 of file BMCTrace.h.

Referenced by getNumSteps().

signals

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

private

Definition at line 70 of file BMCTrace.h.

Referenced by getSignals().

topName

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

private

Definition at line 69 of file BMCTrace.h.

Referenced by getTopName().

---

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