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