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