mirror of
https://github.com/YosysHQ/yosys
synced 2026-03-23 04:49:15 +00:00
Merge 39d9be2df9 into 5fd39ff3e1
This commit is contained in:
commit
f6be844d30
19 changed files with 2153 additions and 3 deletions
1
Makefile
1
Makefile
|
|
@ -953,6 +953,7 @@ MK_TEST_DIRS += tests/verilog
|
|||
|
||||
# Tests that don't generate .mk
|
||||
SH_TEST_DIRS =
|
||||
SH_TEST_DIRS += tests/csa_tree
|
||||
SH_TEST_DIRS += tests/simple
|
||||
SH_TEST_DIRS += tests/simple_abc9
|
||||
SH_TEST_DIRS += tests/hana
|
||||
|
|
|
|||
|
|
@ -23,6 +23,7 @@ OBJS += passes/opt/opt_ffinv.o
|
|||
OBJS += passes/opt/pmux2shiftx.o
|
||||
OBJS += passes/opt/muxpack.o
|
||||
OBJS += passes/opt/opt_balance_tree.o
|
||||
OBJS += passes/opt/csa_tree.o
|
||||
|
||||
OBJS += passes/opt/peepopt.o
|
||||
GENFILES += passes/opt/peepopt_pm.h
|
||||
|
|
|
|||
517
passes/opt/csa_tree.cc
Normal file
517
passes/opt/csa_tree.cc
Normal file
|
|
@ -0,0 +1,517 @@
|
|||
#include "kernel/yosys.h"
|
||||
#include "kernel/sigtools.h"
|
||||
#include "kernel/macc.h"
|
||||
|
||||
#include <queue>
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
PRIVATE_NAMESPACE_BEGIN
|
||||
|
||||
struct Operand {
|
||||
SigSpec sig;
|
||||
bool is_signed;
|
||||
bool negate;
|
||||
};
|
||||
|
||||
struct CsaTreeWorker
|
||||
{
|
||||
Module* module;
|
||||
SigMap sigmap;
|
||||
|
||||
dict<SigBit, pool<Cell*>> bit_consumers;
|
||||
dict<SigBit, int> fanout;
|
||||
|
||||
pool<Cell*> addsub_cells;
|
||||
pool<Cell*> alu_cells;
|
||||
pool<Cell*> macc_cells;
|
||||
|
||||
CsaTreeWorker(Module* module) : module(module), sigmap(module) {}
|
||||
|
||||
static bool is_addsub(Cell* cell)
|
||||
{
|
||||
return cell->type == ID($add) || cell->type == ID($sub);
|
||||
}
|
||||
|
||||
static bool is_alu(Cell* cell)
|
||||
{
|
||||
return cell->type == ID($alu);
|
||||
}
|
||||
|
||||
static bool is_macc(Cell* cell)
|
||||
{
|
||||
return cell->type == ID($macc) || cell->type == ID($macc_v2);
|
||||
}
|
||||
|
||||
bool alu_is_subtract(Cell* cell)
|
||||
{
|
||||
SigSpec bi = sigmap(cell->getPort(ID::BI));
|
||||
SigSpec ci = sigmap(cell->getPort(ID::CI));
|
||||
return GetSize(bi) == 1 && bi[0] == State::S1 && GetSize(ci) == 1 && ci[0] == State::S1;
|
||||
}
|
||||
|
||||
bool alu_is_add(Cell* cell)
|
||||
{
|
||||
SigSpec bi = sigmap(cell->getPort(ID::BI));
|
||||
SigSpec ci = sigmap(cell->getPort(ID::CI));
|
||||
return GetSize(bi) == 1 && bi[0] == State::S0 && GetSize(ci) == 1 && ci[0] == State::S0;
|
||||
}
|
||||
|
||||
bool alu_is_chainable(Cell* cell)
|
||||
{
|
||||
if (!(alu_is_add(cell) || alu_is_subtract(cell)))
|
||||
return false;
|
||||
|
||||
for (auto bit : sigmap(cell->getPort(ID::X)))
|
||||
if (fanout.count(bit) && fanout[bit] > 0)
|
||||
return false;
|
||||
for (auto bit : sigmap(cell->getPort(ID::CO)))
|
||||
if (fanout.count(bit) && fanout[bit] > 0)
|
||||
return false;
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
bool is_chainable(Cell* cell)
|
||||
{
|
||||
return is_addsub(cell) || (is_alu(cell) && alu_is_chainable(cell));
|
||||
}
|
||||
|
||||
void classify_cells()
|
||||
{
|
||||
for (auto cell : module->cells()) {
|
||||
if (is_addsub(cell))
|
||||
addsub_cells.insert(cell);
|
||||
else if (is_alu(cell))
|
||||
alu_cells.insert(cell);
|
||||
else if (is_macc(cell))
|
||||
macc_cells.insert(cell);
|
||||
}
|
||||
}
|
||||
|
||||
void build_fanout_map()
|
||||
{
|
||||
for (auto cell : module->cells())
|
||||
for (auto& conn : cell->connections())
|
||||
if (cell->input(conn.first))
|
||||
for (auto bit : sigmap(conn.second))
|
||||
bit_consumers[bit].insert(cell);
|
||||
|
||||
for (auto& pair : bit_consumers)
|
||||
fanout[pair.first] = pair.second.size();
|
||||
|
||||
for (auto wire : module->wires())
|
||||
if (wire->port_output)
|
||||
for (auto bit : sigmap(SigSpec(wire)))
|
||||
fanout[bit]++;
|
||||
}
|
||||
|
||||
Cell* sole_chainable_consumer(SigSpec sig, const pool<Cell*>& candidates)
|
||||
{
|
||||
Cell* consumer = nullptr;
|
||||
for (auto bit : sig) {
|
||||
if (!fanout.count(bit) || fanout[bit] != 1)
|
||||
return nullptr;
|
||||
if (!bit_consumers.count(bit) || bit_consumers[bit].size() != 1)
|
||||
return nullptr;
|
||||
|
||||
Cell* c = *bit_consumers[bit].begin();
|
||||
if (!candidates.count(c))
|
||||
return nullptr;
|
||||
|
||||
if (consumer == nullptr)
|
||||
consumer = c;
|
||||
else if (consumer != c)
|
||||
return nullptr;
|
||||
}
|
||||
return consumer;
|
||||
}
|
||||
|
||||
dict<Cell*, Cell*> find_parents(const pool<Cell*>& candidates)
|
||||
{
|
||||
dict<Cell*, Cell*> parent_of;
|
||||
for (auto cell : candidates) {
|
||||
Cell* consumer = sole_chainable_consumer(
|
||||
sigmap(cell->getPort(ID::Y)), candidates);
|
||||
if (consumer && consumer != cell)
|
||||
parent_of[cell] = consumer;
|
||||
}
|
||||
return parent_of;
|
||||
}
|
||||
|
||||
pool<Cell*> collect_chain(Cell* root, const dict<Cell*, pool<Cell*>>& children_of)
|
||||
{
|
||||
pool<Cell*> chain;
|
||||
std::queue<Cell*> q;
|
||||
q.push(root);
|
||||
while (!q.empty()) {
|
||||
Cell* cur = q.front(); q.pop();
|
||||
if (!chain.insert(cur).second)
|
||||
continue;
|
||||
auto it = children_of.find(cur);
|
||||
if (it != children_of.end())
|
||||
for (auto child : it->second)
|
||||
q.push(child);
|
||||
}
|
||||
return chain;
|
||||
}
|
||||
|
||||
pool<SigBit> internal_bits(const pool<Cell*>& chain)
|
||||
{
|
||||
pool<SigBit> bits;
|
||||
for (auto cell : chain)
|
||||
for (auto bit : sigmap(cell->getPort(ID::Y)))
|
||||
bits.insert(bit);
|
||||
return bits;
|
||||
}
|
||||
|
||||
static bool overlaps(SigSpec sig, const pool<SigBit>& bits)
|
||||
{
|
||||
for (auto bit : sig)
|
||||
if (bits.count(bit))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool feeds_subtracted_port(Cell* child, Cell* parent)
|
||||
{
|
||||
bool parent_subtracts;
|
||||
if (parent->type == ID($sub))
|
||||
parent_subtracts = true;
|
||||
else if (is_alu(parent))
|
||||
parent_subtracts = alu_is_subtract(parent);
|
||||
else
|
||||
return false;
|
||||
|
||||
if (!parent_subtracts)
|
||||
return false;
|
||||
|
||||
SigSpec child_y = sigmap(child->getPort(ID::Y));
|
||||
SigSpec parent_b = sigmap(parent->getPort(ID::B));
|
||||
for (auto bit : child_y)
|
||||
for (auto pbit : parent_b)
|
||||
if (bit == pbit)
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
std::vector<Operand> extract_chain_operands(
|
||||
const pool<Cell*>& chain,
|
||||
Cell* root,
|
||||
const dict<Cell*, Cell*>& parent_of,
|
||||
int& correction
|
||||
) {
|
||||
pool<SigBit> chain_bits = internal_bits(chain);
|
||||
dict<Cell*, bool> negated;
|
||||
negated[root] = false;
|
||||
{
|
||||
std::queue<Cell*> q;
|
||||
q.push(root);
|
||||
while (!q.empty()) {
|
||||
Cell* cur = q.front(); q.pop();
|
||||
for (auto cell : chain) {
|
||||
if (!parent_of.count(cell) || parent_of.at(cell) != cur)
|
||||
continue;
|
||||
if (negated.count(cell))
|
||||
continue;
|
||||
negated[cell] = negated[cur] ^ feeds_subtracted_port(cell, cur);
|
||||
q.push(cell);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
std::vector<Operand> operands;
|
||||
correction = 0;
|
||||
|
||||
for (auto cell : chain) {
|
||||
bool cell_neg;
|
||||
if (negated.count(cell))
|
||||
cell_neg = negated[cell];
|
||||
else
|
||||
cell_neg = false;
|
||||
|
||||
SigSpec a = sigmap(cell->getPort(ID::A));
|
||||
SigSpec b = sigmap(cell->getPort(ID::B));
|
||||
bool a_signed = cell->getParam(ID::A_SIGNED).as_bool();
|
||||
bool b_signed = cell->getParam(ID::B_SIGNED).as_bool();
|
||||
bool b_sub = (cell->type == ID($sub)) || (is_alu(cell) && alu_is_subtract(cell));
|
||||
|
||||
if (!overlaps(a, chain_bits)) {
|
||||
bool neg = cell_neg;
|
||||
operands.push_back({a, a_signed, neg});
|
||||
if (neg) correction++;
|
||||
}
|
||||
if (!overlaps(b, chain_bits)) {
|
||||
bool neg = cell_neg ^ b_sub;
|
||||
operands.push_back({b, b_signed, neg});
|
||||
if (neg) correction++;
|
||||
}
|
||||
}
|
||||
return operands;
|
||||
}
|
||||
|
||||
bool extract_macc_operands(Cell* cell, std::vector<Operand>& operands, int& correction)
|
||||
{
|
||||
Macc macc(cell);
|
||||
correction = 0;
|
||||
|
||||
for (auto& term : macc.terms) {
|
||||
if (GetSize(term.in_b) != 0)
|
||||
return false;
|
||||
operands.push_back({term.in_a, term.is_signed, term.do_subtract});
|
||||
if (term.do_subtract)
|
||||
correction++;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
SigSpec extend_operand(SigSpec sig, bool is_signed, int width)
|
||||
{
|
||||
if (GetSize(sig) < width) {
|
||||
SigBit pad;
|
||||
if (is_signed && GetSize(sig) > 0)
|
||||
pad = sig[GetSize(sig) - 1];
|
||||
else
|
||||
pad = State::S0;
|
||||
sig.append(SigSpec(pad, width - GetSize(sig)));
|
||||
}
|
||||
if (GetSize(sig) > width)
|
||||
sig = sig.extract(0, width);
|
||||
return sig;
|
||||
}
|
||||
|
||||
SigSpec emit_not(SigSpec sig, int width)
|
||||
{
|
||||
SigSpec out = module->addWire(NEW_ID, width);
|
||||
Cell* inv = module->addCell(NEW_ID, ID($not));
|
||||
inv->setParam(ID::A_SIGNED, false);
|
||||
inv->setParam(ID::A_WIDTH, width);
|
||||
inv->setParam(ID::Y_WIDTH, width);
|
||||
inv->setPort(ID::A, sig);
|
||||
inv->setPort(ID::Y, out);
|
||||
return out;
|
||||
}
|
||||
|
||||
std::pair<SigSpec, SigSpec> emit_fa(SigSpec a, SigSpec b, SigSpec c, int width)
|
||||
{
|
||||
SigSpec sum = module->addWire(NEW_ID, width);
|
||||
SigSpec cout = module->addWire(NEW_ID, width);
|
||||
|
||||
Cell* fa = module->addCell(NEW_ID, ID($fa));
|
||||
fa->setParam(ID::WIDTH, width);
|
||||
fa->setPort(ID::A, a);
|
||||
fa->setPort(ID::B, b);
|
||||
fa->setPort(ID::C, c);
|
||||
fa->setPort(ID::X, cout);
|
||||
fa->setPort(ID::Y, sum);
|
||||
|
||||
SigSpec carry;
|
||||
carry.append(State::S0);
|
||||
carry.append(cout.extract(0, width - 1));
|
||||
return {sum, carry};
|
||||
}
|
||||
|
||||
void emit_final_add(SigSpec a, SigSpec b, SigSpec y, int width)
|
||||
{
|
||||
Cell* add = module->addCell(NEW_ID, ID($add));
|
||||
add->setParam(ID::A_SIGNED, false);
|
||||
add->setParam(ID::B_SIGNED, false);
|
||||
add->setParam(ID::A_WIDTH, width);
|
||||
add->setParam(ID::B_WIDTH, width);
|
||||
add->setParam(ID::Y_WIDTH, width);
|
||||
add->setPort(ID::A, a);
|
||||
add->setPort(ID::B, b);
|
||||
add->setPort(ID::Y, y);
|
||||
}
|
||||
|
||||
struct DepthSig {
|
||||
SigSpec sig;
|
||||
int depth;
|
||||
};
|
||||
|
||||
std::pair<SigSpec, SigSpec> reduce_wallace(std::vector<SigSpec>& sigs, int width, int& fa_count)
|
||||
{
|
||||
std::vector<DepthSig> ops;
|
||||
ops.reserve(sigs.size());
|
||||
for (auto& s : sigs)
|
||||
ops.push_back({s, 0});
|
||||
|
||||
fa_count = 0;
|
||||
|
||||
for (int level = 0; ops.size() > 2; level++) {
|
||||
log_assert(level <= 100);
|
||||
|
||||
std::vector<DepthSig> ready, waiting;
|
||||
for (auto& op : ops) {
|
||||
if (op.depth <= level)
|
||||
ready.push_back(op);
|
||||
else
|
||||
waiting.push_back(op);
|
||||
}
|
||||
|
||||
if (ready.size() < 3) continue;
|
||||
|
||||
std::vector<DepthSig> next;
|
||||
size_t i = 0;
|
||||
while (i + 2 < ready.size()) {
|
||||
auto [sum, carry] = emit_fa(ready[i].sig, ready[i + 1].sig, ready[i + 2].sig, width);
|
||||
int d = std::max({ready[i].depth, ready[i + 1].depth,ready[i + 2].depth}) + 1;
|
||||
next.push_back({sum, d});
|
||||
next.push_back({carry, d});
|
||||
fa_count++;
|
||||
i += 3;
|
||||
}
|
||||
for (; i < ready.size(); i++)
|
||||
next.push_back(ready[i]);
|
||||
for (auto& op : waiting)
|
||||
next.push_back(op);
|
||||
|
||||
ops = std::move(next);
|
||||
}
|
||||
|
||||
log_assert(ops.size() == 2);
|
||||
log(" Tree depth: %d FA levels + 1 final add\n",
|
||||
std::max(ops[0].depth, ops[1].depth));
|
||||
return {ops[0].sig, ops[1].sig};
|
||||
}
|
||||
|
||||
void replace_with_csa_tree(
|
||||
std::vector<Operand>& operands,
|
||||
SigSpec result_y,
|
||||
int correction,
|
||||
const char* desc
|
||||
) {
|
||||
int width = GetSize(result_y);
|
||||
std::vector<SigSpec> extended;
|
||||
extended.reserve(operands.size() + 1);
|
||||
|
||||
for (auto& op : operands) {
|
||||
SigSpec s = extend_operand(op.sig, op.is_signed, width);
|
||||
if (op.negate)
|
||||
s = emit_not(s, width);
|
||||
extended.push_back(s);
|
||||
}
|
||||
|
||||
if (correction > 0)
|
||||
extended.push_back(SigSpec(correction, width));
|
||||
|
||||
int fa_count;
|
||||
auto [a, b] = reduce_wallace(extended, width, fa_count);
|
||||
|
||||
log(" %s → %d $fa + 1 $add (%d operands, module %s)\n",
|
||||
desc, fa_count, (int)operands.size(), log_id(module));
|
||||
|
||||
emit_final_add(a, b, result_y, width);
|
||||
}
|
||||
|
||||
void process_chains()
|
||||
{
|
||||
pool<Cell*> candidates;
|
||||
for (auto cell : addsub_cells)
|
||||
candidates.insert(cell);
|
||||
for (auto cell : alu_cells)
|
||||
if (alu_is_chainable(cell))
|
||||
candidates.insert(cell);
|
||||
|
||||
if (candidates.empty())
|
||||
return;
|
||||
|
||||
auto parent_of = find_parents(candidates);
|
||||
|
||||
dict<Cell*, pool<Cell*>> children_of;
|
||||
pool<Cell*> has_parent;
|
||||
for (auto& [child, parent] : parent_of) {
|
||||
children_of[parent].insert(child);
|
||||
has_parent.insert(child);
|
||||
}
|
||||
|
||||
pool<Cell*> processed;
|
||||
for (auto root : candidates) {
|
||||
if (has_parent.count(root) || processed.count(root))
|
||||
continue;
|
||||
|
||||
pool<Cell*> chain = collect_chain(root, children_of);
|
||||
if (chain.size() < 2)
|
||||
continue;
|
||||
|
||||
for (auto c : chain)
|
||||
processed.insert(c);
|
||||
|
||||
int correction;
|
||||
auto operands = extract_chain_operands(
|
||||
chain, root, parent_of, correction);
|
||||
if (operands.size() < 3)
|
||||
continue;
|
||||
|
||||
replace_with_csa_tree(operands, root->getPort(ID::Y),
|
||||
correction, "Replaced add/sub chain");
|
||||
for (auto cell : chain)
|
||||
module->remove(cell);
|
||||
}
|
||||
}
|
||||
|
||||
void process_maccs()
|
||||
{
|
||||
for (auto cell : macc_cells) {
|
||||
std::vector<Operand> operands;
|
||||
int correction;
|
||||
if (!extract_macc_operands(cell, operands, correction))
|
||||
continue;
|
||||
if (operands.size() < 3)
|
||||
continue;
|
||||
|
||||
replace_with_csa_tree(operands, cell->getPort(ID::Y),
|
||||
correction, "Replaced $macc");
|
||||
module->remove(cell);
|
||||
}
|
||||
}
|
||||
|
||||
void run()
|
||||
{
|
||||
classify_cells();
|
||||
|
||||
if (addsub_cells.empty() && alu_cells.empty() && macc_cells.empty())
|
||||
return;
|
||||
|
||||
build_fanout_map();
|
||||
process_chains();
|
||||
process_maccs();
|
||||
}
|
||||
};
|
||||
|
||||
struct CsaTreePass : public Pass {
|
||||
CsaTreePass() : Pass("csa_tree",
|
||||
"convert add/sub/macc chains to carry-save adder trees") {}
|
||||
|
||||
void help() override
|
||||
{
|
||||
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
|
||||
log("\n");
|
||||
log(" csa_tree [selection]\n");
|
||||
log("\n");
|
||||
log("This pass replaces chains of $add/$sub cells, $alu cells (with constant\n");
|
||||
log("BI/CI), and $macc/$macc_v2 cells (without multiplications) with carry-save\n");
|
||||
log("adder trees using $fa cells and a single final $add.\n");
|
||||
log("\n");
|
||||
log("The tree uses Wallace-tree scheduling: at each level, ready operands are\n");
|
||||
log("grouped into triplets and compressed via full adders, giving\n");
|
||||
log("O(log_{1.5} N) depth for N input operands.\n");
|
||||
log("\n");
|
||||
}
|
||||
|
||||
void execute(std::vector<std::string> args, RTLIL::Design* design) override
|
||||
{
|
||||
log_header(design, "Executing CSA_TREE pass.\n");
|
||||
|
||||
size_t argidx;
|
||||
for (argidx = 1; argidx < args.size(); argidx++)
|
||||
break;
|
||||
extra_args(args, argidx, design);
|
||||
|
||||
for (auto module : design->selected_modules()) {
|
||||
CsaTreeWorker worker(module);
|
||||
worker.run();
|
||||
}
|
||||
}
|
||||
} CsaTreePass;
|
||||
|
||||
PRIVATE_NAMESPACE_END
|
||||
|
|
@ -67,6 +67,10 @@ struct SynthPass : public ScriptPass {
|
|||
log(" -booth\n");
|
||||
log(" run the booth pass to map $mul to Booth encoded multipliers\n");
|
||||
log("\n");
|
||||
log(" -csa\n");
|
||||
log(" run the csa_tree pass to convert $add/$sub chains and $macc cells to\n");
|
||||
log(" carry-save adder trees.\n");
|
||||
log("\n");
|
||||
log(" -noalumacc\n");
|
||||
log(" do not run 'alumacc' pass. i.e. keep arithmetic operators in\n");
|
||||
log(" their direct form ($add, $sub, etc.).\n");
|
||||
|
|
@ -108,7 +112,7 @@ struct SynthPass : public ScriptPass {
|
|||
}
|
||||
|
||||
string top_module, fsm_opts, memory_opts, abc;
|
||||
bool autotop, flatten, noalumacc, nofsm, noabc, noshare, flowmap, booth, hieropt, relative_share;
|
||||
bool autotop, flatten, noalumacc, nofsm, noabc, noshare, flowmap, booth, csa, hieropt, relative_share;
|
||||
int lut;
|
||||
std::vector<std::string> techmap_maps;
|
||||
|
||||
|
|
@ -127,6 +131,7 @@ struct SynthPass : public ScriptPass {
|
|||
noshare = false;
|
||||
flowmap = false;
|
||||
booth = false;
|
||||
csa = false;
|
||||
hieropt = false;
|
||||
relative_share = false;
|
||||
abc = "abc";
|
||||
|
|
@ -187,7 +192,10 @@ struct SynthPass : public ScriptPass {
|
|||
booth = true;
|
||||
continue;
|
||||
}
|
||||
|
||||
if (args[argidx] == "-csa") {
|
||||
csa = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-nordff") {
|
||||
memory_opts += " -nordff";
|
||||
continue;
|
||||
|
|
@ -289,6 +297,8 @@ struct SynthPass : public ScriptPass {
|
|||
run("booth", " (if -booth)");
|
||||
if (!noalumacc)
|
||||
run("alumacc", " (unless -noalumacc)");
|
||||
if (csa || help_mode)
|
||||
run("csa_tree", " (if -csa)");
|
||||
if (!noshare)
|
||||
run("share", " (unless -noshare)");
|
||||
run("opt" + hieropt_flag);
|
||||
|
|
@ -301,7 +311,7 @@ struct SynthPass : public ScriptPass {
|
|||
run("memory_map");
|
||||
run("opt -full");
|
||||
if (help_mode) {
|
||||
run(techmap_cmd, " (unless -extra-map)");
|
||||
run(techmap_cmd, " (unless -extra-map)");
|
||||
run(techmap_cmd + " -map +/techmap.v -map <inject>", " (if -extra-map)");
|
||||
} else {
|
||||
std::string techmap_opts;
|
||||
|
|
|
|||
61
tests/csa_tree/csa_tree_add_chains.ys
Normal file
61
tests/csa_tree/csa_tree_add_chains.ys
Normal file
|
|
@ -0,0 +1,61 @@
|
|||
read_verilog <<EOT
|
||||
module add3(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add5(
|
||||
input [11:0] a, b, c, d, e,
|
||||
output [11:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add8(
|
||||
input [15:0] a, b, c, d, e, f, g, h,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add16(
|
||||
input [15:0] a0, a1, a2, a3, a4, a5, a6, a7,
|
||||
input [15:0] a8, a9, a10, a11, a12, a13, a14, a15,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7
|
||||
+ a8 + a9 + a10 + a11 + a12 + a13 + a14 + a15;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 14 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
96
tests/csa_tree/csa_tree_alu_chains.ys
Normal file
96
tests/csa_tree/csa_tree_alu_chains.ys
Normal file
|
|
@ -0,0 +1,96 @@
|
|||
read_verilog <<EOT
|
||||
module alu_add3(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_add4(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_add5(
|
||||
input [11:0] a, b, c, d, e,
|
||||
output [11:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_add8(
|
||||
input [15:0] a, b, c, d, e, f, g, h,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_add16(
|
||||
input [15:0] a0, a1, a2, a3, a4, a5, a6, a7,
|
||||
input [15:0] a8, a9, a10, a11, a12, a13, a14, a15,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a0 + a1 + a2 + a3 + a4 + a5 + a6 + a7
|
||||
+ a8 + a9 + a10 + a11 + a12 + a13 + a14 + a15;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 14 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
design -reset
|
||||
285
tests/csa_tree/csa_tree_alu_macc_edge_cases.ys
Normal file
285
tests/csa_tree/csa_tree_alu_macc_edge_cases.ys
Normal file
|
|
@ -0,0 +1,285 @@
|
|||
read_verilog <<EOT
|
||||
module alu_add2(
|
||||
input [7:0] a, b,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
select -assert-none t:$fa
|
||||
select -assert-none t:$add
|
||||
select -assert-none t:$sub
|
||||
select -assert-count 1 t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_sub2(
|
||||
input [7:0] a, b,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a - b;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
select -assert-none t:$fa
|
||||
select -assert-none t:$add
|
||||
select -assert-none t:$sub
|
||||
select -assert-count 1 t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_compare(
|
||||
input [7:0] a, b,
|
||||
output y
|
||||
);
|
||||
assign y = (a < b);
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
select -assert-none t:$fa
|
||||
select -assert-none t:$add
|
||||
select -assert-none t:$sub
|
||||
select -assert-count 1 t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_mul(
|
||||
input [7:0] a, b, c,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a * b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-none t:$fa
|
||||
select -assert-min 1 t:$macc t:$macc_v2 %u
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_fanout(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] mid, y
|
||||
);
|
||||
wire [7:0] ab = a + b;
|
||||
assign mid = ab;
|
||||
assign y = ab + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-none t:$fa
|
||||
select -assert-count 2 t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_2port(
|
||||
input [7:0] a, b,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-none t:$fa
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_idempotent(
|
||||
input [15:0] a, b, c, d, e, f, g, h,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
|
||||
csa_tree
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$sub
|
||||
select -assert-none t:$alu
|
||||
|
||||
csa_tree
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$sub
|
||||
select -assert-none t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_mixed_width(
|
||||
input [7:0] a,
|
||||
input [3:0] b,
|
||||
input [15:0] c,
|
||||
input [7:0] d,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_signed(
|
||||
input signed [7:0] a, b, c, d,
|
||||
output signed [9:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module fir_4tap_alu(
|
||||
input clk,
|
||||
input [15:0] x, c0, c1, c2, c3,
|
||||
output reg [31:0] y
|
||||
);
|
||||
reg [15:0] x1, x2, x3;
|
||||
always @(posedge clk) begin
|
||||
x1 <= x;
|
||||
x2 <= x1;
|
||||
x3 <= x2;
|
||||
end
|
||||
|
||||
wire [31:0] sum = x*c0 + x1*c1 + x2*c2 + x3*c3;
|
||||
always @(posedge clk) y <= sum;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-min 1 t:$dff
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_mixed_sign(
|
||||
input signed [7:0] a,
|
||||
input [7:0] b,
|
||||
input signed [7:0] c,
|
||||
output signed [9:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_wide32(
|
||||
input [31:0] a, b, c, d,
|
||||
output [31:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_single(
|
||||
input [7:0] a,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
select -assert-none t:$fa
|
||||
select -assert-none t:$add
|
||||
select -assert-none t:$sub
|
||||
select -assert-none t:$alu
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_mul_survives(
|
||||
input [7:0] a, b, c, d,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a * b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-none t:$fa
|
||||
select -assert-min 1 t:$macc t:$macc_v2 %u
|
||||
design -reset
|
||||
179
tests/csa_tree/csa_tree_alu_macc_equiv.ys
Normal file
179
tests/csa_tree/csa_tree_alu_macc_equiv.ys
Normal file
|
|
@ -0,0 +1,179 @@
|
|||
read_verilog <<EOT
|
||||
module equiv_alu_add3(
|
||||
input [3:0] a, b, c,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_alu_add4(
|
||||
input [3:0] a, b, c, d,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_alu_add8(
|
||||
input [3:0] a, b, c, d, e, f, g, h,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_alu_signed(
|
||||
input signed [3:0] a, b, c, d,
|
||||
output signed [5:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_alu_sub_mixed(
|
||||
input [3:0] a, b, c, d,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b - c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-min 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_alu_sub_all(
|
||||
input [3:0] a, b, c, d,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a - b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-min 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_macc_add3(
|
||||
input [3:0] a, b, c,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_macc_add4(
|
||||
input [3:0] a, b, c, d,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_macc_add8(
|
||||
input [3:0] a, b, c, d, e, f, g, h,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_macc_signed(
|
||||
input signed [3:0] a, b, c, d,
|
||||
output signed [5:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
116
tests/csa_tree/csa_tree_alu_macc_sim.ys
Normal file
116
tests/csa_tree/csa_tree_alu_macc_sim.ys
Normal file
|
|
@ -0,0 +1,116 @@
|
|||
read_verilog <<EOT
|
||||
module sim_alu_add4(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
|
||||
sat -set a 1 -set b 2 -set c 3 -set d 4 -prove y 10
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 255 -set b 1 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 100 -set b 50 -set c 25 -set d 25 -prove y 200
|
||||
sat -set a 255 -set b 255 -set c 255 -set d 255 -prove y 252
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sim_alu_sub_mixed(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b - c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
|
||||
sat -set a 10 -set b 20 -set c 5 -set d 3 -prove y 28
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 100 -set b 50 -set c 30 -set d 10 -prove y 130
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sim_alu_sub_all(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a - b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
|
||||
sat -set a 100 -set b 10 -set c 20 -set d 30 -prove y 40
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 255 -set b 1 -set c 1 -set d 1 -prove y 252
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sim_macc_add4(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
|
||||
sat -set a 1 -set b 2 -set c 3 -set d 4 -prove y 10
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 255 -set b 1 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 100 -set b 50 -set c 25 -set d 25 -prove y 200
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sim_macc_add8(
|
||||
input [7:0] a, b, c, d, e, f, g, h,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
|
||||
sat -set a 1 -set b 2 -set c 3 -set d 4 -set e 5 -set f 6 -set g 7 -set h 8 -prove y 36
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -set e 0 -set f 0 -set g 0 -set h 0 -prove y 0
|
||||
sat -set a 32 -set b 32 -set c 32 -set d 32 -set e 32 -set f 32 -set g 32 -set h 32 -prove y 0
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sim_macc_sub_mixed(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b - c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
|
||||
sat -set a 10 -set b 20 -set c 5 -set d 3 -prove y 28
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 100 -set b 50 -set c 30 -set d 10 -prove y 130
|
||||
design -reset
|
||||
79
tests/csa_tree/csa_tree_alu_sub_chains.ys
Normal file
79
tests/csa_tree/csa_tree_alu_sub_chains.ys
Normal file
|
|
@ -0,0 +1,79 @@
|
|||
read_verilog <<EOT
|
||||
module alu_sub_3op(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a - b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_sub_mixed(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b - c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_sub_all(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a - b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module alu_sub_signed(
|
||||
input signed [7:0] a, b, c, d,
|
||||
output signed [9:0] y
|
||||
);
|
||||
assign y = a + b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt_clean
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$alu
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
147
tests/csa_tree/csa_tree_edge_cases.ys
Normal file
147
tests/csa_tree/csa_tree_edge_cases.ys
Normal file
|
|
@ -0,0 +1,147 @@
|
|||
read_verilog <<EOT
|
||||
module add_1bit(
|
||||
input a, b, c,
|
||||
output [1:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_1bit_wide(
|
||||
input a, b, c, d,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_wide_out(
|
||||
input [7:0] a, b, c, d,
|
||||
output [31:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_mixed(
|
||||
input [7:0] a,
|
||||
input [3:0] b,
|
||||
input [15:0] c,
|
||||
input [7:0] d,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_signed(
|
||||
input signed [7:0] a, b, c, d,
|
||||
output signed [9:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_repeated(
|
||||
input [7:0] a,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + a + a + a;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_const(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + 8'd42;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_two(
|
||||
input [7:0] a, b, c, d, e, f, g, h,
|
||||
output [7:0] y1, y2
|
||||
);
|
||||
assign y1 = a + b + c + d;
|
||||
assign y2 = e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 4 t:$fa
|
||||
select -assert-count 2 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module fir_4tap(
|
||||
input clk,
|
||||
input [15:0] x, c0, c1, c2, c3,
|
||||
output reg [31:0] y
|
||||
);
|
||||
reg [15:0] x1, x2, x3;
|
||||
always @(posedge clk) begin
|
||||
x1 <= x;
|
||||
x2 <= x1;
|
||||
x3 <= x2;
|
||||
end
|
||||
|
||||
wire [31:0] sum = x*c0 + x1*c1 + x2*c2 + x3*c3;
|
||||
always @(posedge clk) y <= sum;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
178
tests/csa_tree/csa_tree_equiv.ys
Normal file
178
tests/csa_tree/csa_tree_equiv.ys
Normal file
|
|
@ -0,0 +1,178 @@
|
|||
read_verilog <<EOT
|
||||
module equiv_add3(
|
||||
input [3:0] a, b, c,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_add4(
|
||||
input [3:0] a, b, c, d,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_add5(
|
||||
input [3:0] a, b, c, d, e,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_add8(
|
||||
input [3:0] a, b, c, d, e, f, g, h,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_signed(
|
||||
input signed [3:0] a, b, c, d,
|
||||
output signed [5:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_mixed(
|
||||
input [1:0] a,
|
||||
input [3:0] b,
|
||||
input [5:0] c,
|
||||
output [5:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_sub_mixed(
|
||||
input [3:0] a, b, c, d,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a + b - c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_sub_all(
|
||||
input [3:0] a, b, c, d,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a - b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_sub_3op(
|
||||
input [3:0] a, b, c,
|
||||
output [3:0] y
|
||||
);
|
||||
assign y = a - b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_sub_signed(
|
||||
input signed [3:0] a, b, c, d,
|
||||
output signed [5:0] y
|
||||
);
|
||||
assign y = a + b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module equiv_double_neg(
|
||||
input [3:0] a, b, c,
|
||||
output [3:0] y
|
||||
);
|
||||
wire [3:0] ab = a - b;
|
||||
assign y = c - ab;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
equiv_opt csa_tree
|
||||
design -load postopt
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
19
tests/csa_tree/csa_tree_idempotent.ys
Normal file
19
tests/csa_tree/csa_tree_idempotent.ys
Normal file
|
|
@ -0,0 +1,19 @@
|
|||
read_verilog <<EOT
|
||||
module add8(
|
||||
input [15:0] a, b, c, d, e, f, g, h,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
|
||||
csa_tree
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
|
||||
csa_tree
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$sub
|
||||
133
tests/csa_tree/csa_tree_macc.ys
Normal file
133
tests/csa_tree/csa_tree_macc.ys
Normal file
|
|
@ -0,0 +1,133 @@
|
|||
read_verilog <<EOT
|
||||
module macc_add3(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$macc t:$macc_v2 %u
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_add4(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$macc t:$macc_v2 %u
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_add5(
|
||||
input [11:0] a, b, c, d, e,
|
||||
output [11:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$macc t:$macc_v2 %u
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_add8(
|
||||
input [15:0] a, b, c, d, e, f, g, h,
|
||||
output [15:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-count 6 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-none t:$macc t:$macc_v2 %u
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_sub_mixed(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b - c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-none t:$macc t:$macc_v2 %u
|
||||
select -assert-min 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_const(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + 8'd42;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-none t:$macc t:$macc_v2 %u
|
||||
select -assert-min 1 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module macc_two(
|
||||
input [7:0] a, b, c, d, e, f, g, h,
|
||||
output [7:0] y1, y2
|
||||
);
|
||||
assign y1 = a + b + c + d;
|
||||
assign y2 = e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
alumacc
|
||||
opt
|
||||
csa_tree
|
||||
opt_clean
|
||||
select -assert-none t:$macc t:$macc_v2 %u
|
||||
select -assert-count 4 t:$fa
|
||||
select -assert-count 2 t:$add
|
||||
design -reset
|
||||
77
tests/csa_tree/csa_tree_negative.ys
Normal file
77
tests/csa_tree/csa_tree_negative.ys
Normal file
|
|
@ -0,0 +1,77 @@
|
|||
read_verilog <<EOT
|
||||
module add2(
|
||||
input [7:0] a, b,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-none t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_fanout(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] mid, y
|
||||
);
|
||||
wire [7:0] ab = a + b;
|
||||
assign mid = ab;
|
||||
assign y = ab + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-none t:$fa
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sub2(
|
||||
input [7:0] a, b,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a - b;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-none t:$fa
|
||||
select -assert-count 1 t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_multi_const(
|
||||
input [7:0] x,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = 8'd1 + 8'd2 + 8'd3 + x;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-none t:$fa
|
||||
select -assert-max 1 t:$add
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module add_partial(
|
||||
input [7:0] a, b, c, d, e,
|
||||
output [7:0] mid, y
|
||||
);
|
||||
wire [7:0] ab = a + b;
|
||||
assign mid = ab;
|
||||
assign y = ab + c + d + e;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 2 t:$add
|
||||
design -reset
|
||||
72
tests/csa_tree/csa_tree_sim.ys
Normal file
72
tests/csa_tree/csa_tree_sim.ys
Normal file
|
|
@ -0,0 +1,72 @@
|
|||
read_verilog <<EOT
|
||||
module sim_add4(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
|
||||
sat -set a 1 -set b 2 -set c 3 -set d 4 -prove y 10
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 255 -set b 1 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 100 -set b 50 -set c 25 -set d 25 -prove y 200
|
||||
sat -set a 255 -set b 255 -set c 255 -set d 255 -prove y 252
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sim_sub_mixed(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b - c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
|
||||
sat -set a 10 -set b 20 -set c 5 -set d 3 -prove y 28
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 100 -set b 50 -set c 30 -set d 10 -prove y 130
|
||||
sat -set a 1 -set b 1 -set c 255 -set d 1 -prove y 4
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sim_sub_all(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a - b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
|
||||
sat -set a 100 -set b 10 -set c 20 -set d 30 -prove y 40
|
||||
sat -set a 0 -set b 0 -set c 0 -set d 0 -prove y 0
|
||||
sat -set a 255 -set b 1 -set c 1 -set d 1 -prove y 252
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sim_double_neg(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
wire [7:0] ab = a - b;
|
||||
assign y = c - ab;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
|
||||
sat -set a 30 -set b 20 -set c 10 -prove y 0
|
||||
sat -set a 50 -set b 25 -set c 100 -prove y 75
|
||||
sat -set a 0 -set b 0 -set c 0 -prove y 0
|
||||
sat -set a 255 -set b 1 -set c 1 -prove y 3
|
||||
design -reset
|
||||
102
tests/csa_tree/csa_tree_sub_chains.ys
Normal file
102
tests/csa_tree/csa_tree_sub_chains.ys
Normal file
|
|
@ -0,0 +1,102 @@
|
|||
read_verilog <<EOT
|
||||
module sub_3op(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a - b + c;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$not
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sub_mixed(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b - c + d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$not
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sub_all(
|
||||
input [7:0] a, b, c, d,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a - b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 3 t:$not
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sub_5op(
|
||||
input [11:0] a, b, c, d, e,
|
||||
output [11:0] y
|
||||
);
|
||||
assign y = a - b + c - d + e;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 4 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 2 t:$not
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sub_signed(
|
||||
input signed [7:0] a, b, c, d,
|
||||
output signed [9:0] y
|
||||
);
|
||||
assign y = a + b - c - d;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 3 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 2 t:$not
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
|
||||
read_verilog <<EOT
|
||||
module sub_double_neg(
|
||||
input [7:0] a, b, c,
|
||||
output [7:0] y
|
||||
);
|
||||
wire [7:0] ab = a - b;
|
||||
assign y = c - ab;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
csa_tree
|
||||
select -assert-count 2 t:$fa
|
||||
select -assert-count 1 t:$add
|
||||
select -assert-count 1 t:$not
|
||||
select -assert-none t:$sub
|
||||
design -reset
|
||||
70
tests/csa_tree/csa_tree_synth.ys
Normal file
70
tests/csa_tree/csa_tree_synth.ys
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
# Assert against abc synth with and without csa, hopefully prevent regressions
|
||||
# Baseline
|
||||
read_verilog <<EOT
|
||||
module bench(
|
||||
input [7:0] a, b, c, d, e, f, g, h,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
opt
|
||||
techmap
|
||||
abc -g AND,OR,XOR
|
||||
select -assert-min 236 t:$_AND_ t:$_OR_ t:$_XOR_ %u
|
||||
design -reset
|
||||
|
||||
# With csa_tree
|
||||
read_verilog <<EOT
|
||||
module bench(
|
||||
input [7:0] a, b, c, d, e, f, g, h,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
opt
|
||||
csa_tree
|
||||
techmap
|
||||
abc -g AND,OR,XOR
|
||||
select -assert-max 235 t:$_AND_ t:$_OR_ t:$_XOR_ %u
|
||||
design -reset
|
||||
|
||||
# Depth-otimal baseline
|
||||
read_verilog <<EOT
|
||||
module bench(
|
||||
input [7:0] a, b, c, d, e, f, g, h,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
opt
|
||||
techmap
|
||||
abc -D 1
|
||||
select -assert-min 240 t:$_AND_ t:$_NAND_ t:$_OR_ t:$_NOR_ t:$_XOR_ t:$_XNOR_ t:$_NOT_ %u
|
||||
design -reset
|
||||
|
||||
# Depth-optimal with csa_tree
|
||||
read_verilog <<EOT
|
||||
module bench(
|
||||
input [7:0] a, b, c, d, e, f, g, h,
|
||||
output [7:0] y
|
||||
);
|
||||
assign y = a + b + c + d + e + f + g + h;
|
||||
endmodule
|
||||
EOT
|
||||
hierarchy -auto-top
|
||||
proc
|
||||
opt
|
||||
csa_tree
|
||||
techmap
|
||||
abc -D 1
|
||||
select -assert-max 236 t:$_AND_ t:$_NAND_ t:$_OR_ t:$_NOR_ t:$_XOR_ t:$_XNOR_ t:$_NOT_ %u
|
||||
design -reset
|
||||
7
tests/csa_tree/run-test.sh
Executable file
7
tests/csa_tree/run-test.sh
Executable file
|
|
@ -0,0 +1,7 @@
|
|||
#!/usr/bin/env bash
|
||||
source ../common-env.sh
|
||||
set -e
|
||||
for x in *.ys; do
|
||||
echo "Running $x.."
|
||||
../../yosys -ql ${x%.ys}.log $x
|
||||
done
|
||||
Loading…
Add table
Add a link
Reference in a new issue