mirror of
https://github.com/verilator/verilator.git
synced 2025-01-03 21:27:35 +00:00
Internals: Emit rand constraint right away. No functional change intended. (#5409)
This change gets rid of most of the shared pointers and useless memory allocations. Also takes advantage of higher-arity bvxor/concat to reduce amount of data sent to the solver. Signed-off-by: Arkadiusz Kozdra <akozdra@antmicro.com>
This commit is contained in:
parent
e04ef5d83a
commit
5cb6f370e9
@ -253,23 +253,6 @@ static Process& getSolver() {
|
|||||||
//======================================================================
|
//======================================================================
|
||||||
// VlRandomizer:: Methods
|
// VlRandomizer:: Methods
|
||||||
|
|
||||||
void VlRandomVar::emit(std::ostream& s) const { s << m_name; }
|
|
||||||
void VlRandomConst::emit(std::ostream& s) const {
|
|
||||||
s << "#b";
|
|
||||||
for (int i = 0; i < m_width; i++) s << (VL_BITISSET_Q(m_val, m_width - i - 1) ? '1' : '0');
|
|
||||||
}
|
|
||||||
void VlRandomBinOp::emit(std::ostream& s) const {
|
|
||||||
s << '(' << m_op << ' ';
|
|
||||||
m_lhs->emit(s);
|
|
||||||
s << ' ';
|
|
||||||
m_rhs->emit(s);
|
|
||||||
s << ')';
|
|
||||||
}
|
|
||||||
void VlRandomExtract::emit(std::ostream& s) const {
|
|
||||||
s << "((_ extract " << m_idx << ' ' << m_idx << ") ";
|
|
||||||
m_expr->emit(s);
|
|
||||||
s << ')';
|
|
||||||
}
|
|
||||||
bool VlRandomVar::set(std::string&& val) const {
|
bool VlRandomVar::set(std::string&& val) const {
|
||||||
VlWide<VL_WQ_WORDS_E> qowp;
|
VlWide<VL_WQ_WORDS_E> qowp;
|
||||||
VL_SET_WQ(qowp, 0ULL);
|
VL_SET_WQ(qowp, 0ULL);
|
||||||
@ -307,27 +290,31 @@ bool VlRandomVar::set(std::string&& val) const {
|
|||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::shared_ptr<const VlRandomExpr> VlRandomizer::randomConstraint(VlRNG& rngr, int bits) {
|
void VlRandomizer::randomConstraint(std::ostream& os, VlRNG& rngr, int bits) {
|
||||||
unsigned long long hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1);
|
const IData hash = VL_RANDOM_RNG_I(rngr) & ((1 << bits) - 1);
|
||||||
std::shared_ptr<const VlRandomExpr> concat = nullptr;
|
int varBits = 0;
|
||||||
std::vector<std::shared_ptr<const VlRandomExpr>> varbits;
|
for (const auto& var : m_vars) varBits += var.second->width();
|
||||||
for (const auto& var : m_vars) {
|
os << "(= #b";
|
||||||
for (int i = 0; i < var.second->width(); i++)
|
for (int i = bits - 1; i >= 0; i--) os << (VL_BITISSET_I(hash, i) ? '1' : '0');
|
||||||
varbits.emplace_back(std::make_shared<const VlRandomExtract>(var.second, i));
|
if (bits > 1) os << " (concat";
|
||||||
}
|
|
||||||
for (int i = 0; i < bits; i++) {
|
for (int i = 0; i < bits; i++) {
|
||||||
std::shared_ptr<const VlRandomExpr> bit = nullptr;
|
IData varBitsLeft = varBits;
|
||||||
for (unsigned j = 0; j * 2 < varbits.size(); j++) {
|
IData varBitsWant = (varBits + 1) / 2;
|
||||||
unsigned idx = j + VL_RANDOM_RNG_I(rngr) % (varbits.size() - j);
|
if (varBits > 2) os << " (bvxor";
|
||||||
auto sel = varbits[idx];
|
for (const auto& var : m_vars) {
|
||||||
std::swap(varbits[idx], varbits[j]);
|
for (int j = 0; j < var.second->width(); j++, varBitsLeft--) {
|
||||||
bit = bit == nullptr ? sel : std::make_shared<const VlRandomBinOp>("bvxor", bit, sel);
|
const bool doEmit = (VL_RANDOM_RNG_I(rngr) % varBitsLeft) < varBitsWant;
|
||||||
|
if (doEmit) {
|
||||||
|
os << " ((_ extract " << j << ' ' << j << ") " << var.second->name() << ')';
|
||||||
|
if (--varBitsWant == 0) break;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
if (varBitsWant == 0) break;
|
||||||
}
|
}
|
||||||
concat = concat == nullptr ? bit
|
if (varBits > 2) os << ')';
|
||||||
: std::make_shared<const VlRandomBinOp>("concat", concat, bit);
|
|
||||||
}
|
}
|
||||||
return std::make_shared<const VlRandomBinOp>(
|
if (bits > 1) os << ')';
|
||||||
"=", concat, std::make_shared<const VlRandomConst>(hash, bits));
|
os << ')';
|
||||||
}
|
}
|
||||||
|
|
||||||
bool VlRandomizer::next(VlRNG& rngr) {
|
bool VlRandomizer::next(VlRNG& rngr) {
|
||||||
@ -356,7 +343,7 @@ bool VlRandomizer::next(VlRNG& rngr) {
|
|||||||
|
|
||||||
for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; i++) {
|
for (int i = 0; i < _VL_SOLVER_HASH_LEN_TOTAL && sat; i++) {
|
||||||
f << "(assert ";
|
f << "(assert ";
|
||||||
randomConstraint(rngr, _VL_SOLVER_HASH_LEN)->emit(f);
|
randomConstraint(f, rngr, _VL_SOLVER_HASH_LEN);
|
||||||
f << ")\n";
|
f << ")\n";
|
||||||
f << "\n(check-sat)\n";
|
f << "\n(check-sat)\n";
|
||||||
sat = parseSolution(f);
|
sat = parseSolution(f);
|
||||||
|
@ -30,11 +30,7 @@
|
|||||||
//=============================================================================
|
//=============================================================================
|
||||||
// VlRandomExpr and subclasses represent expressions for the constraint solver.
|
// VlRandomExpr and subclasses represent expressions for the constraint solver.
|
||||||
|
|
||||||
class VlRandomExpr VL_NOT_FINAL {
|
class VlRandomVar final {
|
||||||
public:
|
|
||||||
virtual void emit(std::ostream& s) const = 0;
|
|
||||||
};
|
|
||||||
class VlRandomVar final : public VlRandomExpr {
|
|
||||||
const char* const m_name; // Variable name
|
const char* const m_name; // Variable name
|
||||||
void* const m_datap; // Reference to variable data
|
void* const m_datap; // Reference to variable data
|
||||||
const int m_width; // Variable width in bits
|
const int m_width; // Variable width in bits
|
||||||
@ -52,44 +48,6 @@ public:
|
|||||||
std::uint32_t randModeIdx() const { return m_randModeIdx; }
|
std::uint32_t randModeIdx() const { return m_randModeIdx; }
|
||||||
bool randModeIdxNone() const { return randModeIdx() == std::numeric_limits<unsigned>::max(); }
|
bool randModeIdxNone() const { return randModeIdx() == std::numeric_limits<unsigned>::max(); }
|
||||||
bool set(std::string&&) const;
|
bool set(std::string&&) const;
|
||||||
void emit(std::ostream& s) const override;
|
|
||||||
};
|
|
||||||
|
|
||||||
class VlRandomConst final : public VlRandomExpr {
|
|
||||||
const QData m_val; // Constant value
|
|
||||||
const int m_width; // Constant width in bits
|
|
||||||
|
|
||||||
public:
|
|
||||||
VlRandomConst(QData val, int width)
|
|
||||||
: m_val{val}
|
|
||||||
, m_width{width} {
|
|
||||||
assert(width <= sizeof(m_val) * 8);
|
|
||||||
}
|
|
||||||
void emit(std::ostream& s) const override;
|
|
||||||
};
|
|
||||||
|
|
||||||
class VlRandomExtract final : public VlRandomExpr {
|
|
||||||
const std::shared_ptr<const VlRandomExpr> m_expr; // Sub-expression
|
|
||||||
const unsigned m_idx; // Extracted index
|
|
||||||
|
|
||||||
public:
|
|
||||||
VlRandomExtract(std::shared_ptr<const VlRandomExpr> expr, unsigned idx)
|
|
||||||
: m_expr{expr}
|
|
||||||
, m_idx{idx} {}
|
|
||||||
void emit(std::ostream& s) const override;
|
|
||||||
};
|
|
||||||
|
|
||||||
class VlRandomBinOp final : public VlRandomExpr {
|
|
||||||
const char* const m_op; // Binary operation identifier
|
|
||||||
const std::shared_ptr<const VlRandomExpr> m_lhs, m_rhs; // Sub-expressions
|
|
||||||
|
|
||||||
public:
|
|
||||||
VlRandomBinOp(const char* op, std::shared_ptr<const VlRandomExpr> lhs,
|
|
||||||
std::shared_ptr<const VlRandomExpr> rhs)
|
|
||||||
: m_op{op}
|
|
||||||
, m_lhs{lhs}
|
|
||||||
, m_rhs{rhs} {}
|
|
||||||
void emit(std::ostream& s) const override;
|
|
||||||
};
|
};
|
||||||
|
|
||||||
//=============================================================================
|
//=============================================================================
|
||||||
@ -103,7 +61,7 @@ class VlRandomizer final {
|
|||||||
const VlQueue<CData>* m_randmode; // rand_mode state;
|
const VlQueue<CData>* m_randmode; // rand_mode state;
|
||||||
|
|
||||||
// PRIVATE METHODS
|
// PRIVATE METHODS
|
||||||
std::shared_ptr<const VlRandomExpr> randomConstraint(VlRNG& rngr, int bits);
|
void randomConstraint(std::ostream& os, VlRNG& rngr, int bits);
|
||||||
bool parseSolution(std::iostream& file);
|
bool parseSolution(std::iostream& file);
|
||||||
|
|
||||||
public:
|
public:
|
||||||
@ -119,6 +77,7 @@ public:
|
|||||||
std::uint32_t randmodeIdx = std::numeric_limits<std::uint32_t>::max()) {
|
std::uint32_t randmodeIdx = std::numeric_limits<std::uint32_t>::max()) {
|
||||||
auto it = m_vars.find(name);
|
auto it = m_vars.find(name);
|
||||||
if (it != m_vars.end()) return;
|
if (it != m_vars.end()) return;
|
||||||
|
// TODO: make_unique once VlRandomizer is per-instance not per-ref
|
||||||
m_vars[name] = std::make_shared<const VlRandomVar>(name, width, &var, randmodeIdx);
|
m_vars[name] = std::make_shared<const VlRandomVar>(name, width, &var, randmodeIdx);
|
||||||
}
|
}
|
||||||
void hard(std::string&& constraint);
|
void hard(std::string&& constraint);
|
||||||
|
Loading…
Reference in New Issue
Block a user