mirror of https://github.com/YosysHQ/yosys.git
Added verification of SAT model to "eval -vloghammer_report" command
This commit is contained in:
parent
259cc1391e
commit
18f9477e95
|
@ -53,17 +53,16 @@ struct SatGen
|
||||||
this->prefix = prefix;
|
this->prefix = prefix;
|
||||||
}
|
}
|
||||||
|
|
||||||
std::vector<int> importSigSpec(RTLIL::SigSpec &sig, int timestep = -1)
|
std::vector<int> importSigSpec(RTLIL::SigSpec sig, int timestep = -1)
|
||||||
{
|
{
|
||||||
assert(timestep < 0 || timestep > 0);
|
assert(timestep < 0 || timestep > 0);
|
||||||
RTLIL::SigSpec s = sig;
|
sigmap->apply(sig);
|
||||||
sigmap->apply(s);
|
sig.expand();
|
||||||
s.expand();
|
|
||||||
|
|
||||||
std::vector<int> vec;
|
std::vector<int> vec;
|
||||||
vec.reserve(s.chunks.size());
|
vec.reserve(sig.chunks.size());
|
||||||
|
|
||||||
for (auto &c : s.chunks)
|
for (auto &c : sig.chunks)
|
||||||
if (c.wire == NULL) {
|
if (c.wire == NULL) {
|
||||||
vec.push_back(c.data.as_bool() ? ez->TRUE : ez->FALSE);
|
vec.push_back(c.data.as_bool() ? ez->TRUE : ez->FALSE);
|
||||||
} else {
|
} else {
|
||||||
|
|
|
@ -24,6 +24,7 @@
|
||||||
#include "kernel/celltypes.h"
|
#include "kernel/celltypes.h"
|
||||||
#include "kernel/consteval.h"
|
#include "kernel/consteval.h"
|
||||||
#include "kernel/sigtools.h"
|
#include "kernel/sigtools.h"
|
||||||
|
#include "kernel/satgen.h"
|
||||||
#include "kernel/log.h"
|
#include "kernel/log.h"
|
||||||
#include <stdlib.h>
|
#include <stdlib.h>
|
||||||
#include <stdio.h>
|
#include <stdio.h>
|
||||||
|
@ -141,6 +142,43 @@ struct VlogHammerReporter
|
||||||
return list;
|
return list;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
void sat_check(RTLIL::Module *module, RTLIL::SigSpec recorded_set_vars, RTLIL::Const recorded_set_vals, RTLIL::SigSpec expected_y)
|
||||||
|
{
|
||||||
|
log("Verifying SAT model..\n");
|
||||||
|
|
||||||
|
ezDefaultSAT ez;
|
||||||
|
SigMap sigmap(module);
|
||||||
|
SatGen satgen(&ez, design, &sigmap);
|
||||||
|
|
||||||
|
for (auto &c : module->cells)
|
||||||
|
if (!satgen.importCell(c.second))
|
||||||
|
log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(c.first), RTLIL::id2cstr(c.second->type));
|
||||||
|
|
||||||
|
std::vector<int> rec_var_vec = satgen.importSigSpec(recorded_set_vars);
|
||||||
|
std::vector<int> rec_val_vec = satgen.importSigSpec(recorded_set_vals);
|
||||||
|
ez.assume(ez.vec_eq(rec_var_vec, rec_val_vec));
|
||||||
|
|
||||||
|
std::vector<int> y_vec = satgen.importSigSpec(module->wires.at("\\y"));
|
||||||
|
std::vector<bool> y_values;
|
||||||
|
|
||||||
|
log(" Created SAT problem with %d variables and %d clauses.\n",
|
||||||
|
ez.numCnfVariables(), ez.numCnfClauses());
|
||||||
|
|
||||||
|
if (!ez.solve(y_vec, y_values))
|
||||||
|
log_error("Failed to find solution to SAT problem.\n");
|
||||||
|
|
||||||
|
expected_y.expand();
|
||||||
|
assert(expected_y.chunks.size() == y_vec.size());
|
||||||
|
for (size_t i = 0; i < y_vec.size(); i++) {
|
||||||
|
RTLIL::State bit = expected_y.chunks.at(i).data.bits.at(0);
|
||||||
|
if ((bit == RTLIL::State::S0 || bit == RTLIL::State::S1) && ((bit == RTLIL::State::S1) != y_values.at(i)))
|
||||||
|
log_error("Found error in SAT model: y[%d] = %d, should be %d.\n",
|
||||||
|
int(i), int(y_values.at(i)), int(bit == RTLIL::State::S1));
|
||||||
|
}
|
||||||
|
|
||||||
|
log(" SAT model verified.\n");
|
||||||
|
}
|
||||||
|
|
||||||
void run()
|
void run()
|
||||||
{
|
{
|
||||||
for (int idx = 0; idx < int(patterns.size()); idx++)
|
for (int idx = 0; idx < int(patterns.size()); idx++)
|
||||||
|
@ -151,6 +189,8 @@ struct VlogHammerReporter
|
||||||
|
|
||||||
for (int mod = 0; mod < int(modules.size()); mod++)
|
for (int mod = 0; mod < int(modules.size()); mod++)
|
||||||
{
|
{
|
||||||
|
RTLIL::SigSpec recorded_set_vars;
|
||||||
|
RTLIL::Const recorded_set_vals;
|
||||||
RTLIL::Module *module = modules[mod];
|
RTLIL::Module *module = modules[mod];
|
||||||
std::string module_name = module_names[mod].c_str();
|
std::string module_name = module_names[mod].c_str();
|
||||||
ConstEval ce(module);
|
ConstEval ce(module);
|
||||||
|
@ -160,6 +200,8 @@ struct VlogHammerReporter
|
||||||
RTLIL::Wire *wire = module->wires.at(inputs[i]);
|
RTLIL::Wire *wire = module->wires.at(inputs[i]);
|
||||||
for (int j = input_widths[i]-1; j >= 0; j--) {
|
for (int j = input_widths[i]-1; j >= 0; j--) {
|
||||||
ce.set(RTLIL::SigSpec(wire, 1, j), bits.back());
|
ce.set(RTLIL::SigSpec(wire, 1, j), bits.back());
|
||||||
|
recorded_set_vars.append(RTLIL::SigSpec(wire, 1, j));
|
||||||
|
recorded_set_vals.bits.push_back(bits.back());
|
||||||
bits.pop_back();
|
bits.pop_back();
|
||||||
}
|
}
|
||||||
if (module == modules.front()) {
|
if (module == modules.front()) {
|
||||||
|
@ -188,6 +230,7 @@ struct VlogHammerReporter
|
||||||
if (module_name == "rtl") {
|
if (module_name == "rtl") {
|
||||||
rtl_sig = sig;
|
rtl_sig = sig;
|
||||||
rtl_sig.expand();
|
rtl_sig.expand();
|
||||||
|
sat_check(module, recorded_set_vars, recorded_set_vals, sig);
|
||||||
} else if (rtl_sig.width > 0) {
|
} else if (rtl_sig.width > 0) {
|
||||||
sig.expand();
|
sig.expand();
|
||||||
if (rtl_sig.width != sig.width)
|
if (rtl_sig.width != sig.width)
|
||||||
|
|
Loading…
Reference in New Issue