riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Added native support for shift operations to ezSAT

This commit is contained in:
Clifford Wolf 2014-07-30 17:17:31 +02:00
parent 45fd26b76e
commit 9b566a7efa
2 changed files with 95 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

90
libs/ezsat/ezsat.cc
View File

@ -977,6 +977,96 @@ std::vector<int> ezSAT::vec_srl(const std::vector<int> &vec1, int shift)
return vec;
}
std::vector<int> ezSAT::vec_shift(const std::vector<int> &vec1, int shift, int extend_left, int extend_right)
{
std::vector<int> vec;
for (int i = 0; i < int(vec1.size()); i++) {
int j = i+shift;
if (j < 0)
vec.push_back(extend_right);
else if (j >= int(vec1.size()))
vec.push_back(extend_left);
else
vec.push_back(vec1[j]);
}
return vec;
}
static int my_clog2(int x)
{
int result = 0;
for (x--; x > 0; result++)
x >>= 1;
return result;
}
std::vector<int> ezSAT::vec_shift_right(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right)
{
int vec2_bits = std::min(my_clog2(vec1.size()) + (vec2_signed ? 1 : 0), int(vec2.size()));
std::vector<int> overflow_bits(vec2.begin() + vec2_bits, vec2.end());
int overflow_left = FALSE, overflow_right = FALSE;
if (vec2_signed) {
int overflow = FALSE;
for (auto bit : overflow_bits)
overflow = OR(overflow, XOR(bit, vec2[vec2_bits-1]));
overflow_left = AND(overflow, NOT(vec2.back()));
overflow_right = AND(overflow, vec2.back());
} else
overflow_left = vec_reduce_or(overflow_bits);
std::vector<int> buffer = vec1;
if (vec2_signed)
while (buffer.size() < vec1.size() + (1 << vec2_bits))
buffer.push_back(extend_left);
std::vector<int> overflow_pattern_left(buffer.size(), extend_left);
std::vector<int> overflow_pattern_right(buffer.size(), extend_right);
buffer = vec_ite(overflow_left, overflow_pattern_left, buffer);
if (vec2_signed)
buffer = vec_ite(overflow_right, overflow_pattern_left, buffer);
for (int i = vec2_bits-1; i >= 0; i--) {
std::vector<int> shifted_buffer;
if (vec2_signed && i == vec2_bits-1)
shifted_buffer = vec_shift(buffer, -(1 << i), extend_left, extend_right);
else
shifted_buffer = vec_shift(buffer, 1 << i, extend_left, extend_right);
buffer = vec_ite(vec2[i], shifted_buffer, buffer);
}
buffer.resize(vec1.size());
return buffer;
}
std::vector<int> ezSAT::vec_shift_left(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right)
{
// vec2_signed is not implemented in vec_shift_left() yet
assert(vec2_signed == false);
int vec2_bits = std::min(my_clog2(vec1.size()), int(vec2.size()));
std::vector<int> overflow_bits(vec2.begin() + vec2_bits, vec2.end());
int overflow = vec_reduce_or(overflow_bits);
std::vector<int> buffer = vec1;
std::vector<int> overflow_pattern_right(buffer.size(), extend_right);
buffer = vec_ite(overflow, overflow_pattern_right, buffer);
for (int i = 0; i < vec2_bits; i++) {
std::vector<int> shifted_buffer;
shifted_buffer = vec_shift(buffer, -(1 << i), extend_left, extend_right);
buffer = vec_ite(vec2[i], shifted_buffer, buffer);
}
buffer.resize(vec1.size());
return buffer;
}
void ezSAT::vec_append(std::vector<int> &vec, const std::vector<int> &vec1) const
{
for (auto bit : vec1)

6
libs/ezsat/ezsat.h
View File

@ -237,7 +237,7 @@ public:
std::vector<int> vec_iff(const std::vector<int> &vec1, const std::vector<int> &vec2);
std::vector<int> vec_ite(const std::vector<int> &vec1, const std::vector<int> &vec2, const std::vector<int> &vec3);
std::vector<int> vec_ite(int sel, const std::vector<int> &vec2, const std::vector<int> &vec3);
std::vector<int> vec_ite(int sel, const std::vector<int> &vec1, const std::vector<int> &vec2);
std::vector<int> vec_count(const std::vector<int> &vec, int numBits, bool clip = true);
std::vector<int> vec_add(const std::vector<int> &vec1, const std::vector<int> &vec2);
@ -265,6 +265,10 @@ public:
std::vector<int> vec_shr(const std::vector<int> &vec1, int shift, bool signExtend = false) { return vec_shl(vec1, -shift, signExtend); }
std::vector<int> vec_srr(const std::vector<int> &vec1, int shift) { return vec_srl(vec1, -shift); }
std::vector<int> vec_shift(const std::vector<int> &vec1, int shift, int extend_left, int extend_right);
std::vector<int> vec_shift_right(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right);
std::vector<int> vec_shift_left(const std::vector<int> &vec1, const std::vector<int> &vec2, bool vec2_signed, int extend_left, int extend_right);
void vec_append(std::vector<int> &vec, const std::vector<int> &vec1) const;
void vec_append_signed(std::vector<int> &vec, const std::vector<int> &vec1, int64_t value);
void vec_append_unsigned(std::vector<int> &vec, const std::vector<int> &vec1, uint64_t value);