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