2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
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.
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.
20 #include "kernel/yosys.h"
21 #include "kernel/sigtools.h"
22 #include "kernel/celltypes.h"
23 #include "kernel/log.h"
33 #include "frontends/verific/verific.h"
37 #ifdef YOSYS_ENABLE_VERIFIC
40 #pragma clang diagnostic push
41 #pragma clang diagnostic ignored "-Woverloaded-virtual"
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"
52 #ifndef SYMBIOTIC_VERIFIC_API_VERSION
53 # error "Only Symbiotic EDA flavored Verific is supported. Please contact office@symbioticeda.com for commercial support for Yosys+Verific."
56 #if SYMBIOTIC_VERIFIC_API_VERSION < 1
57 # error "Please update your version of Symbiotic EDA flavored Verific."
61 #pragma clang diagnostic pop
64 #ifdef VERIFIC_NAMESPACE
65 using namespace Verific
;
70 #ifdef YOSYS_ENABLE_VERIFIC
74 bool verific_import_pending
;
75 string verific_error_msg
;
76 int verific_sva_fsm_limit
;
78 vector
<string
> verific_incdirs
, verific_libdirs
;
80 void msg_func(msg_type_t msg_type
, const char *message_id
, linefile_type linefile
, const char *msg
, va_list args
)
82 string message_prefix
= stringf("VERIFIC-%s [%s] ",
83 msg_type
== VERIFIC_NONE
? "NONE" :
84 msg_type
== VERIFIC_ERROR
? "ERROR" :
85 msg_type
== VERIFIC_WARNING
? "WARNING" :
86 msg_type
== VERIFIC_IGNORE
? "IGNORE" :
87 msg_type
== VERIFIC_INFO
? "INFO" :
88 msg_type
== VERIFIC_COMMENT
? "COMMENT" :
89 msg_type
== VERIFIC_PROGRAM_ERROR
? "PROGRAM_ERROR" : "UNKNOWN", message_id
);
91 string message
= linefile
? stringf("%s:%d: ", LineFile::GetFileName(linefile
), LineFile::GetLineNo(linefile
)) : "";
92 message
+= vstringf(msg
, args
);
94 if (msg_type
== VERIFIC_ERROR
|| msg_type
== VERIFIC_WARNING
|| msg_type
== VERIFIC_PROGRAM_ERROR
)
95 log_warning_noprefix("%s%s\n", message_prefix
.c_str(), message
.c_str());
97 log("%s%s\n", message_prefix
.c_str(), message
.c_str());
99 if (verific_error_msg
.empty() && (msg_type
== VERIFIC_ERROR
|| msg_type
== VERIFIC_PROGRAM_ERROR
))
100 verific_error_msg
= message
;
103 string
get_full_netlist_name(Netlist
*nl
)
105 if (nl
->NumOfRefs() == 1) {
106 Instance
*inst
= (Instance
*)nl
->GetReferences()->GetLast();
107 return get_full_netlist_name(inst
->Owner()) + "." + inst
->Name();
110 return nl
->CellBaseName();
113 // ==================================================================
115 VerificImporter::VerificImporter(bool mode_gates
, bool mode_keep
, bool mode_nosva
, bool mode_names
, bool mode_verific
, bool mode_autocover
, bool mode_fullinit
) :
116 mode_gates(mode_gates
), mode_keep(mode_keep
), mode_nosva(mode_nosva
),
117 mode_names(mode_names
), mode_verific(mode_verific
), mode_autocover(mode_autocover
),
118 mode_fullinit(mode_fullinit
)
122 RTLIL::SigBit
VerificImporter::net_map_at(Net
*net
)
124 if (net
->IsExternalTo(netlist
))
125 log_error("Found external reference to '%s.%s' in netlist '%s', please use -flatten or -extnets.\n",
126 get_full_netlist_name(net
->Owner()).c_str(), net
->Name(), get_full_netlist_name(netlist
).c_str());
128 return net_map
.at(net
);
131 bool is_blackbox(Netlist
*nl
)
133 if (nl
->IsBlackBox())
136 const char *attr
= nl
->GetAttValue("blackbox");
137 if (attr
!= nullptr && strcmp(attr
, "0"))
143 RTLIL::IdString
VerificImporter::new_verific_id(Verific::DesignObj
*obj
)
145 std::string s
= stringf("$verific$%s", obj
->Name());
147 s
+= stringf("$%s:%d", Verific::LineFile::GetFileName(obj
->Linefile()), Verific::LineFile::GetLineNo(obj
->Linefile()));
148 s
+= stringf("$%d", autoidx
++);
152 void VerificImporter::import_attributes(dict
<RTLIL::IdString
, RTLIL::Const
> &attributes
, DesignObj
*obj
)
158 attributes
["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj
->Linefile()), LineFile::GetLineNo(obj
->Linefile()));
160 // FIXME: Parse numeric attributes
161 FOREACH_ATTRIBUTE(obj
, mi
, attr
) {
162 if (attr
->Key()[0] == ' ' || attr
->Value() == nullptr)
164 attributes
[RTLIL::escape_id(attr
->Key())] = RTLIL::Const(std::string(attr
->Value()));
168 RTLIL::SigSpec
VerificImporter::operatorInput(Instance
*inst
)
171 for (int i
= int(inst
->InputSize())-1; i
>= 0; i
--)
172 if (inst
->GetInputBit(i
))
173 sig
.append(net_map_at(inst
->GetInputBit(i
)));
175 sig
.append(RTLIL::State::Sz
);
179 RTLIL::SigSpec
VerificImporter::operatorInput1(Instance
*inst
)
182 for (int i
= int(inst
->Input1Size())-1; i
>= 0; i
--)
183 if (inst
->GetInput1Bit(i
))
184 sig
.append(net_map_at(inst
->GetInput1Bit(i
)));
186 sig
.append(RTLIL::State::Sz
);
190 RTLIL::SigSpec
VerificImporter::operatorInput2(Instance
*inst
)
193 for (int i
= int(inst
->Input2Size())-1; i
>= 0; i
--)
194 if (inst
->GetInput2Bit(i
))
195 sig
.append(net_map_at(inst
->GetInput2Bit(i
)));
197 sig
.append(RTLIL::State::Sz
);
201 RTLIL::SigSpec
VerificImporter::operatorInport(Instance
*inst
, const char *portname
)
203 PortBus
*portbus
= inst
->View()->GetPortBus(portname
);
206 for (unsigned i
= 0; i
< portbus
->Size(); i
++) {
207 Net
*net
= inst
->GetNet(portbus
->ElementAtIndex(i
));
210 sig
.append(RTLIL::State::S0
);
211 else if (net
->IsPwr())
212 sig
.append(RTLIL::State::S1
);
214 sig
.append(net_map_at(net
));
216 sig
.append(RTLIL::State::Sz
);
220 Port
*port
= inst
->View()->GetPort(portname
);
221 log_assert(port
!= NULL
);
222 Net
*net
= inst
->GetNet(port
);
223 return net_map_at(net
);
227 RTLIL::SigSpec
VerificImporter::operatorOutput(Instance
*inst
, const pool
<Net
*, hash_ptr_ops
> *any_all_nets
)
230 RTLIL::Wire
*dummy_wire
= NULL
;
231 for (int i
= int(inst
->OutputSize())-1; i
>= 0; i
--)
232 if (inst
->GetOutputBit(i
) && (!any_all_nets
|| !any_all_nets
->count(inst
->GetOutputBit(i
)))) {
233 sig
.append(net_map_at(inst
->GetOutputBit(i
)));
236 if (dummy_wire
== NULL
)
237 dummy_wire
= module
->addWire(new_verific_id(inst
));
240 sig
.append(RTLIL::SigSpec(dummy_wire
, dummy_wire
->width
- 1));
245 bool VerificImporter::import_netlist_instance_gates(Instance
*inst
, RTLIL::IdString inst_name
)
247 if (inst
->Type() == PRIM_AND
) {
248 module
->addAndGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
252 if (inst
->Type() == PRIM_NAND
) {
253 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
));
254 module
->addAndGate(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), tmp
);
255 module
->addNotGate(inst_name
, tmp
, net_map_at(inst
->GetOutput()));
259 if (inst
->Type() == PRIM_OR
) {
260 module
->addOrGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
264 if (inst
->Type() == PRIM_NOR
) {
265 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
));
266 module
->addOrGate(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), tmp
);
267 module
->addNotGate(inst_name
, tmp
, net_map_at(inst
->GetOutput()));
271 if (inst
->Type() == PRIM_XOR
) {
272 module
->addXorGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
276 if (inst
->Type() == PRIM_XNOR
) {
277 module
->addXnorGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
281 if (inst
->Type() == PRIM_BUF
) {
282 auto outnet
= inst
->GetOutput();
283 if (!any_all_nets
.count(outnet
))
284 module
->addBufGate(inst_name
, net_map_at(inst
->GetInput()), net_map_at(outnet
));
288 if (inst
->Type() == PRIM_INV
) {
289 module
->addNotGate(inst_name
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
293 if (inst
->Type() == PRIM_MUX
) {
294 module
->addMuxGate(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetControl()), net_map_at(inst
->GetOutput()));
298 if (inst
->Type() == PRIM_TRI
) {
299 module
->addMuxGate(inst_name
, RTLIL::State::Sz
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetControl()), net_map_at(inst
->GetOutput()));
303 if (inst
->Type() == PRIM_FADD
)
305 RTLIL::SigSpec a
= net_map_at(inst
->GetInput1()), b
= net_map_at(inst
->GetInput2()), c
= net_map_at(inst
->GetCin());
306 RTLIL::SigSpec x
= inst
->GetCout() ? net_map_at(inst
->GetCout()) : module
->addWire(new_verific_id(inst
));
307 RTLIL::SigSpec y
= inst
->GetOutput() ? net_map_at(inst
->GetOutput()) : module
->addWire(new_verific_id(inst
));
308 RTLIL::SigSpec tmp1
= module
->addWire(new_verific_id(inst
));
309 RTLIL::SigSpec tmp2
= module
->addWire(new_verific_id(inst
));
310 RTLIL::SigSpec tmp3
= module
->addWire(new_verific_id(inst
));
311 module
->addXorGate(new_verific_id(inst
), a
, b
, tmp1
);
312 module
->addXorGate(inst_name
, tmp1
, c
, y
);
313 module
->addAndGate(new_verific_id(inst
), tmp1
, c
, tmp2
);
314 module
->addAndGate(new_verific_id(inst
), a
, b
, tmp3
);
315 module
->addOrGate(new_verific_id(inst
), tmp2
, tmp3
, x
);
319 if (inst
->Type() == PRIM_DFFRS
)
321 VerificClocking
clocking(this, inst
->GetClock());
322 log_assert(clocking
.disable_sig
== State::S0
);
323 log_assert(clocking
.body_net
== nullptr);
325 if (inst
->GetSet()->IsGnd() && inst
->GetReset()->IsGnd())
326 clocking
.addDff(inst_name
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
327 else if (inst
->GetSet()->IsGnd())
328 clocking
.addAdff(inst_name
, net_map_at(inst
->GetReset()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()), State::S0
);
329 else if (inst
->GetReset()->IsGnd())
330 clocking
.addAdff(inst_name
, net_map_at(inst
->GetSet()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()), State::S1
);
332 clocking
.addDffsr(inst_name
, net_map_at(inst
->GetSet()), net_map_at(inst
->GetReset()),
333 net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
340 bool VerificImporter::import_netlist_instance_cells(Instance
*inst
, RTLIL::IdString inst_name
)
342 RTLIL::Cell
*cell
= nullptr;
344 if (inst
->Type() == PRIM_AND
) {
345 cell
= module
->addAnd(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
346 import_attributes(cell
->attributes
, inst
);
350 if (inst
->Type() == PRIM_NAND
) {
351 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
));
352 cell
= module
->addAnd(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), tmp
);
353 import_attributes(cell
->attributes
, inst
);
354 cell
= module
->addNot(inst_name
, tmp
, net_map_at(inst
->GetOutput()));
355 import_attributes(cell
->attributes
, inst
);
359 if (inst
->Type() == PRIM_OR
) {
360 cell
= module
->addOr(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
361 import_attributes(cell
->attributes
, inst
);
365 if (inst
->Type() == PRIM_NOR
) {
366 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
));
367 cell
= module
->addOr(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), tmp
);
368 import_attributes(cell
->attributes
, inst
);
369 cell
= module
->addNot(inst_name
, tmp
, net_map_at(inst
->GetOutput()));
370 import_attributes(cell
->attributes
, inst
);
374 if (inst
->Type() == PRIM_XOR
) {
375 cell
= module
->addXor(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
376 import_attributes(cell
->attributes
, inst
);
380 if (inst
->Type() == PRIM_XNOR
) {
381 cell
= module
->addXnor(inst_name
, net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), net_map_at(inst
->GetOutput()));
382 import_attributes(cell
->attributes
, inst
);
386 if (inst
->Type() == PRIM_INV
) {
387 cell
= module
->addNot(inst_name
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
388 import_attributes(cell
->attributes
, inst
);
392 if (inst
->Type() == PRIM_MUX
) {
393 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()));
394 import_attributes(cell
->attributes
, inst
);
398 if (inst
->Type() == PRIM_TRI
) {
399 cell
= module
->addMux(inst_name
, RTLIL::State::Sz
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetControl()), net_map_at(inst
->GetOutput()));
400 import_attributes(cell
->attributes
, inst
);
404 if (inst
->Type() == PRIM_FADD
)
406 RTLIL::SigSpec a_plus_b
= module
->addWire(new_verific_id(inst
), 2);
407 RTLIL::SigSpec y
= inst
->GetOutput() ? net_map_at(inst
->GetOutput()) : module
->addWire(new_verific_id(inst
));
409 y
.append(net_map_at(inst
->GetCout()));
410 cell
= module
->addAdd(new_verific_id(inst
), net_map_at(inst
->GetInput1()), net_map_at(inst
->GetInput2()), a_plus_b
);
411 import_attributes(cell
->attributes
, inst
);
412 cell
= module
->addAdd(inst_name
, a_plus_b
, net_map_at(inst
->GetCin()), y
);
413 import_attributes(cell
->attributes
, inst
);
417 if (inst
->Type() == PRIM_DFFRS
)
419 VerificClocking
clocking(this, inst
->GetClock());
420 log_assert(clocking
.disable_sig
== State::S0
);
421 log_assert(clocking
.body_net
== nullptr);
423 if (inst
->GetSet()->IsGnd() && inst
->GetReset()->IsGnd())
424 cell
= clocking
.addDff(inst_name
, net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
425 else if (inst
->GetSet()->IsGnd())
426 cell
= clocking
.addAdff(inst_name
, net_map_at(inst
->GetReset()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()), RTLIL::State::S0
);
427 else if (inst
->GetReset()->IsGnd())
428 cell
= clocking
.addAdff(inst_name
, net_map_at(inst
->GetSet()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()), RTLIL::State::S1
);
430 cell
= clocking
.addDffsr(inst_name
, net_map_at(inst
->GetSet()), net_map_at(inst
->GetReset()),
431 net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
432 import_attributes(cell
->attributes
, inst
);
436 if (inst
->Type() == PRIM_DLATCHRS
)
438 if (inst
->GetSet()->IsGnd() && inst
->GetReset()->IsGnd())
439 cell
= module
->addDlatch(inst_name
, net_map_at(inst
->GetControl()), net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
441 cell
= module
->addDlatchsr(inst_name
, net_map_at(inst
->GetControl()), net_map_at(inst
->GetSet()), net_map_at(inst
->GetReset()),
442 net_map_at(inst
->GetInput()), net_map_at(inst
->GetOutput()));
443 import_attributes(cell
->attributes
, inst
);
447 #define IN operatorInput(inst)
448 #define IN1 operatorInput1(inst)
449 #define IN2 operatorInput2(inst)
450 #define OUT operatorOutput(inst)
451 #define FILTERED_OUT operatorOutput(inst, &any_all_nets)
452 #define SIGNED inst->View()->IsSigned()
454 if (inst
->Type() == OPER_ADDER
) {
455 RTLIL::SigSpec out
= OUT
;
456 if (inst
->GetCout() != NULL
)
457 out
.append(net_map_at(inst
->GetCout()));
458 if (inst
->GetCin()->IsGnd()) {
459 cell
= module
->addAdd(inst_name
, IN1
, IN2
, out
, SIGNED
);
460 import_attributes(cell
->attributes
, inst
);
462 RTLIL::SigSpec tmp
= module
->addWire(new_verific_id(inst
), GetSize(out
));
463 cell
= module
->addAdd(new_verific_id(inst
), IN1
, IN2
, tmp
, SIGNED
);
464 import_attributes(cell
->attributes
, inst
);
465 cell
= module
->addAdd(inst_name
, tmp
, net_map_at(inst
->GetCin()), out
, false);
466 import_attributes(cell
->attributes
, inst
);
471 if (inst
->Type() == OPER_MULTIPLIER
) {
472 cell
= module
->addMul(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
473 import_attributes(cell
->attributes
, inst
);
477 if (inst
->Type() == OPER_DIVIDER
) {
478 cell
= module
->addDiv(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
479 import_attributes(cell
->attributes
, inst
);
483 if (inst
->Type() == OPER_MODULO
) {
484 cell
= module
->addMod(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
485 import_attributes(cell
->attributes
, inst
);
489 if (inst
->Type() == OPER_REMAINDER
) {
490 cell
= module
->addMod(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
491 import_attributes(cell
->attributes
, inst
);
495 if (inst
->Type() == OPER_SHIFT_LEFT
) {
496 cell
= module
->addShl(inst_name
, IN1
, IN2
, OUT
, false);
497 import_attributes(cell
->attributes
, inst
);
501 if (inst
->Type() == OPER_ENABLED_DECODER
) {
503 vec
.append(net_map_at(inst
->GetControl()));
504 for (unsigned i
= 1; i
< inst
->OutputSize(); i
++) {
505 vec
.append(RTLIL::State::S0
);
507 cell
= module
->addShl(inst_name
, vec
, IN
, OUT
, false);
508 import_attributes(cell
->attributes
, inst
);
512 if (inst
->Type() == OPER_DECODER
) {
514 vec
.append(RTLIL::State::S1
);
515 for (unsigned i
= 1; i
< inst
->OutputSize(); i
++) {
516 vec
.append(RTLIL::State::S0
);
518 cell
= module
->addShl(inst_name
, vec
, IN
, OUT
, false);
519 import_attributes(cell
->attributes
, inst
);
523 if (inst
->Type() == OPER_SHIFT_RIGHT
) {
524 Net
*net_cin
= inst
->GetCin();
525 Net
*net_a_msb
= inst
->GetInput1Bit(0);
526 if (net_cin
->IsGnd())
527 cell
= module
->addShr(inst_name
, IN1
, IN2
, OUT
, false);
528 else if (net_cin
== net_a_msb
)
529 cell
= module
->addSshr(inst_name
, IN1
, IN2
, OUT
, true);
531 log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst
->Name());
532 import_attributes(cell
->attributes
, inst
);
536 if (inst
->Type() == OPER_REDUCE_AND
) {
537 cell
= module
->addReduceAnd(inst_name
, IN
, net_map_at(inst
->GetOutput()), SIGNED
);
538 import_attributes(cell
->attributes
, inst
);
542 if (inst
->Type() == OPER_REDUCE_OR
) {
543 cell
= module
->addReduceOr(inst_name
, IN
, net_map_at(inst
->GetOutput()), SIGNED
);
544 import_attributes(cell
->attributes
, inst
);
548 if (inst
->Type() == OPER_REDUCE_XOR
) {
549 cell
= module
->addReduceXor(inst_name
, IN
, net_map_at(inst
->GetOutput()), SIGNED
);
550 import_attributes(cell
->attributes
, inst
);
554 if (inst
->Type() == OPER_REDUCE_XNOR
) {
555 cell
= module
->addReduceXnor(inst_name
, IN
, net_map_at(inst
->GetOutput()), SIGNED
);
556 import_attributes(cell
->attributes
, inst
);
560 if (inst
->Type() == OPER_REDUCE_NOR
) {
561 SigSpec t
= module
->ReduceOr(new_verific_id(inst
), IN
, SIGNED
);
562 cell
= module
->addNot(inst_name
, t
, net_map_at(inst
->GetOutput()));
563 import_attributes(cell
->attributes
, inst
);
567 if (inst
->Type() == OPER_LESSTHAN
) {
568 Net
*net_cin
= inst
->GetCin();
569 if (net_cin
->IsGnd())
570 cell
= module
->addLt(inst_name
, IN1
, IN2
, net_map_at(inst
->GetOutput()), SIGNED
);
571 else if (net_cin
->IsPwr())
572 cell
= module
->addLe(inst_name
, IN1
, IN2
, net_map_at(inst
->GetOutput()), SIGNED
);
574 log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst
->Name());
575 import_attributes(cell
->attributes
, inst
);
579 if (inst
->Type() == OPER_WIDE_AND
) {
580 cell
= module
->addAnd(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
581 import_attributes(cell
->attributes
, inst
);
585 if (inst
->Type() == OPER_WIDE_OR
) {
586 cell
= module
->addOr(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
587 import_attributes(cell
->attributes
, inst
);
591 if (inst
->Type() == OPER_WIDE_XOR
) {
592 cell
= module
->addXor(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
593 import_attributes(cell
->attributes
, inst
);
597 if (inst
->Type() == OPER_WIDE_XNOR
) {
598 cell
= module
->addXnor(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
599 import_attributes(cell
->attributes
, inst
);
603 if (inst
->Type() == OPER_WIDE_BUF
) {
604 cell
= module
->addPos(inst_name
, IN
, FILTERED_OUT
, SIGNED
);
605 import_attributes(cell
->attributes
, inst
);
609 if (inst
->Type() == OPER_WIDE_INV
) {
610 cell
= module
->addNot(inst_name
, IN
, OUT
, SIGNED
);
611 import_attributes(cell
->attributes
, inst
);
615 if (inst
->Type() == OPER_MINUS
) {
616 cell
= module
->addSub(inst_name
, IN1
, IN2
, OUT
, SIGNED
);
617 import_attributes(cell
->attributes
, inst
);
621 if (inst
->Type() == OPER_UMINUS
) {
622 cell
= module
->addNeg(inst_name
, IN
, OUT
, SIGNED
);
623 import_attributes(cell
->attributes
, inst
);
627 if (inst
->Type() == OPER_EQUAL
) {
628 cell
= module
->addEq(inst_name
, IN1
, IN2
, net_map_at(inst
->GetOutput()), SIGNED
);
629 import_attributes(cell
->attributes
, inst
);
633 if (inst
->Type() == OPER_NEQUAL
) {
634 cell
= module
->addNe(inst_name
, IN1
, IN2
, net_map_at(inst
->GetOutput()), SIGNED
);
635 import_attributes(cell
->attributes
, inst
);
639 if (inst
->Type() == OPER_WIDE_MUX
) {
640 cell
= module
->addMux(inst_name
, IN1
, IN2
, net_map_at(inst
->GetControl()), OUT
);
641 import_attributes(cell
->attributes
, inst
);
645 if (inst
->Type() == OPER_NTO1MUX
) {
646 cell
= module
->addShr(inst_name
, IN2
, IN1
, net_map_at(inst
->GetOutput()));
647 import_attributes(cell
->attributes
, inst
);
651 if (inst
->Type() == OPER_WIDE_NTO1MUX
)
653 SigSpec data
= IN2
, out
= OUT
;
655 int wordsize_bits
= ceil_log2(GetSize(out
));
656 int wordsize
= 1 << wordsize_bits
;
658 SigSpec sel
= {IN1
, SigSpec(State::S0
, wordsize_bits
)};
661 for (int i
= 0; i
< GetSize(data
); i
+= GetSize(out
)) {
662 SigSpec d
= data
.extract(i
, GetSize(out
));
663 d
.extend_u0(wordsize
);
664 padded_data
.append(d
);
667 cell
= module
->addShr(inst_name
, padded_data
, sel
, out
);
668 import_attributes(cell
->attributes
, inst
);
672 if (inst
->Type() == OPER_SELECTOR
)
674 cell
= module
->addPmux(inst_name
, State::S0
, IN2
, IN1
, net_map_at(inst
->GetOutput()));
675 import_attributes(cell
->attributes
, inst
);
679 if (inst
->Type() == OPER_WIDE_SELECTOR
)
682 cell
= module
->addPmux(inst_name
, SigSpec(State::S0
, GetSize(out
)), IN2
, IN1
, out
);
683 import_attributes(cell
->attributes
, inst
);
687 if (inst
->Type() == OPER_WIDE_TRI
) {
688 cell
= module
->addMux(inst_name
, RTLIL::SigSpec(RTLIL::State::Sz
, inst
->OutputSize()), IN
, net_map_at(inst
->GetControl()), OUT
);
689 import_attributes(cell
->attributes
, inst
);
693 if (inst
->Type() == OPER_WIDE_DFFRS
)
695 VerificClocking
clocking(this, inst
->GetClock());
696 log_assert(clocking
.disable_sig
== State::S0
);
697 log_assert(clocking
.body_net
== nullptr);
699 RTLIL::SigSpec sig_set
= operatorInport(inst
, "set");
700 RTLIL::SigSpec sig_reset
= operatorInport(inst
, "reset");
702 if (sig_set
.is_fully_const() && !sig_set
.as_bool() && sig_reset
.is_fully_const() && !sig_reset
.as_bool())
703 cell
= clocking
.addDff(inst_name
, IN
, OUT
);
705 cell
= clocking
.addDffsr(inst_name
, sig_set
, sig_reset
, IN
, OUT
);
706 import_attributes(cell
->attributes
, inst
);
720 void VerificImporter::merge_past_ffs_clock(pool
<RTLIL::Cell
*> &candidates
, SigBit clock
, bool clock_pol
)
722 bool keep_running
= true;
727 keep_running
= false;
729 dict
<SigBit
, pool
<RTLIL::Cell
*>> dbits_db
;
732 for (auto cell
: candidates
) {
733 SigBit bit
= sigmap(cell
->getPort("\\D"));
734 dbits_db
[bit
].insert(cell
);
738 dbits
.sort_and_unify();
740 for (auto chunk
: dbits
.chunks())
742 SigSpec sig_d
= chunk
;
744 if (chunk
.wire
== nullptr || GetSize(sig_d
) == 1)
747 SigSpec sig_q
= module
->addWire(NEW_ID
, GetSize(sig_d
));
748 RTLIL::Cell
*new_ff
= module
->addDff(NEW_ID
, clock
, sig_d
, sig_q
, clock_pol
);
751 log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d
), log_id(new_ff
));
753 for (int i
= 0; i
< GetSize(sig_d
); i
++)
754 for (auto old_ff
: dbits_db
[sig_d
[i
]])
757 log(" replacing old ff %s on bit %d.\n", log_id(old_ff
), i
);
759 SigBit old_q
= old_ff
->getPort("\\Q");
760 SigBit new_q
= sig_q
[i
];
762 sigmap
.add(old_q
, new_q
);
763 module
->connect(old_q
, new_q
);
764 candidates
.erase(old_ff
);
765 module
->remove(old_ff
);
772 void VerificImporter::merge_past_ffs(pool
<RTLIL::Cell
*> &candidates
)
774 dict
<pair
<SigBit
, int>, pool
<RTLIL::Cell
*>> database
;
776 for (auto cell
: candidates
)
778 SigBit clock
= cell
->getPort("\\CLK");
779 bool clock_pol
= cell
->getParam("\\CLK_POLARITY").as_bool();
780 database
[make_pair(clock
, int(clock_pol
))].insert(cell
);
783 for (auto it
: database
)
784 merge_past_ffs_clock(it
.second
, it
.first
.first
, it
.first
.second
);
787 void VerificImporter::import_netlist(RTLIL::Design
*design
, Netlist
*nl
, std::set
<Netlist
*> &nl_todo
)
789 std::string netlist_name
= nl
->GetAtt(" \\top") ? nl
->CellBaseName() : nl
->Owner()->Name();
790 std::string module_name
= nl
->IsOperator() ? "$verific$" + netlist_name
: RTLIL::escape_id(netlist_name
);
794 if (design
->has(module_name
)) {
795 if (!nl
->IsOperator() && !is_blackbox(nl
))
796 log_cmd_error("Re-definition of module `%s'.\n", netlist_name
.c_str());
800 module
= new RTLIL::Module
;
801 module
->name
= module_name
;
804 if (is_blackbox(nl
)) {
805 log("Importing blackbox module %s.\n", RTLIL::id2cstr(module
->name
));
806 module
->set_bool_attribute("\\blackbox");
808 log("Importing module %s.\n", RTLIL::id2cstr(module
->name
));
820 FOREACH_PORT_OF_NETLIST(nl
, mi
, port
)
826 log(" importing port %s.\n", port
->Name());
828 RTLIL::Wire
*wire
= module
->addWire(RTLIL::escape_id(port
->Name()));
829 import_attributes(wire
->attributes
, port
);
831 wire
->port_id
= nl
->IndexOf(port
) + 1;
833 if (port
->GetDir() == DIR_INOUT
|| port
->GetDir() == DIR_IN
)
834 wire
->port_input
= true;
835 if (port
->GetDir() == DIR_INOUT
|| port
->GetDir() == DIR_OUT
)
836 wire
->port_output
= true;
838 if (port
->GetNet()) {
839 net
= port
->GetNet();
840 if (net_map
.count(net
) == 0)
842 else if (wire
->port_input
)
843 module
->connect(net_map_at(net
), wire
);
845 module
->connect(wire
, net_map_at(net
));
849 FOREACH_PORTBUS_OF_NETLIST(nl
, mi
, portbus
)
852 log(" importing portbus %s.\n", portbus
->Name());
854 RTLIL::Wire
*wire
= module
->addWire(RTLIL::escape_id(portbus
->Name()), portbus
->Size());
855 wire
->start_offset
= min(portbus
->LeftIndex(), portbus
->RightIndex());
856 import_attributes(wire
->attributes
, portbus
);
858 if (portbus
->GetDir() == DIR_INOUT
|| portbus
->GetDir() == DIR_IN
)
859 wire
->port_input
= true;
860 if (portbus
->GetDir() == DIR_INOUT
|| portbus
->GetDir() == DIR_OUT
)
861 wire
->port_output
= true;
863 for (int i
= portbus
->LeftIndex();; i
+= portbus
->IsUp() ? +1 : -1) {
864 if (portbus
->ElementAtIndex(i
) && portbus
->ElementAtIndex(i
)->GetNet()) {
865 net
= portbus
->ElementAtIndex(i
)->GetNet();
866 RTLIL::SigBit
bit(wire
, i
- wire
->start_offset
);
867 if (net_map
.count(net
) == 0)
869 else if (wire
->port_input
)
870 module
->connect(net_map_at(net
), bit
);
872 module
->connect(bit
, net_map_at(net
));
874 if (i
== portbus
->RightIndex())
879 module
->fixup_ports();
881 dict
<Net
*, char, hash_ptr_ops
> init_nets
;
882 pool
<Net
*, hash_ptr_ops
> anyconst_nets
, anyseq_nets
;
883 pool
<Net
*, hash_ptr_ops
> allconst_nets
, allseq_nets
;
884 any_all_nets
.clear();
886 FOREACH_NET_OF_NETLIST(nl
, mi
, net
)
890 RTLIL::Memory
*memory
= new RTLIL::Memory
;
891 memory
->name
= RTLIL::escape_id(net
->Name());
892 log_assert(module
->count_id(memory
->name
) == 0);
893 module
->memories
[memory
->name
] = memory
;
895 int number_of_bits
= net
->Size();
896 int bits_in_word
= number_of_bits
;
897 FOREACH_PORTREF_OF_NET(net
, si
, pr
) {
898 if (pr
->GetInst()->Type() == OPER_READ_PORT
) {
899 bits_in_word
= min
<int>(bits_in_word
, pr
->GetInst()->OutputSize());
902 if (pr
->GetInst()->Type() == OPER_WRITE_PORT
|| pr
->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT
) {
903 bits_in_word
= min
<int>(bits_in_word
, pr
->GetInst()->Input2Size());
906 log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
907 net
->Name(), pr
->GetInst()->View()->Owner()->Name(), pr
->GetInst()->Name());
910 memory
->width
= bits_in_word
;
911 memory
->size
= number_of_bits
/ bits_in_word
;
913 const char *ascii_initdata
= net
->GetWideInitialValue();
914 if (ascii_initdata
) {
915 while (*ascii_initdata
!= 0 && *ascii_initdata
!= '\'')
917 if (*ascii_initdata
== '\'')
919 if (*ascii_initdata
!= 0) {
920 log_assert(*ascii_initdata
== 'b');
923 for (int word_idx
= 0; word_idx
< memory
->size
; word_idx
++) {
924 Const initval
= Const(State::Sx
, memory
->width
);
925 bool initval_valid
= false;
926 for (int bit_idx
= memory
->width
-1; bit_idx
>= 0; bit_idx
--) {
927 if (*ascii_initdata
== 0)
929 if (*ascii_initdata
== '0' || *ascii_initdata
== '1') {
930 initval
[bit_idx
] = (*ascii_initdata
== '0') ? State::S0
: State::S1
;
931 initval_valid
= true;
936 RTLIL::Cell
*cell
= module
->addCell(new_verific_id(net
), "$meminit");
937 cell
->parameters
["\\WORDS"] = 1;
938 if (net
->GetOrigTypeRange()->LeftRangeBound() < net
->GetOrigTypeRange()->RightRangeBound())
939 cell
->setPort("\\ADDR", word_idx
);
941 cell
->setPort("\\ADDR", memory
->size
- word_idx
- 1);
942 cell
->setPort("\\DATA", initval
);
943 cell
->parameters
["\\MEMID"] = RTLIL::Const(memory
->name
.str());
944 cell
->parameters
["\\ABITS"] = 32;
945 cell
->parameters
["\\WIDTH"] = memory
->width
;
946 cell
->parameters
["\\PRIORITY"] = RTLIL::Const(autoidx
-1);
953 if (net
->GetInitialValue())
954 init_nets
[net
] = net
->GetInitialValue();
956 const char *rand_const_attr
= net
->GetAttValue(" rand_const");
957 const char *rand_attr
= net
->GetAttValue(" rand");
959 const char *anyconst_attr
= net
->GetAttValue("anyconst");
960 const char *anyseq_attr
= net
->GetAttValue("anyseq");
962 const char *allconst_attr
= net
->GetAttValue("allconst");
963 const char *allseq_attr
= net
->GetAttValue("allseq");
965 if (rand_const_attr
!= nullptr && (!strcmp(rand_const_attr
, "1") || !strcmp(rand_const_attr
, "'1'"))) {
966 anyconst_nets
.insert(net
);
967 any_all_nets
.insert(net
);
969 else if (rand_attr
!= nullptr && (!strcmp(rand_attr
, "1") || !strcmp(rand_attr
, "'1'"))) {
970 anyseq_nets
.insert(net
);
971 any_all_nets
.insert(net
);
973 else if (anyconst_attr
!= nullptr && (!strcmp(anyconst_attr
, "1") || !strcmp(anyconst_attr
, "'1'"))) {
974 anyconst_nets
.insert(net
);
975 any_all_nets
.insert(net
);
977 else if (anyseq_attr
!= nullptr && (!strcmp(anyseq_attr
, "1") || !strcmp(anyseq_attr
, "'1'"))) {
978 anyseq_nets
.insert(net
);
979 any_all_nets
.insert(net
);
981 else if (allconst_attr
!= nullptr && (!strcmp(allconst_attr
, "1") || !strcmp(allconst_attr
, "'1'"))) {
982 allconst_nets
.insert(net
);
983 any_all_nets
.insert(net
);
985 else if (allseq_attr
!= nullptr && (!strcmp(allseq_attr
, "1") || !strcmp(allseq_attr
, "'1'"))) {
986 allseq_nets
.insert(net
);
987 any_all_nets
.insert(net
);
990 if (net_map
.count(net
)) {
992 log(" skipping net %s.\n", net
->Name());
999 RTLIL::IdString wire_name
= module
->uniquify(mode_names
|| net
->IsUserDeclared() ? RTLIL::escape_id(net
->Name()) : new_verific_id(net
));
1001 if (verific_verbose
)
1002 log(" importing net %s as %s.\n", net
->Name(), log_id(wire_name
));
1004 RTLIL::Wire
*wire
= module
->addWire(wire_name
);
1005 import_attributes(wire
->attributes
, net
);
1007 net_map
[net
] = wire
;
1010 FOREACH_NETBUS_OF_NETLIST(nl
, mi
, netbus
)
1012 bool found_new_net
= false;
1013 for (int i
= netbus
->LeftIndex();; i
+= netbus
->IsUp() ? +1 : -1) {
1014 net
= netbus
->ElementAtIndex(i
);
1015 if (net_map
.count(net
) == 0)
1016 found_new_net
= true;
1017 if (i
== netbus
->RightIndex())
1023 RTLIL::IdString wire_name
= module
->uniquify(mode_names
|| netbus
->IsUserDeclared() ? RTLIL::escape_id(netbus
->Name()) : new_verific_id(netbus
));
1025 if (verific_verbose
)
1026 log(" importing netbus %s as %s.\n", netbus
->Name(), log_id(wire_name
));
1028 RTLIL::Wire
*wire
= module
->addWire(wire_name
, netbus
->Size());
1029 wire
->start_offset
= min(netbus
->LeftIndex(), netbus
->RightIndex());
1030 import_attributes(wire
->attributes
, netbus
);
1032 RTLIL::Const initval
= Const(State::Sx
, GetSize(wire
));
1033 bool initval_valid
= false;
1035 for (int i
= netbus
->LeftIndex();; i
+= netbus
->IsUp() ? +1 : -1)
1037 if (netbus
->ElementAtIndex(i
))
1039 int bitidx
= i
- wire
->start_offset
;
1040 net
= netbus
->ElementAtIndex(i
);
1041 RTLIL::SigBit
bit(wire
, bitidx
);
1043 if (init_nets
.count(net
)) {
1044 if (init_nets
.at(net
) == '0')
1045 initval
.bits
.at(bitidx
) = State::S0
;
1046 if (init_nets
.at(net
) == '1')
1047 initval
.bits
.at(bitidx
) = State::S1
;
1048 initval_valid
= true;
1049 init_nets
.erase(net
);
1052 if (net_map
.count(net
) == 0)
1055 module
->connect(bit
, net_map_at(net
));
1058 if (i
== netbus
->RightIndex())
1063 wire
->attributes
["\\init"] = initval
;
1067 if (verific_verbose
)
1068 log(" skipping netbus %s.\n", netbus
->Name());
1071 SigSpec anyconst_sig
;
1073 SigSpec allconst_sig
;
1076 for (int i
= netbus
->RightIndex();; i
+= netbus
->IsUp() ? -1 : +1) {
1077 net
= netbus
->ElementAtIndex(i
);
1078 if (net
!= nullptr && anyconst_nets
.count(net
)) {
1079 anyconst_sig
.append(net_map_at(net
));
1080 anyconst_nets
.erase(net
);
1082 if (net
!= nullptr && anyseq_nets
.count(net
)) {
1083 anyseq_sig
.append(net_map_at(net
));
1084 anyseq_nets
.erase(net
);
1086 if (net
!= nullptr && allconst_nets
.count(net
)) {
1087 allconst_sig
.append(net_map_at(net
));
1088 allconst_nets
.erase(net
);
1090 if (net
!= nullptr && allseq_nets
.count(net
)) {
1091 allseq_sig
.append(net_map_at(net
));
1092 allseq_nets
.erase(net
);
1094 if (i
== netbus
->LeftIndex())
1098 if (GetSize(anyconst_sig
))
1099 module
->connect(anyconst_sig
, module
->Anyconst(new_verific_id(netbus
), GetSize(anyconst_sig
)));
1101 if (GetSize(anyseq_sig
))
1102 module
->connect(anyseq_sig
, module
->Anyseq(new_verific_id(netbus
), GetSize(anyseq_sig
)));
1104 if (GetSize(allconst_sig
))
1105 module
->connect(allconst_sig
, module
->Allconst(new_verific_id(netbus
), GetSize(allconst_sig
)));
1107 if (GetSize(allseq_sig
))
1108 module
->connect(allseq_sig
, module
->Allseq(new_verific_id(netbus
), GetSize(allseq_sig
)));
1111 for (auto it
: init_nets
)
1114 SigBit bit
= net_map_at(it
.first
);
1115 log_assert(bit
.wire
);
1117 if (bit
.wire
->attributes
.count("\\init"))
1118 initval
= bit
.wire
->attributes
.at("\\init");
1120 while (GetSize(initval
) < GetSize(bit
.wire
))
1121 initval
.bits
.push_back(State::Sx
);
1123 if (it
.second
== '0')
1124 initval
.bits
.at(bit
.offset
) = State::S0
;
1125 if (it
.second
== '1')
1126 initval
.bits
.at(bit
.offset
) = State::S1
;
1128 bit
.wire
->attributes
["\\init"] = initval
;
1131 for (auto net
: anyconst_nets
)
1132 module
->connect(net_map_at(net
), module
->Anyconst(new_verific_id(net
)));
1134 for (auto net
: anyseq_nets
)
1135 module
->connect(net_map_at(net
), module
->Anyseq(new_verific_id(net
)));
1137 pool
<Instance
*, hash_ptr_ops
> sva_asserts
;
1138 pool
<Instance
*, hash_ptr_ops
> sva_assumes
;
1139 pool
<Instance
*, hash_ptr_ops
> sva_covers
;
1140 pool
<Instance
*, hash_ptr_ops
> sva_triggers
;
1142 pool
<RTLIL::Cell
*> past_ffs
;
1144 FOREACH_INSTANCE_OF_NETLIST(nl
, mi
, inst
)
1146 RTLIL::IdString inst_name
= module
->uniquify(mode_names
|| inst
->IsUserDeclared() ? RTLIL::escape_id(inst
->Name()) : new_verific_id(inst
));
1148 if (verific_verbose
)
1149 log(" importing cell %s (%s) as %s.\n", inst
->Name(), inst
->View()->Owner()->Name(), log_id(inst_name
));
1152 goto import_verific_cells
;
1154 if (inst
->Type() == PRIM_PWR
) {
1155 module
->connect(net_map_at(inst
->GetOutput()), RTLIL::State::S1
);
1159 if (inst
->Type() == PRIM_GND
) {
1160 module
->connect(net_map_at(inst
->GetOutput()), RTLIL::State::S0
);
1164 if (inst
->Type() == PRIM_BUF
) {
1165 auto outnet
= inst
->GetOutput();
1166 if (!any_all_nets
.count(outnet
))
1167 module
->addBufGate(inst_name
, net_map_at(inst
->GetInput()), net_map_at(outnet
));
1171 if (inst
->Type() == PRIM_X
) {
1172 module
->connect(net_map_at(inst
->GetOutput()), RTLIL::State::Sx
);
1176 if (inst
->Type() == PRIM_Z
) {
1177 module
->connect(net_map_at(inst
->GetOutput()), RTLIL::State::Sz
);
1181 if (inst
->Type() == OPER_READ_PORT
)
1183 RTLIL::Memory
*memory
= module
->memories
.at(RTLIL::escape_id(inst
->GetInput()->Name()));
1184 int numchunks
= int(inst
->OutputSize()) / memory
->width
;
1185 int chunksbits
= ceil_log2(numchunks
);
1187 if ((numchunks
* memory
->width
) != int(inst
->OutputSize()) || (numchunks
& (numchunks
- 1)) != 0)
1188 log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst
->Name(), inst
->GetInput()->Name());
1190 for (int i
= 0; i
< numchunks
; i
++)
1192 RTLIL::SigSpec addr
= {operatorInput1(inst
), RTLIL::Const(i
, chunksbits
)};
1193 RTLIL::SigSpec data
= operatorOutput(inst
).extract(i
* memory
->width
, memory
->width
);
1195 RTLIL::Cell
*cell
= module
->addCell(numchunks
== 1 ? inst_name
:
1196 RTLIL::IdString(stringf("%s_%d", inst_name
.c_str(), i
)), "$memrd");
1197 cell
->parameters
["\\MEMID"] = memory
->name
.str();
1198 cell
->parameters
["\\CLK_ENABLE"] = false;
1199 cell
->parameters
["\\CLK_POLARITY"] = true;
1200 cell
->parameters
["\\TRANSPARENT"] = false;
1201 cell
->parameters
["\\ABITS"] = GetSize(addr
);
1202 cell
->parameters
["\\WIDTH"] = GetSize(data
);
1203 cell
->setPort("\\CLK", RTLIL::State::Sx
);
1204 cell
->setPort("\\EN", RTLIL::State::Sx
);
1205 cell
->setPort("\\ADDR", addr
);
1206 cell
->setPort("\\DATA", data
);
1211 if (inst
->Type() == OPER_WRITE_PORT
|| inst
->Type() == OPER_CLOCKED_WRITE_PORT
)
1213 RTLIL::Memory
*memory
= module
->memories
.at(RTLIL::escape_id(inst
->GetOutput()->Name()));
1214 int numchunks
= int(inst
->Input2Size()) / memory
->width
;
1215 int chunksbits
= ceil_log2(numchunks
);
1217 if ((numchunks
* memory
->width
) != int(inst
->Input2Size()) || (numchunks
& (numchunks
- 1)) != 0)
1218 log_error("Import of asymmetric memories of this type is not supported yet: %s %s\n", inst
->Name(), inst
->GetOutput()->Name());
1220 for (int i
= 0; i
< numchunks
; i
++)
1222 RTLIL::SigSpec addr
= {operatorInput1(inst
), RTLIL::Const(i
, chunksbits
)};
1223 RTLIL::SigSpec data
= operatorInput2(inst
).extract(i
* memory
->width
, memory
->width
);
1225 RTLIL::Cell
*cell
= module
->addCell(numchunks
== 1 ? inst_name
:
1226 RTLIL::IdString(stringf("%s_%d", inst_name
.c_str(), i
)), "$memwr");
1227 cell
->parameters
["\\MEMID"] = memory
->name
.str();
1228 cell
->parameters
["\\CLK_ENABLE"] = false;
1229 cell
->parameters
["\\CLK_POLARITY"] = true;
1230 cell
->parameters
["\\PRIORITY"] = 0;
1231 cell
->parameters
["\\ABITS"] = GetSize(addr
);
1232 cell
->parameters
["\\WIDTH"] = GetSize(data
);
1233 cell
->setPort("\\EN", RTLIL::SigSpec(net_map_at(inst
->GetControl())).repeat(GetSize(data
)));
1234 cell
->setPort("\\CLK", RTLIL::State::S0
);
1235 cell
->setPort("\\ADDR", addr
);
1236 cell
->setPort("\\DATA", data
);
1238 if (inst
->Type() == OPER_CLOCKED_WRITE_PORT
) {
1239 cell
->parameters
["\\CLK_ENABLE"] = true;
1240 cell
->setPort("\\CLK", net_map_at(inst
->GetClock()));
1247 if (import_netlist_instance_cells(inst
, inst_name
))
1249 if (inst
->IsOperator() && !verific_sva_prims
.count(inst
->Type()))
1250 log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst
->View()->Owner()->Name());
1252 if (import_netlist_instance_gates(inst
, inst_name
))
1256 if (inst
->Type() == PRIM_SVA_ASSERT
|| inst
->Type() == PRIM_SVA_IMMEDIATE_ASSERT
)
1257 sva_asserts
.insert(inst
);
1259 if (inst
->Type() == PRIM_SVA_ASSUME
|| inst
->Type() == PRIM_SVA_IMMEDIATE_ASSUME
)
1260 sva_assumes
.insert(inst
);
1262 if (inst
->Type() == PRIM_SVA_COVER
|| inst
->Type() == PRIM_SVA_IMMEDIATE_COVER
)
1263 sva_covers
.insert(inst
);
1265 if (inst
->Type() == PRIM_SVA_TRIGGERED
)
1266 sva_triggers
.insert(inst
);
1268 if (inst
->Type() == OPER_SVA_STABLE
)
1270 VerificClocking
clocking(this, inst
->GetInput2Bit(0));
1271 log_assert(clocking
.disable_sig
== State::S0
);
1272 log_assert(clocking
.body_net
== nullptr);
1274 log_assert(inst
->Input1Size() == inst
->OutputSize());
1276 SigSpec sig_d
, sig_q
, sig_o
;
1277 sig_q
= module
->addWire(new_verific_id(inst
), inst
->Input1Size());
1279 for (int i
= int(inst
->Input1Size())-1; i
>= 0; i
--){
1280 sig_d
.append(net_map_at(inst
->GetInput1Bit(i
)));
1281 sig_o
.append(net_map_at(inst
->GetOutputBit(i
)));
1284 if (verific_verbose
) {
1285 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking
.posedge
? "pos" : "neg",
1286 log_signal(sig_d
), log_signal(sig_q
), log_signal(clocking
.clock_sig
));
1287 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1288 log_signal(sig_d
), log_signal(sig_q
), log_signal(sig_o
));
1291 clocking
.addDff(new_verific_id(inst
), sig_d
, sig_q
);
1292 module
->addXnor(new_verific_id(inst
), sig_d
, sig_q
, sig_o
);
1298 if (inst
->Type() == PRIM_SVA_STABLE
)
1300 VerificClocking
clocking(this, inst
->GetInput2());
1301 log_assert(clocking
.disable_sig
== State::S0
);
1302 log_assert(clocking
.body_net
== nullptr);
1304 SigSpec sig_d
= net_map_at(inst
->GetInput1());
1305 SigSpec sig_o
= net_map_at(inst
->GetOutput());
1306 SigSpec sig_q
= module
->addWire(new_verific_id(inst
));
1308 if (verific_verbose
) {
1309 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking
.posedge
? "pos" : "neg",
1310 log_signal(sig_d
), log_signal(sig_q
), log_signal(clocking
.clock_sig
));
1311 log(" XNOR with A=%s, B=%s, Y=%s.\n",
1312 log_signal(sig_d
), log_signal(sig_q
), log_signal(sig_o
));
1315 clocking
.addDff(new_verific_id(inst
), sig_d
, sig_q
);
1316 module
->addXnor(new_verific_id(inst
), sig_d
, sig_q
, sig_o
);
1322 if (inst
->Type() == PRIM_SVA_PAST
)
1324 VerificClocking
clocking(this, inst
->GetInput2());
1325 log_assert(clocking
.disable_sig
== State::S0
);
1326 log_assert(clocking
.body_net
== nullptr);
1328 SigBit sig_d
= net_map_at(inst
->GetInput1());
1329 SigBit sig_q
= net_map_at(inst
->GetOutput());
1331 if (verific_verbose
)
1332 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking
.posedge
? "pos" : "neg",
1333 log_signal(sig_d
), log_signal(sig_q
), log_signal(clocking
.clock_sig
));
1335 past_ffs
.insert(clocking
.addDff(new_verific_id(inst
), sig_d
, sig_q
));
1341 if ((inst
->Type() == PRIM_SVA_ROSE
|| inst
->Type() == PRIM_SVA_FELL
))
1343 VerificClocking
clocking(this, inst
->GetInput2());
1344 log_assert(clocking
.disable_sig
== State::S0
);
1345 log_assert(clocking
.body_net
== nullptr);
1347 SigBit sig_d
= net_map_at(inst
->GetInput1());
1348 SigBit sig_o
= net_map_at(inst
->GetOutput());
1349 SigBit sig_q
= module
->addWire(new_verific_id(inst
));
1351 if (verific_verbose
)
1352 log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking
.posedge
? "pos" : "neg",
1353 log_signal(sig_d
), log_signal(sig_q
), log_signal(clocking
.clock_sig
));
1355 clocking
.addDff(new_verific_id(inst
), sig_d
, sig_q
);
1356 module
->addEq(new_verific_id(inst
), {sig_q
, sig_d
}, Const(inst
->Type() == PRIM_SVA_ROSE
? 1 : 2, 2), sig_o
);
1362 if (!mode_keep
&& verific_sva_prims
.count(inst
->Type())) {
1363 if (verific_verbose
)
1364 log(" skipping SVA cell in non k-mode\n");
1368 if (inst
->Type() == PRIM_HDL_ASSERTION
)
1370 SigBit cond
= net_map_at(inst
->GetInput());
1372 if (verific_verbose
)
1373 log(" assert condition %s.\n", log_signal(cond
));
1375 const char *assume_attr
= nullptr; // inst->GetAttValue("assume");
1377 Cell
*cell
= nullptr;
1378 if (assume_attr
!= nullptr && !strcmp(assume_attr
, "1"))
1379 cell
= module
->addAssume(new_verific_id(inst
), cond
, State::S1
);
1381 cell
= module
->addAssert(new_verific_id(inst
), cond
, State::S1
);
1383 import_attributes(cell
->attributes
, inst
);
1387 if (inst
->IsPrimitive())
1390 log_error("Unsupported Verific primitive %s of type %s\n", inst
->Name(), inst
->View()->Owner()->Name());
1392 if (!verific_sva_prims
.count(inst
->Type()))
1393 log_warning("Unsupported Verific primitive %s of type %s\n", inst
->Name(), inst
->View()->Owner()->Name());
1396 import_verific_cells
:
1397 nl_todo
.insert(inst
->View());
1399 RTLIL::Cell
*cell
= module
->addCell(inst_name
, inst
->IsOperator() ?
1400 std::string("$verific$") + inst
->View()->Owner()->Name() : RTLIL::escape_id(inst
->View()->Owner()->Name()));
1402 if (inst
->IsPrimitive() && mode_keep
)
1403 cell
->attributes
["\\keep"] = 1;
1405 dict
<IdString
, vector
<SigBit
>> cell_port_conns
;
1407 if (verific_verbose
)
1408 log(" ports in verific db:\n");
1410 FOREACH_PORTREF_OF_INST(inst
, mi2
, pr
) {
1411 if (verific_verbose
)
1412 log(" .%s(%s)\n", pr
->GetPort()->Name(), pr
->GetNet()->Name());
1413 const char *port_name
= pr
->GetPort()->Name();
1414 int port_offset
= 0;
1415 if (pr
->GetPort()->Bus()) {
1416 port_name
= pr
->GetPort()->Bus()->Name();
1417 port_offset
= pr
->GetPort()->Bus()->IndexOf(pr
->GetPort()) -
1418 min(pr
->GetPort()->Bus()->LeftIndex(), pr
->GetPort()->Bus()->RightIndex());
1420 IdString port_name_id
= RTLIL::escape_id(port_name
);
1421 auto &sigvec
= cell_port_conns
[port_name_id
];
1422 if (GetSize(sigvec
) <= port_offset
) {
1423 SigSpec zwires
= module
->addWire(new_verific_id(inst
), port_offset
+1-GetSize(sigvec
));
1424 for (auto bit
: zwires
)
1425 sigvec
.push_back(bit
);
1427 sigvec
[port_offset
] = net_map_at(pr
->GetNet());
1430 if (verific_verbose
)
1431 log(" ports in yosys db:\n");
1433 for (auto &it
: cell_port_conns
) {
1434 if (verific_verbose
)
1435 log(" .%s(%s)\n", log_id(it
.first
), log_signal(it
.second
));
1436 cell
->setPort(it
.first
, it
.second
);
1442 for (auto inst
: sva_asserts
) {
1444 verific_import_sva_cover(this, inst
);
1445 verific_import_sva_assert(this, inst
);
1448 for (auto inst
: sva_assumes
)
1449 verific_import_sva_assume(this, inst
);
1451 for (auto inst
: sva_covers
)
1452 verific_import_sva_cover(this, inst
);
1454 for (auto inst
: sva_triggers
)
1455 verific_import_sva_trigger(this, inst
);
1457 merge_past_ffs(past_ffs
);
1462 pool
<SigBit
> non_ff_bits
;
1465 ff_types
.setup_internals_ff();
1466 ff_types
.setup_stdcells_mem();
1468 for (auto cell
: module
->cells())
1470 if (ff_types
.cell_known(cell
->type
))
1473 for (auto conn
: cell
->connections())
1475 if (!cell
->output(conn
.first
))
1478 for (auto bit
: conn
.second
)
1479 if (bit
.wire
!= nullptr)
1480 non_ff_bits
.insert(bit
);
1484 for (auto wire
: module
->wires())
1486 if (!wire
->attributes
.count("\\init"))
1489 Const
&initval
= wire
->attributes
.at("\\init");
1490 for (int i
= 0; i
< GetSize(initval
); i
++)
1492 if (initval
[i
] != State::S0
&& initval
[i
] != State::S1
)
1495 if (non_ff_bits
.count(SigBit(wire
, i
)))
1496 initval
[i
] = State::Sx
;
1499 if (initval
.is_fully_undef())
1500 wire
->attributes
.erase("\\init");
1505 // ==================================================================
1507 VerificClocking::VerificClocking(VerificImporter
*importer
, Net
*net
, bool sva_at_only
)
1509 module
= importer
->module
;
1511 log_assert(importer
!= nullptr);
1512 log_assert(net
!= nullptr);
1514 Instance
*inst
= net
->Driver();
1516 if (inst
!= nullptr && inst
->Type() == PRIM_SVA_AT
)
1518 net
= inst
->GetInput1();
1519 body_net
= inst
->GetInput2();
1521 inst
= net
->Driver();
1523 Instance
*body_inst
= body_net
->Driver();
1524 if (body_inst
!= nullptr && body_inst
->Type() == PRIM_SVA_DISABLE_IFF
) {
1525 disable_net
= body_inst
->GetInput1();
1526 disable_sig
= importer
->net_map_at(disable_net
);
1527 body_net
= body_inst
->GetInput2();
1536 // Use while() instead of if() to work around VIPER #13453
1537 while (inst
!= nullptr && inst
->Type() == PRIM_SVA_POSEDGE
)
1539 net
= inst
->GetInput();
1540 inst
= net
->Driver();;
1543 if (inst
!= nullptr && inst
->Type() == PRIM_INV
)
1545 net
= inst
->GetInput();
1546 inst
= net
->Driver();;
1550 // Detect clock-enable circuit
1552 if (inst
== nullptr || inst
->Type() != PRIM_AND
)
1555 Net
*net_dlatch
= inst
->GetInput1();
1556 Instance
*inst_dlatch
= net_dlatch
->Driver();
1558 if (inst_dlatch
== nullptr || inst_dlatch
->Type() != PRIM_DLATCHRS
)
1561 if (!inst_dlatch
->GetSet()->IsGnd() || !inst_dlatch
->GetReset()->IsGnd())
1564 Net
*net_enable
= inst_dlatch
->GetInput();
1565 Net
*net_not_clock
= inst_dlatch
->GetControl();
1567 if (net_enable
== nullptr || net_not_clock
== nullptr)
1570 Instance
*inst_not_clock
= net_not_clock
->Driver();
1572 if (inst_not_clock
== nullptr || inst_not_clock
->Type() != PRIM_INV
)
1575 Net
*net_clock1
= inst_not_clock
->GetInput();
1576 Net
*net_clock2
= inst
->GetInput2();
1578 if (net_clock1
== nullptr || net_clock1
!= net_clock2
)
1581 enable_net
= net_enable
;
1582 enable_sig
= importer
->net_map_at(enable_net
);
1585 inst
= net
->Driver();;
1588 // Detect condition expression
1590 if (body_net
== nullptr)
1593 Instance
*inst_mux
= body_net
->Driver();
1595 if (inst_mux
== nullptr || inst_mux
->Type() != PRIM_MUX
)
1598 if (!inst_mux
->GetInput1()->IsPwr())
1601 Net
*sva_net
= inst_mux
->GetInput2();
1602 if (!verific_is_sva_net(importer
, sva_net
))
1606 cond_net
= inst_mux
->GetControl();
1610 clock_sig
= importer
->net_map_at(clock_net
);
1612 const char *gclk_attr
= clock_net
->GetAttValue("gclk");
1613 if (gclk_attr
!= nullptr && (!strcmp(gclk_attr
, "1") || !strcmp(gclk_attr
, "'1'")))
1617 Cell
*VerificClocking::addDff(IdString name
, SigSpec sig_d
, SigSpec sig_q
, Const init_value
)
1619 log_assert(GetSize(sig_d
) == GetSize(sig_q
));
1621 if (GetSize(init_value
) != 0) {
1622 log_assert(GetSize(sig_q
) == GetSize(init_value
));
1623 if (sig_q
.is_wire()) {
1624 sig_q
.as_wire()->attributes
["\\init"] = init_value
;
1626 Wire
*w
= module
->addWire(NEW_ID
, GetSize(sig_q
));
1627 w
->attributes
["\\init"] = init_value
;
1628 module
->connect(sig_q
, w
);
1633 if (enable_sig
!= State::S1
)
1634 sig_d
= module
->Mux(NEW_ID
, sig_q
, sig_d
, enable_sig
);
1636 if (disable_sig
!= State::S0
) {
1637 log_assert(gclk
== false);
1638 log_assert(GetSize(sig_q
) == GetSize(init_value
));
1639 return module
->addAdff(name
, clock_sig
, disable_sig
, sig_d
, sig_q
, init_value
, posedge
);
1643 return module
->addFf(name
, sig_d
, sig_q
);
1645 return module
->addDff(name
, clock_sig
, sig_d
, sig_q
, posedge
);
1648 Cell
*VerificClocking::addAdff(IdString name
, RTLIL::SigSpec sig_arst
, SigSpec sig_d
, SigSpec sig_q
, Const arst_value
)
1650 log_assert(gclk
== false);
1651 log_assert(disable_sig
== State::S0
);
1653 if (enable_sig
!= State::S1
)
1654 sig_d
= module
->Mux(NEW_ID
, sig_q
, sig_d
, enable_sig
);
1656 return module
->addAdff(name
, clock_sig
, sig_arst
, sig_d
, sig_q
, arst_value
, posedge
);
1659 Cell
*VerificClocking::addDffsr(IdString name
, RTLIL::SigSpec sig_set
, RTLIL::SigSpec sig_clr
, SigSpec sig_d
, SigSpec sig_q
)
1661 log_assert(gclk
== false);
1662 log_assert(disable_sig
== State::S0
);
1664 if (enable_sig
!= State::S1
)
1665 sig_d
= module
->Mux(NEW_ID
, sig_q
, sig_d
, enable_sig
);
1667 return module
->addDffsr(name
, clock_sig
, sig_set
, sig_clr
, sig_d
, sig_q
, posedge
);
1670 // ==================================================================
1672 struct VerificExtNets
1674 int portname_cnt
= 0;
1676 // a map from Net to the same Net one level up in the design hierarchy
1677 std::map
<Net
*, Net
*> net_level_up_drive_up
;
1678 std::map
<Net
*, Net
*> net_level_up_drive_down
;
1680 Net
*route_up(Net
*net
, bool drive_up
, Net
*final_net
= nullptr)
1682 auto &net_level_up
= drive_up
? net_level_up_drive_up
: net_level_up_drive_down
;
1684 if (net_level_up
.count(net
) == 0)
1686 Netlist
*nl
= net
->Owner();
1688 // Simply return if Netlist is not unique
1689 log_assert(nl
->NumOfRefs() == 1);
1691 Instance
*up_inst
= (Instance
*)nl
->GetReferences()->GetLast();
1692 Netlist
*up_nl
= up_inst
->Owner();
1695 string name
= stringf("___extnets_%d", portname_cnt
++);
1696 Port
*new_port
= new Port(name
.c_str(), drive_up
? DIR_OUT
: DIR_IN
);
1698 net
->Connect(new_port
);
1700 // create new Net in up Netlist
1701 Net
*new_net
= final_net
;
1702 if (new_net
== nullptr || new_net
->Owner() != up_nl
) {
1703 new_net
= new Net(name
.c_str());
1704 up_nl
->Add(new_net
);
1706 up_inst
->Connect(new_port
, new_net
);
1708 net_level_up
[net
] = new_net
;
1711 return net_level_up
.at(net
);
1714 Net
*route_up(Net
*net
, bool drive_up
, Netlist
*dest
, Net
*final_net
= nullptr)
1716 while (net
->Owner() != dest
)
1717 net
= route_up(net
, drive_up
, final_net
);
1718 if (final_net
!= nullptr)
1719 log_assert(net
== final_net
);
1723 Netlist
*find_common_ancestor(Netlist
*A
, Netlist
*B
)
1725 std::set
<Netlist
*> ancestors_of_A
;
1727 Netlist
*cursor
= A
;
1729 ancestors_of_A
.insert(cursor
);
1730 if (cursor
->NumOfRefs() != 1)
1732 cursor
= ((Instance
*)cursor
->GetReferences()->GetLast())->Owner();
1737 if (ancestors_of_A
.count(cursor
))
1739 if (cursor
->NumOfRefs() != 1)
1741 cursor
= ((Instance
*)cursor
->GetReferences()->GetLast())->Owner();
1744 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());
1747 void run(Netlist
*nl
)
1753 vector
<tuple
<Instance
*, Port
*, Net
*>> todo_connect
;
1755 FOREACH_INSTANCE_OF_NETLIST(nl
, mi
, inst
)
1758 FOREACH_INSTANCE_OF_NETLIST(nl
, mi
, inst
)
1759 FOREACH_PORTREF_OF_INST(inst
, mi2
, pr
)
1761 Port
*port
= pr
->GetPort();
1762 Net
*net
= pr
->GetNet();
1764 if (!net
->IsExternalTo(nl
))
1767 if (verific_verbose
)
1768 log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl
).c_str(), inst
->Name(), port
->Name());
1770 Netlist
*ext_nl
= net
->Owner();
1772 if (verific_verbose
)
1773 log(" external net owner: %s\n", get_full_netlist_name(ext_nl
).c_str());
1775 Netlist
*ca_nl
= find_common_ancestor(nl
, ext_nl
);
1777 if (verific_verbose
)
1778 log(" common ancestor: %s\n", get_full_netlist_name(ca_nl
).c_str());
1780 Net
*ca_net
= route_up(net
, !port
->IsOutput(), ca_nl
);
1781 Net
*new_net
= ca_net
;
1785 if (verific_verbose
)
1786 log(" net in common ancestor: %s\n", ca_net
->Name());
1788 string name
= stringf("___extnets_%d", portname_cnt
++);
1789 new_net
= new Net(name
.c_str());
1792 Net
*n
= route_up(new_net
, port
->IsOutput(), ca_nl
, ca_net
);
1793 log_assert(n
== ca_net
);
1796 if (verific_verbose
)
1797 log(" new local net: %s\n", new_net
->Name());
1799 log_assert(!new_net
->IsExternalTo(nl
));
1800 todo_connect
.push_back(tuple
<Instance
*, Port
*, Net
*>(inst
, port
, new_net
));
1803 for (auto it
: todo_connect
) {
1804 get
<0>(it
)->Disconnect(get
<1>(it
));
1805 get
<0>(it
)->Connect(get
<1>(it
), get
<2>(it
));
1810 void verific_import(Design
*design
, const std::map
<std::string
,std::string
> ¶meters
, std::string top
)
1812 verific_sva_fsm_limit
= 16;
1814 std::set
<Netlist
*> nl_todo
, nl_done
;
1816 VhdlLibrary
*vhdl_lib
= vhdl_file::GetLibrary("work", 1);
1817 VeriLibrary
*veri_lib
= veri_file::GetLibrary("work", 1);
1818 Array
*netlists
= NULL
;
1819 Array veri_libs
, vhdl_libs
;
1820 if (vhdl_lib
) vhdl_libs
.InsertLast(vhdl_lib
);
1821 if (veri_lib
) veri_libs
.InsertLast(veri_lib
);
1823 Map
verific_params(STRING_HASH
);
1824 for (const auto &i
: parameters
)
1825 verific_params
.Insert(i
.first
.c_str(), i
.second
.c_str());
1828 netlists
= hier_tree::ElaborateAll(&veri_libs
, &vhdl_libs
, &verific_params
);
1831 Array veri_modules
, vhdl_units
;
1834 VeriModule
*veri_module
= veri_lib
->GetModule(top
.c_str(), 1);
1836 veri_modules
.InsertLast(veri_module
);
1839 // Also elaborate all root modules since they may contain bind statements
1841 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib
, mi
, veri_module
) {
1842 if (!veri_module
->IsRootModule()) continue;
1843 veri_modules
.InsertLast(veri_module
);
1848 VhdlDesignUnit
*vhdl_unit
= vhdl_lib
->GetPrimUnit(top
.c_str());
1850 vhdl_units
.InsertLast(vhdl_unit
);
1853 netlists
= hier_tree::Elaborate(&veri_modules
, &vhdl_units
, &verific_params
);
1859 FOREACH_ARRAY_ITEM(netlists
, i
, nl
) {
1860 if (top
.empty() && nl
->CellBaseName() != top
)
1862 nl
->AddAtt(new Att(" \\top", NULL
));
1868 if (!verific_error_msg
.empty())
1869 log_error("%s\n", verific_error_msg
.c_str());
1871 VerificExtNets worker
;
1872 for (auto nl
: nl_todo
)
1875 while (!nl_todo
.empty()) {
1876 Netlist
*nl
= *nl_todo
.begin();
1877 if (nl_done
.count(nl
) == 0) {
1878 VerificImporter
importer(false, false, false, false, false, false, false);
1879 importer
.import_netlist(design
, nl
, nl_todo
);
1888 verific_incdirs
.clear();
1889 verific_libdirs
.clear();
1890 verific_import_pending
= false;
1892 if (!verific_error_msg
.empty())
1893 log_error("%s\n", verific_error_msg
.c_str());
1897 #endif /* YOSYS_ENABLE_VERIFIC */
1899 PRIVATE_NAMESPACE_BEGIN
1901 #ifdef YOSYS_ENABLE_VERIFIC
1902 bool check_noverific_env()
1904 const char *e
= getenv("YOSYS_NOVERIFIC");
1913 struct VerificPass
: public Pass
{
1914 VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
1915 void help() YS_OVERRIDE
1917 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
1919 log(" verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
1921 log("Load the specified Verilog/SystemVerilog files into Verific.\n");
1923 log("All files specified in one call to this command are one compilation unit.\n");
1924 log("Files passed to different calls to this command are treated as belonging to\n");
1925 log("different compilation units.\n");
1927 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
1928 log("the language version (and before file names) to set additional verilog defines.\n");
1929 log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
1932 log(" verific -formal <verilog-file>..\n");
1934 log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
1937 log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
1939 log("Load the specified VHDL files into Verific.\n");
1942 log(" verific -work <libname> {-sv|-vhdl|...} <hdl-file>\n");
1944 log("Load the specified Verilog/SystemVerilog/VHDL file into the specified library.\n");
1945 log("(default library when -work is not present: \"work\")\n");
1948 log(" verific -vlog-incdir <directory>..\n");
1950 log("Add Verilog include directories.\n");
1953 log(" verific -vlog-libdir <directory>..\n");
1955 log("Add Verilog library directories. Verific will search in this directories to\n");
1956 log("find undefined modules.\n");
1959 log(" verific -vlog-define <macro>[=<value>]..\n");
1961 log("Add Verilog defines.\n");
1964 log(" verific -vlog-undef <macro>..\n");
1966 log("Remove Verilog defines previously set with -vlog-define.\n");
1969 log(" verific -set-error <msg_id>..\n");
1970 log(" verific -set-warning <msg_id>..\n");
1971 log(" verific -set-info <msg_id>..\n");
1972 log(" verific -set-ignore <msg_id>..\n");
1974 log("Set message severity. <msg_id> is the string in square brackets when a message\n");
1975 log("is printed, such as VERI-1209.\n");
1978 log(" verific -import [options] <top-module>..\n");
1980 log("Elaborate the design for the specified top modules, import to Yosys and\n");
1981 log("reset the internal state of Verific.\n");
1983 log("Import options:\n");
1986 log(" Elaborate all modules, not just the hierarchy below the given top\n");
1987 log(" modules. With this option the list of modules to import is optional.\n");
1990 log(" Create a gate-level netlist.\n");
1993 log(" Flatten the design in Verific before importing.\n");
1996 log(" Resolve references to external nets by adding module ports as needed.\n");
1998 log(" -autocover\n");
1999 log(" Generate automatic cover statements for all asserts\n");
2001 log(" -fullinit\n");
2002 log(" Keep all register initializations, even those for non-FF registers.\n");
2004 log(" -chparam name value \n");
2005 log(" Elaborate the specified top modules (all modules when -all given) using\n");
2006 log(" this parameter value. Modules on which this parameter does not exist will\n");
2007 log(" cause Verific to produce a VERI-1928 or VHDL-1676 message. This option\n");
2008 log(" can be specified multiple times to override multiple parameters.\n");
2009 log(" String values must be passed in double quotes (\").\n");
2012 log(" Verbose log messages. (-vv is even more verbose than -v.)\n");
2014 log("The following additional import options are useful for debugging the Verific\n");
2015 log("bindings (for Yosys and/or Verific developers):\n");
2018 log(" Keep going after an unsupported verific primitive is found. The\n");
2019 log(" unsupported primitive is added as blockbox module to the design.\n");
2020 log(" This will also add all SVA related cells to the design parallel to\n");
2021 log(" the checker logic inferred by it.\n");
2024 log(" Import Verific netlist as-is without translating to Yosys cell types. \n");
2027 log(" Ignore SVA properties, do not infer checker logic.\n");
2030 log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
2033 log(" Keep all Verific names on instances and nets. By default only\n");
2034 log(" user-declared names are preserved.\n");
2036 log(" -d <dump_file>\n");
2037 log(" Dump the Verific netlist as a verilog file.\n");
2039 log("Visit http://verific.com/ for more information on Verific.\n");
2042 #ifdef YOSYS_ENABLE_VERIFIC
2043 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
2045 static bool set_verific_global_flags
= true;
2047 if (check_noverific_env())
2048 log_cmd_error("This version of Yosys is built without Verific support.\n");
2050 log_header(design
, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
2052 if (set_verific_global_flags
)
2054 Message::SetConsoleOutput(0);
2055 Message::RegisterCallBackMsg(msg_func
);
2057 RuntimeFlags::SetVar("db_preserve_user_nets", 1);
2058 RuntimeFlags::SetVar("db_allow_external_nets", 1);
2059 RuntimeFlags::SetVar("db_infer_wide_operators", 1);
2061 RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
2062 RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
2064 RuntimeFlags::SetVar("vhdl_extract_dualport_rams", 0);
2065 RuntimeFlags::SetVar("vhdl_extract_multiport_rams", 1);
2067 RuntimeFlags::SetVar("vhdl_support_variable_slice", 1);
2068 RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
2070 // Workaround for VIPER #13851
2071 RuntimeFlags::SetVar("veri_create_name_for_unnamed_gen_block", 1);
2073 // WARNING: instantiating unknown module 'XYZ' (VERI-1063)
2074 Message::SetMessageType("VERI-1063", VERIFIC_ERROR
);
2076 // https://github.com/YosysHQ/yosys/issues/1055
2077 RuntimeFlags::SetVar("veri_elaborate_top_level_modules_having_interface_ports", 1) ;
2079 #ifndef DB_PRESERVE_INITIAL_VALUE
2080 # warning Verific was built without DB_PRESERVE_INITIAL_VALUE.
2083 set_verific_global_flags
= false;
2086 verific_verbose
= 0;
2087 verific_sva_fsm_limit
= 16;
2089 const char *release_str
= Message::ReleaseString();
2090 time_t release_time
= Message::ReleaseDate();
2091 char *release_tmstr
= ctime(&release_time
);
2093 if (release_str
== nullptr)
2094 release_str
= "(no release string)";
2096 for (char *p
= release_tmstr
; *p
; p
++)
2097 if (*p
== '\n') *p
= 0;
2099 log("Built with Verific %s, released at %s.\n", release_str
, release_tmstr
);
2102 std::string work
= "work";
2104 if (GetSize(args
) > argidx
&& (args
[argidx
] == "-set-error" || args
[argidx
] == "-set-warning" ||
2105 args
[argidx
] == "-set-info" || args
[argidx
] == "-set-ignore"))
2107 msg_type_t new_type
;
2109 if (args
[argidx
] == "-set-error")
2110 new_type
= VERIFIC_ERROR
;
2111 else if (args
[argidx
] == "-set-warning")
2112 new_type
= VERIFIC_WARNING
;
2113 else if (args
[argidx
] == "-set-info")
2114 new_type
= VERIFIC_INFO
;
2115 else if (args
[argidx
] == "-set-ignore")
2116 new_type
= VERIFIC_IGNORE
;
2120 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2121 Message::SetMessageType(args
[argidx
].c_str(), new_type
);
2126 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vlog-incdir") {
2127 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2128 verific_incdirs
.push_back(args
[argidx
]);
2132 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vlog-libdir") {
2133 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2134 verific_libdirs
.push_back(args
[argidx
]);
2138 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vlog-define") {
2139 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2140 string name
= args
[argidx
];
2141 size_t equal
= name
.find('=');
2142 if (equal
!= std::string::npos
) {
2143 string value
= name
.substr(equal
+1);
2144 name
= name
.substr(0, equal
);
2145 veri_file::DefineCmdLineMacro(name
.c_str(), value
.c_str());
2147 veri_file::DefineCmdLineMacro(name
.c_str());
2153 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vlog-undef") {
2154 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2155 string name
= args
[argidx
];
2156 veri_file::UndefineMacro(name
.c_str());
2161 for (; argidx
< GetSize(args
); argidx
++)
2163 if (args
[argidx
] == "-work" && argidx
+1 < GetSize(args
)) {
2164 work
= args
[++argidx
];
2170 if (GetSize(args
) > argidx
&& (args
[argidx
] == "-vlog95" || args
[argidx
] == "-vlog2k" || args
[argidx
] == "-sv2005" ||
2171 args
[argidx
] == "-sv2009" || args
[argidx
] == "-sv2012" || args
[argidx
] == "-sv" || args
[argidx
] == "-formal"))
2174 unsigned verilog_mode
;
2176 if (args
[argidx
] == "-vlog95")
2177 verilog_mode
= veri_file::VERILOG_95
;
2178 else if (args
[argidx
] == "-vlog2k")
2179 verilog_mode
= veri_file::VERILOG_2K
;
2180 else if (args
[argidx
] == "-sv2005")
2181 verilog_mode
= veri_file::SYSTEM_VERILOG_2005
;
2182 else if (args
[argidx
] == "-sv2009")
2183 verilog_mode
= veri_file::SYSTEM_VERILOG_2009
;
2184 else if (args
[argidx
] == "-sv2012" || args
[argidx
] == "-sv" || args
[argidx
] == "-formal")
2185 verilog_mode
= veri_file::SYSTEM_VERILOG
;
2189 veri_file::DefineMacro("VERIFIC");
2190 veri_file::DefineMacro(args
[argidx
] == "-formal" ? "FORMAL" : "SYNTHESIS");
2192 for (argidx
++; argidx
< GetSize(args
) && GetSize(args
[argidx
]) >= 2 && args
[argidx
].substr(0, 2) == "-D"; argidx
++) {
2193 std::string name
= args
[argidx
].substr(2);
2194 if (args
[argidx
] == "-D") {
2195 if (++argidx
>= GetSize(args
))
2197 name
= args
[argidx
];
2199 size_t equal
= name
.find('=');
2200 if (equal
!= std::string::npos
) {
2201 string value
= name
.substr(equal
+1);
2202 name
= name
.substr(0, equal
);
2203 veri_file::DefineMacro(name
.c_str(), value
.c_str());
2205 veri_file::DefineMacro(name
.c_str());
2209 for (auto &dir
: verific_incdirs
)
2210 veri_file::AddIncludeDir(dir
.c_str());
2211 for (auto &dir
: verific_libdirs
)
2212 veri_file::AddYDir(dir
.c_str());
2214 while (argidx
< GetSize(args
))
2215 file_names
.Insert(args
[argidx
++].c_str());
2217 if (!veri_file::AnalyzeMultipleFiles(&file_names
, verilog_mode
, work
.c_str(), veri_file::MFCU
))
2218 log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
2220 verific_import_pending
= true;
2224 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vhdl87") {
2225 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
2226 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2227 if (!vhdl_file::Analyze(args
[argidx
].c_str(), work
.c_str(), vhdl_file::VHDL_87
))
2228 log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args
[argidx
].c_str());
2229 verific_import_pending
= true;
2233 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vhdl93") {
2234 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2235 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2236 if (!vhdl_file::Analyze(args
[argidx
].c_str(), work
.c_str(), vhdl_file::VHDL_93
))
2237 log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args
[argidx
].c_str());
2238 verific_import_pending
= true;
2242 if (GetSize(args
) > argidx
&& args
[argidx
] == "-vhdl2k") {
2243 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str());
2244 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2245 if (!vhdl_file::Analyze(args
[argidx
].c_str(), work
.c_str(), vhdl_file::VHDL_2K
))
2246 log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args
[argidx
].c_str());
2247 verific_import_pending
= true;
2251 if (GetSize(args
) > argidx
&& (args
[argidx
] == "-vhdl2008" || args
[argidx
] == "-vhdl")) {
2252 vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
2253 for (argidx
++; argidx
< GetSize(args
); argidx
++)
2254 if (!vhdl_file::Analyze(args
[argidx
].c_str(), work
.c_str(), vhdl_file::VHDL_2008
))
2255 log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args
[argidx
].c_str());
2256 verific_import_pending
= true;
2260 if (GetSize(args
) > argidx
&& args
[argidx
] == "-import")
2262 std::set
<Netlist
*> nl_todo
, nl_done
;
2263 bool mode_all
= false, mode_gates
= false, mode_keep
= false;
2264 bool mode_nosva
= false, mode_names
= false, mode_verific
= false;
2265 bool mode_autocover
= false, mode_fullinit
= false;
2266 bool flatten
= false, extnets
= false;
2268 Map
parameters(STRING_HASH
);
2270 for (argidx
++; argidx
< GetSize(args
); argidx
++) {
2271 if (args
[argidx
] == "-all") {
2275 if (args
[argidx
] == "-gates") {
2279 if (args
[argidx
] == "-flatten") {
2283 if (args
[argidx
] == "-extnets") {
2287 if (args
[argidx
] == "-k") {
2291 if (args
[argidx
] == "-nosva") {
2295 if (args
[argidx
] == "-L" && argidx
+1 < GetSize(args
)) {
2296 verific_sva_fsm_limit
= atoi(args
[++argidx
].c_str());
2299 if (args
[argidx
] == "-n") {
2303 if (args
[argidx
] == "-autocover") {
2304 mode_autocover
= true;
2307 if (args
[argidx
] == "-fullinit") {
2308 mode_fullinit
= true;
2311 if (args
[argidx
] == "-chparam" && argidx
+2 < GetSize(args
)) {
2312 const std::string
&key
= args
[++argidx
];
2313 const std::string
&value
= args
[++argidx
];
2314 unsigned new_insertion
= parameters
.Insert(key
.c_str(), value
.c_str(),
2315 1 /* force_overwrite */);
2317 log_warning_noprefix("-chparam %s already specified: overwriting.\n", key
.c_str());
2320 if (args
[argidx
] == "-V") {
2321 mode_verific
= true;
2324 if (args
[argidx
] == "-v") {
2325 verific_verbose
= 1;
2328 if (args
[argidx
] == "-vv") {
2329 verific_verbose
= 2;
2332 if (args
[argidx
] == "-d" && argidx
+1 < GetSize(args
)) {
2333 dumpfile
= args
[++argidx
];
2339 if (argidx
> GetSize(args
) && args
[argidx
].substr(0, 1) == "-")
2340 cmd_error(args
, argidx
, "unknown option");
2344 log("Running hier_tree::ElaborateAll().\n");
2346 VhdlLibrary
*vhdl_lib
= vhdl_file::GetLibrary(work
.c_str(), 1);
2347 VeriLibrary
*veri_lib
= veri_file::GetLibrary(work
.c_str(), 1);
2349 Array veri_libs
, vhdl_libs
;
2350 if (vhdl_lib
) vhdl_libs
.InsertLast(vhdl_lib
);
2351 if (veri_lib
) veri_libs
.InsertLast(veri_lib
);
2353 Array
*netlists
= hier_tree::ElaborateAll(&veri_libs
, &vhdl_libs
, ¶meters
);
2357 FOREACH_ARRAY_ITEM(netlists
, i
, nl
)
2363 if (argidx
== GetSize(args
))
2364 log_cmd_error("No top module specified.\n");
2366 Array veri_modules
, vhdl_units
;
2367 for (; argidx
< GetSize(args
); argidx
++)
2369 const char *name
= args
[argidx
].c_str();
2370 VeriLibrary
* veri_lib
= veri_file::GetLibrary(work
.c_str(), 1);
2373 VeriModule
*veri_module
= veri_lib
->GetModule(name
, 1);
2375 log("Adding Verilog module '%s' to elaboration queue.\n", name
);
2376 veri_modules
.InsertLast(veri_module
);
2380 // Also elaborate all root modules since they may contain bind statements
2382 FOREACH_VERILOG_MODULE_IN_LIBRARY(veri_lib
, mi
, veri_module
) {
2383 if (!veri_module
->IsRootModule()) continue;
2384 veri_modules
.InsertLast(veri_module
);
2388 VhdlLibrary
*vhdl_lib
= vhdl_file::GetLibrary(work
.c_str(), 1);
2389 VhdlDesignUnit
*vhdl_unit
= vhdl_lib
->GetPrimUnit(name
);
2391 log("Adding VHDL unit '%s' to elaboration queue.\n", name
);
2392 vhdl_units
.InsertLast(vhdl_unit
);
2396 log_error("Can't find module/unit '%s'.\n", name
);
2399 log("Running hier_tree::Elaborate().\n");
2400 Array
*netlists
= hier_tree::Elaborate(&veri_modules
, &vhdl_units
, ¶meters
);
2404 FOREACH_ARRAY_ITEM(netlists
, i
, nl
) {
2405 nl
->AddAtt(new Att(" \\top", NULL
));
2411 if (!verific_error_msg
.empty())
2415 for (auto nl
: nl_todo
)
2420 VerificExtNets worker
;
2421 for (auto nl
: nl_todo
)
2425 if (!dumpfile
.empty()) {
2426 VeriWrite veri_writer
;
2427 veri_writer
.WriteFile(dumpfile
.c_str(), Netlist::PresentDesign());
2430 while (!nl_todo
.empty()) {
2431 Netlist
*nl
= *nl_todo
.begin();
2432 if (nl_done
.count(nl
) == 0) {
2433 VerificImporter
importer(mode_gates
, mode_keep
, mode_nosva
,
2434 mode_names
, mode_verific
, mode_autocover
, mode_fullinit
);
2435 importer
.import_netlist(design
, nl
, nl_todo
);
2444 verific_incdirs
.clear();
2445 verific_libdirs
.clear();
2446 verific_import_pending
= false;
2450 log_cmd_error("Missing or unsupported mode parameter.\n");
2453 if (!verific_error_msg
.empty())
2454 log_error("%s\n", verific_error_msg
.c_str());
2457 #else /* YOSYS_ENABLE_VERIFIC */
2458 void execute(std::vector
<std::string
>, RTLIL::Design
*) YS_OVERRIDE
{
2459 log_cmd_error("This version of Yosys is built without Verific support.\n");
2464 struct ReadPass
: public Pass
{
2465 ReadPass() : Pass("read", "load HDL designs") { }
2466 void help() YS_OVERRIDE
2468 // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
2470 log(" read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
2472 log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
2473 log("is only available via Verific.)\n");
2475 log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
2476 log("the language version (and before file names) to set additional verilog defines.\n");
2479 log(" read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
2481 log("Load the specified VHDL files. (Requires Verific.)\n");
2484 log(" read -define <macro>[=<value>]..\n");
2486 log("Set global Verilog/SystemVerilog defines.\n");
2489 log(" read -undef <macro>..\n");
2491 log("Unset global Verilog/SystemVerilog defines.\n");
2494 log(" read -incdir <directory>\n");
2496 log("Add directory to global Verilog/SystemVerilog include directories.\n");
2499 log(" read -verific\n");
2500 log(" read -noverific\n");
2502 log("Subsequent calls to 'read' will either use or not use Verific. Calling 'read'\n");
2503 log("with -verific will result in an error on Yosys binaries that are built without\n");
2504 log("Verific support. The default is to use Verific if it is available.\n");
2507 void execute(std::vector
<std::string
> args
, RTLIL::Design
*design
) YS_OVERRIDE
2509 #ifdef YOSYS_ENABLE_VERIFIC
2510 static bool verific_available
= !check_noverific_env();
2512 static bool verific_available
= false;
2514 static bool use_verific
= verific_available
;
2516 if (args
.size() < 2 || args
[1][0] != '-')
2517 log_cmd_error("Missing mode parameter.\n");
2519 if (args
[1] == "-verific" || args
[1] == "-noverific") {
2520 if (args
.size() != 2)
2521 log_cmd_error("Additional arguments to -verific/-noverific.\n");
2522 if (args
[1] == "-verific") {
2523 if (!verific_available
)
2524 log_cmd_error("This version of Yosys is built without Verific support.\n");
2527 use_verific
= false;
2532 if (args
.size() < 3)
2533 log_cmd_error("Missing file name parameter.\n");
2535 if (args
[1] == "-vlog95" || args
[1] == "-vlog2k") {
2537 args
[0] = "verific";
2539 args
[0] = "read_verilog";
2542 Pass::call(design
, args
);
2546 if (args
[1] == "-sv2005" || args
[1] == "-sv2009" || args
[1] == "-sv2012" || args
[1] == "-sv" || args
[1] == "-formal") {
2548 args
[0] = "verific";
2550 args
[0] = "read_verilog";
2551 if (args
[1] == "-formal")
2552 args
.insert(args
.begin()+1, std::string());
2554 args
.insert(args
.begin()+1, "-defer");
2556 Pass::call(design
, args
);
2560 if (args
[1] == "-vhdl87" || args
[1] == "-vhdl93" || args
[1] == "-vhdl2k" || args
[1] == "-vhdl2008" || args
[1] == "-vhdl") {
2562 args
[0] = "verific";
2563 Pass::call(design
, args
);
2565 log_cmd_error("This version of Yosys is built without Verific support.\n");
2570 if (args
[1] == "-define") {
2572 args
[0] = "verific";
2573 args
[1] = "-vlog-define";
2574 Pass::call(design
, args
);
2576 args
[0] = "verilog_defines";
2577 args
.erase(args
.begin()+1, args
.begin()+2);
2578 for (int i
= 1; i
< GetSize(args
); i
++)
2579 args
[i
] = "-D" + args
[i
];
2580 Pass::call(design
, args
);
2584 if (args
[1] == "-undef") {
2586 args
[0] = "verific";
2587 args
[1] = "-vlog-undef";
2588 Pass::call(design
, args
);
2590 args
[0] = "verilog_defines";
2591 args
.erase(args
.begin()+1, args
.begin()+2);
2592 for (int i
= 1; i
< GetSize(args
); i
++)
2593 args
[i
] = "-U" + args
[i
];
2594 Pass::call(design
, args
);
2598 if (args
[1] == "-incdir") {
2600 args
[0] = "verific";
2601 args
[1] = "-vlog-incdir";
2602 Pass::call(design
, args
);
2604 args
[0] = "verilog_defaults";
2606 for (int i
= 2; i
< GetSize(args
); i
++)
2607 args
[i
] = "-I" + args
[i
];
2608 Pass::call(design
, args
);
2612 log_cmd_error("Missing or unsupported mode parameter.\n");
2616 PRIVATE_NAMESPACE_END