mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 05:19:11 +00:00
Code Activity

Added ezsat vec_const() api

Browse source
This commit is contained in:
Clifford Wolf 2013-11-25 15:10:32 +01:00
parent 8c3f4b3957
commit 11e8118589
2 changed files with 26 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

32
libs/ezsat/ezsat.cc
View file

@ -651,34 +651,42 @@ bool ezSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> &
return false; return false;
} }
std::vector<int> ezSAT::vec_const_signed(int64_t value, int bits) std::vector<int> ezSAT::vec_const(const std::vector<bool> &bits)
{ {
std::vector<int> vec; std::vector<int> vec;
for (int i = 0; i < bits; i++) for (auto bit : bits)
vec.push_back(bit ? TRUE : FALSE);
return vec;
}
std::vector<int> ezSAT::vec_const_signed(int64_t value, int numBits)
{
std::vector<int> vec;
for (int i = 0; i < numBits; i++)
vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE); vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE);
return vec; return vec;
} }
std::vector<int> ezSAT::vec_const_unsigned(uint64_t value, int bits) std::vector<int> ezSAT::vec_const_unsigned(uint64_t value, int numBits)
{ {
std::vector<int> vec; std::vector<int> vec;
for (int i = 0; i < bits; i++) for (int i = 0; i < numBits; i++)
vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE); vec.push_back(((value >> i) & 1) != 0 ? TRUE : FALSE);
return vec; return vec;
} }
std::vector<int> ezSAT::vec_var(int bits) std::vector<int> ezSAT::vec_var(int numBits)
{ {
std::vector<int> vec; std::vector<int> vec;
for (int i = 0; i < bits; i++) for (int i = 0; i < numBits; i++)
vec.push_back(literal()); vec.push_back(literal());
return vec; return vec;
} }
std::vector<int> ezSAT::vec_var(std::string name, int bits) std::vector<int> ezSAT::vec_var(std::string name, int numBits)
{ {
std::vector<int> vec; std::vector<int> vec;
for (int i = 0; i < bits; i++) for (int i = 0; i < numBits; i++)
vec.push_back(VAR(name + "[" + std::to_string(i) + "]")); vec.push_back(VAR(name + "[" + std::to_string(i) + "]"));
return vec; return vec;
} }
@ -782,21 +790,21 @@ static void halfadder(ezSAT *that, int a, int b, int &y, int &x)
x = new_x, y = new_y; x = new_x, y = new_y;
} }
std::vector<int> ezSAT::vec_count(const std::vector<int> &vec, int bits, bool clip) std::vector<int> ezSAT::vec_count(const std::vector<int> &vec, int numBits, bool clip)
{ {
std::vector<int> sum = vec_const_unsigned(0, bits); std::vector<int> sum = vec_const_unsigned(0, numBits);
std::vector<int> carry_vector; std::vector<int> carry_vector;
for (auto bit : vec) { for (auto bit : vec) {
int carry = bit; int carry = bit;
for (int i = 0; i < bits; i++) for (int i = 0; i < numBits; i++)
halfadder(this, carry, sum[i], carry, sum[i]); halfadder(this, carry, sum[i], carry, sum[i]);
carry_vector.push_back(carry); carry_vector.push_back(carry);
} }
if (clip) { if (clip) {
int overflow = vec_reduce_or(carry_vector); int overflow = vec_reduce_or(carry_vector);
sum = vec_ite(overflow, vec_const_unsigned(~0, bits), sum); sum = vec_ite(overflow, vec_const_unsigned(~0, numBits), sum);
} }
#if 0 #if 0

11
libs/ezsat/ezsat.h
View file

@ -203,10 +203,11 @@ public:
// simple helpers for building expressions with bit vectors // simple helpers for building expressions with bit vectors
std::vector<int> vec_const_signed(int64_t value, int bits); std::vector<int> vec_const(const std::vector<bool> &bits);
std::vector<int> vec_const_unsigned(uint64_t value, int bits); std::vector<int> vec_const_signed(int64_t value, int numBits);
std::vector<int> vec_var(int bits); std::vector<int> vec_const_unsigned(uint64_t value, int numBits);
std::vector<int> vec_var(std::string name, int bits); std::vector<int> vec_var(int numBits);
std::vector<int> vec_var(std::string name, int numBits);
std::vector<int> vec_cast(const std::vector<int> &vec1, int toBits, bool signExtend = false); std::vector<int> vec_cast(const std::vector<int> &vec1, int toBits, bool signExtend = false);
std::vector<int> vec_not(const std::vector<int> &vec1); std::vector<int> vec_not(const std::vector<int> &vec1);
@ -218,7 +219,7 @@ public:
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(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> &vec2, const std::vector<int> &vec3);
std::vector<int> vec_count(const std::vector<int> &vec, int bits, bool clip = true); 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); std::vector<int> vec_add(const std::vector<int> &vec1, const std::vector<int> &vec2);
std::vector<int> vec_sub(const std::vector<int> &vec1, const std::vector<int> &vec2); std::vector<int> vec_sub(const std::vector<int> &vec1, const std::vector<int> &vec2);
std::vector<int> vec_neg(const std::vector<int> &vec); std::vector<int> vec_neg(const std::vector<int> &vec);