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

Merge branch 'master' into btor-ng

Browse source
This commit is contained in:
Clifford Wolf 2017-12-14 02:17:01 +01:00
commit a48ec49017
9 changed files with 178 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

67
backends/smt2/smt2.cc
View file

@ -556,15 +556,28 @@ struct Smt2Worker
decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d\n", get_id(cell), abits, width, rd_ports, wr_ports));
bool async_read = false;
if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_zero())
log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
async_read = true;
}
string memstate;
if (async_read) {
memstate = stringf("%s#%d#final", get_id(module), arrayid);
} else {
memstate = stringf("%s#%d#0", get_id(module), arrayid);
}
if (statebv)
{
int mem_size = cell->getParam("\\SIZE").as_int();
int mem_offset = cell->getParam("\\OFFSET").as_int();
makebits(stringf("%s#%d#0", get_id(module), arrayid), width*mem_size, get_id(cell));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d#0| state))\n",
get_id(module), get_id(cell), get_id(module), width*mem_size, get_id(module), arrayid));
makebits(memstate, width*mem_size, get_id(cell));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str()));
for (int i = 0; i < rd_ports; i++)
{
@ -584,9 +597,9 @@ struct Smt2Worker
read_expr += "0";
for (int k = 0; k < mem_size; k++)
read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s#%d#0| state))\n %s)",
read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n %s)",
get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(),
width*(k+1)-1, width*k, get_id(module), arrayid, read_expr.c_str());
width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str());
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n %s) ; %s\n",
get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig)));
@ -600,14 +613,14 @@ struct Smt2Worker
else
{
if (statedt)
dtmembers.push_back(stringf(" (|%s#%d#0| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
get_id(module), arrayid, abits, width, get_id(cell)));
dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
memstate.c_str(), abits, width, get_id(cell)));
else
decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
get_id(module), arrayid, get_id(module), abits, width, get_id(cell)));
decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
memstate.c_str(), get_id(module), abits, width, get_id(cell)));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
get_id(module), get_id(cell), get_id(module), abits, width, get_id(module), arrayid));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n",
get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str()));
for (int i = 0; i < rd_ports; i++)
{
@ -622,8 +635,8 @@ struct Smt2Worker
decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) (|%s_m:R%dA %s| state))) ; %s\n",
get_id(module), idcounter, get_id(module), width, get_id(module), arrayid, get_id(module), i, get_id(cell), log_signal(data_sig)));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n",
get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig)));
decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
@ -869,11 +882,25 @@ struct Smt2Worker
int width = cell->getParam("\\WIDTH").as_int();
int wr_ports = cell->getParam("\\WR_PORTS").as_int();
bool async_read = false;
string initial_memstate, final_memstate;
if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
log_assert(cell->getParam("\\WR_CLK_ENABLE").is_fully_zero());
async_read = true;
initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
}
if (statebv)
{
int mem_size = cell->getParam("\\SIZE").as_int();
int mem_offset = cell->getParam("\\OFFSET").as_int();
if (async_read) {
makebits(final_memstate, width*mem_size, get_id(cell));
}
for (int i = 0; i < wr_ports; i++)
{
SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
@ -912,6 +939,15 @@ struct Smt2Worker
}
else
{
if (async_read) {
if (statedt)
dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
initial_memstate.c_str(), abits, width, get_id(cell)));
else
decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
initial_memstate.c_str(), get_id(module), abits, width, get_id(cell)));
}
for (int i = 0; i < wr_ports; i++)
{
SigSpec addr_sig = cell->getPort("\\WR_ADDR").extract(abits*i, abits);
@ -948,6 +984,9 @@ struct Smt2Worker
std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
if (async_read)
hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));
Const init_data = cell->getParam("\\INIT");
int memsize = cell->getParam("\\SIZE").as_int();

2
kernel/celltypes.h
View file

@ -20,7 +20,7 @@
#ifndef CELLTYPES_H
#define CELLTYPES_H
#include <kernel/yosys.h>
#include "kernel/yosys.h"
YOSYS_NAMESPACE_BEGIN

