2 * yosys -- Yosys Open SYnthesis Suite
4 * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
6 * Permission to use, copy, modify, and/or distribute this software for any
7 * purpose with or without fee is hereby granted, provided that the above
8 * copyright notice and this permission notice appear in all copies.
10 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
11 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
12 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
13 * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
14 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
15 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
16 * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
21 // Currently supported SVA sequence and property syntax:
22 // http://symbiyosys.readthedocs.io/en/latest/verific.html
24 // Next gen property syntax:
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)
32 // antecedent_condition:
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
50 // sequence ##N sequence
51 // sequence ##[*] sequence
52 // sequence ##[+] sequence
53 // sequence ##[N:M] sequence
54 // sequence ##[N:$] sequence
60 // sequence or sequence
61 // sequence and sequence
62 // expression throughout sequence
63 // sequence intersect sequence
64 // sequence within sequence
65 // first_match( sequence )
74 #include "kernel/yosys.h"
75 #include "frontends/verific/verific.h"
79 #ifdef VERIFIC_NAMESPACE
80 using namespace Verific
;
83 PRIVATE_NAMESPACE_BEGIN
85 // Non-deterministic FSM
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
;
94 // Non-deterministic FSM after resolving links
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
;
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.
110 vector
<pair
<vector
<int>, Const
>> edges
;
111 vector
<Const
> accept
, reject
;
113 // additional temp data for getReject()
118 // additional temp data for getDFsm()
125 VerificClocking clocking
;
127 SigBit trigger_sig
= State::S1
, disable_sig
;
128 SigBit throughout_sig
= State::S1
;
129 bool in_cond_mode
= false;
131 vector
<SigBit
> disable_stack
;
132 vector
<SigBit
> throughout_stack
;
134 int startNode
, acceptNode
, condNode
;
135 vector
<SvaNFsmNode
> nodes
;
137 vector
<SvaUFsmNode
> unodes
;
138 dict
<vector
<int>, SvaDFsmNode
> dnodes
;
139 dict
<pair
<SigSpec
, SigSpec
>, SigBit
> cond_eq_cache
;
140 bool materialized
= false;
142 SigBit final_accept_sig
= State::Sx
;
143 SigBit final_reject_sig
= State::Sx
;
145 SvaFsm(const VerificClocking
&clking
, SigBit trig
= State::S1
)
147 module
= clking
.module
;
151 startNode
= createNode();
152 acceptNode
= createNode();
155 condNode
= createNode();
156 in_cond_mode
= false;
159 void pushDisable(SigBit sig
)
161 log_assert(!materialized
);
163 disable_stack
.push_back(disable_sig
);
165 if (disable_sig
== State::S0
)
168 disable_sig
= module
->Or(NEW_ID
, disable_sig
, sig
);
173 log_assert(!materialized
);
174 log_assert(!disable_stack
.empty());
176 disable_sig
= disable_stack
.back();
177 disable_stack
.pop_back();
180 void pushThroughout(SigBit sig
)
182 log_assert(!materialized
);
184 throughout_stack
.push_back(throughout_sig
);
186 if (throughout_sig
== State::S1
)
187 throughout_sig
= sig
;
189 throughout_sig
= module
->And(NEW_ID
, throughout_sig
, sig
);
194 log_assert(!materialized
);
195 log_assert(!throughout_stack
.empty());
197 throughout_sig
= throughout_stack
.back();
198 throughout_stack
.pop_back();
201 int createNode(int link_node
= -1)
203 log_assert(!materialized
);
205 int idx
= GetSize(nodes
);
206 nodes
.push_back(SvaNFsmNode());
207 nodes
.back().is_cond_node
= in_cond_mode
;
209 createLink(link_node
, idx
);
213 int createStartNode()
215 return createNode(startNode
);
218 void createEdge(int from_node
, int to_node
, SigBit ctrl
= State::S1
)
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
);
229 if (from_node
!= startNode
)
230 log_assert(nodes
.at(from_node
).is_cond_node
== nodes
.at(to_node
).is_cond_node
);
232 if (throughout_sig
!= State::S1
) {
233 if (ctrl
!= State::S1
)
234 ctrl
= module
->And(NEW_ID
, throughout_sig
, ctrl
);
236 ctrl
= throughout_sig
;
239 nodes
[from_node
].edges
.push_back(make_pair(to_node
, ctrl
));
242 void createLink(int from_node
, int to_node
, SigBit ctrl
= State::S1
)
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
);
251 if (from_node
!= startNode
)
252 log_assert(nodes
.at(from_node
).is_cond_node
== nodes
.at(to_node
).is_cond_node
);
254 if (throughout_sig
!= State::S1
) {
255 if (ctrl
!= State::S1
)
256 ctrl
= module
->And(NEW_ID
, throughout_sig
, ctrl
);
258 ctrl
= throughout_sig
;
261 nodes
[from_node
].links
.push_back(make_pair(to_node
, ctrl
));
264 void make_link_order(vector
<int> &order
, int node
, int min
)
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);
271 // ----------------------------------------------------
272 // Generating NFSM circuit to acquire accept signal
276 log_assert(!materialized
);
279 vector
<Wire
*> state_wire(GetSize(nodes
));
280 vector
<SigBit
> state_sig(GetSize(nodes
));
281 vector
<SigBit
> next_state_sig(GetSize(nodes
));
283 // Create state signals
286 SigBit not_disable
= State::S1
;
288 if (disable_sig
!= State::S0
)
289 not_disable
= module
->Not(NEW_ID
, disable_sig
);
291 for (int i
= 0; i
< GetSize(nodes
); i
++)
293 Wire
*w
= module
->addWire(NEW_ID
);
298 state_sig
[i
] = module
->Or(NEW_ID
, state_sig
[i
], trigger_sig
);
300 if (disable_sig
!= State::S0
)
301 state_sig
[i
] = module
->And(NEW_ID
, state_sig
[i
], not_disable
);
308 vector
<int> node_order(GetSize(nodes
));
309 vector
<vector
<int>> order_to_nodes
;
311 for (int i
= 0; i
< GetSize(nodes
); i
++)
312 make_link_order(node_order
, i
, 0);
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
);
320 for (int order
= 0; order
< GetSize(order_to_nodes
); order
++)
321 for (int node
: order_to_nodes
[order
])
323 for (auto &it
: nodes
[node
].links
)
325 int target
= it
.first
;
326 SigBit ctrl
= state_sig
[node
];
328 if (it
.second
!= State::S1
)
329 ctrl
= module
->And(NEW_ID
, ctrl
, it
.second
);
331 state_sig
[target
] = module
->Or(NEW_ID
, state_sig
[target
], ctrl
);
336 // Construct activations
339 vector
<SigSpec
> activate_sig(GetSize(nodes
));
340 vector
<SigBit
> activate_bit(GetSize(nodes
));
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
));
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
];
353 next_state_sig
[i
] = module
->ReduceOr(NEW_ID
, activate_sig
[i
]);
359 for (int i
= 0; i
< GetSize(nodes
); i
++)
361 if (next_state_sig
[i
] != State::S0
) {
362 clocking
.addDff(NEW_ID
, next_state_sig
[i
], state_wire
[i
], State::S0
);
364 module
->connect(state_wire
[i
], State::S0
);
368 final_accept_sig
= state_sig
[acceptNode
];
369 return final_accept_sig
;
372 // ----------------------------------------------------
373 // Generating quantifier-based NFSM circuit to acquire reject signal
375 SigBit
getAnyAllRejectWorker(bool /* allMode */)
381 SigBit
getAnyReject()
383 return getAnyAllRejectWorker(false);
386 SigBit
getAllReject()
388 return getAnyAllRejectWorker(true);
391 // ----------------------------------------------------
392 // Generating DFSM circuit to acquire reject signal
394 void node_to_unode(int node
, int unode
, SigSpec ctrl
)
396 if (node
== acceptNode
)
397 unodes
[unode
].accept
.push_back(ctrl
);
399 if (node
== condNode
)
400 unodes
[unode
].cond
.push_back(ctrl
);
402 for (auto &it
: nodes
[node
].edges
) {
403 if (it
.second
!= State::S1
) {
404 SigSpec s
= {ctrl
, it
.second
};
406 unodes
[unode
].edges
.push_back(make_pair(it
.first
, s
));
408 unodes
[unode
].edges
.push_back(make_pair(it
.first
, ctrl
));
412 for (auto &it
: nodes
[node
].links
) {
413 if (it
.second
!= State::S1
) {
414 SigSpec s
= {ctrl
, it
.second
};
416 node_to_unode(it
.first
, unode
, s
);
418 node_to_unode(it
.first
, unode
, ctrl
);
423 void mark_reachable_unode(int unode
)
425 if (unodes
[unode
].reachable
)
428 unodes
[unode
].reachable
= true;
429 for (auto &it
: unodes
[unode
].edges
)
430 mark_reachable_unode(it
.first
);
433 void usortint(vector
<int> &vec
)
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
]);
443 bool cmp_ctrl(const pool
<SigBit
> &ctrl_bits
, const SigSpec
&ctrl
)
445 for (int i
= 0; i
< GetSize(ctrl
); i
++)
446 if (ctrl_bits
.count(ctrl
[i
]) == 0)
451 void create_dnode(const vector
<int> &state
, bool firstmatch
, bool condaccept
)
453 if (dnodes
.count(state
) != 0)
457 dnodes
[state
] = SvaDFsmNode();
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
);
469 dnode
.ctrl
.sort_and_unify();
471 if (GetSize(dnode
.ctrl
) > verific_sva_fsm_limit
) {
472 if (verific_verbose
>= 2) {
473 log(" detected state explosion in DFSM generation:\n");
475 log(" ctrl signal: %s\n", log_signal(dnode
.ctrl
));
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
);
481 for (int i
= 0; i
< (1 << GetSize(dnode
.ctrl
)); i
++)
483 Const
ctrl_val(i
, GetSize(dnode
.ctrl
));
484 pool
<SigBit
> ctrl_bits
;
486 for (int i
= 0; i
< GetSize(dnode
.ctrl
); i
++)
487 if (ctrl_val
[i
] == State::S1
)
488 ctrl_bits
.insert(dnode
.ctrl
[i
]);
490 vector
<int> new_state
;
491 bool accept
= false, cond
= false;
493 for (int unode
: state
) {
494 for (auto &it
: unodes
[unode
].accept
)
495 if (cmp_ctrl(ctrl_bits
, it
))
497 for (auto &it
: unodes
[unode
].cond
)
498 if (cmp_ctrl(ctrl_bits
, it
))
502 bool new_state_cond
= false;
503 bool new_state_noncond
= false;
505 if (accept
&& condaccept
)
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;
515 new_state_noncond
= true;
516 new_state
.push_back(it
.first
);
521 dnode
.accept
.push_back(ctrl_val
);
523 if (condaccept
&& (!new_state_cond
|| !new_state_noncond
))
526 if (new_state
.empty()) {
528 dnode
.reject
.push_back(ctrl_val
);
531 dnode
.edges
.push_back(make_pair(new_state
, ctrl_val
));
532 create_dnode(new_state
, firstmatch
, condaccept
);
536 dnodes
[state
] = dnode
;
539 void optimize_cond(vector
<Const
> &values
)
541 bool did_something
= true;
543 while (did_something
)
545 did_something
= false;
547 for (int i
= 0; i
< GetSize(values
); i
++)
548 for (int j
= 0; j
< GetSize(values
); j
++)
553 log_assert(GetSize(values
[i
]) == GetSize(values
[j
]));
556 bool i_within_j
= true;
557 bool j_within_i
= true;
559 for (int k
= 0; k
< GetSize(values
[i
]); k
++) {
560 if (values
[i
][k
] == State::Sa
&& values
[j
][k
] != State::Sa
) {
564 if (values
[i
][k
] != State::Sa
&& values
[j
][k
] == State::Sa
) {
568 if (values
[i
][k
] == values
[j
][k
])
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();
583 if (delta_pos
< 0 && i_within_j
) {
584 did_something
= true;
585 values
[i
] = values
.back();
590 if (delta_pos
< 0 && j_within_i
) {
591 did_something
= true;
592 values
[j
] = values
.back();
601 SigBit
make_cond_eq(const SigSpec
&ctrl
, const Const
&value
, SigBit enable
= State::S1
)
603 SigSpec sig_a
, sig_b
;
605 log_assert(GetSize(ctrl
) == GetSize(value
));
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
]);
613 if (GetSize(sig_a
) == 0)
616 if (enable
!= State::S1
) {
617 sig_a
.append(enable
);
618 sig_b
.append(State::S1
);
621 auto key
= make_pair(sig_a
, sig_b
);
623 if (cond_eq_cache
.count(key
) == 0)
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
);
630 cond_eq_cache
[key
] = module
->Eq(NEW_ID
, sig_a
, sig_b
);
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
));
638 return cond_eq_cache
.at(key
);
641 void getFirstAcceptReject(SigBit
*accept_p
, SigBit
*reject_p
)
643 log_assert(!materialized
);
646 // Create unlinked NFSM
648 unodes
.resize(GetSize(nodes
));
650 for (int node
= 0; node
< GetSize(nodes
); node
++)
651 node_to_unode(node
, node
, SigSpec());
653 mark_reachable_unode(startNode
);
657 create_dnode(vector
<int>{startNode
}, true, false);
660 // Create DFSM Circuit
662 SigSpec accept_sig
, reject_sig
;
664 for (auto &it
: dnodes
)
666 SvaDFsmNode
&dnode
= it
.second
;
667 dnode
.ffoutwire
= module
->addWire(NEW_ID
);
668 dnode
.statesig
= dnode
.ffoutwire
;
670 if (it
.first
== vector
<int>{startNode
})
671 dnode
.statesig
= module
->Or(NEW_ID
, dnode
.statesig
, trigger_sig
);
674 for (auto &it
: dnodes
)
676 SvaDFsmNode
&dnode
= it
.second
;
677 dict
<vector
<int>, vector
<Const
>> edge_cond
;
679 for (auto &edge
: dnode
.edges
)
680 edge_cond
[edge
.first
].push_back(edge
.second
);
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
));
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
));
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
));
703 for (auto &it
: dnodes
)
705 SvaDFsmNode
&dnode
= it
.second
;
706 if (GetSize(dnode
.nextstate
) == 0) {
707 module
->connect(dnode
.ffoutwire
, State::S0
);
709 if (GetSize(dnode
.nextstate
) == 1) {
710 clocking
.addDff(NEW_ID
, dnode
.nextstate
, dnode
.ffoutwire
, State::S0
);
712 SigSpec nextstate
= module
->ReduceOr(NEW_ID
, dnode
.nextstate
);
713 clocking
.addDff(NEW_ID
, nextstate
, dnode
.ffoutwire
, State::S0
);
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
;
724 final_accept_sig
= module
->ReduceOr(NEW_ID
, accept_sig
);
725 *accept_p
= final_accept_sig
;
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
;
735 final_reject_sig
= module
->ReduceOr(NEW_ID
, reject_sig
);
736 *reject_p
= final_reject_sig
;
740 SigBit
getFirstAccept()
743 getFirstAcceptReject(&accept
, nullptr);
750 getFirstAcceptReject(nullptr, &reject
);
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)
756 log_assert(!materialized
);
759 // Create unlinked NFSM
761 unodes
.resize(GetSize(nodes
));
763 for (int node
= 0; node
< GetSize(nodes
); node
++)
764 node_to_unode(node
, node
, SigSpec());
766 mark_reachable_unode(startNode
);
770 create_dnode(vector
<int>{startNode
}, firstmatch
, condaccept
);
775 for (auto &it
: dnodes
)
777 SvaDFsmNode
&dnode
= it
.second
;
778 dnode
.outnode
= output_fsm
.createNode();
780 if (it
.first
== vector
<int>{startNode
})
781 output_fsm
.createLink(output_start_node
, dnode
.outnode
);
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
));
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
));
798 for (auto &it
: dnodes
)
800 SvaDFsmNode
&dnode
= it
.second
;
801 dict
<vector
<int>, vector
<Const
>> edge_cond
;
803 for (auto &edge
: dnode
.edges
)
804 edge_cond
[edge
.first
].push_back(edge
.second
);
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
));
814 // ----------------------------------------------------
815 // State dump for verbose log messages
822 log(" non-deterministic encoding:\n");
823 for (int i
= 0; i
< GetSize(nodes
); i
++)
825 log(" node %d:%s\n", i
,
826 i
== startNode
? " [start]" :
827 i
== acceptNode
? " [accept]" :
828 i
== condNode
? " [cond]" : "");
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
);
834 log(" edge -> %d\n", it
.first
);
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
);
841 log(" link -> %d\n", it
.first
);
851 log(" unlinked non-deterministic encoding:\n");
852 for (int i
= 0; i
< GetSize(unodes
); i
++)
854 if (!unodes
[i
].reachable
)
857 log(" unode %d:%s\n", i
, i
== startNode
? " [start]" : "");
859 for (auto &it
: unodes
[i
].edges
) {
860 if (!it
.second
.empty())
861 log(" edge %s -> %d\n", log_signal(it
.second
), it
.first
);
863 log(" edge -> %d\n", it
.first
);
866 for (auto &ctrl
: unodes
[i
].accept
) {
868 log(" accept %s\n", log_signal(ctrl
));
873 for (auto &ctrl
: unodes
[i
].cond
) {
875 log(" cond %s\n", log_signal(ctrl
));
887 log(" deterministic encoding:\n");
888 for (auto &it
: dnodes
)
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]" : "");
895 log(" ctrl %s\n", log_signal(it
.second
.ctrl
));
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
]);
904 for (auto &value
: it
.second
.accept
)
905 log(" accept %s\n", log_signal(value
));
907 for (auto &value
: it
.second
.reject
)
908 log(" reject %s\n", log_signal(value
));
915 log(" number of NFSM states: %d\n", GetSize(nodes
));
917 if (!unodes
.empty()) {
919 for (auto &unode
: unodes
)
922 log(" number of reachable UFSM states: %d\n", count
);
926 log(" number of DFSM states: %d\n", GetSize(dnodes
));
928 if (verific_verbose
>= 2) {
934 if (trigger_sig
!= State::S1
)
935 log(" trigger signal: %s\n", log_signal(trigger_sig
));
937 if (final_accept_sig
!= State::Sx
)
938 log(" accept signal: %s\n", log_signal(final_accept_sig
));
940 if (final_reject_sig
!= State::Sx
)
941 log(" reject signal: %s\n", log_signal(final_reject_sig
));
945 PRIVATE_NAMESPACE_END
947 YOSYS_NAMESPACE_BEGIN
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
972 struct VerificSvaImporter
974 VerificImporter
*importer
= nullptr;
975 Module
*module
= nullptr;
977 Netlist
*netlist
= nullptr;
978 Instance
*root
= nullptr;
980 VerificClocking clocking
;
982 bool mode_assert
= false;
983 bool mode_assume
= false;
984 bool mode_cover
= false;
985 bool mode_trigger
= false;
987 Instance
*net_to_ast_driver(Net
*n
)
992 if (n
->IsMultipleDriven())
995 Instance
*inst
= n
->Driver();
1000 if (!verific_sva_prims
.count(inst
->Type()))
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
)
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()); }
1017 // ----------------------------------------------------------
1020 struct ParserErrorException
{
1023 [[noreturn
]] void parser_error(std::string errmsg
)
1025 if (!importer
->mode_keep
)
1026 log_error("%s", errmsg
.c_str());
1027 log_warning("%s", errmsg
.c_str());
1028 throw ParserErrorException();
1031 [[noreturn
]] void parser_error(std::string errmsg
, linefile_type loc
)
1033 parser_error(stringf("%s at %s:%d.\n", errmsg
.c_str(), LineFile::GetFileName(loc
), LineFile::GetLineNo(loc
)));
1036 [[noreturn
]] void parser_error(std::string errmsg
, Instance
*inst
)
1038 parser_error(stringf("%s at %s (%s)", errmsg
.c_str(), inst
->View()->Owner()->Name(), inst
->Name()), inst
->Linefile());
1041 [[noreturn
]] void parser_error(Instance
*inst
)
1044 if (inst
->Type() == PRIM_SVA_MATCH_ITEM_TRIGGER
|| inst
->Type() == PRIM_SVA_MATCH_ITEM_ASSIGN
)
1046 msg
= "SVA sequences with local variable assignments are currently not supported.\n";
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());
1053 dict
<Net
*, bool, hash_ptr_ops
> check_expression_cache
;
1055 bool check_expression(Net
*net
, bool raise_error
= false)
1057 while (!check_expression_cache
.count(net
))
1059 Instance
*inst
= net_to_ast_driver(net
);
1061 if (inst
== nullptr) {
1062 check_expression_cache
[net
] = true;
1066 if (inst
->Type() == PRIM_SVA_AT
)
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
);
1076 if (inst
->Type() == PRIM_SVA_FIRST_MATCH
|| inst
->Type() == PRIM_SVA_NOT
)
1078 check_expression_cache
[net
] = check_expression(inst
->GetInput(), raise_error
);
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
)
1086 check_expression_cache
[net
] = check_expression(inst
->GetInput1(), raise_error
) && check_expression(inst
->GetInput2(), raise_error
);
1090 if (inst
->Type() == PRIM_SVA_SEQ_CONCAT
)
1092 const char *sva_low_s
= inst
->GetAttValue("sva:low");
1093 const char *sva_high_s
= inst
->GetAttValue("sva:high");
1095 int sva_low
= atoi(sva_low_s
);
1096 int sva_high
= atoi(sva_high_s
);
1097 bool sva_inf
= !strcmp(sva_high_s
, "$");
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
);
1102 check_expression_cache
[net
] = false;
1106 check_expression_cache
[net
] = false;
1109 if (raise_error
&& !check_expression_cache
.at(net
))
1110 parser_error(net_to_ast_driver(net
));
1111 return check_expression_cache
.at(net
);
1114 SigBit
parse_expression(Net
*net
)
1116 check_expression(net
, true);
1118 Instance
*inst
= net_to_ast_driver(net
);
1120 if (inst
== nullptr) {
1121 return importer
->net_map_at(net
);
1124 if (inst
->Type() == PRIM_SVA_AT
)
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
);
1133 if (inst
->Type() == PRIM_SVA_FIRST_MATCH
)
1134 return parse_expression(inst
->GetInput());
1136 if (inst
->Type() == PRIM_SVA_NOT
)
1137 return module
->Not(NEW_ID
, parse_expression(inst
->GetInput()));
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()));
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()));
1149 bool check_zero_consecutive_repeat(Net
*net
)
1151 Instance
*inst
= net_to_ast_driver(net
);
1153 if (inst
== nullptr)
1156 if (inst
->Type() != PRIM_SVA_CONSECUTIVE_REPEAT
)
1159 const char *sva_low_s
= inst
->GetAttValue("sva:low");
1160 int sva_low
= atoi(sva_low_s
);
1162 return sva_low
== 0;
1165 int parse_consecutive_repeat(SvaFsm
&fsm
, int start_node
, Net
*net
, bool add_pre_delay
, bool add_post_delay
)
1167 Instance
*inst
= net_to_ast_driver(net
);
1169 log_assert(inst
->Type() == PRIM_SVA_CONSECUTIVE_REPEAT
);
1171 const char *sva_low_s
= inst
->GetAttValue("sva:low");
1172 const char *sva_high_s
= inst
->GetAttValue("sva:high");
1174 int sva_low
= atoi(sva_low_s
);
1175 int sva_high
= atoi(sva_high_s
);
1176 bool sva_inf
= !strcmp(sva_high_s
, "$");
1178 Net
*body_net
= inst
->GetInput();
1180 if (add_pre_delay
|| add_post_delay
)
1181 log_assert(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
);
1189 int node
= fsm
.createNode(start_node
);
1192 if (add_pre_delay
) {
1193 node
= fsm
.createNode(start_node
);
1194 fsm
.createEdge(start_node
, node
);
1197 int prev_node
= node
;
1198 node
= parse_sequence(fsm
, node
, body_net
);
1200 for (int i
= 1; i
< sva_low
; i
++)
1202 int next_node
= fsm
.createNode();
1203 fsm
.createEdge(node
, next_node
);
1206 node
= parse_sequence(fsm
, next_node
, body_net
);
1211 log_assert(prev_node
>= 0);
1212 fsm
.createEdge(node
, prev_node
);
1216 for (int i
= sva_low
; i
< sva_high
; i
++)
1218 int next_node
= fsm
.createNode();
1219 fsm
.createEdge(node
, next_node
);
1222 node
= parse_sequence(fsm
, next_node
, body_net
);
1224 fsm
.createLink(prev_node
, node
);
1228 if (add_post_delay
) {
1229 int next_node
= fsm
.createNode();
1230 fsm
.createEdge(node
, next_node
);
1234 if (add_pre_delay
|| add_post_delay
)
1235 fsm
.createLink(start_node
, node
);
1240 int parse_sequence(SvaFsm
&fsm
, int start_node
, Net
*net
)
1242 if (check_expression(net
)) {
1243 int node
= fsm
.createNode();
1244 fsm
.createLink(start_node
, node
, parse_expression(net
));
1248 Instance
*inst
= net_to_ast_driver(net
);
1250 if (inst
->Type() == PRIM_SVA_AT
)
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
);
1259 if (inst
->Type() == PRIM_SVA_FIRST_MATCH
)
1261 SvaFsm
match_fsm(clocking
);
1262 match_fsm
.createLink(parse_sequence(match_fsm
, match_fsm
.createStartNode(), inst
->GetInput()), match_fsm
.acceptNode
);
1264 int node
= fsm
.createNode();
1265 match_fsm
.getDFsm(fsm
, start_node
, node
);
1267 if (verific_verbose
) {
1268 log(" First Match FSM:\n");
1275 if (inst
->Type() == PRIM_SVA_NEXTTIME
|| inst
->Type() == PRIM_SVA_S_NEXTTIME
)
1277 const char *sva_low_s
= inst
->GetAttValue("sva:low");
1278 const char *sva_high_s
= inst
->GetAttValue("sva:high");
1280 int sva_low
= atoi(sva_low_s
);
1281 int sva_high
= atoi(sva_high_s
);
1282 log_assert(sva_low
== sva_high
);
1284 int node
= start_node
;
1286 for (int i
= 0; i
< sva_low
; i
++) {
1287 int next_node
= fsm
.createNode();
1288 fsm
.createEdge(node
, next_node
);
1292 return parse_sequence(fsm
, node
, inst
->GetInput());
1295 if (inst
->Type() == PRIM_SVA_SEQ_CONCAT
)
1297 const char *sva_low_s
= inst
->GetAttValue("sva:low");
1298 const char *sva_high_s
= inst
->GetAttValue("sva:high");
1300 int sva_low
= atoi(sva_low_s
);
1301 int sva_high
= atoi(sva_high_s
);
1302 bool sva_inf
= !strcmp(sva_high_s
, "$");
1305 bool past_add_delay
= false;
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
--;
1311 node
= parse_sequence(fsm
, start_node
, inst
->GetInput1());
1314 if (check_zero_consecutive_repeat(inst
->GetInput2()) && sva_low
> 0) {
1315 past_add_delay
= true;
1316 sva_low
--, sva_high
--;
1319 for (int i
= 0; i
< sva_low
; i
++) {
1320 int next_node
= fsm
.createNode();
1321 fsm
.createEdge(node
, next_node
);
1327 fsm
.createEdge(node
, node
);
1331 for (int i
= sva_low
; i
< sva_high
; i
++)
1333 int next_node
= fsm
.createNode();
1334 fsm
.createEdge(node
, next_node
);
1335 fsm
.createLink(node
, next_node
);
1341 node
= parse_consecutive_repeat(fsm
, node
, inst
->GetInput2(), true, false);
1343 node
= parse_sequence(fsm
, node
, inst
->GetInput2());
1348 if (inst
->Type() == PRIM_SVA_CONSECUTIVE_REPEAT
)
1350 return parse_consecutive_repeat(fsm
, start_node
, net
, false, false);
1353 if (inst
->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT
|| inst
->Type() == PRIM_SVA_GOTO_REPEAT
)
1355 const char *sva_low_s
= inst
->GetAttValue("sva:low");
1356 const char *sva_high_s
= inst
->GetAttValue("sva:high");
1358 int sva_low
= atoi(sva_low_s
);
1359 int sva_high
= atoi(sva_high_s
);
1360 bool sva_inf
= !strcmp(sva_high_s
, "$");
1362 Net
*body_net
= inst
->GetInput();
1363 int node
= fsm
.createNode(start_node
);
1365 SigBit cond
= parse_expression(body_net
);
1366 SigBit not_cond
= module
->Not(NEW_ID
, cond
);
1368 for (int i
= 0; i
< sva_low
; i
++)
1370 int wait_node
= fsm
.createNode();
1371 fsm
.createEdge(wait_node
, wait_node
, not_cond
);
1374 fsm
.createLink(node
, wait_node
);
1376 fsm
.createEdge(node
, wait_node
);
1378 int next_node
= fsm
.createNode();
1379 fsm
.createLink(wait_node
, next_node
, cond
);
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
);
1393 for (int i
= sva_low
; i
< sva_high
; i
++)
1395 int wait_node
= fsm
.createNode();
1396 fsm
.createEdge(wait_node
, wait_node
, not_cond
);
1399 fsm
.createLink(node
, wait_node
);
1401 fsm
.createEdge(node
, wait_node
);
1403 int next_node
= fsm
.createNode();
1404 fsm
.createLink(wait_node
, next_node
, cond
);
1406 fsm
.createLink(node
, next_node
);
1411 if (inst
->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT
)
1412 fsm
.createEdge(node
, node
);
1417 if (inst
->Type() == PRIM_SVA_SEQ_OR
|| inst
->Type() == PRIM_SVA_OR
)
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
);
1425 if (inst
->Type() == PRIM_SVA_SEQ_AND
|| inst
->Type() == PRIM_SVA_AND
)
1427 SvaFsm
fsm1(clocking
);
1428 fsm1
.createLink(parse_sequence(fsm1
, fsm1
.createStartNode(), inst
->GetInput1()), fsm1
.acceptNode
);
1430 SvaFsm
fsm2(clocking
);
1431 fsm2
.createLink(parse_sequence(fsm2
, fsm2
.createStartNode(), inst
->GetInput2()), fsm2
.acceptNode
);
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
);
1437 int node
= fsm
.createNode();
1438 combined_fsm
.getDFsm(fsm
, start_node
, -1, node
);
1440 if (verific_verbose
)
1442 log(" Left And FSM:\n");
1445 log(" Right And FSM:\n");
1448 log(" Combined And FSM:\n");
1449 combined_fsm
.dump();
1455 if (inst
->Type() == PRIM_SVA_INTERSECT
|| inst
->Type() == PRIM_SVA_WITHIN
)
1457 SvaFsm
intersect_fsm(clocking
);
1459 if (inst
->Type() == PRIM_SVA_INTERSECT
)
1461 intersect_fsm
.createLink(parse_sequence(intersect_fsm
, intersect_fsm
.createStartNode(), inst
->GetInput1()), intersect_fsm
.acceptNode
);
1465 int n
= intersect_fsm
.createNode();
1466 intersect_fsm
.createLink(intersect_fsm
.createStartNode(), n
);
1467 intersect_fsm
.createEdge(n
, n
);
1469 n
= parse_sequence(intersect_fsm
, n
, inst
->GetInput1());
1471 intersect_fsm
.createLink(n
, intersect_fsm
.acceptNode
);
1472 intersect_fsm
.createEdge(n
, n
);
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;
1479 int node
= fsm
.createNode();
1480 intersect_fsm
.getDFsm(fsm
, start_node
, node
, -1, false, true);
1482 if (verific_verbose
) {
1483 log(" Intersect FSM:\n");
1484 intersect_fsm
.dump();
1490 if (inst
->Type() == PRIM_SVA_THROUGHOUT
)
1492 SigBit expr
= parse_expression(inst
->GetInput1());
1494 fsm
.pushThroughout(expr
);
1495 int node
= parse_sequence(fsm
, start_node
, inst
->GetInput2());
1496 fsm
.popThroughout();
1504 void get_fsm_accept_reject(SvaFsm
&fsm
, SigBit
*accept_p
, SigBit
*reject_p
, bool swap_accept_reject
= false)
1506 log_assert(accept_p
!= nullptr || reject_p
!= nullptr);
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();
1515 fsm
.getFirstAcceptReject(accept_p
, reject_p
);
1518 bool eventually_property(Net
*&net
, SigBit
&trig
)
1520 Instance
*inst
= net_to_ast_driver(net
);
1522 if (inst
== nullptr)
1525 if (clocking
.cond_net
!= nullptr)
1526 trig
= importer
->net_map_at(clocking
.cond_net
);
1530 if (inst
->Type() == PRIM_SVA_S_EVENTUALLY
|| inst
->Type() == PRIM_SVA_EVENTUALLY
)
1532 if (mode_cover
|| mode_trigger
)
1535 net
= inst
->GetInput();
1536 clocking
.cond_net
= nullptr;
1541 if (inst
->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION
||
1542 inst
->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION
)
1544 Net
*antecedent_net
= inst
->GetInput1();
1545 Net
*consequent_net
= inst
->GetInput2();
1547 Instance
*consequent_inst
= net_to_ast_driver(consequent_net
);
1549 if (consequent_inst
== nullptr)
1552 if (consequent_inst
->Type() != PRIM_SVA_S_EVENTUALLY
&& consequent_inst
->Type() != PRIM_SVA_EVENTUALLY
)
1555 if (mode_cover
|| mode_trigger
)
1556 parser_error(consequent_inst
);
1560 SvaFsm
antecedent_fsm(clocking
, trig
);
1561 node
= parse_sequence(antecedent_fsm
, antecedent_fsm
.createStartNode(), antecedent_net
);
1562 if (inst
->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION
) {
1563 int next_node
= antecedent_fsm
.createNode();
1564 antecedent_fsm
.createEdge(node
, next_node
);
1567 antecedent_fsm
.createLink(node
, antecedent_fsm
.acceptNode
);
1569 trig
= antecedent_fsm
.getAccept();
1570 net
= consequent_inst
->GetInput();
1571 clocking
.cond_net
= nullptr;
1573 if (verific_verbose
) {
1574 log(" Eventually Antecedent FSM:\n");
1575 antecedent_fsm
.dump();
1584 void parse_property(Net
*net
, SigBit
*accept_p
, SigBit
*reject_p
)
1586 Instance
*inst
= net_to_ast_driver(net
);
1588 SigBit trig
= State::S1
;
1590 if (clocking
.cond_net
!= nullptr)
1591 trig
= importer
->net_map_at(clocking
.cond_net
);
1593 if (inst
== nullptr)
1595 log_assert(trig
== State::S1
);
1597 if (accept_p
!= nullptr)
1598 *accept_p
= importer
->net_map_at(net
);
1599 if (reject_p
!= nullptr)
1600 *reject_p
= module
->Not(NEW_ID
, importer
->net_map_at(net
));
1603 if (inst
->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION
||
1604 inst
->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION
)
1606 Net
*antecedent_net
= inst
->GetInput1();
1607 Net
*consequent_net
= inst
->GetInput2();
1610 SvaFsm
antecedent_fsm(clocking
, trig
);
1611 node
= parse_sequence(antecedent_fsm
, antecedent_fsm
.createStartNode(), antecedent_net
);
1612 if (inst
->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION
) {
1613 int next_node
= antecedent_fsm
.createNode();
1614 antecedent_fsm
.createEdge(node
, next_node
);
1618 Instance
*consequent_inst
= net_to_ast_driver(consequent_net
);
1620 if (consequent_inst
&& (consequent_inst
->Type() == PRIM_SVA_UNTIL
|| consequent_inst
->Type() == PRIM_SVA_S_UNTIL
||
1621 consequent_inst
->Type() == PRIM_SVA_UNTIL_WITH
|| consequent_inst
->Type() == PRIM_SVA_S_UNTIL_WITH
||
1622 consequent_inst
->Type() == PRIM_SVA_ALWAYS
|| consequent_inst
->Type() == PRIM_SVA_S_ALWAYS
))
1624 bool until_with
= consequent_inst
->Type() == PRIM_SVA_UNTIL_WITH
|| consequent_inst
->Type() == PRIM_SVA_S_UNTIL_WITH
;
1626 Net
*until_net
= nullptr;
1627 if (consequent_inst
->Type() == PRIM_SVA_ALWAYS
|| consequent_inst
->Type() == PRIM_SVA_S_ALWAYS
)
1629 consequent_net
= consequent_inst
->GetInput();
1630 consequent_inst
= net_to_ast_driver(consequent_net
);
1634 until_net
= consequent_inst
->GetInput2();
1635 consequent_net
= consequent_inst
->GetInput1();
1636 consequent_inst
= net_to_ast_driver(consequent_net
);
1639 SigBit until_sig
= until_net
? parse_expression(until_net
) : RTLIL::S0
;
1640 SigBit not_until_sig
= module
->Not(NEW_ID
, until_sig
);
1641 antecedent_fsm
.createEdge(node
, node
, not_until_sig
);
1643 antecedent_fsm
.createLink(node
, antecedent_fsm
.acceptNode
, until_with
? State::S1
: not_until_sig
);
1647 antecedent_fsm
.createLink(node
, antecedent_fsm
.acceptNode
);
1650 SigBit antecedent_match
= antecedent_fsm
.getAccept();
1652 if (verific_verbose
) {
1653 log(" Antecedent FSM:\n");
1654 antecedent_fsm
.dump();
1657 bool consequent_not
= false;
1658 if (consequent_inst
&& consequent_inst
->Type() == PRIM_SVA_NOT
) {
1659 consequent_not
= true;
1660 consequent_net
= consequent_inst
->GetInput();
1661 consequent_inst
= net_to_ast_driver(consequent_net
);
1664 SvaFsm
consequent_fsm(clocking
, antecedent_match
);
1665 node
= parse_sequence(consequent_fsm
, consequent_fsm
.createStartNode(), consequent_net
);
1666 consequent_fsm
.createLink(node
, consequent_fsm
.acceptNode
);
1668 get_fsm_accept_reject(consequent_fsm
, accept_p
, reject_p
, consequent_not
);
1670 if (verific_verbose
) {
1671 log(" Consequent FSM:\n");
1672 consequent_fsm
.dump();
1677 bool prop_not
= inst
->Type() == PRIM_SVA_NOT
;
1679 net
= inst
->GetInput();
1680 inst
= net_to_ast_driver(net
);
1683 SvaFsm
fsm(clocking
, trig
);
1684 int node
= parse_sequence(fsm
, fsm
.createStartNode(), net
);
1685 fsm
.createLink(node
, fsm
.acceptNode
);
1687 get_fsm_accept_reject(fsm
, accept_p
, reject_p
, prop_not
);
1689 if (verific_verbose
) {
1690 log(" Sequence FSM:\n");
1700 module
= importer
->module
;
1701 netlist
= root
->Owner();
1703 if (verific_verbose
)
1704 log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root
->Name(), root
->View()->Owner()->Name(),
1705 LineFile::GetFileName(root
->Linefile()), LineFile::GetLineNo(root
->Linefile()));
1707 bool is_user_declared
= root
->IsUserDeclared();
1710 if (!is_user_declared
) {
1711 const char *name
= root
->Name();
1712 for (int i
= 0; name
[i
]; i
++) {
1713 if (i
? (name
[i
] < '0' || name
[i
] > '9') : (name
[i
] != 'i')) {
1714 is_user_declared
= true;
1720 RTLIL::IdString root_name
= module
->uniquify(importer
->mode_names
|| is_user_declared
? RTLIL::escape_id(root
->Name()) : NEW_ID
);
1722 // parse SVA sequence into trigger signal
1724 clocking
= VerificClocking(importer
, root
->GetInput(), true);
1725 SigBit accept_bit
= State::S0
, reject_bit
= State::S0
;
1727 if (clocking
.body_net
== nullptr)
1729 if (clocking
.clock_net
!= nullptr || clocking
.enable_net
!= nullptr || clocking
.disable_net
!= nullptr || clocking
.cond_net
!= nullptr)
1730 parser_error(stringf("Failed to parse SVA clocking"), root
);
1732 if (mode_assert
|| mode_assume
) {
1733 reject_bit
= module
->Not(NEW_ID
, parse_expression(root
->GetInput()));
1735 accept_bit
= parse_expression(root
->GetInput());
1740 Net
*net
= clocking
.body_net
;
1743 if (eventually_property(net
, trig
))
1745 SigBit sig_a
, sig_en
= trig
;
1746 parse_property(net
, &sig_a
, nullptr);
1748 // add final FF stage
1750 SigBit sig_a_q
, sig_en_q
;
1752 if (clocking
.body_net
== nullptr) {
1756 sig_a_q
= module
->addWire(NEW_ID
);
1757 sig_en_q
= module
->addWire(NEW_ID
);
1758 clocking
.addDff(NEW_ID
, sig_a
, sig_a_q
, State::S0
);
1759 clocking
.addDff(NEW_ID
, sig_en
, sig_en_q
, State::S0
);
1762 // generate fair/live cell
1764 RTLIL::Cell
*c
= nullptr;
1766 if (mode_assert
) c
= module
->addLive(root_name
, sig_a_q
, sig_en_q
);
1767 if (mode_assume
) c
= module
->addFair(root_name
, sig_a_q
, sig_en_q
);
1769 importer
->import_attributes(c
->attributes
, root
);
1775 if (mode_assert
|| mode_assume
) {
1776 parse_property(net
, nullptr, &reject_bit
);
1778 parse_property(net
, &accept_bit
, nullptr);
1785 module
->connect(importer
->net_map_at(root
->GetOutput()), accept_bit
);
1789 SigBit sig_a
= module
->Not(NEW_ID
, reject_bit
);
1790 SigBit sig_en
= module
->Or(NEW_ID
, accept_bit
, reject_bit
);
1792 // add final FF stage
1794 SigBit sig_a_q
, sig_en_q
;
1796 if (clocking
.body_net
== nullptr) {
1800 sig_a_q
= module
->addWire(NEW_ID
);
1801 sig_en_q
= module
->addWire(NEW_ID
);
1802 clocking
.addDff(NEW_ID
, sig_a
, sig_a_q
, State::S0
);
1803 clocking
.addDff(NEW_ID
, sig_en
, sig_en_q
, State::S0
);
1806 // generate assert/assume/cover cell
1808 RTLIL::Cell
*c
= nullptr;
1810 if (mode_assert
) c
= module
->addAssert(root_name
, sig_a_q
, sig_en_q
);
1811 if (mode_assume
) c
= module
->addAssume(root_name
, sig_a_q
, sig_en_q
);
1812 if (mode_cover
) c
= module
->addCover(root_name
, sig_a_q
, sig_en_q
);
1814 importer
->import_attributes(c
->attributes
, root
);
1817 catch (ParserErrorException
)
1823 void verific_import_sva_assert(VerificImporter
*importer
, Instance
*inst
)
1825 VerificSvaImporter worker
;
1826 worker
.importer
= importer
;
1828 worker
.mode_assert
= true;
1832 void verific_import_sva_assume(VerificImporter
*importer
, Instance
*inst
)
1834 VerificSvaImporter worker
;
1835 worker
.importer
= importer
;
1837 worker
.mode_assume
= true;
1841 void verific_import_sva_cover(VerificImporter
*importer
, Instance
*inst
)
1843 VerificSvaImporter worker
;
1844 worker
.importer
= importer
;
1846 worker
.mode_cover
= true;
1850 void verific_import_sva_trigger(VerificImporter
*importer
, Instance
*inst
)
1852 VerificSvaImporter worker
;
1853 worker
.importer
= importer
;
1855 worker
.mode_trigger
= true;
1859 bool verific_is_sva_net(VerificImporter
*importer
, Verific::Net
*net
)
1861 VerificSvaImporter worker
;
1862 worker
.importer
= importer
;
1863 return worker
.net_to_ast_driver(net
) != nullptr;