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