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