aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--backends/btor/btor.cc4
-rw-r--r--passes/sat/sim.cc204
-rw-r--r--techlibs/intel_alm/Makefile.inc1
-rw-r--r--techlibs/intel_alm/common/bram_m10k.txt4
-rw-r--r--techlibs/intel_alm/common/bram_m10k_map.v16
-rw-r--r--techlibs/intel_alm/common/mem_sim.v2
-rw-r--r--techlibs/intel_alm/common/quartus_rename.v9
-rw-r--r--techlibs/intel_alm/synth_intel_alm.cc3
-rw-r--r--tests/arch/intel_alm/blockram.ys3
10 files changed, 221 insertions, 27 deletions
diff --git a/Makefile b/Makefile
index 4aabe0181..f60fe30ed 100644
--- a/Makefile
+++ b/Makefile
@@ -129,7 +129,7 @@ LDFLAGS += -rdynamic
LDLIBS += -lrt
endif
-YOSYS_VER := 0.15+7
+YOSYS_VER := 0.15+11
GIT_REV := $(shell git -C $(YOSYS_SRC) rev-parse --short HEAD 2> /dev/null || echo UNKNOWN)
OBJS = kernel/version_$(GIT_REV).o
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index d62cc4c3d..73e88c049 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -678,7 +678,7 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig_y));
int nid = next_nid++;
- btorf("%d state %d\n", nid, sid);
+ btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
if (cell->type == ID($anyconst)) {
int nid2 = next_nid++;
@@ -699,7 +699,7 @@ struct BtorWorker
int one_nid = get_sig_nid(State::S1);
int zero_nid = get_sig_nid(State::S0);
initstate_nid = next_nid++;
- btorf("%d state %d\n", initstate_nid, sid);
+ btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
}
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index d15ae9b57..9d32cc9b3 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -77,6 +77,7 @@ struct OutputWriter
struct SimShared
{
bool debug = false;
+ bool verbose = true;
bool hide_internal = true;
bool writeback = false;
bool zinit = false;
@@ -181,7 +182,7 @@ struct SimInstance
if ((shared->fst) && !(shared->hide_internal && wire->name[0] == '$')) {
fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(wire->name));
if (id==0 && wire->name.isPublic())
- log_warning("Unable to found wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(wire->name)).c_str());
+ log_warning("Unable to find wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(wire->name)).c_str());
fst_handles[wire] = id;
}
@@ -326,6 +327,16 @@ struct SimInstance
return did_something;
}
+ void set_memory_state(IdString memid, Const addr, Const data)
+ {
+ auto &state = mem_database[memid];
+
+ int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
+ for (int i = 0; i < GetSize(data); i++)
+ if (0 <= i+offset && i+offset < GetSize(data))
+ state.data.bits[i+offset] = data.bits[i];
+ }
+
void update_cell(Cell *cell)
{
if (ff_database.count(cell))
@@ -754,7 +765,7 @@ struct SimInstance
IdString name = qsig.as_wire()->name;
fstHandle id = shared->fst->getHandle(scope + "." + RTLIL::unescape_id(name));
if (id==0 && name.isPublic())
- log_warning("Unable to found wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(name)).c_str());
+ log_warning("Unable to find wire %s in input file.\n", (scope + "." + RTLIL::unescape_id(name)).c_str());
if (id!=0) {
Const fst_val = Const::from_string(shared->fst->valueOf(id));
set_state(qsig, fst_val);
@@ -909,7 +920,7 @@ struct SimWorker : SimShared
if (debug)
log("\n===== 0 =====\n");
- else
+ else if (verbose)
log("Simulating cycle 0.\n");
set_inports(reset, State::S1);
@@ -926,7 +937,7 @@ struct SimWorker : SimShared
{
if (debug)
log("\n===== %d =====\n", 10*cycle + 5);
- else
+ else if (verbose)
log("Simulating cycle %d.\n", (cycle*2)+1);
set_inports(clock, State::S0);
set_inports(clockn, State::S1);
@@ -936,7 +947,7 @@ struct SimWorker : SimShared
if (debug)
log("\n===== %d =====\n", 10*cycle + 10);
- else
+ else if (verbose)
log("Simulating cycle %d.\n", (cycle*2)+2);
set_inports(clock, State::S1);
@@ -961,7 +972,7 @@ struct SimWorker : SimShared
}
}
- void run_cosim(Module *topmod, int numcycles)
+ void run_cosim_fst(Module *topmod, int numcycles)
{
log_assert(top == nullptr);
fst = new FstData(sim_filename);
@@ -1053,7 +1064,8 @@ struct SimWorker : SimShared
try {
fst->reconstructAllAtTimes(fst_clock, startCount, stopCount, [&](uint64_t time) {
- log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString());
+ if (verbose)
+ log("Co-simulating %s %d [%lu%s].\n", (all_samples ? "sample" : "cycle"), cycle, (unsigned long)time, fst->getTimescaleString());
bool did_something = false;
for(auto &item : inputs) {
std::string v = fst->valueOf(item.second);
@@ -1092,13 +1104,17 @@ struct SimWorker : SimShared
delete fst;
}
- void run_cosim_witness(Module *topmod)
+ void run_cosim_aiger_witness(Module *topmod)
{
log_assert(top == nullptr);
+ if ((clock.size()+clockn.size())==0)
+ log_error("Clock signal must be specified.\n");
std::ifstream mf(map_filename);
std::string type, symbol;
int variable, index;
dict<int, std::pair<SigBit,bool>> inputs, inits, latches;
+ if (mf.fail())
+ log_cmd_error("Not able to read AIGER witness map file.\n");
while (mf >> type >> variable >> index >> symbol) {
RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
Wire *w = topmod->wire(escaped_s);
@@ -1158,7 +1174,8 @@ struct SimWorker : SimShared
state = 3;
break;
default:
- log("Simulating cycle %d.\n", cycle);
+ if (verbose)
+ log("Simulating cycle %d.\n", cycle);
top->setState(inputs, line);
if (cycle) {
set_inports(clock, State::S1);
@@ -1183,6 +1200,132 @@ struct SimWorker : SimShared
register_output_step(10*cycle);
write_output_files();
}
+
+ std::vector<std::string> split(std::string text, const char *delim)
+ {
+ std::vector<std::string> list;
+ char *p = strdup(text.c_str());
+ char *t = strtok(p, delim);
+ while (t != NULL) {
+ list.push_back(t);
+ t = strtok(NULL, delim);
+ }
+ free(p);
+ return list;
+ }
+
+ std::string signal_name(std::string const & name)
+ {
+ size_t pos = name.find_first_of("@");
+ if (pos==std::string::npos) {
+ pos = name.find_first_of("#");
+ if (pos==std::string::npos)
+ log_error("Line does not contain proper signal name `%s`\n", name.c_str());
+ }
+ return name.substr(0, pos);
+ }
+
+ void run_cosim_btor2_witness(Module *topmod)
+ {
+ log_assert(top == nullptr);
+ if ((clock.size()+clockn.size())==0)
+ log_error("Clock signal must be specified.\n");
+ std::ifstream f;
+ f.open(sim_filename.c_str());
+ if (f.fail() || GetSize(sim_filename) == 0)
+ log_error("Can not open file `%s`\n", sim_filename.c_str());
+
+ int state = 0;
+ int cycle = 0;
+ top = new SimInstance(this, scope, topmod);
+ register_signals();
+ int prev_cycle = 0;
+ int curr_cycle = 0;
+ std::vector<std::string> parts;
+ size_t len = 0;
+ while (!f.eof())
+ {
+ std::string line;
+ std::getline(f, line);
+ if (line.size()==0) continue;
+
+ if (line[0]=='#' || line[0]=='@' || line[0]=='.') {
+ if (line[0]!='.')
+ curr_cycle = atoi(line.c_str()+1);
+ else
+ curr_cycle = -1; // force detect change
+
+ if (curr_cycle != prev_cycle) {
+ if (verbose)
+ log("Simulating cycle %d.\n", cycle);
+ set_inports(clock, State::S1);
+ set_inports(clockn, State::S0);
+ update();
+ register_output_step(10*cycle+0);
+ set_inports(clock, State::S0);
+ set_inports(clockn, State::S1);
+ update();
+ register_output_step(10*cycle+5);
+ cycle++;
+ prev_cycle = curr_cycle;
+ }
+ if (line[0]=='.') break;
+ continue;
+ }
+
+ switch(state)
+ {
+ case 0:
+ if (line=="sat")
+ state = 1;
+ break;
+ case 1:
+ if (line[0]=='b' || line[0]=='j')
+ state = 2;
+ else
+ log_error("Line does not contain property.\n");
+ break;
+ default: // set state or inputs
+ parts = split(line, " ");
+ len = parts.size();
+ if (len<3 || len>4)
+ log_error("Invalid set state line content.\n");
+
+ RTLIL::IdString escaped_s = RTLIL::escape_id(signal_name(parts[len-1]));
+ if (len==3) {
+ Wire *w = topmod->wire(escaped_s);
+ if (!w) {
+ Cell *c = topmod->cell(escaped_s);
+ if (!c)
+ log_warning("Wire/cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
+ else if (c->type.in(ID($anyconst), ID($anyseq))) {
+ SigSpec sig_y= c->getPort(ID::Y);
+ if ((int)parts[1].size() != GetSize(sig_y))
+ log_error("Size of wire %s is different than provided data.\n", log_signal(sig_y));
+ top->set_state(sig_y, Const::from_string(parts[1]));
+ }
+ } else {
+ if ((int)parts[1].size() != w->width)
+ log_error("Size of wire %s is different than provided data.\n", log_signal(w));
+ top->set_state(w, Const::from_string(parts[1]));
+ }
+ } else {
+ Cell *c = topmod->cell(escaped_s);
+ if (!c)
+ log_error("Cell %s not present in module %s\n",log_id(escaped_s),log_id(topmod));
+ if (!c->is_mem_cell())
+ log_error("Cell %s is not memory cell in module %s\n",log_id(escaped_s),log_id(topmod));
+
+ Const addr = Const::from_string(parts[1].substr(1,parts[1].size()-2));
+ Const data = Const::from_string(parts[2]);
+ top->set_memory_state(c->parameters.at(ID::MEMID).decode_string(), addr, data);
+ }
+ break;
+ }
+ }
+ register_output_step(10*cycle);
+ write_output_files();
+ }
};
struct VCDWriter : public OutputWriter
@@ -1311,14 +1454,19 @@ struct AIWWriter : public OutputWriter
void write(std::map<int, bool> &) override
{
if (!aiwfile.is_open()) return;
+ if (worker->map_filename.empty())
+ log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
+
std::ifstream mf(worker->map_filename);
std::string type, symbol;
int variable, index;
+ if (mf.fail())
+ log_cmd_error("Not able to read AIGER witness map file.\n");
while (mf >> type >> variable >> index >> symbol) {
RTLIL::IdString escaped_s = RTLIL::escape_id(symbol);
Wire *w = worker->top->module->wire(escaped_s);
if (!w)
- log_error("Wire %s not present in module %s\n",log_signal(w),log_id(worker->top->module));
+ log_error("Wire %s not present in module %s\n",log_id(escaped_s),log_id(worker->top->module));
if (index < w->start_offset || index > w->start_offset + w->width)
log_error("Index %d for wire %s is out of range\n", index, log_signal(w));
if (type == "input") {
@@ -1455,7 +1603,7 @@ struct SimPass : public Pass {
log(" -map <filename>\n");
log(" read file with port and latch symbols, needed for AIGER witness input\n");
log("\n");
- log(" -scope\n");
+ log(" -scope <name>\n");
log(" scope of simulation top model\n");
log("\n");
log(" -at <time>\n");
@@ -1479,10 +1627,20 @@ struct SimPass : public Pass {
log(" -sim-gate\n");
log(" co-simulation, x in FST can match any value in simulation\n");
log("\n");
+ log(" -q\n");
+ log(" disable per-cycle/sample log message\n");
+ log("\n");
log(" -d\n");
log(" enable debug output\n");
log("\n");
}
+
+
+ static std::string file_base_name(std::string const & path)
+ {
+ return path.substr(path.find_last_of("/\\") + 1);
+ }
+
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
SimWorker worker;
@@ -1544,6 +1702,10 @@ struct SimPass : public Pass {
worker.hide_internal = false;
continue;
}
+ if (args[argidx] == "-q") {
+ worker.verbose = false;
+ continue;
+ }
if (args[argidx] == "-d") {
worker.debug = true;
continue;
@@ -1632,11 +1794,21 @@ struct SimPass : public Pass {
if (worker.sim_filename.empty())
worker.run(top_mod, numcycles);
- else
- if (worker.map_filename.empty())
- worker.run_cosim(top_mod, numcycles);
- else
- worker.run_cosim_witness(top_mod);
+ else {
+ std::string filename_trim = file_base_name(worker.sim_filename);
+ if (filename_trim.size() > 4 && ((filename_trim.compare(filename_trim.size()-4, std::string::npos, ".fst") == 0) ||
+ filename_trim.compare(filename_trim.size()-4, std::string::npos, ".vcd") == 0)) {
+ worker.run_cosim_fst(top_mod, numcycles);
+ } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".aiw") == 0) {
+ if (worker.map_filename.empty())
+ log_cmd_error("For AIGER witness file map parameter is mandatory.\n");
+ worker.run_cosim_aiger_witness(top_mod);
+ } else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) {
+ worker.run_cosim_btor2_witness(top_mod);
+ } else {
+ log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str());
+ }
+ }
}
} SimPass;
diff --git a/techlibs/intel_alm/Makefile.inc b/techlibs/intel_alm/Makefile.inc
index 614d5802c..b5f279a92 100644
--- a/techlibs/intel_alm/Makefile.inc
+++ b/techlibs/intel_alm/Makefile.inc
@@ -19,6 +19,7 @@ $(eval $(call add_share_file,share/intel_alm/cyclonev,techlibs/intel_alm/cyclone
# RAM
$(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/bram_m10k.txt))
+$(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/bram_m10k_map.v))
$(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/bram_m20k.txt))
$(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/bram_m20k_map.v))
$(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/lutram_mlab.txt))
diff --git a/techlibs/intel_alm/common/bram_m10k.txt b/techlibs/intel_alm/common/bram_m10k.txt
index 0d9a49b7d..560711b65 100644
--- a/techlibs/intel_alm/common/bram_m10k.txt
+++ b/techlibs/intel_alm/common/bram_m10k.txt
@@ -1,4 +1,4 @@
-bram MISTRAL_M10K
+bram $__MISTRAL_M10K
init 0 # TODO: Re-enable when I figure out how BRAM init works
abits 13 @D8192x1
dbits 1 @D8192x1
@@ -21,7 +21,7 @@ bram MISTRAL_M10K
endbram
-match MISTRAL_M10K
+match $__MISTRAL_M10K
min efficiency 5
make_transp
endmatch
diff --git a/techlibs/intel_alm/common/bram_m10k_map.v b/techlibs/intel_alm/common/bram_m10k_map.v
new file mode 100644
index 000000000..8f9d4a3b3
--- /dev/null
+++ b/techlibs/intel_alm/common/bram_m10k_map.v
@@ -0,0 +1,16 @@
+// Stub to invert M10K write-enable.
+
+module \$__MISTRAL_M10K (CLK1, A1ADDR, A1DATA, A1EN, B1ADDR, B1DATA, B1EN);
+
+parameter CFG_ABITS = 10;
+parameter CFG_DBITS = 10;
+
+input CLK1;
+input [CFG_ABITS-1:0] A1ADDR, B1ADDR;
+input [CFG_DBITS-1:0] A1DATA;
+input A1EN, B1EN;
+output reg [CFG_DBITS-1:0] B1DATA;
+
+MISTRAL_M10K #(.CFG_ABITS(CFG_ABITS), .CFG_DBITS(CFG_DBITS)) _TECHMAP_REPLACE_ (.CLK1(CLK1), .A1ADDR(A1ADDR), .A1DATA(A1DATA), .A1EN(!A1EN), .B1ADDR(B1ADDR), .B1DATA(B1DATA), .B1EN(B1EN));
+
+endmodule \ No newline at end of file
diff --git a/techlibs/intel_alm/common/mem_sim.v b/techlibs/intel_alm/common/mem_sim.v
index 370e17f27..c9ba8c7f1 100644
--- a/techlibs/intel_alm/common/mem_sim.v
+++ b/techlibs/intel_alm/common/mem_sim.v
@@ -145,7 +145,7 @@ endspecify
`endif
always @(posedge CLK1) begin
- if (A1EN)
+ if (!A1EN)
mem[(A1ADDR + 1) * CFG_DBITS - 1 : A1ADDR * CFG_DBITS] <= A1DATA;
if (B1EN)
diff --git a/techlibs/intel_alm/common/quartus_rename.v b/techlibs/intel_alm/common/quartus_rename.v
index 5850f6907..217dc5de9 100644
--- a/techlibs/intel_alm/common/quartus_rename.v
+++ b/techlibs/intel_alm/common/quartus_rename.v
@@ -157,6 +157,11 @@ output [CFG_DBITS-1:0] B1DATA;
// Much like the MLAB, the M10K has mem_init[01234] parameters which would let
// you initialise the RAM cell via hex literals. If they were implemented.
+// Since the MISTRAL_M10K block has an inverted write-enable (like the real hardware)
+// but the Quartus primitive expects a normal write-enable, we add an inverter.
+wire A1EN_N;
+NOT wren_inv (.IN(A1EN), .OUT(A1EN_N));
+
`RAM_BLOCK #(
.operation_mode("dual_port"),
.logical_ram_name(_TECHMAP_CELLNAME_),
@@ -176,10 +181,10 @@ output [CFG_DBITS-1:0] B1DATA;
.port_b_first_bit_number(0),
.port_b_address_clock("clock0"),
.port_b_read_enable_clock("clock0")
-) _TECHMAP_REPLACE_ (
+) ram_block (
.portaaddr(A1ADDR),
.portadatain(A1DATA),
- .portawe(A1EN),
+ .portawe(A1EN_N),
.portbaddr(B1ADDR),
.portbdataout(B1DATA),
.portbre(B1EN),
diff --git a/techlibs/intel_alm/synth_intel_alm.cc b/techlibs/intel_alm/synth_intel_alm.cc
index 34a5ffa5d..43d3592d5 100644
--- a/techlibs/intel_alm/synth_intel_alm.cc
+++ b/techlibs/intel_alm/synth_intel_alm.cc
@@ -262,8 +262,7 @@ struct SynthIntelALMPass : public ScriptPass {
if (!nobram && check_label("map_bram", "(skip if -nobram)")) {
run(stringf("memory_bram -rules +/intel_alm/common/bram_%s.txt", bram_type.c_str()));
- if (help_mode || bram_type != "m10k")
- run(stringf("techmap -map +/intel_alm/common/bram_%s_map.v", bram_type.c_str()));
+ run(stringf("techmap -map +/intel_alm/common/bram_%s_map.v", bram_type.c_str()));
}
if (!nolutram && check_label("map_lutram", "(skip if -nolutram)")) {
diff --git a/tests/arch/intel_alm/blockram.ys b/tests/arch/intel_alm/blockram.ys
index c157c3165..3b61b9339 100644
--- a/tests/arch/intel_alm/blockram.ys
+++ b/tests/arch/intel_alm/blockram.ys
@@ -2,5 +2,6 @@ read_verilog ../common/blockram.v
chparam -set ADDRESS_WIDTH 10 -set DATA_WIDTH 10 sync_ram_sdp
synth_intel_alm -family cyclonev -noiopad -noclkbuf
cd sync_ram_sdp
+select -assert-count 1 t:MISTRAL_NOT
select -assert-count 1 t:MISTRAL_M10K
-select -assert-none t:MISTRAL_M10K %% t:* %D
+select -assert-none t:MISTRAL_NOT t:MISTRAL_M10K %% t:* %D
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 06:51:04 +0000