projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge pull request #859 from smunaut/ice40_braminit
[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 int numchunks = int(inst->Input2Size()) / memory->width;
1204 int chunksbits = ceil_log2(numchunks);
1205
1206 if ((numchunks * memory->width) != int(inst->Input2Size()) || (numchunks & (numchunks - 1)) != 0)
1207 log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst->Name(), inst->GetOutput()->Name());
1208
1209 for (int i = 0; i < numchunks; i++)
1210 {
1211 RTLIL::SigSpec addr = {operatorInput1(inst), RTLIL::Const(i, chunksbits)};
1212 RTLIL::SigSpec data = operatorInput2(inst).extract(i * memory->width, memory->width);
1213
1214 RTLIL::Cell *cell = module->addCell(numchunks == 1 ? inst_name :
1215 RTLIL::IdString(stringf("%s_%d", inst_name.c_str(), i)), "$memwr");
1216 cell->parameters["\\MEMID"] = memory->name.str();
1217 cell->parameters["\\CLK_ENABLE"] = false;
1218 cell->parameters["\\CLK_POLARITY"] = true;
1219 cell->parameters["\\PRIORITY"] = 0;
1220 cell->parameters["\\ABITS"] = GetSize(addr);
1221 cell->parameters["\\WIDTH"] = GetSize(data);
1222 cell->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst->GetControl())).repeat(GetSize(data)));
1223 cell->setPort("\\CLK", RTLIL::State::S0);
1224 cell->setPort("\\ADDR", addr);
1225 cell->setPort("\\DATA", data);
1226
1227 if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
1228 cell->parameters["\\CLK_ENABLE"] = true;
1229 cell->setPort("\\CLK", net_map_at(inst->GetClock()));
1230 }
1231 }
1232 continue;
1233 }
1234
1235 if (!mode_gates) {
1236 if (import_netlist_instance_cells(inst, inst_name))
1237 continue;
1238 if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
1239 log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
1240 } else {
1241 if (import_netlist_instance_gates(inst, inst_name))
1242 continue;
1243 }
1244
1245 if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT)
1246 sva_asserts.insert(inst);
1247
1248 if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME)
1249 sva_assumes.insert(inst);
1250
1251 if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
1252 sva_covers.insert(inst);
1253
1254 if (inst->Type() == PRIM_SVA_TRIGGERED)
1255 sva_triggers.insert(inst);
1256
1257 if (inst->Type() == OPER_SVA_STABLE)
1258 {
1259 VerificClocking clocking(this, inst->GetInput2Bit(0));
1260 log_assert(clocking.disable_sig == State::S0);
1261 log_assert(clocking.body_net == nullptr);
1262
1263 log_assert(inst->Input1Size() == inst->OutputSize());
1264
1265 SigSpec sig_d, sig_q, sig_o;
1266 sig_q = module->addWire(new_verific_id(inst), inst->Input1Size());
1267
1268 for (int i = int(inst->Input1Size())-1; i >= 0; i--){
1269 sig_d.append(net_map_at(inst->GetInput1Bit(i)));
1270 sig_o.append(net_map_at(inst->GetOutputBit(i)));
1271 }
1272
1273 if (verific_verbose) {
1274 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1275 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1276 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1277 log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
1278 }
1279
1280 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1281 module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
1282
1283 if (!mode_keep)
1284 continue;
1285 }
1286
1287 if (inst->Type() == PRIM_SVA_STABLE)
1288 {
1289 VerificClocking clocking(this, inst->GetInput2());
1290 log_assert(clocking.disable_sig == State::S0);
1291 log_assert(clocking.body_net == nullptr);
1292
1293 SigSpec sig_d = net_map_at(inst->GetInput1());
1294 SigSpec sig_o = net_map_at(inst->GetOutput());
1295 SigSpec sig_q = module->addWire(new_verific_id(inst));
1296
1297 if (verific_verbose) {
1298 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1299 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1300 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1301 log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
1302 }
1303
1304 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1305 module->addXnor(new_verific_id(inst), sig_d, sig_q, sig_o);
1306
1307 if (!mode_keep)
1308 continue;
1309 }
1310
1311 if (inst->Type() == PRIM_SVA_PAST)
1312 {
1313 VerificClocking clocking(this, inst->GetInput2());
1314 log_assert(clocking.disable_sig == State::S0);
1315 log_assert(clocking.body_net == nullptr);
1316
1317 SigBit sig_d = net_map_at(inst->GetInput1());
1318 SigBit sig_q = net_map_at(inst->GetOutput());
1319
1320 if (verific_verbose)
1321 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1322 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1323
1324 past_ffs.insert(clocking.addDff(new_verific_id(inst), sig_d, sig_q));
1325
1326 if (!mode_keep)
1327 continue;
1328 }
1329
1330 if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL))
1331 {
1332 VerificClocking clocking(this, inst->GetInput2());
1333 log_assert(clocking.disable_sig == State::S0);
1334 log_assert(clocking.body_net == nullptr);
1335
1336 SigBit sig_d = net_map_at(inst->GetInput1());
1337 SigBit sig_o = net_map_at(inst->GetOutput());
1338 SigBit sig_q = module->addWire(new_verific_id(inst));
1339
1340 if (verific_verbose)
1341 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
1342 log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
1343
1344 clocking.addDff(new_verific_id(inst), sig_d, sig_q);
1345 module->addEq(new_verific_id(inst), {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
1346
1347 if (!mode_keep)
1348 continue;
1349 }
1350
1351 if (!mode_keep && verific_sva_prims.count(inst->Type())) {
1352 if (verific_verbose)
1353 log(" skipping SVA cell in non k-mode\n");
1354 continue;
1355 }
1356
1357 if (inst->Type() == PRIM_HDL_ASSERTION)
1358 {
1359 SigBit cond = net_map_at(inst->GetInput());
1360
1361 if (verific_verbose)
1362 log(" assert condition %s.\n", log_signal(cond));
1363
1364 const char *assume_attr = nullptr; // inst->GetAttValue("assume");
1365
1366 Cell *cell = nullptr;
1367 if (assume_attr != nullptr && !strcmp(assume_attr, "1"))
1368 cell = module->addAssume(new_verific_id(inst), cond, State::S1);
1369 else
1370 cell = module->addAssert(new_verific_id(inst), cond, State::S1);
1371
1372 import_attributes(cell->attributes, inst);
1373 continue;
1374 }
1375
1376 if (inst->IsPrimitive())
1377 {
1378 if (!mode_keep)
1379 log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
1380
1381 if (!verific_sva_prims.count(inst->Type()))
1382 log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
1383 }
1384
1385 import_verific_cells:
1386 nl_todo.insert(inst->View());
1387
1388 RTLIL::Cell *cell = module->addCell(inst_name, inst->IsOperator() ?
1389 std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
1390
1391 if (inst->IsPrimitive() && mode_keep)
1392 cell->attributes["\\keep"] = 1;
1393
1394 dict<IdString, vector<SigBit>> cell_port_conns;
1395
1396 if (verific_verbose)
1397 log(" ports in verific db:\n");
1398
1399 FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
1400 if (verific_verbose)
1401 log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
1402 const char *port_name = pr->GetPort()->Name();
1403 int port_offset = 0;
1404 if (pr->GetPort()->Bus()) {
1405 port_name = pr->GetPort()->Bus()->Name();
1406 port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
1407 min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
1408 }
1409 IdString port_name_id = RTLIL::escape_id(port_name);
1410 auto &sigvec = cell_port_conns[port_name_id];
1411 if (GetSize(sigvec) <= port_offset) {
1412 SigSpec zwires = module->addWire(new_verific_id(inst), port_offset+1-GetSize(sigvec));
1413 for (auto bit : zwires)
1414 sigvec.push_back(bit);
1415 }
1416 sigvec[port_offset] = net_map_at(pr->GetNet());
1417 }
1418
1419 if (verific_verbose)
1420 log(" ports in yosys db:\n");
1421
1422 for (auto &it : cell_port_conns) {
1423 if (verific_verbose)
1424 log(" .%s(%s)\n", log_id(it.first), log_signal(it.second));
1425 cell->setPort(it.first, it.second);
1426 }
1427 }
1428
1429 if (!mode_nosva)
1430 {
1431 for (auto inst : sva_asserts) {
1432 if (mode_autocover)
1433 verific_import_sva_cover(this, inst);
1434 verific_import_sva_assert(this, inst);
1435 }
1436
1437 for (auto inst : sva_assumes)
1438 verific_import_sva_assume(this, inst);
1439
1440 for (auto inst : sva_covers)
1441 verific_import_sva_cover(this, inst);
1442
1443 for (auto inst : sva_triggers)
1444 verific_import_sva_trigger(this, inst);
1445
1446 merge_past_ffs(past_ffs);
1447 }
1448 }
1449
1450 // ==================================================================
1451
1452 VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
1453 {
1454 module = importer->module;
1455
1456 log_assert(importer != nullptr);
1457 log_assert(net != nullptr);
1458
1459 Instance *inst = net->Driver();
1460
1461 if (inst != nullptr && inst->Type() == PRIM_SVA_AT)
1462 {
1463 net = inst->GetInput1();
1464 body_net = inst->GetInput2();
1465
1466 inst = net->Driver();
1467
1468 Instance *body_inst = body_net->Driver();
1469 if (body_inst != nullptr && body_inst->Type() == PRIM_SVA_DISABLE_IFF) {
1470 disable_net = body_inst->GetInput1();
1471 disable_sig = importer->net_map_at(disable_net);
1472 body_net = body_inst->GetInput2();
1473 }
1474 }
1475 else
1476 {
1477 if (sva_at_only)
1478 return;
1479 }
1480
1481 // Use while() instead of if() to work around VIPER #13453
1482 while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
1483 {
1484 net = inst->GetInput();
1485 inst = net->Driver();;
1486 }
1487
1488 if (inst != nullptr && inst->Type() == PRIM_INV)
1489 {
1490 net = inst->GetInput();
1491 inst = net->Driver();;
1492 posedge = false;
1493 }
1494
1495 // Detect clock-enable circuit
1496 do {
1497 if (inst == nullptr || inst->Type() != PRIM_AND)
1498 break;
1499
1500 Net *net_dlatch = inst->GetInput1();
1501 Instance *inst_dlatch = net_dlatch->Driver();
1502
1503 if (inst_dlatch == nullptr || inst_dlatch->Type() != PRIM_DLATCHRS)
1504 break;
1505
1506 if (!inst_dlatch->GetSet()->IsGnd() || !inst_dlatch->GetReset()->IsGnd())
1507 break;
1508
1509 Net *net_enable = inst_dlatch->GetInput();
1510 Net *net_not_clock = inst_dlatch->GetControl();
1511
1512 if (net_enable == nullptr || net_not_clock == nullptr)
1513 break;
1514
1515 Instance *inst_not_clock = net_not_clock->Driver();
1516
1517 if (inst_not_clock == nullptr || inst_not_clock->Type() != PRIM_INV)
1518 break;
1519
1520 Net *net_clock1 = inst_not_clock->GetInput();
1521 Net *net_clock2 = inst->GetInput2();
1522
1523 if (net_clock1 == nullptr || net_clock1 != net_clock2)
1524 break;
1525
1526 enable_net = net_enable;
1527 enable_sig = importer->net_map_at(enable_net);
1528
1529 net = net_clock1;
1530 inst = net->Driver();;
1531 } while (0);
1532
1533 // Detect condition expression
1534 do {
1535 if (body_net == nullptr)
1536 break;
1537
1538 Instance *inst_mux = body_net->Driver();
1539
1540 if (inst_mux == nullptr || inst_mux->Type() != PRIM_MUX)
1541 break;
1542
1543 if (!inst_mux->GetInput1()->IsPwr())
1544 break;
1545
1546 Net *sva_net = inst_mux->GetInput2();
1547 if (!verific_is_sva_net(importer, sva_net))
1548 break;
1549
1550 body_net = sva_net;
1551 cond_net = inst_mux->GetControl();
1552 } while (0);
1553
1554 clock_net = net;
1555 clock_sig = importer->net_map_at(clock_net);
1556
1557 const char *gclk_attr = clock_net->GetAttValue("gclk");
1558 if (gclk_attr != nullptr && (!strcmp(gclk_attr, "1") || !strcmp(gclk_attr, "'1'")))
1559 gclk = true;
1560 }
1561
1562 Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value)
1563 {
1564 log_assert(GetSize(sig_d) == GetSize(sig_q));
1565
1566 if (GetSize(init_value) != 0) {
1567 log_assert(GetSize(sig_q) == GetSize(init_value));
1568 if (sig_q.is_wire()) {
1569 sig_q.as_wire()->attributes["\\init"] = init_value;
1570 } else {
1571 Wire *w = module->addWire(NEW_ID, GetSize(sig_q));
1572 w->attributes["\\init"] = init_value;
1573 module->connect(sig_q, w);
1574 sig_q = w;
1575 }
1576 }
1577
1578 if (enable_sig != State::S1)
1579 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1580
1581 if (disable_sig != State::S0) {
1582 log_assert(gclk == false);
1583 log_assert(GetSize(sig_q) == GetSize(init_value));
1584 return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
1585 }
1586
1587 if (gclk)
1588 return module->addFf(name, sig_d, sig_q);
1589
1590 return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
1591 }
1592
1593 Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value)
1594 {
1595 log_assert(gclk == false);
1596 log_assert(disable_sig == State::S0);
1597
1598 if (enable_sig != State::S1)
1599 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1600
1601 return module->addAdff(name, clock_sig, sig_arst, sig_d, sig_q, arst_value, posedge);
1602 }
1603
1604 Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q)
1605 {
1606 log_assert(gclk == false);
1607 log_assert(disable_sig == State::S0);
1608
1609 if (enable_sig != State::S1)
1610 sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
1611
1612 return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
1613 }
1614
1615 // ==================================================================
1616
1617 struct VerificExtNets
1618 {
1619 int portname_cnt = 0;
1620
1621 // a map from Net to the same Net one level up in the design hierarchy
1622 std::map<Net*, Net*> net_level_up;
1623
1624 Net *get_net_level_up(Net *net)
1625 {
1626 if (net_level_up.count(net) == 0)
1627 {
1628 Netlist *nl = net->Owner();
1629
1630 // Simply return if Netlist is not unique
1631 if (nl->NumOfRefs() != 1)
1632 return net;
1633
1634 Instance *up_inst = (Instance*)nl->GetReferences()->GetLast();
1635 Netlist *up_nl = up_inst->Owner();
1636
1637 // create new Port
1638 string name = stringf("___extnets_%d", portname_cnt++);
1639 Port *new_port = new Port(name.c_str(), DIR_OUT);
1640 nl->Add(new_port);
1641 net->Connect(new_port);
1642
1643 // create new Net in up Netlist
1644 Net *new_net = new Net(name.c_str());
1645 up_nl->Add(new_net);
1646 up_inst->Connect(new_port, new_net);
1647
1648 net_level_up[net] = new_net;
1649 }
1650
1651 return net_level_up.at(net);
1652 }
1653
1654 void run(Netlist *nl)
1655 {
1656 MapIter mi, mi2;
1657 Instance *inst;
1658 PortRef *pr;
1659
1660 vector<tuple<Instance*, Port*, Net*>> todo_connect;
1661
1662 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1663 run(inst->View());
1664
1665 FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
1666 FOREACH_PORTREF_OF_INST(inst, mi2, pr)
1667 {
1668 Port *port = pr->GetPort();
1669 Net *net = pr->GetNet();
1670
1671 if (!net->IsExternalTo(nl))
1672 continue;
1673
1674 if (verific_verbose)
1675 log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name());
1676
1677 while (net->IsExternalTo(nl))
1678 {
1679 Net *newnet = get_net_level_up(net);
1680 if (newnet == net) break;
1681
1682 if (verific_verbose)
1683 log(" external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name());
1684 net = newnet;
1685 }
1686
1687 if (verific_verbose)
1688 log(" final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : "");
1689 todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net));
1690 }
1691
1692 for (auto it : todo_connect) {
1693 get<0>(it)->Disconnect(get<1>(it));
1694 get<0>(it)->Connect(get<1>(it), get<2>(it));
1695 }
1696 }
1697 };
1698
1699 void verific_import(Design *design, std::string top)
1700 {
1701 verific_sva_fsm_limit = 16;
1702
1703 std::set<Netlist*> nl_todo, nl_done;
1704
1705 {
1706 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
1707 VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
1708
1709 Array veri_libs, vhdl_libs;
1710 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
1711 if (veri_lib) veri_libs.InsertLast(veri_lib);
1712
1713 Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
1714 Netlist *nl;
1715 int i;
1716
1717 FOREACH_ARRAY_ITEM(netlists, i, nl) {
1718 if (top.empty() || nl->Owner()->Name() == top)
1719 nl_todo.insert(nl);
1720 }
1721
1722 delete netlists;
1723 }
1724
1725 if (!verific_error_msg.empty())
1726 log_error("%s\n", verific_error_msg.c_str());
1727
1728 VerificExtNets worker;
1729 for (auto nl : nl_todo)
1730 worker.run(nl);
1731
1732 while (!nl_todo.empty()) {
1733 Netlist *nl = *nl_todo.begin();
1734 if (nl_done.count(nl) == 0) {
1735 VerificImporter importer(false, false, false, false, false, false);
1736 importer.import_netlist(design, nl, nl_todo);
1737 }
1738 nl_todo.erase(nl);
1739 nl_done.insert(nl);
1740 }
1741
1742 veri_file::Reset();
1743 vhdl_file::Reset();
1744 Libset::Reset();
1745 verific_incdirs.clear();
1746 verific_libdirs.clear();
1747 verific_import_pending = false;
1748
1749 if (!verific_error_msg.empty())
1750 log_error("%s\n", verific_error_msg.c_str());
1751 }
1752
1753 YOSYS_NAMESPACE_END
1754 #endif /* YOSYS_ENABLE_VERIFIC */
1755
1756 PRIVATE_NAMESPACE_BEGIN
1757
1758 #ifdef YOSYS_ENABLE_VERIFIC
1759 bool check_noverific_env()
1760 {
1761 const char *e = getenv("YOSYS_NOVERIFIC");
1762 if (e == nullptr)
1763 return false;
1764 if (atoi(e) == 0)
1765 return false;
1766 return true;
1767 }
1768 #endif
1769
1770 struct VerificPass : public Pass {
1771 VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
1772 void help() YS_OVERRIDE
1773 {
1774 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1775 log("\n");
1776 log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
1777 log("\n");
1778 log("Load the specified Verilog/SystemVerilog files into Verific.\n");
1779 log("\n");
1780 log("All files specified in one call to this command are one compilation unit.\n");
1781 log("Files passed to different calls to this command are treated as belonging to\n");
1782 log("different compilation units.\n");
1783 log("\n");
1784 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
1785 log("the language version (and before file names) to set additional verilog defines.\n");
1786 log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
1787 log("\n");
1788 log("\n");
1789 log(" verific -formal <verilog-file>..\n");
1790 log("\n");
1791 log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
1792 log("\n");
1793 log("\n");
1794 log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
1795 log("\n");
1796 log("Load the specified VHDL files into Verific.\n");
1797 log("\n");
1798 log("\n");
1799 log(" verific -work <libname> {-sv|-vhdl|...} <hdl-file>\n");
1800 log("\n");
1801 log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
1802 log("(default library when -work is not present: \"work\")\n");
1803 log("\n");
1804 log("\n");
1805 log(" verific -vlog-incdir <directory>..\n");
1806 log("\n");
1807 log("Add Verilog include directories.\n");
1808 log("\n");
1809 log("\n");
1810 log(" verific -vlog-libdir <directory>..\n");
1811 log("\n");
1812 log("Add Verilog library directories. Verific will search in this directories to\n");
1813 log("find undefined modules.\n");
1814 log("\n");
1815 log("\n");
1816 log(" verific -vlog-define <macro>[=<value>]..\n");
1817 log("\n");
1818 log("Add Verilog defines.\n");
1819 log("\n");
1820 log("\n");
1821 log(" verific -vlog-undef <macro>..\n");
1822 log("\n");
1823 log("Remove Verilog defines previously set with -vlog-define.\n");
1824 log("\n");
1825 log("\n");
1826 log(" verific -set-error <msg_id>..\n");
1827 log(" verific -set-warning <msg_id>..\n");
1828 log(" verific -set-info <msg_id>..\n");
1829 log(" verific -set-ignore <msg_id>..\n");
1830 log("\n");
1831 log("Set message severity. <msg_id> is the string in square brackets when a message\n");
1832 log("is printed, such as VERI-1209.\n");
1833 log("\n");
1834 log("\n");
1835 log(" verific -import [options] <top-module>..\n");
1836 log("\n");
1837 log("Elaborate the design for the specified top modules, import to Yosys and\n");
1838 log("reset the internal state of Verific.\n");
1839 log("\n");
1840 log("Import options:\n");
1841 log("\n");
1842 log(" -all\n");
1843 log(" Elaborate all modules, not just the hierarchy below the given top\n");
1844 log(" modules. With this option the list of modules to import is optional.\n");
1845 log("\n");
1846 log(" -gates\n");
1847 log(" Create a gate-level netlist.\n");
1848 log("\n");
1849 log(" -flatten\n");
1850 log(" Flatten the design in Verific before importing.\n");
1851 log("\n");
1852 log(" -extnets\n");
1853 log(" Resolve references to external nets by adding module ports as needed.\n");
1854 log("\n");
1855 log(" -autocover\n");
1856 log(" Generate automatic cover statements for all asserts\n");
1857 log("\n");
1858 log(" -chparam name value \n");
1859 log(" Elaborate the specified top modules (all modules when -all given) using\n");
1860 log(" this parameter value. Modules on which this parameter does not exist will\n");
1861 log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n");
1862 log(" can be specified multiple times to override multiple parameters.\n");
1863 log(" String values must be passed in double quotes (\").\n");
1864 log("\n");
1865 log(" -v, -vv\n");
1866 log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
1867 log("\n");
1868 log("The following additional import options are useful for debugging the Verific\n");
1869 log("bindings (for Yosys and/or Verific developers):\n");
1870 log("\n");
1871 log(" -k\n");
1872 log(" Keep going after an unsupported verific primitive is found. The\n");
1873 log(" unsupported primitive is added as blockbox module to the design.\n");
1874 log(" This will also add all SVA related cells to the design parallel to\n");
1875 log(" the checker logic inferred by it.\n");
1876 log("\n");
1877 log(" -V\n");
1878 log(" Import Verific netlist as-is without translating to Yosys cell types. \n");
1879 log("\n");
1880 log(" -nosva\n");
1881 log(" Ignore SVA properties, do not infer checker logic.\n");
1882 log("\n");
1883 log(" -L <int>\n");
1884 log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
1885 log("\n");
1886 log(" -n\n");
1887 log(" Keep all Verific names on instances and nets. By default only\n");
1888 log(" user-declared names are preserved.\n");
1889 log("\n");
1890 log(" -d <dump_file>\n");
1891 log(" Dump the Verific netlist as a verilog file.\n");
1892 log("\n");
1893 log("Visit http://verific.com/ for more information on Verific.\n");
1894 log("\n");
1895 }
1896 #ifdef YOSYS_ENABLE_VERIFIC
1897 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
1898 {
1899 static bool set_verific_global_flags = true;
1900
1901 if (check_noverific_env())
1902 log_cmd_error("This version of Yosys is built without Verific support.\n");
1903
1904 log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
1905
1906 if (set_verific_global_flags)
1907 {
1908 Message::SetConsoleOutput(0);
1909 Message::RegisterCallBackMsg(msg_func);
1910
1911 RuntimeFlags::SetVar("db_preserve_user_nets", 1);
1912 RuntimeFlags::SetVar("db_allow_external_nets", 1);
1913 RuntimeFlags::SetVar("db_infer_wide_operators", 1);
1914
1915 RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
1916 RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
1917
1918 RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
1919 RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
1920
1921 RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
1922 RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
1923
1924 // Workaround for VIPER #13851
1925 RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
1926
1927 // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
1928 Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
1929
1930 #ifndef DB_PRESERVE_INITIAL_VALUE
1931 # warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
1932 #endif
1933
1934 set_verific_global_flags = false;
1935 }
1936
1937 verific_verbose = 0;
1938 verific_sva_fsm_limit = 16;
1939
1940 const char *release_str = Message::ReleaseString();
1941 time_t release_time = Message::ReleaseDate();
1942 char *release_tmstr = ctime(&release_time);
1943
1944 if (release_str == nullptr)
1945 release_str = "(no release string)";
1946
1947 for (char *p = release_tmstr; *p; p++)
1948 if (*p == '\n') *p = 0;
1949
1950 log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);
1951
1952 int argidx = 1;
1953 std::string work = "work";
1954
1955 if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
1956 args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
1957 {
1958 msg_type_t new_type;
1959
1960 if (args[argidx] == "-set-error")
1961 new_type = VERIFIC_ERROR;
1962 else if (args[argidx] == "-set-warning")
1963 new_type = VERIFIC_WARNING;
1964 else if (args[argidx] == "-set-info")
1965 new_type = VERIFIC_INFO;
1966 else if (args[argidx] == "-set-ignore")
1967 new_type = VERIFIC_IGNORE;
1968 else
1969 log_abort();
1970
1971 for (argidx++; argidx < GetSize(args); argidx++)
1972 Message::SetMessageType(args[argidx].c_str(), new_type);
1973
1974 goto check_error;
1975 }
1976
1977 if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
1978 for (argidx++; argidx < GetSize(args); argidx++)
1979 verific_incdirs.push_back(args[argidx]);
1980 goto check_error;
1981 }
1982
1983 if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
1984 for (argidx++; argidx < GetSize(args); argidx++)
1985 verific_libdirs.push_back(args[argidx]);
1986 goto check_error;
1987 }
1988
1989 if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
1990 for (argidx++; argidx < GetSize(args); argidx++) {
1991 string name = args[argidx];
1992 size_t equal = name.find('=');
1993 if (equal != std::string::npos) {
1994 string value = name.substr(equal+1);
1995 name = name.substr(0, equal);
1996 veri_file::DefineCmdLineMacro(name.c_str(), value.c_str());
1997 } else {
1998 veri_file::DefineCmdLineMacro(name.c_str());
1999 }
2000 }
2001 goto check_error;
2002 }
2003
2004 if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") {
2005 for (argidx++; argidx < GetSize(args); argidx++) {
2006 string name = args[argidx];
2007 veri_file::UndefineMacro(name.c_str());
2008 }
2009 goto check_error;
2010 }
2011
2012 for (; argidx < GetSize(args); argidx++)
2013 {
2014 if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
2015 work = args[++argidx];
2016 continue;
2017 }
2018 break;
2019 }
2020
2021 if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
2022 args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
2023 {
2024 Array file_names;
2025 unsigned verilog_mode;
2026
2027 if (args[argidx] == "-vlog95")
2028 verilog_mode = veri_file::VERILOG_95;
2029 else if (args[argidx] == "-vlog2k")
2030 verilog_mode = veri_file::VERILOG_2K;
2031 else if (args[argidx] == "-sv2005")
2032 verilog_mode = veri_file::SYSTEM_VERILOG_2005;
2033 else if (args[argidx] == "-sv2009")
2034 verilog_mode = veri_file::SYSTEM_VERILOG_2009;
2035 else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")
2036 verilog_mode = veri_file::SYSTEM_VERILOG;
2037 else
2038 log_abort();
2039
2040 veri_file::DefineMacro("VERIFIC");
2041 veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
2042
2043 for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) {
2044 std::string name = args[argidx].substr(2);
2045 if (args[argidx] == "-D") {
2046 if (++argidx >= GetSize(args))
2047 break;
2048 name = args[argidx];
2049 }
2050 size_t equal = name.find('=');
2051 if (equal != std::string::npos) {
2052 string value = name.substr(equal+1);
2053 name = name.substr(0, equal);
2054 veri_file::DefineMacro(name.c_str(), value.c_str());
2055 } else {
2056 veri_file::DefineMacro(name.c_str());
2057 }
2058 }
2059
2060 for (auto &dir : verific_incdirs)
2061 veri_file::AddIncludeDir(dir.c_str());
2062 for (auto &dir : verific_libdirs)
2063 veri_file::AddYDir(dir.c_str());
2064
2065 while (argidx < GetSize(args))
2066 file_names.Insert(args[argidx++].c_str());
2067
2068 if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU))
2069 log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
2070
2071 verific_import_pending = true;
2072 goto check_error;
2073 }
2074
2075 if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
2076 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
2077 for (argidx++; argidx < GetSize(args); argidx++)
2078 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87))
2079 log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
2080 verific_import_pending = true;
2081 goto check_error;
2082 }
2083
2084 if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
2085 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2086 for (argidx++; argidx < GetSize(args); argidx++)
2087 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93))
2088 log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
2089 verific_import_pending = true;
2090 goto check_error;
2091 }
2092
2093 if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
2094 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2095 for (argidx++; argidx < GetSize(args); argidx++)
2096 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K))
2097 log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
2098 verific_import_pending = true;
2099 goto check_error;
2100 }
2101
2102 if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
2103 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
2104 for (argidx++; argidx < GetSize(args); argidx++)
2105 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008))
2106 log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
2107 verific_import_pending = true;
2108 goto check_error;
2109 }
2110
2111 if (GetSize(args) > argidx && args[argidx] == "-import")
2112 {
2113 std::set<Netlist*> nl_todo, nl_done;
2114 bool mode_all = false, mode_gates = false, mode_keep = false;
2115 bool mode_nosva = false, mode_names = false, mode_verific = false;
2116 bool mode_autocover = false;
2117 bool flatten = false, extnets = false;
2118 string dumpfile;
2119 Map parameters(STRING_HASH);
2120
2121 for (argidx++; argidx < GetSize(args); argidx++) {
2122 if (args[argidx] == "-all") {
2123 mode_all = true;
2124 continue;
2125 }
2126 if (args[argidx] == "-gates") {
2127 mode_gates = true;
2128 continue;
2129 }
2130 if (args[argidx] == "-flatten") {
2131 flatten = true;
2132 continue;
2133 }
2134 if (args[argidx] == "-extnets") {
2135 extnets = true;
2136 continue;
2137 }
2138 if (args[argidx] == "-k") {
2139 mode_keep = true;
2140 continue;
2141 }
2142 if (args[argidx] == "-nosva") {
2143 mode_nosva = true;
2144 continue;
2145 }
2146 if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
2147 verific_sva_fsm_limit = atoi(args[++argidx].c_str());
2148 continue;
2149 }
2150 if (args[argidx] == "-n") {
2151 mode_names = true;
2152 continue;
2153 }
2154 if (args[argidx] == "-autocover") {
2155 mode_autocover = true;
2156 continue;
2157 }
2158 if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) {
2159 const std::string &key = args[++argidx];
2160 const std::string &value = args[++argidx];
2161 unsigned new_insertion = parameters.Insert(key.c_str(), value.c_str(),
2162 1 /* force_overwrite */);
2163 if (!new_insertion)
2164 log_warning_noprefix("-chparam %s already specified: overwriting.\n", key.c_str());
2165 continue;
2166 }
2167 if (args[argidx] == "-V") {
2168 mode_verific = true;
2169 continue;
2170 }
2171 if (args[argidx] == "-v") {
2172 verific_verbose = 1;
2173 continue;
2174 }
2175 if (args[argidx] == "-vv") {
2176 verific_verbose = 2;
2177 continue;
2178 }
2179 if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {
2180 dumpfile = args[++argidx];
2181 continue;
2182 }
2183 break;
2184 }
2185
2186 if (argidx > GetSize(args) && args[argidx].substr(0, 1) == "-")
2187 cmd_error(args, argidx, "unknown option");
2188
2189 if (mode_all)
2190 {
2191 log("Running hier_tree::ElaborateAll().\n");
2192
2193 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2194 VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
2195
2196 Array veri_libs, vhdl_libs;
2197 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
2198 if (veri_lib) veri_libs.InsertLast(veri_lib);
2199
2200 Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs, &parameters);
2201 Netlist *nl;
2202 int i;
2203
2204 FOREACH_ARRAY_ITEM(netlists, i, nl)
2205 nl_todo.insert(nl);
2206 delete netlists;
2207 }
2208 else
2209 {
2210 if (argidx == GetSize(args))
2211 log_cmd_error("No top module specified.\n");
2212
2213 Array veri_modules, vhdl_units;
2214 for (; argidx < GetSize(args); argidx++)
2215 {
2216 const char *name = args[argidx].c_str();
2217
2218 VeriModule *veri_module = veri_file::GetModule(name);
2219 if (veri_module) {
2220 log("Adding Verilog module '%s' to elaboration queue.\n", name);
2221 veri_modules.InsertLast(veri_module);
2222 continue;
2223 }
2224
2225 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2226 VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
2227 if (vhdl_unit) {
2228 log("Adding VHDL unit '%s' to elaboration queue.\n", name);
2229 vhdl_units.InsertLast(vhdl_unit);
2230 continue;
2231 }
2232
2233 log_error("Can't find module/unit '%s'.\n", name);
2234 }
2235
2236 log("Running hier_tree::Elaborate().\n");
2237 Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units, &parameters);
2238 Netlist *nl;
2239 int i;
2240
2241 FOREACH_ARRAY_ITEM(netlists, i, nl)
2242 nl_todo.insert(nl);
2243 delete netlists;
2244 }
2245
2246 if (!verific_error_msg.empty())
2247 goto check_error;
2248
2249 if (flatten) {
2250 for (auto nl : nl_todo)
2251 nl->Flatten();
2252 }
2253
2254 if (extnets) {
2255 VerificExtNets worker;
2256 for (auto nl : nl_todo)
2257 worker.run(nl);
2258 }
2259
2260 if (!dumpfile.empty()) {
2261 VeriWrite veri_writer;
2262 veri_writer.WriteFile(dumpfile.c_str(), Netlist::PresentDesign());
2263 }
2264
2265 while (!nl_todo.empty()) {
2266 Netlist *nl = *nl_todo.begin();
2267 if (nl_done.count(nl) == 0) {
2268 VerificImporter importer(mode_gates, mode_keep, mode_nosva,
2269 mode_names, mode_verific, mode_autocover);
2270 importer.import_netlist(design, nl, nl_todo);
2271 }
2272 nl_todo.erase(nl);
2273 nl_done.insert(nl);
2274 }
2275
2276 veri_file::Reset();
2277 vhdl_file::Reset();
2278 Libset::Reset();
2279 verific_incdirs.clear();
2280 verific_libdirs.clear();
2281 verific_import_pending = false;
2282 goto check_error;
2283 }
2284
2285 log_cmd_error("Missing or unsupported mode parameter.\n");
2286
2287 check_error:
2288 if (!verific_error_msg.empty())
2289 log_error("%s\n", verific_error_msg.c_str());
2290
2291 }
2292 #else /* YOSYS_ENABLE_VERIFIC */
2293 void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
2294 log_cmd_error("This version of Yosys is built without Verific support.\n");
2295 }
2296 #endif
2297 } VerificPass;
2298
2299 struct ReadPass : public Pass {
2300 ReadPass() : Pass("read", "load HDL designs") { }
2301 void help() YS_OVERRIDE
2302 {
2303 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2304 log("\n");
2305 log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
2306 log("\n");
2307 log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
2308 log("is only available via Verific.)\n");
2309 log("\n");
2310 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2311 log("the language version (and before file names) to set additional verilog defines.\n");
2312 log("\n");
2313 log("\n");
2314 log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2315 log("\n");
2316 log("Load the specified VHDL files. (Requires Verific.)\n");
2317 log("\n");
2318 log("\n");
2319 log(" read -define <macro>[=<value>]..\n");
2320 log("\n");
2321 log("Set global Verilog/SystemVerilog defines.\n");
2322 log("\n");
2323 log("\n");
2324 log(" read -undef <macro>..\n");
2325 log("\n");
2326 log("Unset global Verilog/SystemVerilog defines.\n");
2327 log("\n");
2328 log("\n");
2329 log(" read -incdir <directory>\n");
2330 log("\n");
2331 log("Add directory to global Verilog/SystemVerilog include directories.\n");
2332 log("\n");
2333 }
2334 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
2335 {
2336 if (args.size() < 2 || args[1][0] != '-')
2337 log_cmd_error("Missing mode parameter.\n");
2338
2339 if (args.size() < 3)
2340 log_cmd_error("Missing file name parameter.\n");
2341
2342 #ifdef YOSYS_ENABLE_VERIFIC
2343 bool use_verific = !check_noverific_env();
2344 #else
2345 bool use_verific = false;
2346 #endif
2347
2348 if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
2349 if (use_verific) {
2350 args[0] = "verific";
2351 } else {
2352 args[0] = "read_verilog";
2353 args.erase(args.begin()+1, args.begin()+2);
2354 }
2355 Pass::call(design, args);
2356 return;
2357 }
2358
2359 if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
2360 if (use_verific) {
2361 args[0] = "verific";
2362 } else {
2363 args[0] = "read_verilog";
2364 if (args[1] == "-formal")
2365 args.insert(args.begin()+1, std::string());
2366 args[1] = "-sv";
2367 }
2368 Pass::call(design, args);
2369 return;
2370 }
2371
2372 if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
2373 if (use_verific) {
2374 args[0] = "verific";
2375 Pass::call(design, args);
2376 } else {
2377 log_cmd_error("This version of Yosys is built without Verific support.\n");
2378 }
2379 return;
2380 }
2381
2382 if (args[1] == "-define") {
2383 if (use_verific) {
2384 args[0] = "verific";
2385 args[1] = "-vlog-define";
2386 Pass::call(design, args);
2387 }
2388 args[0] = "verilog_defines";
2389 args.erase(args.begin()+1, args.begin()+2);
2390 for (int i = 1; i < GetSize(args); i++)
2391 args[i] = "-D" + args[i];
2392 Pass::call(design, args);
2393 return;
2394 }
2395
2396 if (args[1] == "-undef") {
2397 if (use_verific) {
2398 args[0] = "verific";
2399 args[1] = "-vlog-undef";
2400 Pass::call(design, args);
2401 }
2402 args[0] = "verilog_defines";
2403 args.erase(args.begin()+1, args.begin()+2);
2404 for (int i = 1; i < GetSize(args); i++)
2405 args[i] = "-U" + args[i];
2406 Pass::call(design, args);
2407 return;
2408 }
2409
2410 if (args[1] == "-incdir") {
2411 if (use_verific) {
2412 args[0] = "verific";
2413 args[1] = "-vlog-incdir";
2414 Pass::call(design, args);
2415 }
2416 args[0] = "verilog_defaults";
2417 args[1] = "-add";
2418 for (int i = 2; i < GetSize(args); i++)
2419 args[i] = "-I" + args[i];
2420 Pass::call(design, args);
2421 return;
2422 }
2423
2424 log_cmd_error("Missing or unsupported mode parameter.\n");
2425 }
2426 } ReadPass;
2427
2428 PRIVATE_NAMESPACE_END