mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 03:32:29 +00:00
Code Activity

Added support for shifter cells to SAT generator

Browse source
This commit is contained in:
Clifford Wolf 2013-06-08 15:12:08 +02:00
parent 92f04eab10
commit 23a7973094
3 changed files with 43 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

33
kernel/satgen.h
View file

@ -51,11 +51,7 @@ struct SatGen
this->prefix = prefix;
}
virtual ~SatGen()
{
}
virtual std::vector<int> importSigSpec(RTLIL::SigSpec &sig)
std::vector<int> importSigSpec(RTLIL::SigSpec &sig)
{
RTLIL::SigSpec s = sig;
sigmap->apply(s);
@ -93,7 +89,7 @@ struct SatGen
vec_y.push_back(ez->literal());
}
virtual bool importCell(RTLIL::Cell *cell)
bool importCell(RTLIL::Cell *cell)
{
if (cell->type == "$_AND_" || cell->type == "$_OR_" || cell->type == "$_XOR_" ||
cell->type == "$and" || cell->type == "$or" || cell->type == "$xor" || cell->type == "$xnor" ||
@ -216,9 +212,32 @@ struct SatGen
return true;
}
// Unsupported internal cell types: $shl $shr $sshl $sshr $mul $div $mod $pow
if (cell->type == "$shl" || cell->type == "$shr" || cell->type == "$sshl" || cell->type == "$sshr") {
std::vector<int> a = importSigSpec(cell->connections.at("\\A"));
std::vector<int> b = importSigSpec(cell->connections.at("\\B"));
std::vector<int> y = importSigSpec(cell->connections.at("\\Y"));
char shift_left = cell->type == "$shl" || cell->type == "$sshl";
bool sign_extend = cell->type == "$sshr";
while (y.size() < a.size())
y.push_back(ez->literal());
std::vector<int> tmp = a;
for (size_t i = 0; i < b.size(); i++)
{
std::vector<int> tmp_shifted(tmp.size());
for (size_t j = 0; j < tmp.size(); j++) {
int idx = j + (1 << i) * (shift_left ? -1 : +1);
tmp_shifted.at(j) = (0 <= idx && idx < int(tmp.size())) ? tmp.at(idx) : sign_extend ? tmp.back() : ez->FALSE;
}
tmp = ez->vec_ite(b.at(i), tmp_shifted, tmp);
}
ez->assume(ez->vec_eq(tmp, y));
return true;
}
// Unsupported internal cell types: $mul $div $mod $pow
return false;
}
};
#endif

17
passes/sat/example.v
View file

@ -51,7 +51,20 @@ endmodule
// ------------------------------------
module example003(clk, rst, y);
module example003(a_shl, a_shr, a_sshl, a_sshr, sh, y_shl, y_shr, y_sshl, y_sshr);
input [7:0] a_shl, a_shr;
input signed [7:0] a_sshl, a_sshr;
input [3:0] sh;
output [7:0] y_shl = a_shl << sh, y_shr = a_shr >> sh;
output signed [7:0] y_sshl = a_sshl <<< sh, y_sshr = a_sshr >>> sh;
endmodule
// ------------------------------------
module example004(clk, rst, y);
input clk, rst;
output y;
@ -59,7 +72,7 @@ output y;
reg [3:0] counter;
always @(posedge clk)
case (1)
case (1'b1)
rst, counter == 9:
counter <= 0;
default:

3
passes/sat/example.ys
View file

@ -2,4 +2,5 @@ read_verilog example.v
proc; opt_clean
sat_solve -set y 1'b1 example001
sat_solve -set y 1'b1 example002
sat_solve -set y 1'b1 example003
sat_solve -set y_sshl 8'hf0 -set y_sshr 8'hf0 -set sh 4'd3 example003
sat_solve -set y 1'b1 example004