aboutsummaryrefslogtreecommitdiffstats
path: root/kernel/satgen.h
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/satgen.h')
-rw-r--r--kernel/satgen.h150
1 files changed, 146 insertions, 4 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 2f5efe674..e118c1569 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -2,11 +2,11 @@
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
+ *
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
- *
+ *
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
@@ -29,7 +29,37 @@
YOSYS_NAMESPACE_BEGIN
-typedef ezMiniSAT ezDefaultSAT;
+// defined in kernel/register.cc
+extern struct SatSolver *yosys_satsolver_list;
+extern struct SatSolver *yosys_satsolver;
+
+struct SatSolver
+{
+ string name;
+ SatSolver *next;
+ virtual ezSAT *create() = 0;
+
+ SatSolver(string name) : name(name) {
+ next = yosys_satsolver_list;
+ yosys_satsolver_list = this;
+ }
+
+ virtual ~SatSolver() {
+ auto p = &yosys_satsolver_list;
+ while (*p) {
+ if (*p == this)
+ *p = next;
+ else
+ p = &(*p)->next;
+ }
+ if (yosys_satsolver == this)
+ yosys_satsolver = yosys_satsolver_list;
+ }
+};
+
+struct ezSatPtr : public std::unique_ptr<ezSAT> {
+ ezSatPtr() : unique_ptr<ezSAT>(yosys_satsolver->create()) { }
+};
struct SatGen
{
@@ -38,6 +68,7 @@ struct SatGen
std::string prefix;
SigPool initial_state;
std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en;
+ std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en;
std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals;
bool ignore_div_by_zero;
bool model_undef;
@@ -131,6 +162,13 @@ struct SatGen
sig_en = asserts_en[pf];
}
+ void getAssumes(RTLIL::SigSpec &sig_a, RTLIL::SigSpec &sig_en, int timestep = -1)
+ {
+ std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+ sig_a = assumes_a[pf];
+ sig_en = assumes_en[pf];
+ }
+
int importAsserts(int timestep = -1)
{
std::vector<int> check_bits, enable_bits;
@@ -145,6 +183,20 @@ struct SatGen
return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
}
+ int importAssumes(int timestep = -1)
+ {
+ std::vector<int> check_bits, enable_bits;
+ std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+ if (model_undef) {
+ check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(assumes_a[pf], timestep)), importDefSigSpec(assumes_a[pf], timestep));
+ enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(assumes_en[pf], timestep)), importDefSigSpec(assumes_en[pf], timestep));
+ } else {
+ check_bits = importDefSigSpec(assumes_a[pf], timestep);
+ enable_bits = importDefSigSpec(assumes_en[pf], timestep);
+ }
+ return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
+ }
+
int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1)
{
if (timestep_rhs < 0)
@@ -928,7 +980,7 @@ struct SatGen
div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->CONST_FALSE);
}
} else {
- int copy_a_bits = std::min(cell->getPort("\\A").size(), cell->getPort("\\B").size());
+ int copy_a_bits = min(cell->getPort("\\A").size(), cell->getPort("\\B").size());
div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
@@ -996,6 +1048,88 @@ struct SatGen
return true;
}
+ if (cell->type == "$sop")
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
+ int y = importDefSigSpec(cell->getPort("\\Y"), timestep).at(0);
+
+ int width = cell->getParam("\\WIDTH").as_int();
+ int depth = cell->getParam("\\DEPTH").as_int();
+
+ vector<State> table_raw = cell->getParam("\\TABLE").bits;
+ while (GetSize(table_raw) < 2*width*depth)
+ table_raw.push_back(State::S0);
+
+ vector<vector<int>> table(depth);
+
+ for (int i = 0; i < depth; i++)
+ for (int j = 0; j < width; j++)
+ {
+ bool pat0 = (table_raw[2*width*i + 2*j + 0] == State::S1);
+ bool pat1 = (table_raw[2*width*i + 2*j + 1] == State::S1);
+
+ if (pat0 && !pat1)
+ table.at(i).push_back(0);
+ else if (!pat0 && pat1)
+ table.at(i).push_back(1);
+ else
+ table.at(i).push_back(-1);
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> products, undef_products;
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
+ int undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep).at(0);
+
+ for (int i = 0; i < depth; i++)
+ {
+ std::vector<int> cmp_a, cmp_ua, cmp_b;
+
+ for (int j = 0; j < width; j++)
+ if (table.at(i).at(j) >= 0) {
+ cmp_a.push_back(a.at(j));
+ cmp_ua.push_back(undef_a.at(j));
+ cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
+ }
+
+ std::vector<int> masked_a = ez->vec_or(cmp_a, cmp_ua);
+ std::vector<int> masked_b = ez->vec_or(cmp_b, cmp_ua);
+
+ int masked_eq = ez->vec_eq(masked_a, masked_b);
+ int any_undef = ez->expression(ezSAT::OpOr, cmp_ua);
+
+ undef_products.push_back(ez->AND(any_undef, masked_eq));
+ products.push_back(ez->AND(ez->NOT(any_undef), masked_eq));
+ }
+
+ int yy = ez->expression(ezSAT::OpOr, products);
+ ez->SET(undef_y, ez->AND(ez->NOT(yy), ez->expression(ezSAT::OpOr, undef_products)));
+ undefGating(y, yy, undef_y);
+ }
+ else
+ {
+ std::vector<int> products;
+
+ for (int i = 0; i < depth; i++)
+ {
+ std::vector<int> cmp_a, cmp_b;
+
+ for (int j = 0; j < width; j++)
+ if (table.at(i).at(j) >= 0) {
+ cmp_a.push_back(a.at(j));
+ cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE);
+ }
+
+ products.push_back(ez->vec_eq(cmp_a, cmp_b));
+ }
+
+ ez->SET(y, ez->expression(ezSAT::OpOr, products));
+ }
+
+ return true;
+ }
+
if (cell->type == "$fa")
{
std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
@@ -1204,6 +1338,14 @@ struct SatGen
return true;
}
+ if (cell->type == "$assume")
+ {
+ std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
+ assumes_a[pf].append((*sigmap)(cell->getPort("\\A")));
+ assumes_en[pf].append((*sigmap)(cell->getPort("\\EN")));
+ return true;
+ }
+
// Unsupported internal cell types: $pow $lut
// .. and all sequential cells except $dff and $_DFF_[NP]_
return false;
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-01 01:36:11 +0000