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