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