projects / yosys.git / blob
? search:


94138cdd67f77dafdc0fd0547d554198b525d8b7
[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(" -v, -vv\n");
1859 log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
1860 log("\n");
1861 log("The following additional import options are useful for debugging the Verific\n");
1862 log("bindings (for Yosys and/or Verific developers):\n");
1863 log("\n");
1864 log(" -k\n");
1865 log(" Keep going after an unsupported verific primitive is found. The\n");
1866 log(" unsupported primitive is added as blockbox module to the design.\n");
1867 log(" This will also add all SVA related cells to the design parallel to\n");
1868 log(" the checker logic inferred by it.\n");
1869 log("\n");
1870 log(" -V\n");
1871 log(" Import Verific netlist as-is without translating to Yosys cell types. \n");
1872 log("\n");
1873 log(" -nosva\n");
1874 log(" Ignore SVA properties, do not infer checker logic.\n");
1875 log("\n");
1876 log(" -L <int>\n");
1877 log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
1878 log("\n");
1879 log(" -n\n");
1880 log(" Keep all Verific names on instances and nets. By default only\n");
1881 log(" user-declared names are preserved.\n");
1882 log("\n");
1883 log(" -d <dump_file>\n");
1884 log(" Dump the Verific netlist as a verilog file.\n");
1885 log("\n");
1886 log("Visit http://verific.com/ for more information on Verific.\n");
1887 log("\n");
1888 }
1889 #ifdef YOSYS_ENABLE_VERIFIC
1890 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
1891 {
1892 static bool set_verific_global_flags = true;
1893
1894 if (check_noverific_env())
1895 log_cmd_error("This version of Yosys is built without Verific support.\n");
1896
1897 log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
1898
1899 if (set_verific_global_flags)
1900 {
1901 Message::SetConsoleOutput(0);
1902 Message::RegisterCallBackMsg(msg_func);
1903
1904 RuntimeFlags::SetVar("db_preserve_user_nets", 1);
1905 RuntimeFlags::SetVar("db_allow_external_nets", 1);
1906 RuntimeFlags::SetVar("db_infer_wide_operators", 1);
1907
1908 RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
1909 RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
1910
1911 RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
1912 RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
1913
1914 RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
1915 RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
1916
1917 // Workaround for VIPER #13851
1918 RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
1919
1920 // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
1921 Message::SetMessageType("VERI-1063", VERIFIC_ERROR);
1922
1923 set_verific_global_flags = false;
1924 }
1925
1926 verific_verbose = 0;
1927 verific_sva_fsm_limit = 16;
1928
1929 const char *release_str = Message::ReleaseString();
1930 time_t release_time = Message::ReleaseDate();
1931 char *release_tmstr = ctime(&release_time);
1932
1933 if (release_str == nullptr)
1934 release_str = "(no release string)";
1935
1936 for (char *p = release_tmstr; *p; p++)
1937 if (*p == '\n') *p = 0;
1938
1939 log("Built with Verific %s, released at %s.\n", release_str, release_tmstr);
1940
1941 int argidx = 1;
1942 std::string work = "work";
1943
1944 if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" ||
1945 args[argidx] == "-set-info" || args[argidx] == "-set-ignore"))
1946 {
1947 msg_type_t new_type;
1948
1949 if (args[argidx] == "-set-error")
1950 new_type = VERIFIC_ERROR;
1951 else if (args[argidx] == "-set-warning")
1952 new_type = VERIFIC_WARNING;
1953 else if (args[argidx] == "-set-info")
1954 new_type = VERIFIC_INFO;
1955 else if (args[argidx] == "-set-ignore")
1956 new_type = VERIFIC_IGNORE;
1957 else
1958 log_abort();
1959
1960 for (argidx++; argidx < GetSize(args); argidx++)
1961 Message::SetMessageType(args[argidx].c_str(), new_type);
1962
1963 goto check_error;
1964 }
1965
1966 if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
1967 for (argidx++; argidx < GetSize(args); argidx++)
1968 verific_incdirs.push_back(args[argidx]);
1969 goto check_error;
1970 }
1971
1972 if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
1973 for (argidx++; argidx < GetSize(args); argidx++)
1974 verific_libdirs.push_back(args[argidx]);
1975 goto check_error;
1976 }
1977
1978 if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
1979 for (argidx++; argidx < GetSize(args); argidx++) {
1980 string name = args[argidx];
1981 size_t equal = name.find('=');
1982 if (equal != std::string::npos) {
1983 string value = name.substr(equal+1);
1984 name = name.substr(0, equal);
1985 veri_file::DefineCmdLineMacro(name.c_str(), value.c_str());
1986 } else {
1987 veri_file::DefineCmdLineMacro(name.c_str());
1988 }
1989 }
1990 goto check_error;
1991 }
1992
1993 if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") {
1994 for (argidx++; argidx < GetSize(args); argidx++) {
1995 string name = args[argidx];
1996 veri_file::UndefineMacro(name.c_str());
1997 }
1998 goto check_error;
1999 }
2000
2001 for (; argidx < GetSize(args); argidx++)
2002 {
2003 if (args[argidx] == "-work" && argidx+1 < GetSize(args)) {
2004 work = args[++argidx];
2005 continue;
2006 }
2007 break;
2008 }
2009
2010 if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
2011 args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
2012 {
2013 Array file_names;
2014 unsigned verilog_mode;
2015
2016 if (args[argidx] == "-vlog95")
2017 verilog_mode = veri_file::VERILOG_95;
2018 else if (args[argidx] == "-vlog2k")
2019 verilog_mode = veri_file::VERILOG_2K;
2020 else if (args[argidx] == "-sv2005")
2021 verilog_mode = veri_file::SYSTEM_VERILOG_2005;
2022 else if (args[argidx] == "-sv2009")
2023 verilog_mode = veri_file::SYSTEM_VERILOG_2009;
2024 else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")
2025 verilog_mode = veri_file::SYSTEM_VERILOG;
2026 else
2027 log_abort();
2028
2029 veri_file::DefineMacro("VERIFIC");
2030 veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
2031
2032 for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) {
2033 std::string name = args[argidx].substr(2);
2034 if (args[argidx] == "-D") {
2035 if (++argidx >= GetSize(args))
2036 break;
2037 name = args[argidx];
2038 }
2039 size_t equal = name.find('=');
2040 if (equal != std::string::npos) {
2041 string value = name.substr(equal+1);
2042 name = name.substr(0, equal);
2043 veri_file::DefineMacro(name.c_str(), value.c_str());
2044 } else {
2045 veri_file::DefineMacro(name.c_str());
2046 }
2047 }
2048
2049 for (auto &dir : verific_incdirs)
2050 veri_file::AddIncludeDir(dir.c_str());
2051 for (auto &dir : verific_libdirs)
2052 veri_file::AddYDir(dir.c_str());
2053
2054 while (argidx < GetSize(args))
2055 file_names.Insert(args[argidx++].c_str());
2056
2057 if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU))
2058 log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
2059
2060 verific_import_pending = true;
2061 goto check_error;
2062 }
2063
2064 if (GetSize(args) > argidx && args[argidx] == "-vhdl87") {
2065 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
2066 for (argidx++; argidx < GetSize(args); argidx++)
2067 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_87))
2068 log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
2069 verific_import_pending = true;
2070 goto check_error;
2071 }
2072
2073 if (GetSize(args) > argidx && args[argidx] == "-vhdl93") {
2074 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2075 for (argidx++; argidx < GetSize(args); argidx++)
2076 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_93))
2077 log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
2078 verific_import_pending = true;
2079 goto check_error;
2080 }
2081
2082 if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") {
2083 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2084 for (argidx++; argidx < GetSize(args); argidx++)
2085 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2K))
2086 log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
2087 verific_import_pending = true;
2088 goto check_error;
2089 }
2090
2091 if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) {
2092 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
2093 for (argidx++; argidx < GetSize(args); argidx++)
2094 if (!vhdl_file::Analyze(args[argidx].c_str(), work.c_str(), vhdl_file::VHDL_2008))
2095 log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
2096 verific_import_pending = true;
2097 goto check_error;
2098 }
2099
2100 if (GetSize(args) > argidx && args[argidx] == "-import")
2101 {
2102 std::set<Netlist*> nl_todo, nl_done;
2103 bool mode_all = false, mode_gates = false, mode_keep = false;
2104 bool mode_nosva = false, mode_names = false, mode_verific = false;
2105 bool mode_autocover = false;
2106 bool flatten = false, extnets = false;
2107 string dumpfile;
2108
2109 for (argidx++; argidx < GetSize(args); argidx++) {
2110 if (args[argidx] == "-all") {
2111 mode_all = true;
2112 continue;
2113 }
2114 if (args[argidx] == "-gates") {
2115 mode_gates = true;
2116 continue;
2117 }
2118 if (args[argidx] == "-flatten") {
2119 flatten = true;
2120 continue;
2121 }
2122 if (args[argidx] == "-extnets") {
2123 extnets = true;
2124 continue;
2125 }
2126 if (args[argidx] == "-k") {
2127 mode_keep = true;
2128 continue;
2129 }
2130 if (args[argidx] == "-nosva") {
2131 mode_nosva = true;
2132 continue;
2133 }
2134 if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
2135 verific_sva_fsm_limit = atoi(args[++argidx].c_str());
2136 continue;
2137 }
2138 if (args[argidx] == "-n") {
2139 mode_names = true;
2140 continue;
2141 }
2142 if (args[argidx] == "-autocover") {
2143 mode_autocover = true;
2144 continue;
2145 }
2146 if (args[argidx] == "-V") {
2147 mode_verific = true;
2148 continue;
2149 }
2150 if (args[argidx] == "-v") {
2151 verific_verbose = 1;
2152 continue;
2153 }
2154 if (args[argidx] == "-vv") {
2155 verific_verbose = 2;
2156 continue;
2157 }
2158 if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {
2159 dumpfile = args[++argidx];
2160 continue;
2161 }
2162 break;
2163 }
2164
2165 if (argidx > GetSize(args) && args[argidx].substr(0, 1) == "-")
2166 cmd_error(args, argidx, "unknown option");
2167
2168 if (mode_all)
2169 {
2170 log("Running hier_tree::ElaborateAll().\n");
2171
2172 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2173 VeriLibrary *veri_lib = veri_file::GetLibrary(work.c_str(), 1);
2174
2175 Array veri_libs, vhdl_libs;
2176 if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
2177 if (veri_lib) veri_libs.InsertLast(veri_lib);
2178
2179 Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
2180 Netlist *nl;
2181 int i;
2182
2183 FOREACH_ARRAY_ITEM(netlists, i, nl)
2184 nl_todo.insert(nl);
2185 delete netlists;
2186 }
2187 else
2188 {
2189 if (argidx == GetSize(args))
2190 log_cmd_error("No top module specified.\n");
2191
2192 Array veri_modules, vhdl_units;
2193 for (; argidx < GetSize(args); argidx++)
2194 {
2195 const char *name = args[argidx].c_str();
2196
2197 VeriModule *veri_module = veri_file::GetModule(name);
2198 if (veri_module) {
2199 log("Adding Verilog module '%s' to elaboration queue.\n", name);
2200 veri_modules.InsertLast(veri_module);
2201 continue;
2202 }
2203
2204 VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary(work.c_str(), 1);
2205 VhdlDesignUnit *vhdl_unit = vhdl_lib->GetPrimUnit(name);
2206 if (vhdl_unit) {
2207 log("Adding VHDL unit '%s' to elaboration queue.\n", name);
2208 vhdl_units.InsertLast(vhdl_unit);
2209 continue;
2210 }
2211
2212 log_error("Can't find module/unit '%s'.\n", name);
2213 }
2214
2215 log("Running hier_tree::Elaborate().\n");
2216 Array *netlists = hier_tree::Elaborate(&veri_modules, &vhdl_units);
2217 Netlist *nl;
2218 int i;
2219
2220 FOREACH_ARRAY_ITEM(netlists, i, nl)
2221 nl_todo.insert(nl);
2222 delete netlists;
2223 }
2224
2225 if (!verific_error_msg.empty())
2226 goto check_error;
2227
2228 if (flatten) {
2229 for (auto nl : nl_todo)
2230 nl->Flatten();
2231 }
2232
2233 if (extnets) {
2234 VerificExtNets worker;
2235 for (auto nl : nl_todo)
2236 worker.run(nl);
2237 }
2238
2239 if (!dumpfile.empty()) {
2240 VeriWrite veri_writer;
2241 veri_writer.WriteFile(dumpfile.c_str(), Netlist::PresentDesign());
2242 }
2243
2244 while (!nl_todo.empty()) {
2245 Netlist *nl = *nl_todo.begin();
2246 if (nl_done.count(nl) == 0) {
2247 VerificImporter importer(mode_gates, mode_keep, mode_nosva,
2248 mode_names, mode_verific, mode_autocover);
2249 importer.import_netlist(design, nl, nl_todo);
2250 }
2251 nl_todo.erase(nl);
2252 nl_done.insert(nl);
2253 }
2254
2255 veri_file::Reset();
2256 vhdl_file::Reset();
2257 Libset::Reset();
2258 verific_incdirs.clear();
2259 verific_libdirs.clear();
2260 verific_import_pending = false;
2261 goto check_error;
2262 }
2263
2264 log_cmd_error("Missing or unsupported mode parameter.\n");
2265
2266 check_error:
2267 if (!verific_error_msg.empty())
2268 log_error("%s\n", verific_error_msg.c_str());
2269
2270 }
2271 #else /* YOSYS_ENABLE_VERIFIC */
2272 void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
2273 log_cmd_error("This version of Yosys is built without Verific support.\n");
2274 }
2275 #endif
2276 } VerificPass;
2277
2278 struct ReadPass : public Pass {
2279 ReadPass() : Pass("read", "load HDL designs") { }
2280 void help() YS_OVERRIDE
2281 {
2282 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2283 log("\n");
2284 log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
2285 log("\n");
2286 log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
2287 log("is only available via Verific.)\n");
2288 log("\n");
2289 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2290 log("the language version (and before file names) to set additional verilog defines.\n");
2291 log("\n");
2292 log("\n");
2293 log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2294 log("\n");
2295 log("Load the specified VHDL files. (Requires Verific.)\n");
2296 log("\n");
2297 log("\n");
2298 log(" read -define <macro>[=<value>]..\n");
2299 log("\n");
2300 log("Set global Verilog/SystemVerilog defines.\n");
2301 log("\n");
2302 log("\n");
2303 log(" read -undef <macro>..\n");
2304 log("\n");
2305 log("Unset global Verilog/SystemVerilog defines.\n");
2306 log("\n");
2307 log("\n");
2308 log(" read -incdir <directory>\n");
2309 log("\n");
2310 log("Add directory to global Verilog/SystemVerilog include directories.\n");
2311 log("\n");
2312 }
2313 void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
2314 {
2315 if (args.size() < 2)
2316 log_cmd_error("Missing mode parameter.\n");
2317
2318 if (args.size() < 3)
2319 log_cmd_error("Missing file name parameter.\n");
2320
2321 #ifdef YOSYS_ENABLE_VERIFIC
2322 bool use_verific = !check_noverific_env();
2323 #else
2324 bool use_verific = false;
2325 #endif
2326
2327 if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
2328 if (use_verific) {
2329 args[0] = "verific";
2330 } else {
2331 args[0] = "read_verilog";
2332 args.erase(args.begin()+1, args.begin()+2);
2333 }
2334 Pass::call(design, args);
2335 return;
2336 }
2337
2338 if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
2339 if (use_verific) {
2340 args[0] = "verific";
2341 } else {
2342 args[0] = "read_verilog";
2343 if (args[1] == "-formal")
2344 args.insert(args.begin()+1, std::string());
2345 args[1] = "-sv";
2346 }
2347 Pass::call(design, args);
2348 return;
2349 }
2350
2351 if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
2352 if (use_verific) {
2353 args[0] = "verific";
2354 Pass::call(design, args);
2355 } else {
2356 log_cmd_error("This version of Yosys is built without Verific support.\n");
2357 }
2358 return;
2359 }
2360
2361 if (args[1] == "-define") {
2362 if (use_verific) {
2363 args[0] = "verific";
2364 args[1] = "-vlog-define";
2365 Pass::call(design, args);
2366 }
2367 args[0] = "verilog_defines";
2368 args.erase(args.begin()+1, args.begin()+2);
2369 for (int i = 1; i < GetSize(args); i++)
2370 args[i] = "-D" + args[i];
2371 Pass::call(design, args);
2372 return;
2373 }
2374
2375 if (args[1] == "-undef") {
2376 if (use_verific) {
2377 args[0] = "verific";
2378 args[1] = "-vlog-undef";
2379 Pass::call(design, args);
2380 }
2381 args[0] = "verilog_defines";
2382 args.erase(args.begin()+1, args.begin()+2);
2383 for (int i = 1; i < GetSize(args); i++)
2384 args[i] = "-U" + args[i];
2385 Pass::call(design, args);
2386 return;
2387 }
2388
2389 if (args[1] == "-incdir") {
2390 if (use_verific) {
2391 args[0] = "verific";
2392 args[1] = "-vlog-incdir";
2393 Pass::call(design, args);
2394 }
2395 args[0] = "verilog_defaults";
2396 args[1] = "-add";
2397 for (int i = 2; i < GetSize(args); i++)
2398 args[i] = "-I" + args[i];
2399 Pass::call(design, args);
2400 return;
2401 }
2402
2403 log_cmd_error("Missing or unsupported mode parameter.\n");
2404 }
2405 } ReadPass;
2406
2407 PRIVATE_NAMESPACE_END