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