circt::bmc Namespace Reference

Classes
class	BMCTrace

Functions
void	circt_bmc_record_trace (BMCTrace *trace, uint32_t step, const char *name, uint32_t width, BMCTrace::Handle handle)
	Runtime entry point called by JIT-compiled BMC code.
bool	circt_bmc_print_trace (BMCTrace *trace, BMCTrace::Handle context, BMCTrace::Handle model, BMCTrace::ModelEval modelEval, BMCTrace::GetNumeralBinaryString getNumeralBinaryString)
	Runtime entry point called on the SAT path while the Z3 context and model are still alive.

Function Documentation

circt_bmc_print_trace()

bool circt::bmc::circt_bmc_print_trace	(	BMCTrace *	trace,
		BMCTrace::Handle	context,
		BMCTrace::Handle	model,
		BMCTrace::ModelEval	modelEval,
		BMCTrace::GetNumeralBinaryString	getNumeralBinaryString )

Runtime entry point called on the SAT path while the Z3 context and model are still alive.

Definition at line 122 of file BMCTrace.cpp.

References context, and circt::bmc::BMCTrace::printTextTrace().

circt_bmc_record_trace()

void circt::bmc::circt_bmc_record_trace	(	BMCTrace *	trace,
		uint32_t	step,
		const char *	name,
		uint32_t	width,
		BMCTrace::Handle	handle )

Runtime entry point called by JIT-compiled BMC code.

Definition at line 112 of file BMCTrace.cpp.

References circt::bmc::BMCTrace::record().