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