projects / yosys.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Merge remote-tracking branch 'upstream/master'
[yosys.git] / frontends / verific / verificsva.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
21 // Currently supported SVA sequence and property syntax:
22 // http://symbiyosys.readthedocs.io/en/latest/verific.html
23 //
24 // Next gen property syntax:
25 // basic_property
26 // [antecedent_condition] property
27 // [antecedent_condition] always.. property
28 // [antecedent_condition] eventually.. basic_property
29 // [antecedent_condition] property until.. expression
30 // [antecedent_condition] basic_property until.. basic_property (assert/assume only)
31 //
32 // antecedent_condition:
33 // sequence |->
34 // sequence |=>
35 //
36 // basic_property:
37 // sequence
38 // not basic_property
39 // sequence #-# basic_property
40 // sequence #=# basic_property
41 // basic_property or basic_property (cover only)
42 // basic_property and basic_property (assert/assume only)
43 // basic_property implies basic_property
44 // basic_property iff basic_property
45 //
46 // sequence:
47 // expression
48 // sequence ##N sequence
49 // sequence ##[*] sequence
50 // sequence ##[+] sequence
51 // sequence ##[N:M] sequence
52 // sequence ##[N:$] sequence
53 // expression [*]
54 // expression [+]
55 // expression [*N]
56 // expression [*N:M]
57 // expression [*N:$]
58 // sequence or sequence
59 // sequence and sequence
60 // expression throughout sequence
61 // sequence intersect sequence
62 // sequence within sequence
63 // first_match( sequence )
64 // expression [=N]
65 // expression [=N:M]
66 // expression [=N:$]
67 // expression [->N]
68 // expression [->N:M]
69 // expression [->N:$]
70
71
72 #include "kernel/yosys.h"
73 #include "frontends/verific/verific.h"
74
75 USING_YOSYS_NAMESPACE
76
77 #ifdef VERIFIC_NAMESPACE
78 using namespace Verific;
79 #endif
80
81 PRIVATE_NAMESPACE_BEGIN
82
83 // Non-deterministic FSM
84 struct SvaNFsmNode
85 {
86 // Edge: Activate the target node if ctrl signal is true, consumes clock cycle
87 // Link: Activate the target node if ctrl signal is true, doesn't consume clock cycle
88 vector<pair<int, SigBit>> edges, links;
89 bool is_cond_node;
90 };
91
92 // Non-deterministic FSM after resolving links
93 struct SvaUFsmNode
94 {
95 // Edge: Activate the target node if all bits in ctrl signal are true, consumes clock cycle
96 // Accept: This node functions as an accept node if all bits in ctrl signal are true
97 vector<pair<int, SigSpec>> edges;
98 vector<SigSpec> accept, cond;
99 bool reachable;
100 };
101
102 // Deterministic FSM
103 struct SvaDFsmNode
104 {
105 // A DFSM state corresponds to a set of NFSM states. We represent DFSM states as sorted vectors
106 // of NFSM state node ids. Edge/accept controls are constants matched against the ctrl sigspec.
107 SigSpec ctrl;
108 vector<pair<vector<int>, Const>> edges;
109 vector<Const> accept, reject;
110
111 // additional temp data for getReject()
112 Wire *ffoutwire;
113 SigBit statesig;
114 SigSpec nextstate;
115
116 // additional temp data for getDFsm()
117 int outnode;
118 };
119
120 struct SvaFsm
121 {
122 Module *module;
123 VerificClocking clocking;
124
125 SigBit trigger_sig = State::S1, disable_sig;
126 SigBit throughout_sig = State::S1;
127 bool in_cond_mode = false;
128
129 vector<SigBit> disable_stack;
130 vector<SigBit> throughout_stack;
131
132 int startNode, acceptNode, condNode;
133 vector<SvaNFsmNode> nodes;
134
135 vector<SvaUFsmNode> unodes;
136 dict<vector<int>, SvaDFsmNode> dnodes;
137 dict<pair<SigSpec, SigSpec>, SigBit> cond_eq_cache;
138 bool materialized = false;
139
140 SigBit final_accept_sig = State::Sx;
141 SigBit final_reject_sig = State::Sx;
142
143 SvaFsm(const VerificClocking &clking, SigBit trig = State::S1)
144 {
145 module = clking.module;
146 clocking = clking;
147 trigger_sig = trig;
148
149 startNode = createNode();
150 acceptNode = createNode();
151
152 in_cond_mode = true;
153 condNode = createNode();
154 in_cond_mode = false;
155 }
156
157 void pushDisable(SigBit sig)
158 {
159 log_assert(!materialized);
160
161 disable_stack.push_back(disable_sig);
162
163 if (disable_sig == State::S0)
164 disable_sig = sig;
165 else
166 disable_sig = module->Or(NEW_ID, disable_sig, sig);
167 }
168
169 void popDisable()
170 {
171 log_assert(!materialized);
172 log_assert(!disable_stack.empty());
173
174 disable_sig = disable_stack.back();
175 disable_stack.pop_back();
176 }
177
178 void pushThroughout(SigBit sig)
179 {
180 log_assert(!materialized);
181
182 throughout_stack.push_back(throughout_sig);
183
184 if (throughout_sig == State::S1)
185 throughout_sig = sig;
186 else
187 throughout_sig = module->And(NEW_ID, throughout_sig, sig);
188 }
189
190 void popThroughout()
191 {
192 log_assert(!materialized);
193 log_assert(!throughout_stack.empty());
194
195 throughout_sig = throughout_stack.back();
196 throughout_stack.pop_back();
197 }
198
199 int createNode(int link_node = -1)
200 {
201 log_assert(!materialized);
202
203 int idx = GetSize(nodes);
204 nodes.push_back(SvaNFsmNode());
205 nodes.back().is_cond_node = in_cond_mode;
206 if (link_node >= 0)
207 createLink(link_node, idx);
208 return idx;
209 }
210
211 int createStartNode()
212 {
213 return createNode(startNode);
214 }
215
216 void createEdge(int from_node, int to_node, SigBit ctrl = State::S1)
217 {
218 log_assert(!materialized);
219 log_assert(0 <= from_node && from_node < GetSize(nodes));
220 log_assert(0 <= to_node && to_node < GetSize(nodes));
221 log_assert(from_node != acceptNode);
222 log_assert(to_node != acceptNode);
223 log_assert(from_node != condNode);
224 log_assert(to_node != condNode);
225 log_assert(to_node != startNode);
226
227 if (from_node != startNode)
228 log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node);
229
230 if (throughout_sig != State::S1) {
231 if (ctrl != State::S1)
232 ctrl = module->And(NEW_ID, throughout_sig, ctrl);
233 else
234 ctrl = throughout_sig;
235 }
236
237 nodes[from_node].edges.push_back(make_pair(to_node, ctrl));
238 }
239
240 void createLink(int from_node, int to_node, SigBit ctrl = State::S1)
241 {
242 log_assert(!materialized);
243 log_assert(0 <= from_node && from_node < GetSize(nodes));
244 log_assert(0 <= to_node && to_node < GetSize(nodes));
245 log_assert(from_node != acceptNode);
246 log_assert(from_node != condNode);
247 log_assert(to_node != startNode);
248
249 if (from_node != startNode)
250 log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node);
251
252 if (throughout_sig != State::S1) {
253 if (ctrl != State::S1)
254 ctrl = module->And(NEW_ID, throughout_sig, ctrl);
255 else
256 ctrl = throughout_sig;
257 }
258
259 nodes[from_node].links.push_back(make_pair(to_node, ctrl));
260 }
261
262 void make_link_order(vector<int> &order, int node, int min)
263 {
264 order[node] = std::max(order[node], min);
265 for (auto &it : nodes[node].links)
266 make_link_order(order, it.first, order[node]+1);
267 }
268
269 // ----------------------------------------------------
270 // Generating NFSM circuit to acquire accept signal
271
272 SigBit getAccept()
273 {
274 log_assert(!materialized);
275 materialized = true;
276
277 vector<Wire*> state_wire(GetSize(nodes));
278 vector<SigBit> state_sig(GetSize(nodes));
279 vector<SigBit> next_state_sig(GetSize(nodes));
280
281 // Create state signals
282
283 {
284 SigBit not_disable = State::S1;
285
286 if (disable_sig != State::S0)
287 not_disable = module->Not(NEW_ID, disable_sig);
288
289 for (int i = 0; i < GetSize(nodes); i++)
290 {
291 Wire *w = module->addWire(NEW_ID);
292 state_wire[i] = w;
293 state_sig[i] = w;
294
295 if (i == startNode)
296 state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig);
297
298 if (disable_sig != State::S0)
299 state_sig[i] = module->And(NEW_ID, state_sig[i], not_disable);
300 }
301 }
302
303 // Follow Links
304
305 {
306 vector<int> node_order(GetSize(nodes));
307 vector<vector<int>> order_to_nodes;
308
309 for (int i = 0; i < GetSize(nodes); i++)
310 make_link_order(node_order, i, 0);
311
312 for (int i = 0; i < GetSize(nodes); i++) {
313 if (node_order[i] >= GetSize(order_to_nodes))
314 order_to_nodes.resize(node_order[i]+1);
315 order_to_nodes[node_order[i]].push_back(i);
316 }
317
318 for (int order = 0; order < GetSize(order_to_nodes); order++)
319 for (int node : order_to_nodes[order])
320 {
321 for (auto &it : nodes[node].links)
322 {
323 int target = it.first;
324 SigBit ctrl = state_sig[node];
325
326 if (it.second != State::S1)
327 ctrl = module->And(NEW_ID, ctrl, it.second);
328
329 state_sig[target] = module->Or(NEW_ID, state_sig[target], ctrl);
330 }
331 }
332 }
333
334 // Construct activations
335
336 {
337 vector<SigSpec> activate_sig(GetSize(nodes));
338 vector<SigBit> activate_bit(GetSize(nodes));
339
340 for (int i = 0; i < GetSize(nodes); i++) {
341 for (auto &it : nodes[i].edges)
342 activate_sig[it.first].append(module->And(NEW_ID, state_sig[i], it.second));
343 }
344
345 for (int i = 0; i < GetSize(nodes); i++) {
346 if (GetSize(activate_sig[i]) == 0)
347 next_state_sig[i] = State::S0;
348 else if (GetSize(activate_sig[i]) == 1)
349 next_state_sig[i] = activate_sig[i];
350 else
351 next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]);
352 }
353 }
354
355 // Create state FFs
356
357 for (int i = 0; i < GetSize(nodes); i++)
358 {
359 if (next_state_sig[i] != State::S0) {
360 clocking.addDff(NEW_ID, next_state_sig[i], state_wire[i], Const(0, 1));
361 } else {
362 module->connect(state_wire[i], State::S0);
363 }
364 }
365
366 final_accept_sig = state_sig[acceptNode];
367 return final_accept_sig;
368 }
369
370 // ----------------------------------------------------
371 // Generating quantifier-based NFSM circuit to acquire reject signal
372
373 SigBit getAnyAllRejectWorker(bool /* allMode */)
374 {
375 // FIXME
376 log_abort();
377 }
378
379 SigBit getAnyReject()
380 {
381 return getAnyAllRejectWorker(false);
382 }
383
384 SigBit getAllReject()
385 {
386 return getAnyAllRejectWorker(true);
387 }
388
389 // ----------------------------------------------------
390 // Generating DFSM circuit to acquire reject signal
391
392 void node_to_unode(int node, int unode, SigSpec ctrl)
393 {
394 if (node == acceptNode)
395 unodes[unode].accept.push_back(ctrl);
396
397 if (node == condNode)
398 unodes[unode].cond.push_back(ctrl);
399
400 for (auto &it : nodes[node].edges) {
401 if (it.second != State::S1) {
402 SigSpec s = {ctrl, it.second};
403 s.sort_and_unify();
404 unodes[unode].edges.push_back(make_pair(it.first, s));
405 } else {
406 unodes[unode].edges.push_back(make_pair(it.first, ctrl));
407 }
408 }
409
410 for (auto &it : nodes[node].links) {
411 if (it.second != State::S1) {
412 SigSpec s = {ctrl, it.second};
413 s.sort_and_unify();
414 node_to_unode(it.first, unode, s);
415 } else {
416 node_to_unode(it.first, unode, ctrl);
417 }
418 }
419 }
420
421 void mark_reachable_unode(int unode)
422 {
423 if (unodes[unode].reachable)
424 return;
425
426 unodes[unode].reachable = true;
427 for (auto &it : unodes[unode].edges)
428 mark_reachable_unode(it.first);
429 }
430
431 void usortint(vector<int> &vec)
432 {
433 vector<int> newvec;
434 std::sort(vec.begin(), vec.end());
435 for (int i = 0; i < GetSize(vec); i++)
436 if (i == GetSize(vec)-1 || vec[i] != vec[i+1])
437 newvec.push_back(vec[i]);
438 vec.swap(newvec);
439 }
440
441 bool cmp_ctrl(const pool<SigBit> &ctrl_bits, const SigSpec &ctrl)
442 {
443 for (int i = 0; i < GetSize(ctrl); i++)
444 if (ctrl_bits.count(ctrl[i]) == 0)
445 return false;
446 return true;
447 }
448
449 void create_dnode(const vector<int> &state, bool firstmatch, bool condaccept)
450 {
451 if (dnodes.count(state) != 0)
452 return;
453
454 SvaDFsmNode dnode;
455 dnodes[state] = SvaDFsmNode();
456
457 for (int unode : state) {
458 log_assert(unodes[unode].reachable);
459 for (auto &it : unodes[unode].edges)
460 dnode.ctrl.append(it.second);
461 for (auto &it : unodes[unode].accept)
462 dnode.ctrl.append(it);
463 for (auto &it : unodes[unode].cond)
464 dnode.ctrl.append(it);
465 }
466
467 dnode.ctrl.sort_and_unify();
468
469 if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) {
470 if (verific_verbose >= 2) {
471 log(" detected state explosion in DFSM generation:\n");
472 dump();
473 log(" ctrl signal: %s\n", log_signal(dnode.ctrl));
474 }
475 log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
476 GetSize(dnode.ctrl), verific_sva_fsm_limit);
477 }
478
479 for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)
480 {
481 Const ctrl_val(i, GetSize(dnode.ctrl));
482 pool<SigBit> ctrl_bits;
483
484 for (int i = 0; i < GetSize(dnode.ctrl); i++)
485 if (ctrl_val[i] == State::S1)
486 ctrl_bits.insert(dnode.ctrl[i]);
487
488 vector<int> new_state;
489 bool accept = false, cond = false;
490
491 for (int unode : state) {
492 for (auto &it : unodes[unode].accept)
493 if (cmp_ctrl(ctrl_bits, it))
494 accept = true;
495 for (auto &it : unodes[unode].cond)
496 if (cmp_ctrl(ctrl_bits, it))
497 cond = true;
498 }
499
500 bool new_state_cond = false;
501 bool new_state_noncond = false;
502
503 if (accept && condaccept)
504 accept = cond;
505
506 if (!accept || !firstmatch) {
507 for (int unode : state)
508 for (auto &it : unodes[unode].edges)
509 if (cmp_ctrl(ctrl_bits, it.second)) {
510 if (nodes.at(it.first).is_cond_node)
511 new_state_cond = true;
512 else
513 new_state_noncond = true;
514 new_state.push_back(it.first);
515 }
516 }
517
518 if (accept)
519 dnode.accept.push_back(ctrl_val);
520
521 if (condaccept && (!new_state_cond || !new_state_noncond))
522 new_state.clear();
523
524 if (new_state.empty()) {
525 if (!accept)
526 dnode.reject.push_back(ctrl_val);
527 } else {
528 usortint(new_state);
529 dnode.edges.push_back(make_pair(new_state, ctrl_val));
530 create_dnode(new_state, firstmatch, condaccept);
531 }
532 }
533
534 dnodes[state] = dnode;
535 }
536
537 void optimize_cond(vector<Const> &values)
538 {
539 bool did_something = true;
540
541 while (did_something)
542 {
543 did_something = false;
544
545 for (int i = 0; i < GetSize(values); i++)
546 for (int j = 0; j < GetSize(values); j++)
547 {
548 if (i == j)
549 continue;
550
551 log_assert(GetSize(values[i]) == GetSize(values[j]));
552
553 int delta_pos = -1;
554 bool i_within_j = true;
555 bool j_within_i = true;
556
557 for (int k = 0; k < GetSize(values[i]); k++) {
558 if (values[i][k] == State::Sa && values[j][k] != State::Sa) {
559 i_within_j = false;
560 continue;
561 }
562 if (values[i][k] != State::Sa && values[j][k] == State::Sa) {
563 j_within_i = false;
564 continue;
565 }
566 if (values[i][k] == values[j][k])
567 continue;
568 if (delta_pos >= 0)
569 goto next_pair;
570 delta_pos = k;
571 }
572
573 if (delta_pos >= 0 && i_within_j && j_within_i) {
574 did_something = true;
575 values[i][delta_pos] = State::Sa;
576 values[j] = values.back();
577 values.pop_back();
578 goto next_pair;
579 }
580
581 if (delta_pos < 0 && i_within_j) {
582 did_something = true;
583 values[i] = values.back();
584 values.pop_back();
585 goto next_pair;
586 }
587
588 if (delta_pos < 0 && j_within_i) {
589 did_something = true;
590 values[j] = values.back();
591 values.pop_back();
592 goto next_pair;
593 }
594 next_pair:;
595 }
596 }
597 }
598
599 SigBit make_cond_eq(const SigSpec &ctrl, const Const &value, SigBit enable = State::S1)
600 {
601 SigSpec sig_a, sig_b;
602
603 log_assert(GetSize(ctrl) == GetSize(value));
604
605 for (int i = 0; i < GetSize(ctrl); i++)
606 if (value[i] != State::Sa) {
607 sig_a.append(ctrl[i]);
608 sig_b.append(value[i]);
609 }
610
611 if (GetSize(sig_a) == 0)
612 return enable;
613
614 if (enable != State::S1) {
615 sig_a.append(enable);
616 sig_b.append(State::S1);
617 }
618
619 auto key = make_pair(sig_a, sig_b);
620
621 if (cond_eq_cache.count(key) == 0)
622 {
623 if (sig_b == State::S1)
624 cond_eq_cache[key] = sig_a;
625 else if (sig_b == State::S0)
626 cond_eq_cache[key] = module->Not(NEW_ID, sig_a);
627 else
628 cond_eq_cache[key] = module->Eq(NEW_ID, sig_a, sig_b);
629
630 if (verific_verbose >= 2) {
631 log(" Cond: %s := %s == %s\n", log_signal(cond_eq_cache[key]),
632 log_signal(sig_a), log_signal(sig_b));
633 }
634 }
635
636 return cond_eq_cache.at(key);
637 }
638
639 void getFirstAcceptReject(SigBit *accept_p, SigBit *reject_p)
640 {
641 log_assert(!materialized);
642 materialized = true;
643
644 // Create unlinked NFSM
645
646 unodes.resize(GetSize(nodes));
647
648 for (int node = 0; node < GetSize(nodes); node++)
649 node_to_unode(node, node, SigSpec());
650
651 mark_reachable_unode(startNode);
652
653 // Create DFSM
654
655 create_dnode(vector<int>{startNode}, true, false);
656 dnodes.sort();
657
658 // Create DFSM Circuit
659
660 SigSpec accept_sig, reject_sig;
661
662 for (auto &it : dnodes)
663 {
664 SvaDFsmNode &dnode = it.second;
665 dnode.ffoutwire = module->addWire(NEW_ID);
666 dnode.statesig = dnode.ffoutwire;
667
668 if (it.first == vector<int>{startNode})
669 dnode.statesig = module->Or(NEW_ID, dnode.statesig, trigger_sig);
670 }
671
672 for (auto &it : dnodes)
673 {
674 SvaDFsmNode &dnode = it.second;
675 dict<vector<int>, vector<Const>> edge_cond;
676
677 for (auto &edge : dnode.edges)
678 edge_cond[edge.first].push_back(edge.second);
679
680 for (auto &it : edge_cond) {
681 optimize_cond(it.second);
682 for (auto &value : it.second)
683 dnodes.at(it.first).nextstate.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
684 }
685
686 if (accept_p) {
687 vector<Const> accept_cond = dnode.accept;
688 optimize_cond(accept_cond);
689 for (auto &value : accept_cond)
690 accept_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
691 }
692
693 if (reject_p) {
694 vector<Const> reject_cond = dnode.reject;
695 optimize_cond(reject_cond);
696 for (auto &value : reject_cond)
697 reject_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
698 }
699 }
700
701 for (auto &it : dnodes)
702 {
703 SvaDFsmNode &dnode = it.second;
704 if (GetSize(dnode.nextstate) == 0) {
705 module->connect(dnode.ffoutwire, State::S0);
706 } else
707 if (GetSize(dnode.nextstate) == 1) {
708 clocking.addDff(NEW_ID, dnode.nextstate, dnode.ffoutwire, State::S0);
709 } else {
710 SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate);
711 clocking.addDff(NEW_ID, nextstate, dnode.ffoutwire, State::S0);
712 }
713 }
714
715 if (accept_p)
716 {
717 if (GetSize(accept_sig) == 0)
718 final_accept_sig = State::S0;
719 else if (GetSize(accept_sig) == 1)
720 final_accept_sig = accept_sig;
721 else
722 final_accept_sig = module->ReduceOr(NEW_ID, accept_sig);
723 *accept_p = final_accept_sig;
724 }
725
726 if (reject_p)
727 {
728 if (GetSize(reject_sig) == 0)
729 final_reject_sig = State::S0;
730 else if (GetSize(reject_sig) == 1)
731 final_reject_sig = reject_sig;
732 else
733 final_reject_sig = module->ReduceOr(NEW_ID, reject_sig);
734 *reject_p = final_reject_sig;
735 }
736 }
737
738 SigBit getFirstAccept()
739 {
740 SigBit accept;
741 getFirstAcceptReject(&accept, nullptr);
742 return accept;
743 }
744
745 SigBit getReject()
746 {
747 SigBit reject;
748 getFirstAcceptReject(nullptr, &reject);
749 return reject;
750 }
751
752 void getDFsm(SvaFsm &output_fsm, int output_start_node, int output_accept_node, int output_reject_node = -1, bool firstmatch = true, bool condaccept = false)
753 {
754 log_assert(!materialized);
755 materialized = true;
756
757 // Create unlinked NFSM
758
759 unodes.resize(GetSize(nodes));
760
761 for (int node = 0; node < GetSize(nodes); node++)
762 node_to_unode(node, node, SigSpec());
763
764 mark_reachable_unode(startNode);
765
766 // Create DFSM
767
768 create_dnode(vector<int>{startNode}, firstmatch, condaccept);
769 dnodes.sort();
770
771 // Create DFSM Graph
772
773 for (auto &it : dnodes)
774 {
775 SvaDFsmNode &dnode = it.second;
776 dnode.outnode = output_fsm.createNode();
777
778 if (it.first == vector<int>{startNode})
779 output_fsm.createLink(output_start_node, dnode.outnode);
780
781 if (output_accept_node >= 0) {
782 vector<Const> accept_cond = dnode.accept;
783 optimize_cond(accept_cond);
784 for (auto &value : accept_cond)
785 output_fsm.createLink(it.second.outnode, output_accept_node, make_cond_eq(dnode.ctrl, value));
786 }
787
788 if (output_reject_node >= 0) {
789 vector<Const> reject_cond = dnode.reject;
790 optimize_cond(reject_cond);
791 for (auto &value : reject_cond)
792 output_fsm.createLink(it.second.outnode, output_reject_node, make_cond_eq(dnode.ctrl, value));
793 }
794 }
795
796 for (auto &it : dnodes)
797 {
798 SvaDFsmNode &dnode = it.second;
799 dict<vector<int>, vector<Const>> edge_cond;
800
801 for (auto &edge : dnode.edges)
802 edge_cond[edge.first].push_back(edge.second);
803
804 for (auto &it : edge_cond) {
805 optimize_cond(it.second);
806 for (auto &value : it.second)
807 output_fsm.createEdge(dnode.outnode, dnodes.at(it.first).outnode, make_cond_eq(dnode.ctrl, value));
808 }
809 }
810 }
811
812 // ----------------------------------------------------
813 // State dump for verbose log messages
814
815 void dump_nodes()
816 {
817 if (nodes.empty())
818 return;
819
820 log(" non-deterministic encoding:\n");
821 for (int i = 0; i < GetSize(nodes); i++)
822 {
823 log(" node %d:%s\n", i,
824 i == startNode ? " [start]" :
825 i == acceptNode ? " [accept]" :
826 i == condNode ? " [cond]" : "");
827
828 for (auto &it : nodes[i].edges) {
829 if (it.second != State::S1)
830 log(" egde %s -> %d\n", log_signal(it.second), it.first);
831 else
832 log(" egde -> %d\n", it.first);
833 }
834
835 for (auto &it : nodes[i].links) {
836 if (it.second != State::S1)
837 log(" link %s -> %d\n", log_signal(it.second), it.first);
838 else
839 log(" link -> %d\n", it.first);
840 }
841 }
842 }
843
844 void dump_unodes()
845 {
846 if (unodes.empty())
847 return;
848
849 log(" unlinked non-deterministic encoding:\n");
850 for (int i = 0; i < GetSize(unodes); i++)
851 {
852 if (!unodes[i].reachable)
853 continue;
854
855 log(" unode %d:%s\n", i, i == startNode ? " [start]" : "");
856
857 for (auto &it : unodes[i].edges) {
858 if (!it.second.empty())
859 log(" egde %s -> %d\n", log_signal(it.second), it.first);
860 else
861 log(" egde -> %d\n", it.first);
862 }
863
864 for (auto &ctrl : unodes[i].accept) {
865 if (!ctrl.empty())
866 log(" accept %s\n", log_signal(ctrl));
867 else
868 log(" accept\n");
869 }
870
871 for (auto &ctrl : unodes[i].cond) {
872 if (!ctrl.empty())
873 log(" cond %s\n", log_signal(ctrl));
874 else
875 log(" cond\n");
876 }
877 }
878 }
879
880 void dump_dnodes()
881 {
882 if (dnodes.empty())
883 return;
884
885 log(" deterministic encoding:\n");
886 for (auto &it : dnodes)
887 {
888 log(" dnode {");
889 for (int i = 0; i < GetSize(it.first); i++)
890 log("%s%d", i ? "," : "", it.first[i]);
891 log("}:%s\n", GetSize(it.first) == 1 && it.first[0] == startNode ? " [start]" : "");
892
893 log(" ctrl %s\n", log_signal(it.second.ctrl));
894
895 for (auto &edge : it.second.edges) {
896 log(" edge %s -> {", log_signal(edge.second));
897 for (int i = 0; i < GetSize(edge.first); i++)
898 log("%s%d", i ? "," : "", edge.first[i]);
899 log("}\n");
900 }
901
902 for (auto &value : it.second.accept)
903 log(" accept %s\n", log_signal(value));
904
905 for (auto &value : it.second.reject)
906 log(" reject %s\n", log_signal(value));
907 }
908 }
909
910 void dump()
911 {
912 if (!nodes.empty())
913 log(" number of NFSM states: %d\n", GetSize(nodes));
914
915 if (!unodes.empty()) {
916 int count = 0;
917 for (auto &unode : unodes)
918 if (unode.reachable)
919 count++;
920 log(" number of reachable UFSM states: %d\n", count);
921 }
922
923 if (!dnodes.empty())
924 log(" number of DFSM states: %d\n", GetSize(dnodes));
925
926 if (verific_verbose >= 2) {
927 dump_nodes();
928 dump_unodes();
929 dump_dnodes();
930 }
931
932 if (trigger_sig != State::S1)
933 log(" trigger signal: %s\n", log_signal(trigger_sig));
934
935 if (final_accept_sig != State::Sx)
936 log(" accept signal: %s\n", log_signal(final_accept_sig));
937
938 if (final_reject_sig != State::Sx)
939 log(" reject signal: %s\n", log_signal(final_reject_sig));
940 }
941 };
942
943 PRIVATE_NAMESPACE_END
944
945 YOSYS_NAMESPACE_BEGIN
946
947 pool<int> verific_sva_prims = {
948 // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
949 PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
950 PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
951 PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
952 PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
953 PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
954 PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
955 PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
956 PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
957 PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
958 PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
959 PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
960 PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
961 PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
962 PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
963 PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
964 PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
965 PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
966 PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
967 PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
968 };
969
970 struct VerificSvaImporter
971 {
972 VerificImporter *importer = nullptr;
973 Module *module = nullptr;
974
975 Netlist *netlist = nullptr;
976 Instance *root = nullptr;
977
978 VerificClocking clocking;
979
980 bool mode_assert = false;
981 bool mode_assume = false;
982 bool mode_cover = false;
983 bool mode_trigger = false;
984
985 Instance *net_to_ast_driver(Net *n)
986 {
987 if (n == nullptr)
988 return nullptr;
989
990 if (n->IsMultipleDriven())
991 return nullptr;
992
993 Instance *inst = n->Driver();
994
995 if (inst == nullptr)
996 return nullptr;
997
998 if (!verific_sva_prims.count(inst->Type()))
999 return nullptr;
1000
1001 if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
1002 inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE ||
1003 inst->Type() == PRIM_SVA_PAST || inst->Type() == PRIM_SVA_TRIGGERED)
1004 return nullptr;
1005
1006 return inst;
1007 }
1008
1009 Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
1010 Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
1011 Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
1012 Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
1013 Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
1014
1015 // ----------------------------------------------------------
1016 // SVA Importer
1017
1018 struct ParserErrorException {
1019 };
1020
1021 [[noreturn]] void parser_error(std::string errmsg)
1022 {
1023 if (!importer->mode_keep)
1024 log_error("%s", errmsg.c_str());
1025 log_warning("%s", errmsg.c_str());
1026 throw ParserErrorException();
1027 }
1028
1029 [[noreturn]] void parser_error(std::string errmsg, linefile_type loc)
1030 {
1031 parser_error(stringf("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc)));
1032 }
1033
1034 [[noreturn]] void parser_error(std::string errmsg, Instance *inst)
1035 {
1036 parser_error(stringf("%s at %s (%s)", errmsg.c_str(), inst->View()->Owner()->Name(), inst->Name()), inst->Linefile());
1037 }
1038
1039 [[noreturn]] void parser_error(Instance *inst)
1040 {
1041 parser_error(stringf("Verific SVA primitive %s (%s) is currently unsupported in this context",
1042 inst->View()->Owner()->Name(), inst->Name()), inst->Linefile());
1043 }
1044
1045 dict<Net*, bool, hash_ptr_ops> check_expression_cache;
1046
1047 bool check_expression(Net *net, bool raise_error = false)
1048 {
1049 while (!check_expression_cache.count(net))
1050 {
1051 Instance *inst = net_to_ast_driver(net);
1052
1053 if (inst == nullptr) {
1054 check_expression_cache[net] = true;
1055 break;
1056 }
1057
1058 if (inst->Type() == PRIM_SVA_AT)
1059 {
1060 VerificClocking new_clocking(importer, net);
1061 log_assert(new_clocking.cond_net == nullptr);
1062 if (!clocking.property_matches_sequence(new_clocking))
1063 parser_error("Mixed clocking is currently not supported", inst);
1064 check_expression_cache[net] = check_expression(new_clocking.body_net, raise_error);
1065 break;
1066 }
1067
1068 if (inst->Type() == PRIM_SVA_FIRST_MATCH || inst->Type() == PRIM_SVA_NOT)
1069 {
1070 check_expression_cache[net] = check_expression(inst->GetInput(), raise_error);
1071 break;
1072 }
1073
1074 if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_INTERSECT ||
1075 inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT ||
1076 inst->Type() == PRIM_SVA_OR || inst->Type() == PRIM_SVA_AND)
1077 {
1078 check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error);
1079 break;
1080 }
1081
1082 if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
1083 {
1084 const char *sva_low_s = inst->GetAttValue("sva:low");
1085 const char *sva_high_s = inst->GetAttValue("sva:high");
1086
1087 int sva_low = atoi(sva_low_s);
1088 int sva_high = atoi(sva_high_s);
1089 bool sva_inf = !strcmp(sva_high_s, "$");
1090
1091 if (sva_low == 0 && sva_high == 0 && !sva_inf)
1092 check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error);
1093 else
1094 check_expression_cache[net] = false;
1095 break;
1096 }
1097
1098 check_expression_cache[net] = false;
1099 }
1100
1101 if (raise_error && !check_expression_cache.at(net))
1102 parser_error(net_to_ast_driver(net));
1103 return check_expression_cache.at(net);
1104 }
1105
1106 SigBit parse_expression(Net *net)
1107 {
1108 check_expression(net, true);
1109
1110 Instance *inst = net_to_ast_driver(net);
1111
1112 if (inst == nullptr) {
1113 return importer->net_map_at(net);
1114 }
1115
1116 if (inst->Type() == PRIM_SVA_AT)
1117 {
1118 VerificClocking new_clocking(importer, net);
1119 log_assert(new_clocking.cond_net == nullptr);
1120 if (!clocking.property_matches_sequence(new_clocking))
1121 parser_error("Mixed clocking is currently not supported", inst);
1122 return parse_expression(new_clocking.body_net);
1123 }
1124
1125 if (inst->Type() == PRIM_SVA_FIRST_MATCH)
1126 return parse_expression(inst->GetInput());
1127
1128 if (inst->Type() == PRIM_SVA_NOT)
1129 return module->Not(NEW_ID, parse_expression(inst->GetInput()));
1130
1131 if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR)
1132 return module->Or(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2()));
1133
1134 if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND || inst->Type() == PRIM_SVA_INTERSECT ||
1135 inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_SEQ_CONCAT)
1136 return module->And(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2()));
1137
1138 log_abort();
1139 }
1140
1141 bool check_zero_consecutive_repeat(Net *net)
1142 {
1143 Instance *inst = net_to_ast_driver(net);
1144
1145 if (inst == nullptr)
1146 return false;
1147
1148 if (inst->Type() != PRIM_SVA_CONSECUTIVE_REPEAT)
1149 return false;
1150
1151 const char *sva_low_s = inst->GetAttValue("sva:low");
1152 int sva_low = atoi(sva_low_s);
1153
1154 return sva_low == 0;
1155 }
1156
1157 int parse_consecutive_repeat(SvaFsm &fsm, int start_node, Net *net, bool add_pre_delay, bool add_post_delay)
1158 {
1159 Instance *inst = net_to_ast_driver(net);
1160
1161 log_assert(inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT);
1162
1163 const char *sva_low_s = inst->GetAttValue("sva:low");
1164 const char *sva_high_s = inst->GetAttValue("sva:high");
1165
1166 int sva_low = atoi(sva_low_s);
1167 int sva_high = atoi(sva_high_s);
1168 bool sva_inf = !strcmp(sva_high_s, "$");
1169
1170 Net *body_net = inst->GetInput();
1171
1172 if (add_pre_delay || add_post_delay)
1173 log_assert(sva_low == 0);
1174
1175 if (sva_low == 0) {
1176 if (!add_pre_delay && !add_post_delay)
1177 parser_error("Possibly zero-length consecutive repeat must follow or precede a delay of at least one cycle", inst);
1178 sva_low++;
1179 }
1180
1181 int node = fsm.createNode(start_node);
1182 start_node = node;
1183
1184 if (add_pre_delay) {
1185 node = fsm.createNode(start_node);
1186 fsm.createEdge(start_node, node);
1187 }
1188
1189 int prev_node = node;
1190 node = parse_sequence(fsm, node, body_net);
1191
1192 for (int i = 1; i < sva_low; i++)
1193 {
1194 int next_node = fsm.createNode();
1195 fsm.createEdge(node, next_node);
1196
1197 prev_node = node;
1198 node = parse_sequence(fsm, next_node, body_net);
1199 }
1200
1201 if (sva_inf)
1202 {
1203 log_assert(prev_node >= 0);
1204 fsm.createEdge(node, prev_node);
1205 }
1206 else
1207 {
1208 for (int i = sva_low; i < sva_high; i++)
1209 {
1210 int next_node = fsm.createNode();
1211 fsm.createEdge(node, next_node);
1212
1213 prev_node = node;
1214 node = parse_sequence(fsm, next_node, body_net);
1215
1216 fsm.createLink(prev_node, node);
1217 }
1218 }
1219
1220 if (add_post_delay) {
1221 int next_node = fsm.createNode();
1222 fsm.createEdge(node, next_node);
1223 node = next_node;
1224 }
1225
1226 if (add_pre_delay || add_post_delay)
1227 fsm.createLink(start_node, node);
1228
1229 return node;
1230 }
1231
1232 int parse_sequence(SvaFsm &fsm, int start_node, Net *net)
1233 {
1234 if (check_expression(net)) {
1235 int node = fsm.createNode();
1236 fsm.createLink(start_node, node, parse_expression(net));
1237 return node;
1238 }
1239
1240 Instance *inst = net_to_ast_driver(net);
1241
1242 if (inst->Type() == PRIM_SVA_AT)
1243 {
1244 VerificClocking new_clocking(importer, net);
1245 log_assert(new_clocking.cond_net == nullptr);
1246 if (!clocking.property_matches_sequence(new_clocking))
1247 parser_error("Mixed clocking is currently not supported", inst);
1248 return parse_sequence(fsm, start_node, new_clocking.body_net);
1249 }
1250
1251 if (inst->Type() == PRIM_SVA_FIRST_MATCH)
1252 {
1253 SvaFsm match_fsm(clocking);
1254 match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode);
1255
1256 int node = fsm.createNode();
1257 match_fsm.getDFsm(fsm, start_node, node);
1258
1259 if (verific_verbose) {
1260 log(" First Match FSM:\n");
1261 match_fsm.dump();
1262 }
1263
1264 return node;
1265 }
1266
1267 if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
1268 {
1269 const char *sva_low_s = inst->GetAttValue("sva:low");
1270 const char *sva_high_s = inst->GetAttValue("sva:high");
1271
1272 int sva_low = atoi(sva_low_s);
1273 int sva_high = atoi(sva_high_s);
1274 bool sva_inf = !strcmp(sva_high_s, "$");
1275
1276 int node = -1;
1277 bool past_add_delay = false;
1278
1279 if (check_zero_consecutive_repeat(inst->GetInput1()) && sva_low > 0) {
1280 node = parse_consecutive_repeat(fsm, start_node, inst->GetInput1(), false, true);
1281 sva_low--, sva_high--;
1282 } else {
1283 node = parse_sequence(fsm, start_node, inst->GetInput1());
1284 }
1285
1286 if (check_zero_consecutive_repeat(inst->GetInput2()) && sva_low > 0) {
1287 past_add_delay = true;
1288 sva_low--, sva_high--;
1289 }
1290
1291 for (int i = 0; i < sva_low; i++) {
1292 int next_node = fsm.createNode();
1293 fsm.createEdge(node, next_node);
1294 node = next_node;
1295 }
1296
1297 if (sva_inf)
1298 {
1299 fsm.createEdge(node, node);
1300 }
1301 else
1302 {
1303 for (int i = sva_low; i < sva_high; i++)
1304 {
1305 int next_node = fsm.createNode();
1306 fsm.createEdge(node, next_node);
1307 fsm.createLink(node, next_node);
1308 node = next_node;
1309 }
1310 }
1311
1312 if (past_add_delay)
1313 node = parse_consecutive_repeat(fsm, node, inst->GetInput2(), true, false);
1314 else
1315 node = parse_sequence(fsm, node, inst->GetInput2());
1316
1317 return node;
1318 }
1319
1320 if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
1321 {
1322 return parse_consecutive_repeat(fsm, start_node, net, false, false);
1323 }
1324
1325 if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT)
1326 {
1327 const char *sva_low_s = inst->GetAttValue("sva:low");
1328 const char *sva_high_s = inst->GetAttValue("sva:high");
1329
1330 int sva_low = atoi(sva_low_s);
1331 int sva_high = atoi(sva_high_s);
1332 bool sva_inf = !strcmp(sva_high_s, "$");
1333
1334 Net *body_net = inst->GetInput();
1335 int node = fsm.createNode(start_node);
1336
1337 SigBit cond = parse_expression(body_net);
1338 SigBit not_cond = module->Not(NEW_ID, cond);
1339
1340 for (int i = 0; i < sva_low; i++)
1341 {
1342 int wait_node = fsm.createNode();
1343 fsm.createEdge(wait_node, wait_node, not_cond);
1344
1345 if (i == 0)
1346 fsm.createLink(node, wait_node);
1347 else
1348 fsm.createEdge(node, wait_node);
1349
1350 int next_node = fsm.createNode();
1351 fsm.createLink(wait_node, next_node, cond);
1352
1353 node = next_node;
1354 }
1355
1356 if (sva_inf)
1357 {
1358 int wait_node = fsm.createNode();
1359 fsm.createEdge(wait_node, wait_node, not_cond);
1360 fsm.createEdge(node, wait_node);
1361 fsm.createLink(wait_node, node, cond);
1362 }
1363 else
1364 {
1365 for (int i = sva_low; i < sva_high; i++)
1366 {
1367 int wait_node = fsm.createNode();
1368 fsm.createEdge(wait_node, wait_node, not_cond);
1369
1370 if (i == 0)
1371 fsm.createLink(node, wait_node);
1372 else
1373 fsm.createEdge(node, wait_node);
1374
1375 int next_node = fsm.createNode();
1376 fsm.createLink(wait_node, next_node, cond);
1377
1378 fsm.createLink(node, next_node);
1379 node = next_node;
1380 }
1381 }
1382
1383 if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT)
1384 fsm.createEdge(node, node);
1385
1386 return node;
1387 }
1388
1389 if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR)
1390 {
1391 int node = parse_sequence(fsm, start_node, inst->GetInput1());
1392 int node2 = parse_sequence(fsm, start_node, inst->GetInput2());
1393 fsm.createLink(node2, node);
1394 return node;
1395 }
1396
1397 if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND)
1398 {
1399 SvaFsm fsm1(clocking);
1400 fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode);
1401
1402 SvaFsm fsm2(clocking);
1403 fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode);
1404
1405 SvaFsm combined_fsm(clocking);
1406 fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
1407 fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
1408
1409 int node = fsm.createNode();
1410 combined_fsm.getDFsm(fsm, start_node, -1, node);
1411
1412 if (verific_verbose)
1413 {
1414 log(" Left And FSM:\n");
1415 fsm1.dump();
1416
1417 log(" Right And FSM:\n");
1418 fsm1.dump();
1419
1420 log(" Combined And FSM:\n");
1421 combined_fsm.dump();
1422 }
1423
1424 return node;
1425 }
1426
1427 if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN)
1428 {
1429 SvaFsm intersect_fsm(clocking);
1430
1431 if (inst->Type() == PRIM_SVA_INTERSECT)
1432 {
1433 intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput1()), intersect_fsm.acceptNode);
1434 }
1435 else
1436 {
1437 int n = intersect_fsm.createNode();
1438 intersect_fsm.createLink(intersect_fsm.createStartNode(), n);
1439 intersect_fsm.createEdge(n, n);
1440
1441 n = parse_sequence(intersect_fsm, n, inst->GetInput1());
1442
1443 intersect_fsm.createLink(n, intersect_fsm.acceptNode);
1444 intersect_fsm.createEdge(n, n);
1445 }
1446
1447 intersect_fsm.in_cond_mode = true;
1448 intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput2()), intersect_fsm.condNode);
1449 intersect_fsm.in_cond_mode = false;
1450
1451 int node = fsm.createNode();
1452 intersect_fsm.getDFsm(fsm, start_node, node, -1, false, true);
1453
1454 if (verific_verbose) {
1455 log(" Intersect FSM:\n");
1456 intersect_fsm.dump();
1457 }
1458
1459 return node;
1460 }
1461
1462 if (inst->Type() == PRIM_SVA_THROUGHOUT)
1463 {
1464 SigBit expr = parse_expression(inst->GetInput1());
1465
1466 fsm.pushThroughout(expr);
1467 int node = parse_sequence(fsm, start_node, inst->GetInput2());
1468 fsm.popThroughout();
1469
1470 return node;
1471 }
1472
1473 parser_error(inst);
1474 }
1475
1476 void get_fsm_accept_reject(SvaFsm &fsm, SigBit *accept_p, SigBit *reject_p, bool swap_accept_reject = false)
1477 {
1478 log_assert(accept_p != nullptr || reject_p != nullptr);
1479
1480 if (swap_accept_reject)
1481 get_fsm_accept_reject(fsm, reject_p, accept_p);
1482 else if (reject_p == nullptr)
1483 *accept_p = fsm.getAccept();
1484 else if (accept_p == nullptr)
1485 *reject_p = fsm.getReject();
1486 else
1487 fsm.getFirstAcceptReject(accept_p, reject_p);
1488 }
1489
1490 bool eventually_property(Net *&net, SigBit &trig)
1491 {
1492 Instance *inst = net_to_ast_driver(net);
1493
1494 if (inst == nullptr)
1495 return false;
1496
1497 if (clocking.cond_net != nullptr)
1498 trig = importer->net_map_at(clocking.cond_net);
1499 else
1500 trig = State::S1;
1501
1502 if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
1503 {
1504 if (mode_cover || mode_trigger)
1505 parser_error(inst);
1506
1507 net = inst->GetInput();
1508 clocking.cond_net = nullptr;
1509
1510 return true;
1511 }
1512
1513 if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
1514 inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
1515 {
1516 Net *antecedent_net = inst->GetInput1();
1517 Net *consequent_net = inst->GetInput2();
1518
1519 Instance *consequent_inst = net_to_ast_driver(consequent_net);
1520
1521 if (consequent_inst == nullptr)
1522 return false;
1523
1524 if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY)
1525 return false;
1526
1527 if (mode_cover || mode_trigger)
1528 parser_error(consequent_inst);
1529
1530 int node;
1531
1532 SvaFsm antecedent_fsm(clocking, trig);
1533 node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
1534 if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
1535 int next_node = antecedent_fsm.createNode();
1536 antecedent_fsm.createEdge(node, next_node);
1537 node = next_node;
1538 }
1539 antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
1540
1541 trig = antecedent_fsm.getAccept();
1542 net = consequent_inst->GetInput();
1543 clocking.cond_net = nullptr;
1544
1545 if (verific_verbose) {
1546 log(" Eventually Antecedent FSM:\n");
1547 antecedent_fsm.dump();
1548 }
1549
1550 return true;
1551 }
1552
1553 return false;
1554 }
1555
1556 void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
1557 {
1558 Instance *inst = net_to_ast_driver(net);
1559
1560 SigBit trig = State::S1;
1561
1562 if (clocking.cond_net != nullptr)
1563 trig = importer->net_map_at(clocking.cond_net);
1564
1565 if (inst == nullptr)
1566 {
1567 log_assert(trig == State::S1);
1568
1569 if (accept_p != nullptr)
1570 *accept_p = importer->net_map_at(net);
1571 if (reject_p != nullptr)
1572 *reject_p = module->Not(NEW_ID, importer->net_map_at(net));
1573 }
1574 else
1575 if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
1576 inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
1577 {
1578 Net *antecedent_net = inst->GetInput1();
1579 Net *consequent_net = inst->GetInput2();
1580 int node;
1581
1582 SvaFsm antecedent_fsm(clocking, trig);
1583 node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
1584 if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
1585 int next_node = antecedent_fsm.createNode();
1586 antecedent_fsm.createEdge(node, next_node);
1587 node = next_node;
1588 }
1589
1590 Instance *consequent_inst = net_to_ast_driver(consequent_net);
1591
1592 if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
1593 consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH))
1594 {
1595 bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
1596
1597 Net *until_net = consequent_inst->GetInput2();
1598 consequent_net = consequent_inst->GetInput1();
1599 consequent_inst = net_to_ast_driver(consequent_net);
1600
1601 SigBit until_sig = parse_expression(until_net);
1602 SigBit not_until_sig = module->Not(NEW_ID, until_sig);
1603 antecedent_fsm.createEdge(node, node, not_until_sig);
1604
1605 antecedent_fsm.createLink(node, antecedent_fsm.acceptNode, until_with ? State::S1 : not_until_sig);
1606 }
1607 else
1608 {
1609 antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
1610 }
1611
1612 SigBit antecedent_match = antecedent_fsm.getAccept();
1613
1614 if (verific_verbose) {
1615 log(" Antecedent FSM:\n");
1616 antecedent_fsm.dump();
1617 }
1618
1619 bool consequent_not = false;
1620 if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) {
1621 consequent_not = true;
1622 consequent_net = consequent_inst->GetInput();
1623 consequent_inst = net_to_ast_driver(consequent_net);
1624 }
1625
1626 SvaFsm consequent_fsm(clocking, antecedent_match);
1627 node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net);
1628 consequent_fsm.createLink(node, consequent_fsm.acceptNode);
1629
1630 get_fsm_accept_reject(consequent_fsm, accept_p, reject_p, consequent_not);
1631
1632 if (verific_verbose) {
1633 log(" Consequent FSM:\n");
1634 consequent_fsm.dump();
1635 }
1636 }
1637 else
1638 {
1639 bool prop_not = inst->Type() == PRIM_SVA_NOT;
1640 if (prop_not) {
1641 net = inst->GetInput();
1642 inst = net_to_ast_driver(net);
1643 }
1644
1645 SvaFsm fsm(clocking, trig);
1646 int node = parse_sequence(fsm, fsm.createStartNode(), net);
1647 fsm.createLink(node, fsm.acceptNode);
1648
1649 get_fsm_accept_reject(fsm, accept_p, reject_p, prop_not);
1650
1651 if (verific_verbose) {
1652 log(" Sequence FSM:\n");
1653 fsm.dump();
1654 }
1655 }
1656 }
1657
1658 void import()
1659 {
1660 try
1661 {
1662 module = importer->module;
1663 netlist = root->Owner();
1664
1665 if (verific_verbose)
1666 log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
1667 LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
1668
1669 RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
1670
1671 // parse SVA sequence into trigger signal
1672
1673 clocking = VerificClocking(importer, root->GetInput(), true);
1674 SigBit accept_bit = State::S0, reject_bit = State::S0;
1675
1676 if (clocking.body_net == nullptr)
1677 {
1678 if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr || clocking.cond_net != nullptr)
1679 parser_error(stringf("Failed to parse SVA clocking"), root);
1680
1681 if (mode_assert || mode_assume) {
1682 reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput()));
1683 } else {
1684 accept_bit = parse_expression(root->GetInput());
1685 }
1686 }
1687 else
1688 {
1689 Net *net = clocking.body_net;
1690 SigBit trig;
1691
1692 if (eventually_property(net, trig))
1693 {
1694 SigBit sig_a, sig_en = trig;
1695 parse_property(net, &sig_a, nullptr);
1696
1697 // add final FF stage
1698
1699 SigBit sig_a_q, sig_en_q;
1700
1701 if (clocking.body_net == nullptr) {
1702 sig_a_q = sig_a;
1703 sig_en_q = sig_en;
1704 } else {
1705 sig_a_q = module->addWire(NEW_ID);
1706 sig_en_q = module->addWire(NEW_ID);
1707 clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
1708 clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
1709 }
1710
1711 // generate fair/live cell
1712
1713 RTLIL::Cell *c = nullptr;
1714
1715 if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q);
1716 if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q);
1717
1718 importer->import_attributes(c->attributes, root);
1719
1720 return;
1721 }
1722 else
1723 {
1724 if (mode_assert || mode_assume) {
1725 parse_property(net, nullptr, &reject_bit);
1726 } else {
1727 parse_property(net, &accept_bit, nullptr);
1728 }
1729 }
1730 }
1731
1732 if (mode_trigger)
1733 {
1734 module->connect(importer->net_map_at(root->GetOutput()), accept_bit);
1735 }
1736 else
1737 {
1738 SigBit sig_a = module->Not(NEW_ID, reject_bit);
1739 SigBit sig_en = module->Or(NEW_ID, accept_bit, reject_bit);
1740
1741 // add final FF stage
1742
1743 SigBit sig_a_q, sig_en_q;
1744
1745 if (clocking.body_net == nullptr) {
1746 sig_a_q = sig_a;
1747 sig_en_q = sig_en;
1748 } else {
1749 sig_a_q = module->addWire(NEW_ID);
1750 sig_en_q = module->addWire(NEW_ID);
1751 clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
1752 clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
1753 }
1754
1755 // generate assert/assume/cover cell
1756
1757 RTLIL::Cell *c = nullptr;
1758
1759 if (mode_assert) c = module->addAssert(root_name, sig_a_q, sig_en_q);
1760 if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q);
1761 if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_q);
1762
1763 importer->import_attributes(c->attributes, root);
1764 }
1765 }
1766 catch (ParserErrorException)
1767 {
1768 }
1769 }
1770 };
1771
1772 void verific_import_sva_assert(VerificImporter *importer, Instance *inst)
1773 {
1774 VerificSvaImporter worker;
1775 worker.importer = importer;
1776 worker.root = inst;
1777 worker.mode_assert = true;
1778 worker.import();
1779 }
1780
1781 void verific_import_sva_assume(VerificImporter *importer, Instance *inst)
1782 {
1783 VerificSvaImporter worker;
1784 worker.importer = importer;
1785 worker.root = inst;
1786 worker.mode_assume = true;
1787 worker.import();
1788 }
1789
1790 void verific_import_sva_cover(VerificImporter *importer, Instance *inst)
1791 {
1792 VerificSvaImporter worker;
1793 worker.importer = importer;
1794 worker.root = inst;
1795 worker.mode_cover = true;
1796 worker.import();
1797 }
1798
1799 void verific_import_sva_trigger(VerificImporter *importer, Instance *inst)
1800 {
1801 VerificSvaImporter worker;
1802 worker.importer = importer;
1803 worker.root = inst;
1804 worker.mode_trigger = true;
1805 worker.import();
1806 }
1807
1808 bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net)
1809 {
1810 VerificSvaImporter worker;
1811 worker.importer = importer;
1812 return worker.net_to_ast_driver(net) != nullptr;
1813 }
1814
1815 YOSYS_NAMESPACE_END