2
kernel/cost.h
View file

@ -20,7 +20,7 @@
#ifndef COST_H
#define COST_H
#include <kernel/yosys.h>
#include "kernel/yosys.h"
YOSYS_NAMESPACE_BEGIN

11
kernel/rtlil.cc
View file

@ -172,6 +172,17 @@ bool RTLIL::Const::is_fully_zero() const
return true;
}
bool RTLIL::Const::is_fully_ones() const
{
cover("kernel.rtlil.const.is_fully_ones");
for (auto bit : bits)
if (bit != RTLIL::State::S1)
return false;
return true;
}
bool RTLIL::Const::is_fully_def() const
{
cover("kernel.rtlil.const.is_fully_def");

1
kernel/rtlil.h
View file

@ -480,6 +480,7 @@ struct RTLIL::Const
inline const RTLIL::State &operator[](int index) const { return bits.at(index); }
bool is_fully_zero() const;
bool is_fully_ones() const;
bool is_fully_def() const;
bool is_fully_undef() const;

9
passes/opt/opt_clean.cc
View file

@ -91,9 +91,16 @@ void rmunused_module_cells(Module *module, bool verbose)
Cell *cell = it.second;
for (auto &it2 : cell->connections()) {
if (!ct_all.cell_known(cell->type) || ct_all.cell_output(cell->type, it2.first))
for (auto bit : sigmap(it2.second))
for (auto raw_bit : it2.second) {
if (raw_bit.wire == nullptr)
continue;
auto bit = sigmap(raw_bit);
if (bit.wire == nullptr)
log_warning("Driver-driver conflict for %s between cell %s.%s and constant %s in %s: Resolved using constant.\n",
log_signal(raw_bit), log_id(cell), log_id(it2.first), log_signal(bit), log_id(module));
if (bit.wire != nullptr)
wire2driver[bit].insert(cell);
}
}
if (keep_cache.query(cell))
queue.insert(cell);

5
passes/proc/proc_dff.cc
View file

@ -322,6 +322,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
}
}
SigSpec sig_q = sig;
ce.assign_map.apply(insig);
ce.assign_map.apply(rstval);
ce.assign_map.apply(sig);
@ -350,13 +351,13 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
else if (!rstval.is_fully_const() && !ce.eval(rstval))
{
log_warning("Async reset value `%s' is not constant!\n", log_signal(rstval));
gen_dffsr(mod, insig, rstval, sig,
gen_dffsr(mod, insig, rstval, sig_q,
sync_edge->type == RTLIL::SyncType::STp,
sync_level && sync_level->type == RTLIL::SyncType::ST1,
sync_edge->signal, sync_level->signal, proc);
}
else
gen_dff(mod, insig, rstval.as_const(), sig,
gen_dff(mod, insig, rstval.as_const(), sig_q,
sync_edge && sync_edge->type == RTLIL::SyncType::STp,
sync_level && sync_level->type == RTLIL::SyncType::ST1,
sync_edge ? sync_edge->signal : SigSpec(),

81
passes/sat/clk2fflogic.cc
View file

@ -72,6 +72,87 @@ struct Clk2fflogicPass : public Pass {
for (auto cell : vector<Cell*>(module->selected_cells()))
{
if (cell->type.in("$mem"))
{
int abits = cell->getParam("\\ABITS").as_int();
int width = cell->getParam("\\WIDTH").as_int();
int rd_ports = cell->getParam("\\RD_PORTS").as_int();
int wr_ports = cell->getParam("\\WR_PORTS").as_int();
for (int i = 0; i < rd_ports; i++) {
if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
log_error("Read port %d of memory %s.%s is clocked. This is not supported by \"clk2fflogic\"! "
"Call \"memory\" with -nordff to avoid this error.\n", i, log_id(cell), log_id(module));
}
Const wr_clk_en_param = cell->getParam("\\WR_CLK_ENABLE");
Const wr_clk_pol_param = cell->getParam("\\WR_CLK_POLARITY");
SigSpec wr_clk_port = cell->getPort("\\WR_CLK");
SigSpec wr_en_port = cell->getPort("\\WR_EN");
SigSpec wr_addr_port = cell->getPort("\\WR_ADDR");
SigSpec wr_data_port = cell->getPort("\\WR_DATA");
for (int wport = 0; wport < wr_ports; wport++)
{
bool clken = wr_clk_en_param[wport] == State::S1;
bool clkpol = wr_clk_pol_param[wport] == State::S1;
if (!clken)
continue;
SigBit clk = wr_clk_port[wport];
SigSpec en = wr_en_port.extract(wport*width, width);
SigSpec addr = wr_addr_port.extract(wport*abits, abits);
SigSpec data = wr_data_port.extract(wport*width, width);
log("Modifying write port %d on memory %s.%s: CLK=%s, A=%s, D=%s\n",
wport, log_id(module), log_id(cell), log_signal(clk),
log_signal(addr), log_signal(data));
Wire *past_clk = module->addWire(NEW_ID);
past_clk->attributes["\\init"] = clkpol ? State::S1 : State::S0;
module->addFf(NEW_ID, clk, past_clk);
SigSpec clock_edge_pattern;
if (clkpol) {
clock_edge_pattern.append_bit(State::S0);
clock_edge_pattern.append_bit(State::S1);
} else {
clock_edge_pattern.append_bit(State::S1);
clock_edge_pattern.append_bit(State::S0);
}
SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern);
SigSpec en_q = module->addWire(NEW_ID, GetSize(addr));
module->addFf(NEW_ID, en, en_q);
SigSpec addr_q = module->addWire(NEW_ID, GetSize(addr));
module->addFf(NEW_ID, addr, addr_q);
SigSpec data_q = module->addWire(NEW_ID, GetSize(data));
module->addFf(NEW_ID, data, data_q);
wr_clk_port[wport] = State::S0;
wr_en_port.replace(wport*width, module->Mux(NEW_ID, Const(0, GetSize(en_q)), en_q, clock_edge));
wr_addr_port.replace(wport*abits, addr_q);
wr_data_port.replace(wport*width, data_q);
wr_clk_en_param[wport] = State::S0;
wr_clk_pol_param[wport] = State::S0;
}
cell->setParam("\\WR_CLK_ENABLE", wr_clk_en_param);
cell->setParam("\\WR_CLK_POLARITY", wr_clk_pol_param);
cell->setPort("\\WR_CLK", wr_clk_port);
cell->setPort("\\WR_EN", wr_en_port);
cell->setPort("\\WR_ADDR", wr_addr_port);
cell->setPort("\\WR_DATA", wr_data_port);
}
if (cell->type.in("$dlatch"))
{
bool enpol = cell->parameters["\\EN_POLARITY"].as_bool();

38
techlibs/ice40/cells_sim.v
View file

@ -1193,7 +1193,7 @@ module SB_IO_OD (
input DOUT1,
input DOUT0,
output DIN1,
output DIN0,
output DIN0
);
parameter [5:0] PIN_TYPE = 6'b000000;
parameter [0:0] NEG_TRIGGER = 1'b0;
@ -1205,44 +1205,44 @@ module SB_IO_OD (
reg outena_q;
generate if (!NEG_TRIGGER) begin
always @(posedge INPUT_CLK) if (CLOCK_ENABLE) din_q_0 <= PACKAGE_PIN;
always @(negedge INPUT_CLK) if (CLOCK_ENABLE) din_q_1 <= PACKAGE_PIN;
always @(posedge OUTPUT_CLK) if (CLOCK_ENABLE) dout_q_0 <= D_OUT_0;
always @(negedge OUTPUT_CLK) if (CLOCK_ENABLE) dout_q_1 <= D_OUT_1;
always @(posedge OUTPUT_CLK) if (CLOCK_ENABLE) outena_q <= OUTPUT_ENABLE;
always @(posedge INPUTCLK) if (CLOCKENABLE) din_q_0 <= PACKAGEPIN;
always @(negedge INPUTCLK) if (CLOCKENABLE) din_q_1 <= PACKAGEPIN;
always @(posedge OUTPUTCLK) if (CLOCKENABLE) dout_q_0 <= DOUT0;
always @(negedge OUTPUTCLK) if (CLOCKENABLE) dout_q_1 <= DOUT1;
always @(posedge OUTPUTCLK) if (CLOCKENABLE) outena_q <= OUTPUTENABLE;
end else begin
always @(negedge INPUT_CLK) if (CLOCK_ENABLE) din_q_0 <= PACKAGE_PIN;
always @(posedge INPUT_CLK) if (CLOCK_ENABLE) din_q_1 <= PACKAGE_PIN;
always @(negedge OUTPUT_CLK) if (CLOCK_ENABLE) dout_q_0 <= D_OUT_0;
always @(posedge OUTPUT_CLK) if (CLOCK_ENABLE) dout_q_1 <= D_OUT_1;
always @(negedge OUTPUT_CLK) if (CLOCK_ENABLE) outena_q <= OUTPUT_ENABLE;
always @(negedge INPUTCLK) if (CLOCKENABLE) din_q_0 <= PACKAGEPIN;
always @(posedge INPUTCLK) if (CLOCKENABLE) din_q_1 <= PACKAGEPIN;
always @(negedge OUTPUTCLK) if (CLOCKENABLE) dout_q_0 <= DOUT0;
always @(posedge OUTPUTCLK) if (CLOCKENABLE) dout_q_1 <= DOUT1;
always @(negedge OUTPUTCLK) if (CLOCKENABLE) outena_q <= OUTPUTENABLE;
end endgenerate
always @* begin
if (!PIN_TYPE[1] || !LATCH_INPUT_VALUE)
din_0 = PIN_TYPE[0] ? PACKAGE_PIN : din_q_0;
if (!PIN_TYPE[1] || !LATCHINPUTVALUE)
din_0 = PIN_TYPE[0] ? PACKAGEPIN : din_q_0;
din_1 = din_q_1;
end
// work around simulation glitches on dout in DDR mode
reg outclk_delayed_1;
reg outclk_delayed_2;
always @* outclk_delayed_1 <= OUTPUT_CLK;
always @* outclk_delayed_1 <= OUTPUTCLK;
always @* outclk_delayed_2 <= outclk_delayed_1;
always @* begin
if (PIN_TYPE[3])
dout = PIN_TYPE[2] ? !dout_q_0 : D_OUT_0;
dout = PIN_TYPE[2] ? !dout_q_0 : DOUT0;
else
dout = (outclk_delayed_2 ^ NEG_TRIGGER) || PIN_TYPE[2] ? dout_q_0 : dout_q_1;
end
assign D_IN_0 = din_0, D_IN_1 = din_1;
assign DIN0 = din_0, DIN1 = din_1;
generate
if (PIN_TYPE[5:4] == 2'b01) assign PACKAGE_PIN = dout ? 1'bz : 1'b0;
if (PIN_TYPE[5:4] == 2'b10) assign PACKAGE_PIN = OUTPUT_ENABLE ? (dout ? 1'bz : 1'b0) : 1'bz;
if (PIN_TYPE[5:4] == 2'b11) assign PACKAGE_PIN = outena_q ? (dout ? 1'bz : 1'b0) : 1'bz;
if (PIN_TYPE[5:4] == 2'b01) assign PACKAGEPIN = dout ? 1'bz : 1'b0;
if (PIN_TYPE[5:4] == 2'b10) assign PACKAGEPIN = OUTPUTENABLE ? (dout ? 1'bz : 1'b0) : 1'bz;
if (PIN_TYPE[5:4] == 2'b11) assign PACKAGEPIN = outena_q ? (dout ? 1'bz : 1'b0) : 1'bz;
endgenerate
`endif
endmodule