projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge pull request #2089 from rswarbrick/modports
[yosys.git] / frontends / verific / verific.cc
1 /*
2 * yosys -- Yosys Open SYnthesis Suite
3 *
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
5 *
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
9 *
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
17 *
18 */
19
20 #include "kernel/yosys.h"
21 #include "kernel/sigtools.h"
22 #include "kernel/celltypes.h"
23 #include "kernel/log.h"
24 #include <stdlib.h>
25 #include <stdio.h>
26 #include <string.h>
27
28 #ifndef _WIN32
29 # include <unistd.h>
30 # include <dirent.h>
31 #endif
32
33 #include "frontends/verific/verific.h"
34
35 USING_YOSYS_NAMESPACE
36
37 #ifdef YOSYS_ENABLE_VERIFIC
38
39 #ifdef __clang__
40 #pragma clang diagnostic push
41 #pragma clang diagnostic ignored "-Woverloaded-virtual"
42 #endif
43
44 #include "veri_file.h"
45 #include "vhdl_file.h"
46 #include "hier_tree.h"
47 #include "VeriModule.h"
48 #include "VeriWrite.h"
49 #include "VhdlUnits.h"
50 #include "VeriLibrary.h"
51
52 #ifndef SYMBIOTIC_VERIFIC_API_VERSION
53 # error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
54 #endif
55
56 #if SYMBIOTIC_VERIFIC_API_VERSION < 1
57 # error "Please update your version of Symbiotic EDA flavored Verific."
58 #endif
59
60 #ifdef __clang__
61 #pragma clang diagnostic pop
62 #endif
63
64 #ifdef VERIFIC_NAMESPACE
65 using namespace Verific;
66 #endif
67
68 #endif
69
70 #ifdef YOSYS_ENABLE_VERIFIC
71 YOSYS_NAMESPACE_BEGIN
72
73 int verific_verbose;
74 bool verific_import_pending;
75 string verific_error_msg;
76 int verific_sva_fsm_limit;
77
78 vector<string> verific_incdirs, verific_libdirs;
79
80 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
81 {
82 string message_prefix = stringf("VERIFIC-%s [%s] ",
83 msg_type == VERIFIC_NONE ? "NONE" :
84 msg_type == VERIFIC_ERROR ? "ERROR" :
85 msg_type == VERIFIC_WARNING ? "WARNING" :
86 msg_type == VERIFIC_IGNORE ? "IGNORE" :
87 msg_type == VERIFIC_INFO ? "INFO" :
88 msg_type == VERIFIC_COMMENT ? "COMMENT" :
89 msg_type == VERIFIC_PROGRAM_ERROR ? "PROGRAM_ERROR" : "UNKNOWN", message_id);
90
91 string message = linefile ? stringf("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile)) : "";
92 message += vstringf(msg, args);
93
94 if (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_WARNING || msg_type == VERIFIC_PROGRAM_ERROR)
95 log_warning_noprefix("%s%s\n", message_prefix.c_str(), message.c_str());
96 else
97 log("%s%s\n", message_prefix.c_str(), message.c_str());
98
99 if (verific_error_msg.empty() && (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_PROGRAM_ERROR))
100 verific_error_msg = message;
101 }
102
103 string get_full_netlist_name(Netlist *nl)
104 {
105 if (nl->NumOfRefs() == 1) {
106 Instance *inst = (Instance*)nl->GetReferences()->GetLast();
107 return get_full_netlist_name(inst->Owner()) + "." + inst->Name();
108 }
109
110 return nl->CellBaseName();
111 }
112
113 // ==================================================================
114
115 VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) :
116 mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
117 mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover),
118 mode_fullinit(mode_fullinit)
119 {
120 }
121
122 RTLIL::SigBit VerificImporter::net_map_at(Net *net)
123 {
124 if (net->IsExternalTo(netlist))
125 log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n",
126 get_full_netlist_name(net->Owner()).c_str(), net->Name(), get_full_netlist_name(netlist).c_str());
127
128 return net_map.at(net);
129 }
130
131 bool is_blackbox(Netlist *nl)
132 {
133 if (nl->IsBlackBox() || nl->IsEmptyBox())
134 return true;
135
136 const char *attr = nl->GetAttValue("blackbox");
137 if (attr != nullptr && strcmp(attr, "0"))
138 return true;
139
140 return false;
141 }
142
143 RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj)
144 {
145 std::string s = stringf("$verific$%s", obj->Name());
146 if (obj->Linefile())
147 s += stringf("$%s:%d", Verific::LineFile::GetFileName(obj->Linefile()), Verific::LineFile::GetLineNo(obj->Linefile()));
148 s += stringf("$%d", autoidx++);
149 return s;
150 }
151
152 void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj, Netlist *nl)
153 {
154 MapIter mi;
155 Att *attr;
156
157 if (obj->Linefile())
158 attributes[ID::src] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
159
160 // FIXME: Parse numeric attributes
161 FOREACH_ATTRIBUTE(obj, mi, attr) {
162 if (attr->Key()[0] == ' ' || attr->Value() == nullptr)
163 continue;
164 attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
165 }
166
167 if (nl) {
168 auto type_range = nl->GetTypeRange(obj->Name());
169 if (!type_range)
170 return;
171 if (!type_range->IsTypeEnum())
172 return;
173 if (nl->IsFromVhdl() && strcmp(type_range->GetTypeName(), "STD_LOGIC") == 0)
174 return;
175 auto type_name = type_range->GetTypeName();
176 if (!type_name)
177 return;
178 attributes.emplace(ID::wiretype, RTLIL::escape_id(type_name));
179
180 MapIter mi;
181 const char *k, *v;
182 FOREACH_MAP_ITEM(type_range->GetEnumIdMap(), mi, &k, &v) {
183 if (nl->IsFromVerilog()) {
184 // Expect <decimal>'b<binary>
185 auto p = strchr(v, '\'');
186 if (p) {
187 if (*(p+1) != 'b')
188 p = nullptr;
189 else
190 for (auto q = p+2; *q != '\0'; q++)
191 if (*q != '0' && *q != '1') {
192 p = nullptr;
193 break;
194 }
195 }
196 if (p == nullptr)
197 log_error("Expected TypeRange value '%s' to be of form <decimal>'b<binary>.\n", v);
198 attributes.emplace(stringf("\\enum_value_%s", p+2), RTLIL::escape_id(k));
199 }
200 else if (nl->IsFromVhdl()) {
201 // Expect "<binary>"
202 auto p = v;
203 if (p) {
204 if (*p != '"')
205 p = nullptr;
206 else {
207 auto *q = p+1;
208 for (; *q != '"'; q++)
209 if (*q != '0' && *q != '1') {
210 p = nullptr;
211 break;
212 }
213 if (p && *(q+1) != '\0')
214 p = nullptr;
215 }
216 }
217 if (p == nullptr)
218 log_error("Expected TypeRange value '%s' to be of form \"<binary>\".\n", v);
219 auto l = strlen(p);
220 auto q = (char*)malloc(l+1-2);
221 strncpy(q, p+1, l-2);
222 q[l-2] = '\0';
223 attributes.emplace(stringf("\\enum_value_%s", q), RTLIL::escape_id(k));
224 free(q);
225 }
226 }
227 }
228 }
229
230 RTLIL::SigSpec VerificImporter::operatorInput(Instance *inst)
231 {
232 RTLIL::SigSpec sig;
233 for (int i = int(inst->InputSize())-1; i >= 0; i--)
234 if (inst->GetInputBit(i))
235 sig.append(net_map_at(inst->GetInputBit(i)));
236 else
237 sig.append(RTLIL::State::Sz);
238 return sig;
239 }
240
241 RTLIL::SigSpec VerificImporter::operatorInput1(Instance *inst)
242 {
243 RTLIL::SigSpec sig;
244 for (int i = int(inst->Input1Size())-1; i >= 0; i--)
245 if (inst->GetInput1Bit(i))
246 sig.append(net_map_at(inst->GetInput1Bit(i)));
247 else
248 sig.append(RTLIL::State::Sz);
249 return sig;
250 }
251
252 RTLIL::SigSpec VerificImporter::operatorInput2(Instance *inst)
253 {
254 RTLIL::SigSpec sig;
255 for (int i = int(inst->Input2Size())-1; i >= 0; i--)
256 if (inst->GetInput2Bit(i))
257 sig.append(net_map_at(inst->GetInput2Bit(i)));
258 else
259 sig.append(RTLIL::State::Sz);
260 return sig;
261 }
262
263 RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portname)
264 {
265 PortBus *portbus = inst->View()->GetPortBus(portname);
266 if (portbus) {
267 RTLIL::SigSpec sig;
268 for (unsigned i = 0; i < portbus->Size(); i++) {
269 Net *net = inst->GetNet(portbus->ElementAtIndex(i));
270 if (net) {
271 if (net->IsGnd())
272 sig.append(RTLIL::State::S0);
273 else if (net->IsPwr())
274 sig.append(RTLIL::State::S1);
275 else
276 sig.append(net_map_at(net));
277 } else
278 sig.append(RTLIL::State::Sz);
279 }
280 return sig;
281 } else {
282 Port *port = inst->View()->GetPort(portname);
283 log_assert(port != NULL);
284 Net *net = inst->GetNet(port);
285 return net_map_at(net);
286 }
287 }
288
289 RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*, hash_ptr_ops> *any_all_nets)
290 {
291 RTLIL::SigSpec sig;
292 RTLIL::Wire *dummy_wire = NULL;
293 for (int i = int(inst->OutputSize())-1; i >= 0; i--)
294 if (inst->GetOutputBit(i) && (!any_all_nets || !any_all_nets->count(inst->GetOutputBit(i)))) {
295 sig.append(net_map_at(inst->GetOutputBit(i)));
296 dummy_wire = NULL;
297 } else {
298 if (dummy_wire == NULL)
299 dummy_wire = module->addWire(new_verific_id(inst));
300 else
301 dummy_wire->width++;
302 sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
303 }
304 return sig;
305 }
306
307 bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name)
308 {
309 if (inst->Type() == PRIM_AND) {
310 module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
311 return true;
312 }
313
314 if (inst->Type() == PRIM_NAND) {
315 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
316 module->addAndGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
317 module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
318 return true;
319 }
320
321 if (inst->Type() == PRIM_OR) {
322 module->addOrGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
323 return true;
324 }
325
326 if (inst->Type() == PRIM_NOR) {
327 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
328 module->addOrGate(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
329 module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput()));
330 return true;
331 }
332
333 if (inst->Type() == PRIM_XOR) {
334 module->addXorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
335 return true;
336 }
337
338 if (inst->Type() == PRIM_XNOR) {
339 module->addXnorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
340 return true;
341 }
342
343 if (inst->Type() == PRIM_BUF) {
344 auto outnet = inst->GetOutput();
345 if (!any_all_nets.count(outnet))
346 module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
347 return true;
348 }
349
350 if (inst->Type() == PRIM_INV) {
351 module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
352 return true;
353 }
354
355 if (inst->Type() == PRIM_MUX) {
356 module->addMuxGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
357 return true;
358 }
359
360 if (inst->Type() == PRIM_TRI) {
361 module->addMuxGate(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
362 return true;
363 }
364
365 if (inst->Type() == PRIM_FADD)
366 {
367 RTLIL::SigSpec a = net_map_at(inst->GetInput1()), b = net_map_at(inst->GetInput2()), c = net_map_at(inst->GetCin());
368 RTLIL::SigSpec x = inst->GetCout() ? net_map_at(inst->GetCout()) : module->addWire(new_verific_id(inst));
369 RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
370 RTLIL::SigSpec tmp1 = module->addWire(new_verific_id(inst));
371 RTLIL::SigSpec tmp2 = module->addWire(new_verific_id(inst));
372 RTLIL::SigSpec tmp3 = module->addWire(new_verific_id(inst));
373 module->addXorGate(new_verific_id(inst), a, b, tmp1);
374 module->addXorGate(inst_name, tmp1, c, y);
375 module->addAndGate(new_verific_id(inst), tmp1, c, tmp2);
376 module->addAndGate(new_verific_id(inst), a, b, tmp3);
377 module->addOrGate(new_verific_id(inst), tmp2, tmp3, x);
378 return true;
379 }
380
381 if (inst->Type() == PRIM_DFFRS)
382 {
383 VerificClocking clocking(this, inst->GetClock());
384 log_assert(clocking.disable_sig == State::S0);
385 log_assert(clocking.body_net == nullptr);
386
387 if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
388 clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
389 else if (inst->GetSet()->IsGnd())
390 clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S0);
391 else if (inst->GetReset()->IsGnd())
392 clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S1);
393 else
394 clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
395 net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
396 return true;
397 }
398
399 return false;
400 }
401
402 bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name)
403 {
404 RTLIL::Cell *cell = nullptr;
405
406 if (inst->Type() == PRIM_AND) {
407 cell = module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
408 import_attributes(cell->attributes, inst);
409 return true;
410 }
411
412 if (inst->Type() == PRIM_NAND) {
413 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
414 cell = module->addAnd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
415 import_attributes(cell->attributes, inst);
416 cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
417 import_attributes(cell->attributes, inst);
418 return true;
419 }
420
421 if (inst->Type() == PRIM_OR) {
422 cell = module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
423 import_attributes(cell->attributes, inst);
424 return true;
425 }
426
427 if (inst->Type() == PRIM_NOR) {
428 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst));
429 cell = module->addOr(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp);
430 import_attributes(cell->attributes, inst);
431 cell = module->addNot(inst_name, tmp, net_map_at(inst->GetOutput()));
432 import_attributes(cell->attributes, inst);
433 return true;
434 }
435
436 if (inst->Type() == PRIM_XOR) {
437 cell = module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
438 import_attributes(cell->attributes, inst);
439 return true;
440 }
441
442 if (inst->Type() == PRIM_XNOR) {
443 cell = module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput()));
444 import_attributes(cell->attributes, inst);
445 return true;
446 }
447
448 if (inst->Type() == PRIM_INV) {
449 cell = module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
450 import_attributes(cell->attributes, inst);
451 return true;
452 }
453
454 if (inst->Type() == PRIM_MUX) {
455 cell = module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
456 import_attributes(cell->attributes, inst);
457 return true;
458 }
459
460 if (inst->Type() == PRIM_TRI) {
461 cell = module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput()));
462 import_attributes(cell->attributes, inst);
463 return true;
464 }
465
466 if (inst->Type() == PRIM_FADD)
467 {
468 RTLIL::SigSpec a_plus_b = module->addWire(new_verific_id(inst), 2);
469 RTLIL::SigSpec y = inst->GetOutput() ? net_map_at(inst->GetOutput()) : module->addWire(new_verific_id(inst));
470 if (inst->GetCout())
471 y.append(net_map_at(inst->GetCout()));
472 cell = module->addAdd(new_verific_id(inst), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b);
473 import_attributes(cell->attributes, inst);
474 cell = module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y);
475 import_attributes(cell->attributes, inst);
476 return true;
477 }
478
479 if (inst->Type() == PRIM_DFFRS)
480 {
481 VerificClocking clocking(this, inst->GetClock());
482 log_assert(clocking.disable_sig == State::S0);
483 log_assert(clocking.body_net == nullptr);
484
485 if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
486 cell = clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
487 else if (inst->GetSet()->IsGnd())
488 cell = clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
489 else if (inst->GetReset()->IsGnd())
490 cell = clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
491 else
492 cell = clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
493 net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
494 import_attributes(cell->attributes, inst);
495 return true;
496 }
497
498 if (inst->Type() == PRIM_DLATCHRS)
499 {
500 if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
501 cell = module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
502 else
503 cell = module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
504 net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
505 import_attributes(cell->attributes, inst);
506 return true;
507 }
508
509 #define IN operatorInput(inst)
510 #define IN1 operatorInput1(inst)
511 #define IN2 operatorInput2(inst)
512 #define OUT operatorOutput(inst)
513 #define FILTERED_OUT operatorOutput(inst, &any_all_nets)
514 #define SIGNED inst->View()->IsSigned()
515
516 if (inst->Type() == OPER_ADDER) {
517 RTLIL::SigSpec out = OUT;
518 if (inst->GetCout() != NULL)
519 out.append(net_map_at(inst->GetCout()));
520 if (inst->GetCin()->IsGnd()) {
521 cell = module->addAdd(inst_name, IN1, IN2, out, SIGNED);
522 import_attributes(cell->attributes, inst);
523 } else {
524 RTLIL::SigSpec tmp = module->addWire(new_verific_id(inst), GetSize(out));
525 cell = module->addAdd(new_verific_id(inst), IN1, IN2, tmp, SIGNED);
526 import_attributes(cell->attributes, inst);
527 cell = module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false);
528 import_attributes(cell->attributes, inst);
529 }
530 return true;
531 }
532
533 if (inst->Type() == OPER_MULTIPLIER) {
534 cell = module->addMul(inst_name, IN1, IN2, OUT, SIGNED);
535 import_attributes(cell->attributes, inst);
536 return true;
537 }
538
539 if (inst->Type() == OPER_DIVIDER) {
540 cell = module->addDiv(inst_name, IN1, IN2, OUT, SIGNED);
541 import_attributes(cell->attributes, inst);
542 return true;
543 }
544
545 if (inst->Type() == OPER_MODULO) {
546 cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
547 import_attributes(cell->attributes, inst);
548 return true;
549 }
550
551 if (inst->Type() == OPER_REMAINDER) {
552 cell = module->addMod(inst_name, IN1, IN2, OUT, SIGNED);
553 import_attributes(cell->attributes, inst);
554 return true;
555 }
556
557 if (inst->Type() == OPER_SHIFT_LEFT) {
558 cell = module->addShl(inst_name, IN1, IN2, OUT, false);
559 import_attributes(cell->attributes, inst);
560 return true;
561 }
562
563 if (inst->Type() == OPER_ENABLED_DECODER) {
564 RTLIL::SigSpec vec;
565 vec.append(net_map_at(inst->GetControl()));
566 for (unsigned i = 1; i < inst->OutputSize(); i++) {
567 vec.append(RTLIL::State::S0);
568 }
569 cell = module->addShl(inst_name, vec, IN, OUT, false);
570 import_attributes(cell->attributes, inst);
571 return true;
572 }
573
574 if (inst->Type() == OPER_DECODER) {
575 RTLIL::SigSpec vec;
576 vec.append(RTLIL::State::S1);
577 for (unsigned i = 1; i < inst->OutputSize(); i++) {
578 vec.append(RTLIL::State::S0);
579 }
580 cell = module->addShl(inst_name, vec, IN, OUT, false);
581 import_attributes(cell->attributes, inst);
582 return true;
583 }
584
585 if (inst->Type() == OPER_SHIFT_RIGHT) {
586 Net *net_cin = inst->GetCin();
587 Net *net_a_msb = inst->GetInput1Bit(0);
588 if (net_cin->IsGnd())
589 cell = module->addShr(inst_name, IN1, IN2, OUT, false);
590 else if (net_cin == net_a_msb)
591 cell = module->addSshr(inst_name, IN1, IN2, OUT, true);
592 else
593 log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name());
594 import_attributes(cell->attributes, inst);
595 return true;
596 }
597
598 if (inst->Type() == OPER_REDUCE_AND) {
599 cell = module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
600 import_attributes(cell->attributes, inst);
601 return true;
602 }
603
604 if (inst->Type() == OPER_REDUCE_NAND) {
605 Wire *tmp = module->addWire(NEW_ID);
606 cell = module->addReduceAnd(inst_name, IN, tmp, SIGNED);
607 module->addNot(NEW_ID, tmp, net_map_at(inst->GetOutput()));
608 import_attributes(cell->attributes, inst);
609 return true;
610 }
611
612 if (inst->Type() == OPER_REDUCE_OR) {
613 cell = module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
614 import_attributes(cell->attributes, inst);
615 return true;
616 }
617
618 if (inst->Type() == OPER_REDUCE_XOR) {
619 cell = module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
620 import_attributes(cell->attributes, inst);
621 return true;
622 }
623
624 if (inst->Type() == OPER_REDUCE_XNOR) {
625 cell = module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED);
626 import_attributes(cell->attributes, inst);
627 return true;
628 }
629
630 if (inst->Type() == OPER_REDUCE_NOR) {
631 SigSpec t = module->ReduceOr(new_verific_id(inst), IN, SIGNED);
632 cell = module->addNot(inst_name, t, net_map_at(inst->GetOutput()));
633 import_attributes(cell->attributes, inst);
634 return true;
635 }
636
637 if (inst->Type() == OPER_LESSTHAN) {
638 Net *net_cin = inst->GetCin();
639 if (net_cin->IsGnd())
640 cell = module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
641 else if (net_cin->IsPwr())
642 cell = module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
643 else
644 log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
645 import_attributes(cell->attributes, inst);
646 return true;
647 }
648
649 if (inst->Type() == OPER_WIDE_AND) {
650 cell = module->addAnd(inst_name, IN1, IN2, OUT, SIGNED);
651 import_attributes(cell->attributes, inst);
652 return true;
653 }
654
655 if (inst->Type() == OPER_WIDE_OR) {
656 cell = module->addOr(inst_name, IN1, IN2, OUT, SIGNED);
657 import_attributes(cell->attributes, inst);
658 return true;
659 }
660
661 if (inst->Type() == OPER_WIDE_XOR) {
662 cell = module->addXor(inst_name, IN1, IN2, OUT, SIGNED);
663 import_attributes(cell->attributes, inst);
664 return true;
665 }
666
667 if (inst->Type() == OPER_WIDE_XNOR) {
668 cell = module->addXnor(inst_name, IN1, IN2, OUT, SIGNED);
669 import_attributes(cell->attributes, inst);
670 return true;
671 }
672
673 if (inst->Type() == OPER_WIDE_BUF) {
674 cell = module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
675 import_attributes(cell->attributes, inst);
676 return true;
677 }
678
679 if (inst->Type() == OPER_WIDE_INV) {
680 cell = module->addNot(inst_name, IN, OUT, SIGNED);
681 import_attributes(cell->attributes, inst);
682 return true;
683 }
684
685 if (inst->Type() == OPER_MINUS) {
686 cell = module->addSub(inst_name, IN1, IN2, OUT, SIGNED);
687 import_attributes(cell->attributes, inst);
688 return true;
689 }
690
691 if (inst->Type() == OPER_UMINUS) {
692 cell = module->addNeg(inst_name, IN, OUT, SIGNED);
693 import_attributes(cell->attributes, inst);
694 return true;
695 }
696
697 if (inst->Type() == OPER_EQUAL) {
698 cell = module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
699 import_attributes(cell->attributes, inst);
700 return true;
701 }
702
703 if (inst->Type() == OPER_NEQUAL) {
704 cell = module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED);
705 import_attributes(cell->attributes, inst);
706 return true;
707 }
708
709 if (inst->Type() == OPER_WIDE_MUX) {
710 cell = module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT);
711 import_attributes(cell->attributes, inst);
712 return true;
713 }
714
715 if (inst->Type() == OPER_NTO1MUX) {
716 cell = module->addShr(inst_name, IN2, IN1, net_map_at(inst->GetOutput()));
717 import_attributes(cell->attributes, inst);
718 return true;
719 }
720
721 if (inst->Type() == OPER_WIDE_NTO1MUX)
722 {
723 SigSpec data = IN2, out = OUT;
724
725 int wordsize_bits = ceil_log2(GetSize(out));
726 int wordsize = 1 << wordsize_bits;
727
728 SigSpec sel = {IN1, SigSpec(State::S0, wordsize_bits)};
729
730 SigSpec padded_data;
731 for (int i = 0; i < GetSize(data); i += GetSize(out)) {
732 SigSpec d = data.extract(i, GetSize(out));
733 d.extend_u0(wordsize);
734 padded_data.append(d);
735 }
736
737 cell = module->addShr(inst_name, padded_data, sel, out);
738 import_attributes(cell->attributes, inst);
739 return true;
740 }
741
742 if (inst->Type() == OPER_SELECTOR)
743 {
744 cell = module->addPmux(inst_name, State::S0, IN2, IN1, net_map_at(inst->GetOutput()));
745 import_attributes(cell->attributes, inst);
746 return true;
747 }
748
749 if (inst->Type() == OPER_WIDE_SELECTOR)
750 {
751 SigSpec out = OUT;
752 cell = module->addPmux(inst_name, SigSpec(State::S0, GetSize(out)), IN2, IN1, out);
753 import_attributes(cell->attributes, inst);
754 return true;
755 }
756
757 if (inst->Type() == OPER_WIDE_TRI) {
758 cell = module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT);
759 import_attributes(cell->attributes, inst);
760 return true;
761 }
762
763 if (inst->Type() == OPER_WIDE_DFFRS)
764 {
765 VerificClocking clocking(this, inst->GetClock());
766 log_assert(clocking.disable_sig == State::S0);
767 log_assert(clocking.body_net == nullptr);
768
769 RTLIL::SigSpec sig_set = operatorInport(inst, "set");
770 RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
771
772 if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
773 cell = clocking.addDff(inst_name, IN, OUT);
774 else
775 cell = clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
776 import_attributes(cell->attributes, inst);
777
778 return true;
779 }
780
781 #undef IN
782 #undef IN1
783 #undef IN2
784 #undef OUT
785 #undef SIGNED
786
787 return false;
788 }
789
790 void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBit clock, bool clock_pol)
791 {
792 bool keep_running = true;
793 SigMap sigmap;
794
795 while (keep_running)
796 {
797 keep_running = false;
798
799 dict<SigBit, pool<RTLIL::Cell*>> dbits_db;
800 SigSpec dbits;
801
802 for (auto cell : candidates) {
803 SigBit bit = sigmap(cell->getPort(ID::D));
804 dbits_db[bit].insert(cell);
805 dbits.append(bit);
806 }
807
808 dbits.sort_and_unify();
809
810 for (auto chunk : dbits.chunks())
811 {
812 SigSpec sig_d = chunk;
813
814 if (chunk.wire == nullptr || GetSize(sig_d) == 1)
815 continue;
816
817 SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d));
818 RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol);
819
820 if (verific_verbose)
821 log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff));
822
823 for (int i = 0; i < GetSize(sig_d); i++)
824 for (auto old_ff : dbits_db[sig_d[i]])
825 {
826 if (verific_verbose)
827 log(" replacing old ff %s on bit %d.\n", log_id(old_ff), i);
828
829 SigBit old_q = old_ff->getPort(ID::Q);
830 SigBit new_q = sig_q[i];
831
832 sigmap.add(old_q, new_q);
833 module->connect(old_q, new_q);
834 candidates.erase(old_ff);
835 module->remove(old_ff);
836 keep_running = true;
837 }
838 }
839 }
840 }
841
842 void VerificImporter::merge_past_ffs(pool<RTLIL::Cell*> &candidates)
843 {
844 dict<pair<SigBit, int>, pool<RTLIL::Cell*>> database;
845
846 for (auto cell : candidates)
847 {
848 SigBit clock = cell->getPort(ID::CLK);
849 bool clock_pol = cell->getParam(ID::CLK_POLARITY).as_bool();
850 database[make_pair(clock, int(clock_pol))].insert(cell);
851 }
852
853 for (auto it : database)
854 merge_past_ffs_clock(it.second, it.first.first, it.first.second);
855 }
856
857 void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool norename)
858 {
859 std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
860 std::string module_name = netlist_name;
861
862 if (nl->IsOperator() || nl->IsPrimitive()) {
863 module_name = "$verific$" + module_name;
864 } else {
865 if (!norename && *nl->Name()) {
866 module_name += "(";
867 module_name += nl->Name();
868 module_name += ")";
869 }
870 module_name = "\\" + module_name;
871 }
872
873 netlist = nl;
874
875 if (design->has(module_name)) {
876 if (!nl->IsOperator() && !is_blackbox(nl))
877 log_cmd_error("Re-definition of module `%s'.\n", netlist_name.c_str());
878 return;
879 }
880
881 module = new RTLIL::Module;
882 module->name = module_name;
883 design->add(module);
884
885 if (is_blackbox(nl)) {
886 log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name));
887 module->set_bool_attribute(ID::blackbox);
888 } else {
889 log("Importing module %s.\n", RTLIL::id2cstr(module->name));
890 }
891
892 SetIter si;
893 MapIter mi, mi2;
894 Port *port;
895 PortBus *portbus;
896 Net *net;
897 NetBus *netbus;
898 Instance *inst;
899 PortRef *pr;
900
901 FOREACH_PORT_OF_NETLIST(nl, mi, port)
902 {
903 if (port->Bus())
904 continue;
905
906 if (verific_verbose)
907 log(" importing port %s.\n", port->Name());
908
909 RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
910 import_attributes(wire->attributes, port, nl);
911
912 wire->port_id = nl->IndexOf(port) + 1;
913
914 if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
915 wire->port_input = true;
916 if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
917 wire->port_output = true;
918
919 if (port->GetNet()) {
920 net = port->GetNet();
921 if (net_map.count(net) == 0)
922 net_map[net] = wire;
923 else if (wire->port_input)
924 module->connect(net_map_at(net), wire);
925 else
926 module->connect(wire, net_map_at(net));
927 }
928 }
929
930 FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
931 {
932 if (verific_verbose)
933 log(" importing portbus %s.\n", portbus->Name());
934
935 RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
936 wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
937 import_attributes(wire->attributes, portbus, nl);
938
939 if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
940 wire->port_input = true;
941 if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
942 wire->port_output = true;
943
944 for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
945 if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
946 net = portbus->ElementAtIndex(i)->GetNet();
947 RTLIL::SigBit bit(wire, i - wire->start_offset);
948 if (net_map.count(net) == 0)
949 net_map[net] = bit;
950 else if (wire->port_input)
951 module->connect(net_map_at(net), bit);
952 else
953 module->connect(bit, net_map_at(net));
954 }
955 if (i == portbus->RightIndex())
956 break;
957 }
958 }
959
960 module->fixup_ports();
961
962 dict<Net*, char, hash_ptr_ops> init_nets;
963 pool<Net*, hash_ptr_ops> anyconst_nets, anyseq_nets;
964 pool<Net*, hash_ptr_ops> allconst_nets, allseq_nets;
965 any_all_nets.clear();
966
967 FOREACH_NET_OF_NETLIST(nl, mi, net)
968 {
969 if (net->IsRamNet())
970 {
971 RTLIL::Memory *memory = new RTLIL::Memory;
972 memory->name = RTLIL::escape_id(net->Name());
973 log_assert(module->count_id(memory->name) == 0);
974 module->memories[memory->name] = memory;
975
976 int number_of_bits = net->Size();
977 number_of_bits = 1 << ceil_log2(number_of_bits);
978 int bits_in_word = number_of_bits;
979 FOREACH_PORTREF_OF_NET(net, si, pr) {
980 if (pr->GetInst()->Type() == OPER_READ_PORT) {
981 bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
982 continue;
983 }
984 if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
985 bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
986 continue;
987 }
988 log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
989 net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
990 }
991
992 memory->width = bits_in_word;
993 memory->size = number_of_bits / bits_in_word;
994
995 const char *ascii_initdata = net->GetWideInitialValue();
996 if (ascii_initdata) {
997 while (*ascii_initdata != 0 && *ascii_initdata != '\'')
998 ascii_initdata++;
999 if (*ascii_initdata == '\'')
1000 ascii_initdata++;
1001 if (*ascii_initdata != 0) {
1002 log_assert(*ascii_initdata == 'b');
1003 ascii_initdata++;
1004 }
1005 for (int word_idx = 0; word_idx < memory->size; word_idx++) {
1006 Const initval = Const(State::Sx, memory->width);
1007 bool initval_valid = false;
1008 for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) {
1009 if (*ascii_initdata == 0)
1010 break;
1011 if (*ascii_initdata == '0' || *ascii_initdata == '1') {
1012 initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1;
1013 initval_valid = true;
1014 }
1015 ascii_initdata++;
1016 }
1017 if (initval_valid) {
1018 RTLIL::Cell *cell = module->addCell(new_verific_id(net), ID($meminit));
1019 cell->parameters[ID::WORDS] = 1;
1020 if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
1021 cell->setPort(ID::ADDR, word_idx);
1022 else
1023 cell->setPort(ID::ADDR, memory->size - word_idx - 1);
1024 cell->setPort(ID::DATA, initval);
1025 cell->parameters[ID::MEMID] = RTLIL::Const(memory->name.str());
1026 cell->parameters[ID::ABITS] = 32;
1027 cell->parameters[ID::WIDTH] = memory->width;
1028 cell->parameters[ID::PRIORITY] = RTLIL::Const(autoidx-1);
1029 }
1030 }
1031 }
1032 continue;
1033 }
1034
1035 if (net->GetInitialValue())
1036 init_nets[net] = net->GetInitialValue();
1037
1038 const char *rand_const_attr = net->GetAttValue(" rand_const");
1039 const char *rand_attr = net->GetAttValue(" rand");
1040
1041 const char *anyconst_attr = net->GetAttValue("anyconst");
1042 const char *anyseq_attr = net->GetAttValue("anyseq");
1043
1044 const char *allconst_attr = net->GetAttValue("allconst");
1045 const char *allseq_attr = net->GetAttValue("allseq");
1046
1047 if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'"))) {
1048 anyconst_nets.insert(net);
1049 any_all_nets.insert(net);
1050 }
1051 else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'"))) {
1052 anyseq_nets.insert(net);
1053 any_all_nets.insert(net);
1054 }
1055 else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'"))) {
1056 anyconst_nets.insert(net);
1057 any_all_nets.insert(net);
1058 }
1059 else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'"))) {
1060 anyseq_nets.insert(net);
1061 any_all_nets.insert(net);
1062 }
1063 else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'"))) {
1064 allconst_nets.insert(net);
1065 any_all_nets.insert(net);
1066 }
1067 else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'"))) {
1068 allseq_nets.insert(net);
1069 any_all_nets.insert(net);
1070 }
1071
1072 if (net_map.count(net)) {
1073 if (verific_verbose)
1074 log(" skipping net %s.\n", net->Name());
1075 continue;
1076 }
1077
1078 if (net->Bus())
1079 continue;
1080
1081 RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : new_verific_id(net));
1082
1083 if (verific_verbose)
1084 log(" importing net %s as %s.\n", net->Name(), log_id(wire_name));
1085
1086 RTLIL::Wire *wire = module->addWire(wire_name);
1087 import_attributes(wire->attributes, net, nl);
1088
1089 net_map[net] = wire;
1090 }
1091
1092 FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
1093 {
1094 bool found_new_net = false;
1095 for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
1096 net = netbus->ElementAtIndex(i);
1097 if (net_map.count(net) == 0)
1098 found_new_net = true;
1099 if (i == netbus->RightIndex())
1100 break;
1101 }
1102
1103 if (found_new_net)
1104 {
1105 RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : new_verific_id(netbus));
1106
1107 if (verific_verbose)
1108 log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name));
1109
1110 RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
1111 wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
1112 import_attributes(wire->attributes, netbus, nl);
1113
1114 RTLIL::Const initval = Const(State::Sx, GetSize(wire));
1115 bool initval_valid = false;
1116
1117 for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
1118 {
1119 if (netbus->ElementAtIndex(i))
1120 {
1121 int bitidx = i - wire->start_offset;
1122 net = netbus->ElementAtIndex(i);
1123 RTLIL::SigBit bit(wire, bitidx);
1124
1125 if (init_nets.count(net)) {
1126 if (init_nets.at(net) == '0')
1127 initval.bits.at(bitidx) = State::S0;
1128 if (init_nets.at(net) == '1')
1129 initval.bits.at(bitidx) = State::S1;
1130 initval_valid = true;
1131 init_nets.erase(net);
1132 }
1133
1134 if (net_map.count(net) == 0)
1135 net_map[net] = bit;
1136 else
1137 module->connect(bit, net_map_at(net));
1138 }
1139
1140 if (i == netbus->RightIndex())
1141 break;
1142 }
1143
1144 if (initval_valid)
1145 wire->attributes[ID::init] = initval;
1146 }
1147 else
1148 {
1149 if (verific_verbose)
1150 log(" skipping netbus %s.\n", netbus->Name());
1151 }
1152
1153 SigSpec anyconst_sig;
1154 SigSpec anyseq_sig;
1155 SigSpec allconst_sig;
1156 SigSpec allseq_sig;
1157
1158 for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
1159 net = netbus->ElementAtIndex(i);
1160 if (net != nullptr && anyconst_nets.count(net)) {
1161 anyconst_sig.append(net_map_at(net));
1162 anyconst_nets.erase(net);
1163 }
1164 if (net != nullptr && anyseq_nets.count(net)) {
1165 anyseq_sig.append(net_map_at(net));
1166 anyseq_nets.erase(net);
1167 }
1168 if (net != nullptr && allconst_nets.count(net)) {
1169 allconst_sig.append(net_map_at(net));
1170 allconst_nets.erase(net);
1171 }
1172 if (net != nullptr && allseq_nets.count(net)) {
1173 allseq_sig.append(net_map_at(net));
1174 allseq_nets.erase(net);
1175 }
1176 if (i == netbus->LeftIndex())
1177 break;
1178 }
1179
1180 if (GetSize(anyconst_sig))
1181 module->connect(anyconst_sig, module->Anyconst(new_verific_id(netbus), GetSize(anyconst_sig)));
1182
1183 if (GetSize(anyseq_sig))
1184 module->connect(anyseq_sig, module->Anyseq(new_verific_id(netbus), GetSize(anyseq_sig)));
1185
1186 if (GetSize(allconst_sig))
1187 module->connect(allconst_sig, module->Allconst(new_verific_id(netbus), GetSize(allconst_sig)));
1188
1189 if (GetSize(allseq_sig))
1190 module->connect(allseq_sig, module->Allseq(new_verific_id(netbus), GetSize(allseq_sig)));
1191 }
1192
1193 for (auto it : init_nets)
1194 {
1195 Const initval;
1196 SigBit bit = net_map_at(it.first);
1197 log_assert(bit.wire);
1198
1199 if (bit.wire->attributes.count(ID::init))
1200 initval = bit.wire->attributes.at(ID::init);
1201
1202 while (GetSize(initval) < GetSize(bit.wire))
1203 initval.bits.push_back(State::Sx);
1204
1205 if (it.second == '0')
1206 initval.bits.at(bit.offset) = State::S0;
1207 if (it.second == '1')
1208 initval.bits.at(bit.offset) = State::S1;
1209
1210 bit.wire->attributes[ID::init] = initval;
1211 }
1212
1213 for (auto net : anyconst_nets)
1214 module->connect(net_map_at(net), module->Anyconst(new_verific_id(net)));
1215
1216 for (auto net : anyseq_nets)
1217 module->connect(net_map_at(net), module->Anyseq(new_verific_id(net)));
1218
1219 pool<Instance*, hash_ptr_ops> sva_asserts;
1220 pool<Instance*, hash_ptr_ops> sva_assumes;
1221 pool<Instance*, hash_ptr_ops> sva_covers;
1222 pool<Instance*, hash_ptr_ops> sva_triggers;
1223
1224 pool<RTLIL::Cell*> past_ffs;
1225
1226 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1227 {
1228 RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : new_verific_id(inst));
1229
1230 if (verific_verbose)
1231 log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name));
1232
1233 if (mode_verific)
1234 goto import_verific_cells;
1235
1236 if (inst->Type() == PRIM_PWR) {
1237 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S1);
1238 continue;
1239 }
1240
1241 if (inst->Type() == PRIM_GND) {
1242 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::S0);
1243 continue;
1244 }
1245
1246 if (inst->Type() == PRIM_BUF) {
1247 auto outnet = inst->GetOutput();
1248 if (!any_all_nets.count(outnet))
1249 module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
1250 continue;
1251 }
1252
1253 if (inst->Type() == PRIM_X) {
1254 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sx);
1255 continue;
1256 }
1257
1258 if (inst->Type() == PRIM_Z) {
1259 module->connect(net_map_at(inst->GetOutput()), RTLIL::State::Sz);
1260 continue;
1261 }
1262
1263 if (inst->Type() == OPER_READ_PORT)
1264 {
1265 RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
1266 int numchunks = int(inst->OutputSize()) / memory->width;
1267 int chunksbits = ceil_log2(numchunks);
1268
1269 for (int i = 0; i < numchunks; i++)
1270 {
1271 RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
1272 RTLIL::SigSpec data = operatorOutput(inst).extract(i * memory->width, memory->width);
1273
1274 RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
1275 RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), ID($memrd));
1276 cell->parameters[ID::MEMID] = memory->name.str();
1277 cell->parameters[ID::CLK_ENABLE] = false;
1278 cell->parameters[ID::CLK_POLARITY] = true;
1279 cell->parameters[ID::TRANSPARENT] = false;
1280 cell->parameters[ID::ABITS] = GetSize(addr);
1281 cell->parameters[ID::WIDTH] = GetSize(data);
1282 cell->setPort(ID::CLK, RTLIL::State::Sx);
1283 cell->setPort(ID::EN, RTLIL::State::Sx);
1284 cell->setPort(ID::ADDR, addr);
1285 cell->setPort(ID::DATA, data);
1286 }
1287 continue;
1288 }
1289
1290 if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
1291 {
1292 RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
1293 int numchunks = int(inst->Input2Size()) / memory->width;
1294 int chunksbits = ceil_log2(numchunks);
1295
1296 for (int i = 0; i < numchunks; i++)
1297 {
1298 RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
1299 RTLIL::SigSpec data = operatorInput2(inst).extract(i * memory->width, memory->width);
1300
1301 RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
1302 RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), ID($memwr));
1303 cell->parameters[ID::MEMID] = memory->name.str();
1304 cell->parameters[ID::CLK_ENABLE] = false;
1305 cell->parameters[ID::CLK_POLARITY] = true;
1306 cell->parameters[ID::PRIORITY] = 0;
1307 cell->parameters[ID::ABITS] = GetSize(addr);
1308 cell->parameters[ID::WIDTH] = GetSize(data);
1309 cell->setPort(ID::EN, RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
1310 cell->setPort(ID::CLK, RTLIL::State::S0);
1311 cell->setPort(ID::ADDR, addr);
1312 cell->setPort(ID::DATA, data);
1313
1314 if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
1315 cell->parameters[ID::CLK_ENABLE] = true;
1316 cell->setPort(ID::CLK, net_map_at(inst->GetClock()));
1317 }
1318 }
1319 continue;
1320 }
1321
1322 if (!mode_gates) {
1323 if (import_netlist_instance_cells(inst, inst_name))
1324 continue;
1325 if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
1326 log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
1327 } else {
1328 if (import_netlist_instance_gates(inst, inst_name))
1329 continue;
1330 }
1331
1332 if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
1333 sva_asserts.insert(inst);
1334
1335 if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_RESTRICT)
1336 sva_assumes.insert(inst);
1337
1338 if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
1339 sva_covers.insert(inst);
1340
1341 if (inst->Type() == PRIM_SVA_TRIGGERED)
1342 sva_triggers.insert(inst);
1343
1344 if (inst->Type() == OPER_SVA_STABLE)
1345 {
1346 VerificClocking clocking(this, inst->GetInput2Bit(0));
1347 log_assert(clocking.disable_sig == State::S0);
1348 log_assert(clocking.body_net == nullptr);
1349
1350 log_assert(inst->Input1Size() == inst->OutputSize());
1351
1352 SigSpec sig_d, sig_q, sig_o;
1353 sig_q = module->addWire(new_verific_id(inst), inst->Input1Size());
1354
1355 for (int i = int(inst->Input1Size())-1; i >= 0; i--){
1356 sig_d.append(net_map_at(inst->GetInput1Bit(i)));
1357 sig_o.append(net_map_at(inst->GetOutputBit(i)));
1358 }
1359
1360 if (verific_verbose) {
1361 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1362 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1363 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1364 log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
1365 }
1366
1367 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1368 module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
1369
1370 if (!mode_keep)
1371 continue;
1372 }
1373
1374 if (inst->Type() == PRIM_SVA_STABLE)
1375 {
1376 VerificClocking clocking(this, inst->GetInput2());
1377 log_assert(clocking.disable_sig == State::S0);
1378 log_assert(clocking.body_net == nullptr);
1379
1380 SigSpec sig_d = net_map_at(inst->GetInput1());
1381 SigSpec sig_o = net_map_at(inst->GetOutput());
1382 SigSpec sig_q = module->addWire(new_verific_id(inst));
1383
1384 if (verific_verbose) {
1385 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1386 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1387 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1388 log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
1389 }
1390
1391 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1392 module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
1393
1394 if (!mode_keep)
1395 continue;
1396 }
1397
1398 if (inst->Type() == PRIM_SVA_PAST)
1399 {
1400 VerificClocking clocking(this, inst->GetInput2());
1401 log_assert(clocking.disable_sig == State::S0);
1402 log_assert(clocking.body_net == nullptr);
1403
1404 SigBit sig_d = net_map_at(inst->GetInput1());
1405 SigBit sig_q = net_map_at(inst->GetOutput());
1406
1407 if (verific_verbose)
1408 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1409 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1410
1411 past_ffs.insert(clocking.addDff(new_verific_id(inst), sig_d, sig_q));
1412
1413 if (!mode_keep)
1414 continue;
1415 }
1416
1417 if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL))
1418 {
1419 VerificClocking clocking(this, inst->GetInput2());
1420 log_assert(clocking.disable_sig == State::S0);
1421 log_assert(clocking.body_net == nullptr);
1422
1423 SigBit sig_d = net_map_at(inst->GetInput1());
1424 SigBit sig_o = net_map_at(inst->GetOutput());
1425 SigBit sig_q = module->addWire(new_verific_id(inst));
1426
1427 if (verific_verbose)
1428 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1429 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1430
1431 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1432 module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
1433
1434 if (!mode_keep)
1435 continue;
1436 }
1437
1438 if (!mode_keep && verific_sva_prims.count(inst->Type())) {
1439 if (verific_verbose)
1440 log(" skipping SVA cell in non k-mode\n");
1441 continue;
1442 }
1443
1444 if (inst->Type() == PRIM_HDL_ASSERTION)
1445 {
1446 SigBit cond = net_map_at(inst->GetInput());
1447
1448 if (verific_verbose)
1449 log(" assert condition %s.\n", log_signal(cond));
1450
1451 const char *assume_attr = nullptr; // inst->GetAttValue("assume");
1452
1453 Cell *cell = nullptr;
1454 if (assume_attr != nullptr && !strcmp(assume_attr, "1"))
1455 cell = module->addAssume(new_verific_id(inst), cond, State::S1);
1456 else
1457 cell = module->addAssert(new_verific_id(inst), cond, State::S1);
1458
1459 import_attributes(cell->attributes, inst);
1460 continue;
1461 }
1462
1463 if (inst->IsPrimitive())
1464 {
1465 if (!mode_keep)
1466 log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
1467
1468 if (!verific_sva_prims.count(inst->Type()))
1469 log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
1470 }
1471
1472 import_verific_cells:
1473 nl_todo.insert(inst->View());
1474
1475 std::string inst_type = inst->View()->Owner()->Name();
1476
1477 if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) {
1478 inst_type = "$verific$" + inst_type;
1479 } else {
1480 if (*inst->View()->Name()) {
1481 inst_type += "(";
1482 inst_type += inst->View()->Name();
1483 inst_type += ")";
1484 }
1485 inst_type = "\\" + inst_type;
1486 }
1487
1488 RTLIL::Cell *cell = module->addCell(inst_name, inst_type);
1489
1490 if (inst->IsPrimitive() && mode_keep)
1491 cell->attributes[ID::keep] = 1;
1492
1493 dict<IdString, vector<SigBit>> cell_port_conns;
1494
1495 if (verific_verbose)
1496 log(" ports in verific db:\n");
1497
1498 FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
1499 if (verific_verbose)
1500 log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
1501 const char *port_name = pr->GetPort()->Name();
1502 int port_offset = 0;
1503 if (pr->GetPort()->Bus()) {
1504 port_name = pr->GetPort()->Bus()->Name();
1505 port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
1506 min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
1507 }
1508 IdString port_name_id = RTLIL::escape_id(port_name);
1509 auto &sigvec = cell_port_conns[port_name_id];
1510 if (GetSize(sigvec) <= port_offset) {
1511 SigSpec zwires = module->addWire(new_verific_id(inst), port_offset+1-GetSize(sigvec));
1512 for (auto bit : zwires)
1513 sigvec.push_back(bit);
1514 }
1515 sigvec[port_offset] = net_map_at(pr->GetNet());
1516 }
1517
1518 if (verific_verbose)
1519 log(" ports in yosys db:\n");
1520
1521 for (auto &it : cell_port_conns) {
1522 if (verific_verbose)
1523 log(" .%s(%s)\n", log_id(it.first), log_signal(it.second));
1524 cell->setPort(it.first, it.second);
1525 }
1526 }
1527
1528 if (!mode_nosva)
1529 {
1530 for (auto inst : sva_asserts) {
1531 if (mode_autocover)
1532 verific_import_sva_cover(this, inst);
1533 verific_import_sva_assert(this, inst);
1534 }
1535
1536 for (auto inst : sva_assumes)
1537 verific_import_sva_assume(this, inst);
1538
1539 for (auto inst : sva_covers)
1540 verific_import_sva_cover(this, inst);
1541
1542 for (auto inst : sva_triggers)
1543 verific_import_sva_trigger(this, inst);
1544
1545 merge_past_ffs(past_ffs);
1546 }
1547
1548 if (!mode_fullinit)
1549 {
1550 pool<SigBit> non_ff_bits;
1551 CellTypes ff_types;
1552
1553 ff_types.setup_internals_ff();
1554 ff_types.setup_stdcells_mem();
1555
1556 for (auto cell : module->cells())
1557 {
1558 if (ff_types.cell_known(cell->type))
1559 continue;
1560
1561 for (auto conn : cell->connections())
1562 {
1563 if (!cell->output(conn.first))
1564 continue;
1565
1566 for (auto bit : conn.second)
1567 if (bit.wire != nullptr)
1568 non_ff_bits.insert(bit);
1569 }
1570 }
1571
1572 for (auto wire : module->wires())
1573 {
1574 if (!wire->attributes.count(ID::init))
1575 continue;
1576
1577 Const &initval = wire->attributes.at(ID::init);
1578 for (int i = 0; i < GetSize(initval); i++)
1579 {
1580 if (initval[i] != State::S0 && initval[i] != State::S1)
1581 continue;
1582
1583 if (non_ff_bits.count(SigBit(wire, i)))
1584 initval[i] = State::Sx;
1585 }
1586
1587 if (initval.is_fully_undef())
1588 wire->attributes.erase(ID::init);
1589 }
1590 }
1591 }
1592
1593 // ==================================================================
1594
1595 VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
1596 {
1597 module = importer->module;
1598
1599 log_assert(importer != nullptr);
1600 log_assert(net != nullptr);
1601
1602 Instance *inst = net->Driver();
1603
1604 if (inst != nullptr && inst->Type() == PRIM_SVA_AT)
1605 {
1606 net = inst->GetInput1();
1607 body_net = inst->GetInput2();
1608
1609 inst = net->Driver();
1610
1611 Instance *body_inst = body_net->Driver();
1612 if (body_inst != nullptr && body_inst->Type() == PRIM_SVA_DISABLE_IFF) {
1613 disable_net = body_inst->GetInput1();
1614 disable_sig = importer->net_map_at(disable_net);
1615 body_net = body_inst->GetInput2();
1616 }
1617 }
1618 else
1619 {
1620 if (sva_at_only)
1621 return;
1622 }
1623
1624 // Use while() instead of if() to work around VIPER #13453
1625 while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
1626 {
1627 net = inst->GetInput();
1628 inst = net->Driver();;
1629 }
1630
1631 if (inst != nullptr && inst->Type() == PRIM_INV)
1632 {
1633 net = inst->GetInput();
1634 inst = net->Driver();;
1635 posedge = false;
1636 }
1637
1638 // Detect clock-enable circuit
1639 do {
1640 if (inst == nullptr || inst->Type() != PRIM_AND)
1641 break;
1642
1643 Net *net_dlatch = inst->GetInput1();
1644 Instance *inst_dlatch = net_dlatch->Driver();
1645
1646 if (inst_dlatch == nullptr || inst_dlatch->Type() != PRIM_DLATCHRS)
1647 break;
1648
1649 if (!inst_dlatch->GetSet()->IsGnd() || !inst_dlatch->GetReset()->IsGnd())
1650 break;
1651
1652 Net *net_enable = inst_dlatch->GetInput();
1653 Net *net_not_clock = inst_dlatch->GetControl();
1654
1655 if (net_enable == nullptr || net_not_clock == nullptr)
1656 break;
1657
1658 Instance *inst_not_clock = net_not_clock->Driver();
1659
1660 if (inst_not_clock == nullptr || inst_not_clock->Type() != PRIM_INV)
1661 break;
1662
1663 Net *net_clock1 = inst_not_clock->GetInput();
1664 Net *net_clock2 = inst->GetInput2();
1665
1666 if (net_clock1 == nullptr || net_clock1 != net_clock2)
1667 break;
1668
1669 enable_net = net_enable;
1670 enable_sig = importer->net_map_at(enable_net);
1671
1672 net = net_clock1;
1673 inst = net->Driver();;
1674 } while (0);
1675
1676 // Detect condition expression
1677 do {
1678 if (body_net == nullptr)
1679 break;
1680
1681 Instance *inst_mux = body_net->Driver();
1682
1683 if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX)
1684 break;
1685
1686 if (!inst_mux->GetInput1()->IsPwr())
1687 break;
1688
1689 Net *sva_net = inst_mux->GetInput2();
1690 if (!verific_is_sva_net(importer, sva_net))
1691 break;
1692
1693 body_net = sva_net;
1694 cond_net = inst_mux->GetControl();
1695 } while (0);
1696
1697 clock_net = net;
1698 clock_sig = importer->net_map_at(clock_net);
1699
1700 const char *gclk_attr = clock_net->GetAttValue("gclk");
1701 if (gclk_attr != nullptr && (!strcmp(gclk_attr, "1") || !strcmp(gclk_attr, "'1'")))
1702 gclk = true;
1703 }
1704
1705 Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value)
1706 {
1707 log_assert(GetSize(sig_d) == GetSize(sig_q));
1708
1709 if (GetSize(init_value) != 0) {
1710 log_assert(GetSize(sig_q) == GetSize(init_value));
1711 if (sig_q.is_wire()) {
1712 sig_q.as_wire()->attributes[ID::init] = init_value;
1713 } else {
1714 Wire *w = module->addWire(NEW_ID, GetSize(sig_q));
1715 w->attributes[ID::init] = init_value;
1716 module->connect(sig_q, w);
1717 sig_q = w;
1718 }
1719 }
1720
1721 if (enable_sig != State::S1)
1722 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1723
1724 if (disable_sig != State::S0) {
1725 log_assert(gclk == false);
1726 log_assert(GetSize(sig_q) == GetSize(init_value));
1727 return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
1728 }
1729
1730 if (gclk)
1731 return module->addFf(name, sig_d, sig_q);
1732
1733 return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
1734 }
1735
1736 Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value)
1737 {
1738 log_assert(gclk == false);
1739 log_assert(disable_sig == State::S0);
1740
1741 if (enable_sig != State::S1)
1742 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1743
1744 return module->addAdff(name, clock_sig, sig_arst, sig_d, sig_q, arst_value, posedge);
1745 }
1746
1747 Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q)
1748 {
1749 log_assert(gclk == false);
1750 log_assert(disable_sig == State::S0);
1751
1752 if (enable_sig != State::S1)
1753 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1754
1755 return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
1756 }
1757
1758 // ==================================================================
1759
1760 struct VerificExtNets
1761 {
1762 int portname_cnt = 0;
1763
1764 // a map from Net to the same Net one level up in the design hierarchy
1765 std::map<Net*, Net*> net_level_up_drive_up;
1766 std::map<Net*, Net*> net_level_up_drive_down;
1767
1768 Net *route_up(Net *net, bool drive_up, Net *final_net = nullptr)
1769 {
1770 auto &net_level_up = drive_up ? net_level_up_drive_up : net_level_up_drive_down;
1771
1772 if (net_level_up.count(net) == 0)
1773 {
1774 Netlist *nl = net->Owner();
1775
1776 // Simply return if Netlist is not unique
1777 log_assert(nl->NumOfRefs() == 1);
1778
1779 Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
1780 Netlist *up_nl = up_inst->Owner();
1781
1782 // create new Port
1783 string name = stringf("___extnets_%d", portname_cnt++);
1784 Port *new_port = new Port(name.c_str(), drive_up ? DIR_OUT : DIR_IN);
1785 nl->Add(new_port);
1786 net->Connect(new_port);
1787
1788 // create new Net in up Netlist
1789 Net *new_net = final_net;
1790 if (new_net == nullptr || new_net->Owner() != up_nl) {
1791 new_net = new Net(name.c_str());
1792 up_nl->Add(new_net);
1793 }
1794 up_inst->Connect(new_port, new_net);
1795
1796 net_level_up[net] = new_net;
1797 }
1798
1799 return net_level_up.at(net);
1800 }
1801
1802 Net *route_up(Net *net, bool drive_up, Netlist *dest, Net *final_net = nullptr)
1803 {
1804 while (net->Owner() != dest)
1805 net = route_up(net, drive_up, final_net);
1806 if (final_net != nullptr)
1807 log_assert(net == final_net);
1808 return net;
1809 }
1810
1811 Netlist *find_common_ancestor(Netlist *A, Netlist *B)
1812 {
1813 std::set<Netlist*> ancestors_of_A;
1814
1815 Netlist *cursor = A;
1816 while (1) {
1817 ancestors_of_A.insert(cursor);
1818 if (cursor->NumOfRefs() != 1)
1819 break;
1820 cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
1821 }
1822
1823 cursor = B;
1824 while (1) {
1825 if (ancestors_of_A.count(cursor))
1826 return cursor;
1827 if (cursor->NumOfRefs() != 1)
1828 break;
1829 cursor = ((Instance*)cursor->GetReferences()->GetLast())->Owner();
1830 }
1831
1832 log_error("No common ancestor found between %s and %s.\n", get_full_netlist_name(A).c_str(), get_full_netlist_name(B).c_str());
1833 }
1834
1835 void run(Netlist *nl)
1836 {
1837 MapIter mi, mi2;
1838 Instance *inst;
1839 PortRef *pr;
1840
1841 vector<tuple<Instance*, Port*, Net*>> todo_connect;
1842
1843 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1844 run(inst->View());
1845
1846 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1847 FOREACH_PORTREF_OF_INST(inst, mi2, pr)
1848 {
1849 Port *port = pr->GetPort();
1850 Net *net = pr->GetNet();
1851
1852 if (!net->IsExternalTo(nl))
1853 continue;
1854
1855 if (verific_verbose)
1856 log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
1857
1858 Netlist *ext_nl = net->Owner();
1859
1860 if (verific_verbose)
1861 log(" external net owner: %s\n", get_full_netlist_name(ext_nl).c_str());
1862
1863 Netlist *ca_nl = find_common_ancestor(nl, ext_nl);
1864
1865 if (verific_verbose)
1866 log(" common ancestor: %s\n", get_full_netlist_name(ca_nl).c_str());
1867
1868 Net *ca_net = route_up(net, !port->IsOutput(), ca_nl);
1869 Net *new_net = ca_net;
1870
1871 if (ca_nl != nl)
1872 {
1873 if (verific_verbose)
1874 log(" net in common ancestor: %s\n", ca_net->Name());
1875
1876 string name = stringf("___extnets_%d", portname_cnt++);
1877 new_net = new Net(name.c_str());
1878 nl->Add(new_net);
1879
1880 Net *n YS_ATTRIBUTE(unused) = route_up(new_net, port->IsOutput(), ca_nl, ca_net);
1881 log_assert(n == ca_net);
1882 }
1883
1884 if (verific_verbose)
1885 log(" new local net: %s\n", new_net->Name());
1886
1887 log_assert(!new_net->IsExternalTo(nl));
1888 todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, new_net));
1889 }
1890
1891 for (auto it : todo_connect) {
1892 get<0>(it)->Disconnect(get<1>(it));
1893 get<0>(it)->Connect(get<1>(it), get<2>(it));
1894 }
1895 }
1896 };
1897
1898 void verific_import(Design *design, const std::map<std::string,std::string> &parameters, std::string top)
1899 {
1900 verific_sva_fsm_limit = 16;
1901
1902 std::set<Netlist*> nl_todo, nl_done;
1903
1904 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
1905 VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
1906 Array *netlists = NULL;
1907 Array veri_libs, vhdl_libs;
1908 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
1909 if (veri_lib) veri_libs.InsertLast(veri_lib);
1910
1911 Map verific_params(STRING_HASH);
1912 for (const auto &i : parameters)
1913 verific_params.Insert(i.first.c_str(), i.second.c_str());
1914
1915 if (top.empty()) {
1916 netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &verific_params);
1917 }
1918 else {
1919 Array veri_modules, vhdl_units;
1920
1921 if (veri_lib) {
1922 VeriModule *veri_module = veri_lib->GetModule(top.c_str(), 1);
1923 if (veri_module) {
1924 veri_modules.InsertLast(veri_module);
1925 }
1926
1927 // Also elaborate all root modules since they may contain bind statements
1928 MapIter mi;
1929 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
1930 if (!veri_module->IsRootModule()) continue;
1931 veri_modules.InsertLast(veri_module);
1932 }
1933 }
1934
1935 if (vhdl_lib) {
1936 VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(top.c_str());
1937 if (vhdl_unit)
1938 vhdl_units.InsertLast(vhdl_unit);
1939 }
1940
1941 netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &verific_params);
1942 }
1943
1944 Netlist *nl;
1945 int i;
1946
1947 FOREACH_ARRAY_ITEM(netlists, i, nl) {
1948 if (top.empty() && nl->CellBaseName() != top)
1949 continue;
1950 nl->AddAtt(new Att(" \\top", NULL));
1951 nl_todo.insert(nl);
1952 }
1953
1954 delete netlists;
1955
1956 if (!verific_error_msg.empty())
1957 log_error("%s\n", verific_error_msg.c_str());
1958
1959 for (auto nl : nl_todo)
1960 nl->ChangePortBusStructures(1 /* hierarchical */);
1961
1962 VerificExtNets worker;
1963 for (auto nl : nl_todo)
1964 worker.run(nl);
1965
1966 while (!nl_todo.empty()) {
1967 Netlist *nl = *nl_todo.begin();
1968 if (nl_done.count(nl) == 0) {
1969 VerificImporter importer(false, false, false, false, false, false, false);
1970 importer.import_netlist(design, nl, nl_todo, nl->Owner()->Name() == top);
1971 }
1972 nl_todo.erase(nl);
1973 nl_done.insert(nl);
1974 }
1975
1976 veri_file::Reset();
1977 vhdl_file::Reset();
1978 Libset::Reset();
1979 verific_incdirs.clear();
1980 verific_libdirs.clear();
1981 verific_import_pending = false;
1982
1983 if (!verific_error_msg.empty())
1984 log_error("%s\n", verific_error_msg.c_str());
1985 }
1986
1987 YOSYS_NAMESPACE_END
1988 #endif /* YOSYS_ENABLE_VERIFIC */
1989
1990 PRIVATE_NAMESPACE_BEGIN
1991
1992 #ifdef YOSYS_ENABLE_VERIFIC
1993 bool check_noverific_env()
1994 {
1995 const char *e = getenv("YOSYS_NOVERIFIC");
1996 if (e == nullptr)
1997 return false;
1998 if (atoi(e) == 0)
1999 return false;
2000 return true;
2001 }
2002 #endif
2003
2004 struct VerificPass : public Pass {
2005 VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
2006 void help() YS_OVERRIDE
2007 {
2008 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2009 log("\n");
2010 log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
2011 log("\n");
2012 log("Load the specified Verilog/SystemVerilog files into Verific.\n");
2013 log("\n");
2014 log("All files specified in one call to this command are one compilation unit.\n");
2015 log("Files passed to different calls to this command are treated as belonging to\n");
2016 log("different compilation units.\n");
2017 log("\n");
2018 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2019 log("the language version (and before file names) to set additional verilog defines.\n");
2020 log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
2021 log("\n");
2022 log("\n");
2023 log(" verific -formal <verilog-file>..\n");
2024 log("\n");
2025 log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
2026 log("\n");
2027 log("\n");
2028 log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2029 log("\n");
2030 log("Load the specified VHDL files into Verific.\n");
2031 log("\n");
2032 log("\n");
2033 log(" verific [-work <libname>] {-sv|-vhdl|...} <hdl-file>\n");
2034 log("\n");
2035 log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
2036 log("(default library when -work is not present: \"work\")\n");
2037 log("\n");
2038 log("\n");
2039 log(" verific [-L <libname>] {-sv|-vhdl|...} <hdl-file>\n");
2040 log("\n");
2041 log("Look up external definitions in the specified library.\n");
2042 log("(-L may be used more than once)\n");
2043 log("\n");
2044 log("\n");
2045 log(" verific -vlog-incdir <directory>..\n");
2046 log("\n");
2047 log("Add Verilog include directories.\n");
2048 log("\n");
2049 log("\n");
2050 log(" verific -vlog-libdir <directory>..\n");
2051 log("\n");
2052 log("Add Verilog library directories. Verific will search in this directories to\n");
2053 log("find undefined modules.\n");
2054 log("\n");
2055 log("\n");
2056 log(" verific -vlog-define <macro>[=<value>]..\n");
2057 log("\n");
2058 log("Add Verilog defines.\n");
2059 log("\n");
2060 log("\n");
2061 log(" verific -vlog-undef <macro>..\n");
2062 log("\n");
2063 log("Remove Verilog defines previously set with -vlog-define.\n");
2064 log("\n");
2065 log("\n");
2066 log(" verific -set-error <msg_id>..\n");
2067 log(" verific -set-warning <msg_id>..\n");
2068 log(" verific -set-info <msg_id>..\n");
2069 log(" verific -set-ignore <msg_id>..\n");
2070 log("\n");
2071 log("Set message severity. <msg_id> is the string in square brackets when a message\n");
2072 log("is printed, such as VERI-1209.\n");
2073 log("\n");
2074 log("\n");
2075 log(" verific -import [options] <top-module>..\n");
2076 log("\n");
2077 log("Elaborate the design for the specified top modules, import to Yosys and\n");
2078 log("reset the internal state of Verific.\n");
2079 log("\n");
2080 log("Import options:\n");
2081 log("\n");
2082 log(" -all\n");
2083 log(" Elaborate all modules, not just the hierarchy below the given top\n");
2084 log(" modules. With this option the list of modules to import is optional.\n");
2085 log("\n");
2086 log(" -gates\n");
2087 log(" Create a gate-level netlist.\n");
2088 log("\n");
2089 log(" -flatten\n");
2090 log(" Flatten the design in Verific before importing.\n");
2091 log("\n");
2092 log(" -extnets\n");
2093 log(" Resolve references to external nets by adding module ports as needed.\n");
2094 log("\n");
2095 log(" -autocover\n");
2096 log(" Generate automatic cover statements for all asserts\n");
2097 log("\n");
2098 log(" -fullinit\n");
2099 log(" Keep all register initializations, even those for non-FF registers.\n");
2100 log("\n");
2101 log(" -chparam name value \n");
2102 log(" Elaborate the specified top modules (all modules when -all given) using\n");
2103 log(" this parameter value. Modules on which this parameter does not exist will\n");
2104 log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n");
2105 log(" can be specified multiple times to override multiple parameters.\n");
2106 log(" String values must be passed in double quotes (\").\n");
2107 log("\n");
2108 log(" -v, -vv\n");
2109 log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
2110 log("\n");
2111 log("The following additional import options are useful for debugging the Verific\n");
2112 log("bindings (for Yosys and/or Verific developers):\n");
2113 log("\n");
2114 log(" -k\n");
2115 log(" Keep going after an unsupported verific primitive is found. The\n");
2116 log(" unsupported primitive is added as blockbox module to the design.\n");
2117 log(" This will also add all SVA related cells to the design parallel to\n");
2118 log(" the checker logic inferred by it.\n");
2119 log("\n");
2120 log(" -V\n");
2121 log(" Import Verific netlist as-is without translating to Yosys cell types. \n");
2122 log("\n");
2123 log(" -nosva\n");
2124 log(" Ignore SVA properties, do not infer checker logic.\n");
2125 log("\n");
2126 log(" -L <int>\n");
2127 log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
2128 log("\n");
2129 log(" -n\n");
2130 log(" Keep all Verific names on instances and nets. By default only\n");
2131 log(" user-declared names are preserved.\n");
2132 log("\n");
2133 log(" -d <dump_file>\n");
2134 log(" Dump the Verific netlist as a verilog file.\n");
2135 log("\n");
2136 log("\n");
2137 log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n");
2138 log("https://www.symbioticeda.com/seda-suite\n");
2139 log("\n");
2140 log("Contact office@symbioticeda.com for free evaluation\n");
2141 log("binaries of Symbiotic EDA Suite.\n");
2142 log("\n");
2143 }
2144 #ifdef YOSYS_ENABLE_VERIFIC
2145 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
2146 {
2147 static bool set_verific_global_flags = true;
2148
2149 if (check_noverific_env())
2150 log_cmd_error("This version of Yosys is built without Verific support.\n"
2151 "\n"
2152 "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
2153 "https://www.symbioticeda.com/seda-suite\n"
2154 "\n"
2155 "Contact office@symbioticeda.com for free evaluation\n"
2156 "binaries of Symbiotic EDA Suite.\n");
2157
2158 log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
2159
2160 if (set_verific_global_flags)
2161 {
2162 Message::SetConsoleOutput(0);
2163 Message::RegisterCallBackMsg(msg_func);
2164
2165 RuntimeFlags::SetVar("db_preserve_user_nets", 1);
2166 RuntimeFlags::SetVar("db_allow_external_nets", 1);
2167 RuntimeFlags::SetVar("db_infer_wide_operators", 1);
2168
2169 RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
2170 RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
2171
2172 RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
2173 RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
2174
2175 RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
2176 RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
2177
2178 // Workaround for VIPER #13851
2179 RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
2180
2181 // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
2182 Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
2183
2184 // https://github.com/YosysHQ/yosys/issues/1055
2185 RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
2186
2187 #ifndef DB_PRESERVE_INITIAL_VALUE
2188 # warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
2189 #endif
2190
2191 set_verific_global_flags = false;
2192 }
2193
2194 verific_verbose = 0;
2195 verific_sva_fsm_limit = 16;
2196
2197 const char *release_str = Message::ReleaseString();
2198 time_t release_time = Message::ReleaseDate();
2199 char *release_tmstr = ctime(&release_time);
2200
2201 if (release_str == nullptr)
2202 release_str = "(no release string)";
2203
2204 for (char *p = release_tmstr; *p; p++)
2205 if (*p == '\n') *p = 0;
2206
2207 log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);
2208
2209 int argidx = 1;
2210 std::string work = "work";
2211
2212 if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
2213 args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
2214 {
2215 msg_type_t new_type;
2216
2217 if (args[argidx] == "-set-error")
2218 new_type = VERIFIC_ERROR;
2219 else if (args[argidx] == "-set-warning")
2220 new_type = VERIFIC_WARNING;
2221 else if (args[argidx] == "-set-info")
2222 new_type = VERIFIC_INFO;
2223 else if (args[argidx] == "-set-ignore")
2224 new_type = VERIFIC_IGNORE;
2225 else
2226 log_abort();
2227
2228 for (argidx++; argidx < GetSize(args); argidx++)
2229 Message::SetMessageType(args[argidx].c_str(), new_type);
2230
2231 goto check_error;
2232 }
2233
2234 if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
2235 for (argidx++; argidx < GetSize(args); argidx++)
2236 verific_incdirs.push_back(args[argidx]);
2237 goto check_error;
2238 }
2239
2240 if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
2241 for (argidx++; argidx < GetSize(args); argidx++)
2242 verific_libdirs.push_back(args[argidx]);
2243 goto check_error;
2244 }
2245
2246 if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
2247 for (argidx++; argidx < GetSize(args); argidx++) {
2248 string name = args[argidx];
2249 size_t equal = name.find('=');
2250 if (equal != std::string::npos) {
2251 string value = name.substr(equal+1);
2252 name = name.substr(0, equal);
2253 veri_file::DefineCmdLineMacro(name.c_str(), value.c_str());
2254 } else {
2255 veri_file::DefineCmdLineMacro(name.c_str());
2256 }
2257 }
2258 goto check_error;
2259 }
2260
2261 if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") {
2262 for (argidx++; argidx < GetSize(args); argidx++) {
2263 string name = args[argidx];
2264 veri_file::UndefineMacro(name.c_str());
2265 }
2266 goto check_error;
2267 }
2268
2269 veri_file::RemoveAllLOptions();
2270 for (; argidx < GetSize(args); argidx++)
2271 {
2272 if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
2273 work = args[++argidx];
2274 continue;
2275 }
2276 if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
2277 veri_file::AddLOption(args[++argidx].c_str());
2278 continue;
2279 }
2280 break;
2281 }
2282
2283 if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
2284 args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
2285 {
2286 Array file_names;
2287 unsigned verilog_mode;
2288
2289 if (args[argidx] == "-vlog95")
2290 verilog_mode = veri_file::VERILOG_95;
2291 else if (args[argidx] == "-vlog2k")
2292 verilog_mode = veri_file::VERILOG_2K;
2293 else if (args[argidx] == "-sv2005")
2294 verilog_mode = veri_file::SYSTEM_VERILOG_2005;
2295 else if (args[argidx] == "-sv2009")
2296 verilog_mode = veri_file::SYSTEM_VERILOG_2009;
2297 else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")
2298 verilog_mode = veri_file::SYSTEM_VERILOG;
2299 else
2300 log_abort();
2301
2302 veri_file::DefineMacro("VERIFIC");
2303 veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
2304
2305 for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].compare(0, 2, "-D") == 0; argidx++) {
2306 std::string name = args[argidx].substr(2);
2307 if (args[argidx] == "-D") {
2308 if (++argidx >= GetSize(args))
2309 break;
2310 name = args[argidx];
2311 }
2312 size_t equal = name.find('=');
2313 if (equal != std::string::npos) {
2314 string value = name.substr(equal+1);
2315 name = name.substr(0, equal);
2316 veri_file::DefineMacro(name.c_str(), value.c_str());
2317 } else {
2318 veri_file::DefineMacro(name.c_str());
2319 }
2320 }
2321
2322 for (auto &dir : verific_incdirs)
2323 veri_file::AddIncludeDir(dir.c_str());
2324 for (auto &dir : verific_libdirs)
2325 veri_file::AddYDir(dir.c_str());
2326
2327 while (argidx < GetSize(args))
2328 file_names.Insert(args[argidx++].c_str());
2329
2330 if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU))
2331 log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
2332
2333 verific_import_pending = true;
2334 goto check_error;
2335 }
2336
2337 if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
2338 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
2339 for (argidx++; argidx < GetSize(args); argidx++)
2340 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87))
2341 log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
2342 verific_import_pending = true;
2343 goto check_error;
2344 }
2345
2346 if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
2347 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2348 for (argidx++; argidx < GetSize(args); argidx++)
2349 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93))
2350 log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
2351 verific_import_pending = true;
2352 goto check_error;
2353 }
2354
2355 if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
2356 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2357 for (argidx++; argidx < GetSize(args); argidx++)
2358 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K))
2359 log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
2360 verific_import_pending = true;
2361 goto check_error;
2362 }
2363
2364 if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
2365 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
2366 for (argidx++; argidx < GetSize(args); argidx++)
2367 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008))
2368 log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
2369 verific_import_pending = true;
2370 goto check_error;
2371 }
2372
2373 if (GetSize(args) > argidx && args[argidx] == "-import")
2374 {
2375 std::set<Netlist*> nl_todo, nl_done;
2376 bool mode_all = false, mode_gates = false, mode_keep = false;
2377 bool mode_nosva = false, mode_names = false, mode_verific = false;
2378 bool mode_autocover = false, mode_fullinit = false;
2379 bool flatten = false, extnets = false;
2380 string dumpfile;
2381 Map parameters(STRING_HASH);
2382
2383 for (argidx++; argidx < GetSize(args); argidx++) {
2384 if (args[argidx] == "-all") {
2385 mode_all = true;
2386 continue;
2387 }
2388 if (args[argidx] == "-gates") {
2389 mode_gates = true;
2390 continue;
2391 }
2392 if (args[argidx] == "-flatten") {
2393 flatten = true;
2394 continue;
2395 }
2396 if (args[argidx] == "-extnets") {
2397 extnets = true;
2398 continue;
2399 }
2400 if (args[argidx] == "-k") {
2401 mode_keep = true;
2402 continue;
2403 }
2404 if (args[argidx] == "-nosva") {
2405 mode_nosva = true;
2406 continue;
2407 }
2408 if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
2409 verific_sva_fsm_limit = atoi(args[++argidx].c_str());
2410 continue;
2411 }
2412 if (args[argidx] == "-n") {
2413 mode_names = true;
2414 continue;
2415 }
2416 if (args[argidx] == "-autocover") {
2417 mode_autocover = true;
2418 continue;
2419 }
2420 if (args[argidx] == "-fullinit") {
2421 mode_fullinit = true;
2422 continue;
2423 }
2424 if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
2425 const std::string &key = args[++argidx];
2426 const std::string &value = args[++argidx];
2427 unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
2428 1 /* force_overwrite */);
2429 if (!new_insertion)
2430 log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
2431 continue;
2432 }
2433 if (args[argidx] == "-V") {
2434 mode_verific = true;
2435 continue;
2436 }
2437 if (args[argidx] == "-v") {
2438 verific_verbose = 1;
2439 continue;
2440 }
2441 if (args[argidx] == "-vv") {
2442 verific_verbose = 2;
2443 continue;
2444 }
2445 if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {
2446 dumpfile = args[++argidx];
2447 continue;
2448 }
2449 break;
2450 }
2451
2452 if (argidx > GetSize(args) && args[argidx].compare(0, 1, "-") == 0)
2453 cmd_error(args, argidx, "unknown option");
2454
2455 std::set<std::string> top_mod_names;
2456
2457 if (mode_all)
2458 {
2459 log("Running hier_tree::ElaborateAll().\n");
2460
2461 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2462 VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
2463
2464 Array veri_libs, vhdl_libs;
2465 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
2466 if (veri_lib) veri_libs.InsertLast(veri_lib);
2467
2468 Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
2469 Netlist *nl;
2470 int i;
2471
2472 FOREACH_ARRAY_ITEM(netlists, i, nl)
2473 nl_todo.insert(nl);
2474 delete netlists;
2475 }
2476 else
2477 {
2478 if (argidx == GetSize(args))
2479 cmd_error(args, argidx, "No top module specified.\n");
2480
2481 Array veri_modules, vhdl_units;
2482 for (; argidx < GetSize(args); argidx++)
2483 {
2484 const char *name = args[argidx].c_str();
2485 top_mod_names.insert(name);
2486 VeriLibrary* veri_lib = veri_file::GetLibrary(work.c_str(), 1);
2487
2488 if (veri_lib) {
2489 VeriModule *veri_module = veri_lib->GetModule(name, 1);
2490 if (veri_module) {
2491 log("Adding Verilog module '%s' to elaboration queue.\n", name);
2492 veri_modules.InsertLast(veri_module);
2493 continue;
2494 }
2495
2496 // Also elaborate all root modules since they may contain bind statements
2497 MapIter mi;
2498 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib, mi, veri_module) {
2499 if (!veri_module->IsRootModule()) continue;
2500 veri_modules.InsertLast(veri_module);
2501 }
2502 }
2503
2504 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2505 VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
2506 if (vhdl_unit) {
2507 log("Adding VHDL unit '%s' to elaboration queue.\n", name);
2508 vhdl_units.InsertLast(vhdl_unit);
2509 continue;
2510 }
2511
2512 log_error("Can't find module/unit '%s'.\n", name);
2513 }
2514
2515 log("Running hier_tree::Elaborate().\n");
2516 Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
2517 Netlist *nl;
2518 int i;
2519
2520 FOREACH_ARRAY_ITEM(netlists, i, nl) {
2521 nl->AddAtt(new Att(" \\top", NULL));
2522 nl_todo.insert(nl);
2523 }
2524 delete netlists;
2525 }
2526
2527 if (!verific_error_msg.empty())
2528 goto check_error;
2529
2530 if (flatten) {
2531 for (auto nl : nl_todo)
2532 nl->Flatten();
2533 }
2534
2535 if (extnets) {
2536 VerificExtNets worker;
2537 for (auto nl : nl_todo)
2538 worker.run(nl);
2539 }
2540
2541 for (auto nl : nl_todo)
2542 nl->ChangePortBusStructures(1 /* hierarchical */);
2543
2544 if (!dumpfile.empty()) {
2545 VeriWrite veri_writer;
2546 veri_writer.WriteFile(dumpfile.c_str(), Netlist::PresentDesign());
2547 }
2548
2549 while (!nl_todo.empty()) {
2550 Netlist *nl = *nl_todo.begin();
2551 if (nl_done.count(nl) == 0) {
2552 VerificImporter importer(mode_gates, mode_keep, mode_nosva,
2553 mode_names, mode_verific, mode_autocover, mode_fullinit);
2554 importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->Owner()->Name()));
2555 }
2556 nl_todo.erase(nl);
2557 nl_done.insert(nl);
2558 }
2559
2560 veri_file::Reset();
2561 vhdl_file::Reset();
2562 Libset::Reset();
2563 verific_incdirs.clear();
2564 verific_libdirs.clear();
2565 verific_import_pending = false;
2566 goto check_error;
2567 }
2568
2569 cmd_error(args, argidx, "Missing or unsupported mode parameter.\n");
2570
2571 check_error:
2572 if (!verific_error_msg.empty())
2573 log_error("%s\n", verific_error_msg.c_str());
2574
2575 }
2576 #else /* YOSYS_ENABLE_VERIFIC */
2577 void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
2578 log_cmd_error("This version of Yosys is built without Verific support.\n"
2579 "\n"
2580 "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
2581 "https://www.symbioticeda.com/seda-suite\n"
2582 "\n"
2583 "Contact office@symbioticeda.com for free evaluation\n"
2584 "binaries of Symbiotic EDA Suite.\n");
2585 }
2586 #endif
2587 } VerificPass;
2588
2589 struct ReadPass : public Pass {
2590 ReadPass() : Pass("read", "load HDL designs") { }
2591 void help() YS_OVERRIDE
2592 {
2593 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2594 log("\n");
2595 log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
2596 log("\n");
2597 log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
2598 log("is only available via Verific.)\n");
2599 log("\n");
2600 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2601 log("the language version (and before file names) to set additional verilog defines.\n");
2602 log("\n");
2603 log("\n");
2604 log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2605 log("\n");
2606 log("Load the specified VHDL files. (Requires Verific.)\n");
2607 log("\n");
2608 log("\n");
2609 log(" read -define <macro>[=<value>]..\n");
2610 log("\n");
2611 log("Set global Verilog/SystemVerilog defines.\n");
2612 log("\n");
2613 log("\n");
2614 log(" read -undef <macro>..\n");
2615 log("\n");
2616 log("Unset global Verilog/SystemVerilog defines.\n");
2617 log("\n");
2618 log("\n");
2619 log(" read -incdir <directory>\n");
2620 log("\n");
2621 log("Add directory to global Verilog/SystemVerilog include directories.\n");
2622 log("\n");
2623 log("\n");
2624 log(" read -verific\n");
2625 log(" read -noverific\n");
2626 log("\n");
2627 log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n");
2628 log("with -verific will result in an error on Yosys binaries that are built without\n");
2629 log("Verific support. The default is to use Verific if it is available.\n");
2630 log("\n");
2631 }
2632 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
2633 {
2634 #ifdef YOSYS_ENABLE_VERIFIC
2635 static bool verific_available = !check_noverific_env();
2636 #else
2637 static bool verific_available = false;
2638 #endif
2639 static bool use_verific = verific_available;
2640
2641 if (args.size() < 2 || args[1][0] != '-')
2642 cmd_error(args, 1, "Missing mode parameter.\n");
2643
2644 if (args[1] == "-verific" || args[1] == "-noverific") {
2645 if (args.size() != 2)
2646 cmd_error(args, 1, "Additional arguments to -verific/-noverific.\n");
2647 if (args[1] == "-verific") {
2648 if (!verific_available)
2649 cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
2650 use_verific = true;
2651 } else {
2652 use_verific = false;
2653 }
2654 return;
2655 }
2656
2657 if (args.size() < 3)
2658 cmd_error(args, 3, "Missing file name parameter.\n");
2659
2660 if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
2661 if (use_verific) {
2662 args[0] = "verific";
2663 } else {
2664 args[0] = "read_verilog";
2665 args[1] = "-defer";
2666 }
2667 Pass::call(design, args);
2668 return;
2669 }
2670
2671 if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
2672 if (use_verific) {
2673 args[0] = "verific";
2674 } else {
2675 args[0] = "read_verilog";
2676 if (args[1] == "-formal")
2677 args.insert(args.begin()+1, std::string());
2678 args[1] = "-sv";
2679 args.insert(args.begin()+1, "-defer");
2680 }
2681 Pass::call(design, args);
2682 return;
2683 }
2684
2685 if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
2686 if (use_verific) {
2687 args[0] = "verific";
2688 Pass::call(design, args);
2689 } else {
2690 cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
2691 }
2692 return;
2693 }
2694
2695 if (args[1] == "-define") {
2696 if (use_verific) {
2697 args[0] = "verific";
2698 args[1] = "-vlog-define";
2699 Pass::call(design, args);
2700 }
2701 args[0] = "verilog_defines";
2702 args.erase(args.begin()+1, args.begin()+2);
2703 for (int i = 1; i < GetSize(args); i++)
2704 args[i] = "-D" + args[i];
2705 Pass::call(design, args);
2706 return;
2707 }
2708
2709 if (args[1] == "-undef") {
2710 if (use_verific) {
2711 args[0] = "verific";
2712 args[1] = "-vlog-undef";
2713 Pass::call(design, args);
2714 }
2715 args[0] = "verilog_defines";
2716 args.erase(args.begin()+1, args.begin()+2);
2717 for (int i = 1; i < GetSize(args); i++)
2718 args[i] = "-U" + args[i];
2719 Pass::call(design, args);
2720 return;
2721 }
2722
2723 if (args[1] == "-incdir") {
2724 if (use_verific) {
2725 args[0] = "verific";
2726 args[1] = "-vlog-incdir";
2727 Pass::call(design, args);
2728 }
2729 args[0] = "verilog_defaults";
2730 args[1] = "-add";
2731 for (int i = 2; i < GetSize(args); i++)
2732 args[i] = "-I" + args[i];
2733 Pass::call(design, args);
2734 return;
2735 }
2736
2737 cmd_error(args, 1, "Missing or unsupported mode parameter.\n");
2738 }
2739 } ReadPass;
2740
2741 PRIVATE_NAMESPACE_END