group__uart.html


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "https://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en-US">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=11"/>
<meta name="generator" content="Doxygen 1.9.5"/>
<meta name="viewport" content="width=device-width, initial-scale=1"/>
<title>Sensor Watch: UART</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="search/search.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="search/searchdata.js"></script>
<script type="text/javascript" src="search/search.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
 <tbody>
 <tr id="projectrow">
  <td id="projectalign">
   <div id="projectname">Sensor Watch<span id="projectnumber">&#160;0.0.2</span>
   </div>
   <div id="projectbrief">A board replacement for the classic Casio F-91W wristwatch, powered by a Microchip SAM L22 microcontroller.</div>
  </td>
 </tr>
 </tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.9.5 -->
<script type="text/javascript">
/* @license magnet:?xt=urn:btih:d3d9a9a6595521f9666a5e94cc830dab83b65699&amp;dn=expat.txt MIT */
var searchBox = new SearchBox("searchBox", "search/",'.html');
/* @license-end */
</script>
<script type="text/javascript" src="menudata.js"></script>
<script type="text/javascript" src="menu.js"></script>
<script type="text/javascript">
/* @license magnet:?xt=urn:btih:d3d9a9a6595521f9666a5e94cc830dab83b65699&amp;dn=expat.txt MIT */
$(function() {
  initMenu('',true,false,'search.php','Search');
  $(document).ready(function() { init_search(); });
});
/* @license-end */
</script>
<div id="main-nav"></div>
</div><!-- top -->
<!-- window showing the filter options -->
<div id="MSearchSelectWindow"
     onmouseover="return searchBox.OnSearchSelectShow()"
     onmouseout="return searchBox.OnSearchSelectHide()"
     onkeydown="return searchBox.OnSearchSelectKey(event)">
</div>

<!-- iframe showing the search results (closed by default) -->
<div id="MSearchResultsWindow">
<div id="MSearchResults">
<div class="SRPage">
<div id="SRIndex">
<div id="SRResults"></div>
<div class="SRStatus" id="Loading">Loading...</div>
<div class="SRStatus" id="Searching">Searching...</div>
<div class="SRStatus" id="NoMatches">No Matches</div>
</div>
</div>
</div>
</div>

<div class="header">
  <div class="summary">
<a href="#func-members">Functions</a>  </div>
  <div class="headertitle"><div class="title">UART</div></div>
</div><!--header-->
<div class="contents">

<p>This section covers functions related to the UART peripheral.  
<a href="#details">More...</a></p>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a id="func-members" name="func-members"></a>
Functions</h2></td></tr>
<tr class="memitem:ga38e750d3e02939bf056fde77f4ef6235"><td class="memItemLeft" align="right" valign="top">void&#160;</td><td class="memItemRight" valign="bottom"><a class="el" href="group__uart.html#ga38e750d3e02939bf056fde77f4ef6235">watch_enable_uart</a> (const uint8_t tx_pin, const uint8_t rx_pin, uint32_t baud)</td></tr>
<tr class="memdesc:ga38e750d3e02939bf056fde77f4ef6235"><td class="mdescLeft">&#160;</td><td class="mdescRight">Initializes the debug UART.  <a href="group__uart.html#ga38e750d3e02939bf056fde77f4ef6235">More...</a><br /></td></tr>
<tr class="separator:ga38e750d3e02939bf056fde77f4ef6235"><td class="memSeparator" colspan="2">&#160;</td></tr>
<tr class="memitem:ga5d62683298c511f24adaab4bf6615c50"><td class="memItemLeft" align="right" valign="top">void&#160;</td><td class="memItemRight" valign="bottom"><a class="el" href="group__uart.html#ga5d62683298c511f24adaab4bf6615c50">watch_uart_puts</a> (char *s)</td></tr>
<tr class="memdesc:ga5d62683298c511f24adaab4bf6615c50"><td class="mdescLeft">&#160;</td><td class="mdescRight">Transmits a string of bytes on the UART's TX pin.  <a href="group__uart.html#ga5d62683298c511f24adaab4bf6615c50">More...</a><br /></td></tr>
<tr class="separator:ga5d62683298c511f24adaab4bf6615c50"><td class="memSeparator" colspan="2">&#160;</td></tr>
<tr class="memitem:ga0c400bfcd52bb71e8de62c5ab2373db6"><td class="memItemLeft" align="right" valign="top">char&#160;</td><td class="memItemRight" valign="bottom"><a class="el" href="group__uart.html#ga0c400bfcd52bb71e8de62c5ab2373db6">watch_uart_getc</a> (void)</td></tr>
<tr class="memdesc:ga0c400bfcd52bb71e8de62c5ab2373db6"><td class="mdescLeft">&#160;</td><td class="mdescRight">Receives a single byte from the UART's RX pin.  <a href="group__uart.html#ga0c400bfcd52bb71e8de62c5ab2373db6">More...</a><br /></td></tr>
<tr class="separator:ga0c400bfcd52bb71e8de62c5ab2373db6"><td class="memSeparator" colspan="2">&#160;</td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<p >This section covers functions related to the UART peripheral. </p>
<h2 class="groupheader">Function Documentation</h2>
<a id="ga38e750d3e02939bf056fde77f4ef6235" name="ga38e750d3e02939bf056fde77f4ef6235"></a>
<h2 class="memtitle"><span class="permalink"><a href="#ga38e750d3e02939bf056fde77f4ef6235">&#9670;&#160;</a></span>watch_enable_uart()</h2>

<div class="memitem">
<div class="memproto">
      <table class="memname">
        <tr>
          <td class="memname">void watch_enable_uart </td>
          <td>(</td>
          <td class="paramtype">const uint8_t&#160;</td>
          <td class="paramname"><em>tx_pin</em>, </td>
        </tr>
        <tr>
          <td class="paramkey"></td>
          <td></td>
          <td class="paramtype">const uint8_t&#160;</td>
          <td class="paramname"><em>rx_pin</em>, </td>
        </tr>
        <tr>
          <td class="paramkey"></td>
          <td></td>
          <td class="paramtype">uint32_t&#160;</td>
          <td class="paramname"><em>baud</em>&#160;</td>
        </tr>
        <tr>
          <td></td>
          <td>)</td>
          <td></td><td></td>
        </tr>
      </table>
</div><div class="memdoc">

<p>Initializes the debug UART. </p>
<dl class="params"><dt>Parameters</dt><dd>
  <table class="params">
    <tr><td class="paramname">tx_pin</td><td>The pin the watch will use to transmit, or 0 for a receive-only UART. If specified, must be either A2 or A4. </td></tr>
    <tr><td class="paramname">rx_pin</td><td>The pin the watch will use to receive, or 0 for a transmit-only UART. If specified, must be A1, A2, A3 or A4 (pin A0 cannot receive UART data). </td></tr>
    <tr><td class="paramname">baud</td><td>The baud rate for the UART. A typical value is 19200. </td></tr>
  </table>
  </dd>
</dl>

</div>
</div>
<a id="ga0c400bfcd52bb71e8de62c5ab2373db6" name="ga0c400bfcd52bb71e8de62c5ab2373db6"></a>
<h2 class="memtitle"><span class="permalink"><a href="#ga0c400bfcd52bb71e8de62c5ab2373db6">&#9670;&#160;</a></span>watch_uart_getc()</h2>

<div class="memitem">
<div class="memproto">
      <table class="memname">
        <tr>
          <td class="memname">char watch_uart_getc </td>
          <td>(</td>
          <td class="paramtype">void&#160;</td>
          <td class="paramname"></td><td>)</td>
          <td></td>
        </tr>
      </table>
</div><div class="memdoc">

<p>Receives a single byte from the UART's RX pin. </p>
<dl class="section return"><dt>Returns</dt><dd>the received byte. </dd></dl>
<dl class="section note"><dt>Note</dt><dd>This method will block until a byte is received! </dd></dl>

</div>
</div>
<a id="ga5d62683298c511f24adaab4bf6615c50" name="ga5d62683298c511f24adaab4bf6615c50"></a>
<h2 class="memtitle"><span class="permalink"><a href="#ga5d62683298c511f24adaab4bf6615c50">&#9670;&#160;</a></span>watch_uart_puts()</h2>

<div class="memitem">
<div class="memproto">
      <table class="memname">
        <tr>
          <td class="memname">void watch_uart_puts </td>
          <td>(</td>
          <td class="paramtype">char *&#160;</td>
          <td class="paramname"><em>s</em></td><td>)</td>
          <td></td>
        </tr>
      </table>
</div><div class="memdoc">

<p>Transmits a string of bytes on the UART's TX pin. </p>
<dl class="params"><dt>Parameters</dt><dd>
  <table class="params">
    <tr><td class="paramname">s</td><td>A null-terminated string containing the bytes you wish to transmit. </td></tr>
  </table>
  </dd>
</dl>

</div>
</div>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated by&#160;<a href="https://www.doxygen.org/index.html"><img class="footer" src="doxygen.svg" width="104" height="31" alt="doxygen"/></a> 1.9.5
</small></address>
</body>
</html>
/*
 *  yosys -- Yosys Open SYnthesis Suite
 *
 *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
 *
 *  Permission to use, copy, modify, and/or distribute this software for any
 *  purpose with or without fee is hereby granted, provided that the above
 *  copyright notice and this permission notice appear in all copies.
 *
 *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
 *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
 *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *
 */


// Currently supported SVA sequence and property syntax:
// http://symbiyosys.readthedocs.io/en/latest/verific.html
//
// Next gen property syntax:
//   basic_property
//   [antecedent_condition] property
//   [antecedent_condition] always.. property
//   [antecedent_condition] eventually.. basic_property
//   [antecedent_condition] property until.. expression
//   [antecedent_condition] basic_property until.. basic_property      (assert/assume only)
//
// antecedent_condition:
//   sequence |->
//   sequence |=>
//
// basic_property:
//   sequence
//   not basic_property
//   nexttime basic_property
//   nexttime[N] basic_property
//   sequence #-# basic_property
//   sequence #=# basic_property
//   basic_property or basic_property           (cover only)
//   basic_property and basic_property          (assert/assume only)
//   basic_property implies basic_property
//   basic_property iff basic_property
//
// sequence:
//   expression
//   sequence ##N sequence
//   sequence ##[*] sequence
//   sequence ##[+] sequence
//   sequence ##[N:M] sequence
//   sequence ##[N:$] sequence
//   expression [*]
//   expression [+]
//   expression [*N]
//   expression [*N:M]
//   expression [*N:$]
//   sequence or sequence
//   sequence and sequence
//   expression throughout sequence
//   sequence intersect sequence
//   sequence within sequence
//   first_match( sequence )
//   expression [=N]
//   expression [=N:M]
//   expression [=N:$]
//   expression [->N]
//   expression [->N:M]
//   expression [->N:$]


#include "kernel/yosys.h"
#include "frontends/verific/verific.h"

USING_YOSYS_NAMESPACE

#ifdef VERIFIC_NAMESPACE
using namespace Verific;
#endif

PRIVATE_NAMESPACE_BEGIN

// Non-deterministic FSM
struct SvaNFsmNode
{
	// Edge: Activate the target node if ctrl signal is true, consumes clock cycle
	// Link: Activate the target node if ctrl signal is true, doesn't consume clock cycle
	vector<pair<int, SigBit>> edges, links;
	bool is_cond_node;
};

// Non-deterministic FSM after resolving links
struct SvaUFsmNode
{
	// Edge: Activate the target node if all bits in ctrl signal are true, consumes clock cycle
	// Accept: This node functions as an accept node if all bits in ctrl signal are true
	vector<pair<int, SigSpec>> edges;
	vector<SigSpec> accept, cond;
	bool reachable;
};

// Deterministic FSM
struct SvaDFsmNode
{
	// A DFSM state corresponds to a set of NFSM states. We represent DFSM states as sorted vectors
	// of NFSM state node ids. Edge/accept controls are constants matched against the ctrl sigspec.
	SigSpec ctrl;
	vector<pair<vector<int>, Const>> edges;
	vector<Const> accept, reject;

	// additional temp data for getReject()
	Wire *ffoutwire;
	SigBit statesig;
	SigSpec nextstate;

	// additional temp data for getDFsm()
	int outnode;
};

struct SvaFsm
{
	Module *module;
	VerificClocking clocking;

	SigBit trigger_sig = State::S1, disable_sig;
	SigBit throughout_sig = State::S1;
	bool in_cond_mode = false;

	vector<SigBit> disable_stack;
	vector<SigBit> throughout_stack;

	int startNode, acceptNode, condNode;
	vector<SvaNFsmNode> nodes;

	vector<SvaUFsmNode> unodes;
	dict<vector<int>, SvaDFsmNode> dnodes;
	dict<pair<SigSpec, SigSpec>, SigBit> cond_eq_cache;
	bool materialized = false;

	SigBit final_accept_sig = State::Sx;
	SigBit final_reject_sig = State::Sx;

	SvaFsm(const VerificClocking &clking, SigBit trig = State::S1)
	{
		module = clking.module;
		clocking = clking;
		trigger_sig = trig;

		startNode = createNode();
		acceptNode = createNode();

		in_cond_mode = true;
		condNode = createNode();
		in_cond_mode = false;
	}

	void pushDisable(SigBit sig)
	{
		log_assert(!materialized);

		disable_stack.push_back(disable_sig);

		if (disable_sig == State::S0)
			disable_sig = sig;
		else
			disable_sig = module->Or(NEW_ID, disable_sig, sig);
	}

	void popDisable()
	{
		log_assert(!materialized);
		log_assert(!disable_stack.empty());

		disable_sig = disable_stack.back();
		disable_stack.pop_back();
	}

	void pushThroughout(SigBit sig)
	{
		log_assert(!materialized);

		throughout_stack.push_back(throughout_sig);

		if (throughout_sig == State::S1)
			throughout_sig = sig;
		else
			throughout_sig = module->And(NEW_ID, throughout_sig, sig);
	}

	void popThroughout()
	{
		log_assert(!materialized);
		log_assert(!throughout_stack.empty());

		throughout_sig = throughout_stack.back();
		throughout_stack.pop_back();
	}

	int createNode(int link_node = -1)
	{
		log_assert(!materialized);

		int idx = GetSize(nodes);
		nodes.push_back(SvaNFsmNode());
		nodes.back().is_cond_node = in_cond_mode;
		if (link_node >= 0)
			createLink(link_node, idx);
		return idx;
	}

	int createStartNode()
	{
		return createNode(startNode);
	}

	void createEdge(int from_node, int to_node, SigBit ctrl = State::S1)
	{
		log_assert(!materialized);
		log_assert(0 <= from_node && from_node < GetSize(nodes));
		log_assert(0 <= to_node && to_node < GetSize(nodes));
		log_assert(from_node != acceptNode);
		log_assert(to_node != acceptNode);
		log_assert(from_node != condNode);
		log_assert(to_node != condNode);
		log_assert(to_node != startNode);

		if (from_node != startNode)
			log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node);

		if (throughout_sig != State::S1) {
			if (ctrl != State::S1)
				ctrl = module->And(NEW_ID, throughout_sig, ctrl);
			else
				ctrl = throughout_sig;
		}

		nodes[from_node].edges.push_back(make_pair(to_node, ctrl));
	}

	void createLink(int from_node, int to_node, SigBit ctrl = State::S1)
	{
		log_assert(!materialized);
		log_assert(0 <= from_node && from_node < GetSize(nodes));
		log_assert(0 <= to_node && to_node < GetSize(nodes));
		log_assert(from_node != acceptNode);
		log_assert(from_node != condNode);
		log_assert(to_node != startNode);

		if (from_node != startNode)
			log_assert(nodes.at(from_node).is_cond_node == nodes.at(to_node).is_cond_node);

		if (throughout_sig != State::S1) {
			if (ctrl != State::S1)
				ctrl = module->And(NEW_ID, throughout_sig, ctrl);
			else
				ctrl = throughout_sig;
		}

		nodes[from_node].links.push_back(make_pair(to_node, ctrl));
	}

	void make_link_order(vector<int> &order, int node, int min)
	{
		order[node] = std::max(order[node], min);
		for (auto &it : nodes[node].links)
			make_link_order(order, it.first, order[node]+1);
	}

	// ----------------------------------------------------
	// Generating NFSM circuit to acquire accept signal

	SigBit getAccept()
	{
		log_assert(!materialized);
		materialized = true;

		vector<Wire*> state_wire(GetSize(nodes));
		vector<SigBit> state_sig(GetSize(nodes));
		vector<SigBit> next_state_sig(GetSize(nodes));

		// Create state signals

		{
			SigBit not_disable = State::S1;

			if (disable_sig != State::S0)
				not_disable = module->Not(NEW_ID, disable_sig);

			for (int i = 0; i < GetSize(nodes); i++)
			{
				Wire *w = module->addWire(NEW_ID);
				state_wire[i] = w;
				state_sig[i] = w;

				if (i == startNode)
					state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig);

				if (disable_sig != State::S0)
					state_sig[i] = module->And(NEW_ID, state_sig[i], not_disable);
			}
		}

		// Follow Links

		{
			vector<int> node_order(GetSize(nodes));
			vector<vector<int>> order_to_nodes;

			for (int i = 0; i < GetSize(nodes); i++)
				make_link_order(node_order, i, 0);

			for (int i = 0; i < GetSize(nodes); i++) {
				if (node_order[i] >= GetSize(order_to_nodes))
					order_to_nodes.resize(node_order[i]+1);
				order_to_nodes[node_order[i]].push_back(i);
			}

			for (int order = 0; order < GetSize(order_to_nodes); order++)
			for (int node : order_to_nodes[order])
			{
				for (auto &it : nodes[node].links)
				{
					int target = it.first;
					SigBit ctrl = state_sig[node];

					if (it.second != State::S1)
						ctrl = module->And(NEW_ID, ctrl, it.second);

					state_sig[target] = module->Or(NEW_ID, state_sig[target], ctrl);
				}
			}
		}

		// Construct activations

		{
			vector<SigSpec> activate_sig(GetSize(nodes));
			vector<SigBit> activate_bit(GetSize(nodes));

			for (int i = 0; i < GetSize(nodes); i++) {
				for (auto &it : nodes[i].edges)
					activate_sig[it.first].append(module->And(NEW_ID, state_sig[i], it.second));
			}

			for (int i = 0; i < GetSize(nodes); i++) {
				if (GetSize(activate_sig[i]) == 0)
					next_state_sig[i] = State::S0;
				else if (GetSize(activate_sig[i]) == 1)
					next_state_sig[i] = activate_sig[i];
				else
					next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]);
			}
		}

		// Create state FFs

		for (int i = 0; i < GetSize(nodes); i++)
		{
			if (next_state_sig[i] != State::S0) {
				clocking.addDff(NEW_ID, next_state_sig[i], state_wire[i], State::S0);
			} else {
				module->connect(state_wire[i], State::S0);
			}
		}

		final_accept_sig = state_sig[acceptNode];
		return final_accept_sig;
	}

	// ----------------------------------------------------
	// Generating quantifier-based NFSM circuit to acquire reject signal

	SigBit getAnyAllRejectWorker(bool /* allMode */)
	{
		// FIXME
		log_abort();
	}

	SigBit getAnyReject()
	{
		return getAnyAllRejectWorker(false);
	}

	SigBit getAllReject()
	{
		return getAnyAllRejectWorker(true);
	}

	// ----------------------------------------------------
	// Generating DFSM circuit to acquire reject signal

	void node_to_unode(int node, int unode, SigSpec ctrl)
	{
		if (node == acceptNode)
			unodes[unode].accept.push_back(ctrl);

		if (node == condNode)
			unodes[unode].cond.push_back(ctrl);

		for (auto &it : nodes[node].edges) {
			if (it.second != State::S1) {
				SigSpec s = {ctrl, it.second};
				s.sort_and_unify();
				unodes[unode].edges.push_back(make_pair(it.first, s));
			} else {
				unodes[unode].edges.push_back(make_pair(it.first, ctrl));
			}
		}

		for (auto &it : nodes[node].links) {
			if (it.second != State::S1) {
				SigSpec s = {ctrl, it.second};
				s.sort_and_unify();
				node_to_unode(it.first, unode, s);
			} else {
				node_to_unode(it.first, unode, ctrl);
			}
		}
	}

	void mark_reachable_unode(int unode)
	{
		if (unodes[unode].reachable)
			return;

		unodes[unode].reachable = true;
		for (auto &it : unodes[unode].edges)
			mark_reachable_unode(it.first);
	}

	void usortint(vector<int> &vec)
	{
		vector<int> newvec;
		std::sort(vec.begin(), vec.end());
		for (int i = 0; i < GetSize(vec); i++)
			if (i == GetSize(vec)-1 || vec[i] != vec[i+1])
				newvec.push_back(vec[i]);
		vec.swap(newvec);
	}

	bool cmp_ctrl(const pool<SigBit> &ctrl_bits, const SigSpec &ctrl)
	{
		for (int i = 0; i < GetSize(ctrl); i++)
			if (ctrl_bits.count(ctrl[i]) == 0)
				return false;
		return true;
	}

	void create_dnode(const vector<int> &state, bool firstmatch, bool condaccept)
	{
		if (dnodes.count(state) != 0)
			return;

		SvaDFsmNode dnode;
		dnodes[state] = SvaDFsmNode();

		for (int unode : state) {
			log_assert(unodes[unode].reachable);
			for (auto &it : unodes[unode].edges)
				dnode.ctrl.append(it.second);
			for (auto &it : unodes[unode].accept)
				dnode.ctrl.append(it);
			for (auto &it : unodes[unode].cond)
				dnode.ctrl.append(it);
		}

		dnode.ctrl.sort_and_unify();

		if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) {
			if (verific_verbose >= 2) {
				log("    detected state explosion in DFSM generation:\n");
				dump();
				log("      ctrl signal: %s\n", log_signal(dnode.ctrl));
			}
			log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n",
					GetSize(dnode.ctrl), verific_sva_fsm_limit);
		}

		for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)
		{
			Const ctrl_val(i, GetSize(dnode.ctrl));
			pool<SigBit> ctrl_bits;

			for (int i = 0; i < GetSize(dnode.ctrl); i++)
				if (ctrl_val[i] == State::S1)
					ctrl_bits.insert(dnode.ctrl[i]);

			vector<int> new_state;
			bool accept = false, cond = false;

			for (int unode : state) {
				for (auto &it : unodes[unode].accept)
					if (cmp_ctrl(ctrl_bits, it))
						accept = true;
				for (auto &it : unodes[unode].cond)
					if (cmp_ctrl(ctrl_bits, it))
						cond = true;
			}

			bool new_state_cond = false;
			bool new_state_noncond = false;

			if (accept && condaccept)
				accept = cond;

			if (!accept || !firstmatch) {
				for (int unode : state)
				for (auto &it : unodes[unode].edges)
					if (cmp_ctrl(ctrl_bits, it.second)) {
						if (nodes.at(it.first).is_cond_node)
							new_state_cond = true;
						else
							new_state_noncond = true;
						new_state.push_back(it.first);
					}
			}

			if (accept)
				dnode.accept.push_back(ctrl_val);

			if (condaccept && (!new_state_cond || !new_state_noncond))
				new_state.clear();

			if (new_state.empty()) {
				if (!accept)
					dnode.reject.push_back(ctrl_val);
			} else {
				usortint(new_state);
				dnode.edges.push_back(make_pair(new_state, ctrl_val));
				create_dnode(new_state, firstmatch, condaccept);
			}
		}

		dnodes[state] = dnode;
	}

	void optimize_cond(vector<Const> &values)
	{
		bool did_something = true;

		while (did_something)
		{
			did_something = false;

			for (int i = 0; i < GetSize(values); i++)
			for (int j = 0; j < GetSize(values); j++)
			{
				if (i == j)
					continue;

				log_assert(GetSize(values[i]) == GetSize(values[j]));

				int delta_pos = -1;
				bool i_within_j = true;
				bool j_within_i = true;

				for (int k = 0; k < GetSize(values[i]); k++) {
					if (values[i][k] == State::Sa && values[j][k] != State::Sa) {
						i_within_j = false;
						continue;
					}
					if (values[i][k] != State::Sa && values[j][k] == State::Sa) {
						j_within_i = false;
						continue;
					}
					if (values[i][k] == values[j][k])
						continue;
					if (delta_pos >= 0)
						goto next_pair;
					delta_pos = k;
				}

				if (delta_pos >= 0 && i_within_j && j_within_i) {
					did_something = true;
					values[i][delta_pos] = State::Sa;
					values[j] = values.back();
					values.pop_back();
					goto next_pair;
				}

				if (delta_pos < 0 && i_within_j) {
					did_something = true;
					values[i] = values.back();
					values.pop_back();
					goto next_pair;
				}

				if (delta_pos < 0 && j_within_i) {
					did_something = true;
					values[j] = values.back();
					values.pop_back();
					goto next_pair;
				}
		next_pair:;
			}
		}
	}

	SigBit make_cond_eq(const SigSpec &ctrl, const Const &value, SigBit enable = State::S1)
	{
		SigSpec sig_a, sig_b;

		log_assert(GetSize(ctrl) == GetSize(value));

		for (int i = 0; i < GetSize(ctrl); i++)
			if (value[i] != State::Sa) {
				sig_a.append(ctrl[i]);
				sig_b.append(value[i]);
			}

		if (GetSize(sig_a) == 0)
			return enable;

		if (enable != State::S1) {
			sig_a.append(enable);
			sig_b.append(State::S1);
		}

		auto key = make_pair(sig_a, sig_b);

		if (cond_eq_cache.count(key) == 0)
		{
			if (sig_b == State::S1)
				cond_eq_cache[key] = sig_a;
			else if (sig_b == State::S0)
				cond_eq_cache[key] = module->Not(NEW_ID, sig_a);
			else
				cond_eq_cache[key] = module->Eq(NEW_ID, sig_a, sig_b);

			if (verific_verbose >= 2) {
				log("    Cond: %s := %s == %s\n", log_signal(cond_eq_cache[key]),
						log_signal(sig_a), log_signal(sig_b));
			}
		}

		return cond_eq_cache.at(key);
	}

	void getFirstAcceptReject(SigBit *accept_p, SigBit *reject_p)
	{
		log_assert(!materialized);
		materialized = true;

		// Create unlinked NFSM

		unodes.resize(GetSize(nodes));

		for (int node = 0; node < GetSize(nodes); node++)
			node_to_unode(node, node, SigSpec());

		mark_reachable_unode(startNode);

		// Create DFSM

		create_dnode(vector<int>{startNode}, true, false);
		dnodes.sort();

		// Create DFSM Circuit

		SigSpec accept_sig, reject_sig;

		for (auto &it : dnodes)
		{
			SvaDFsmNode &dnode = it.second;
			dnode.ffoutwire = module->addWire(NEW_ID);
			dnode.statesig = dnode.ffoutwire;

			if (it.first == vector<int>{startNode})
				dnode.statesig = module->Or(NEW_ID, dnode.statesig, trigger_sig);
		}

		for (auto &it : dnodes)
		{
			SvaDFsmNode &dnode = it.second;
			dict<vector<int>, vector<Const>> edge_cond;

			for (auto &edge : dnode.edges)
				edge_cond[edge.first].push_back(edge.second);

			for (auto &it : edge_cond) {
				optimize_cond(it.second);
				for (auto &value : it.second)
					dnodes.at(it.first).nextstate.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
			}

			if (accept_p) {
				vector<Const> accept_cond = dnode.accept;
				optimize_cond(accept_cond);
				for (auto &value : accept_cond)
					accept_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
			}

			if (reject_p) {
				vector<Const> reject_cond = dnode.reject;
				optimize_cond(reject_cond);
				for (auto &value : reject_cond)
					reject_sig.append(make_cond_eq(dnode.ctrl, value, dnode.statesig));
			}
		}

		for (auto &it : dnodes)
		{
			SvaDFsmNode &dnode = it.second;
			if (GetSize(dnode.nextstate) == 0) {
				module->connect(dnode.ffoutwire, State::S0);
			} else
			if (GetSize(dnode.nextstate) == 1) {
				clocking.addDff(NEW_ID, dnode.nextstate, dnode.ffoutwire, State::S0);
			} else {
				SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate);
				clocking.addDff(NEW_ID, nextstate, dnode.ffoutwire, State::S0);
			}
		}

		if (accept_p)
		{
			if (GetSize(accept_sig) == 0)
				final_accept_sig = State::S0;
			else if (GetSize(accept_sig) == 1)
				final_accept_sig = accept_sig;
			else
				final_accept_sig = module->ReduceOr(NEW_ID, accept_sig);
			*accept_p = final_accept_sig;
		}

		if (reject_p)
		{
			if (GetSize(reject_sig) == 0)
				final_reject_sig = State::S0;
			else if (GetSize(reject_sig) == 1)
				final_reject_sig = reject_sig;
			else
				final_reject_sig = module->ReduceOr(NEW_ID, reject_sig);
			*reject_p = final_reject_sig;
		}
	}

	SigBit getFirstAccept()
	{
		SigBit accept;
		getFirstAcceptReject(&accept, nullptr);
		return accept;
	}

	SigBit getReject()
	{
		SigBit reject;
		getFirstAcceptReject(nullptr, &reject);
		return reject;
	}

	void getDFsm(SvaFsm &output_fsm, int output_start_node, int output_accept_node, int output_reject_node = -1, bool firstmatch = true, bool condaccept = false)
	{
		log_assert(!materialized);
		materialized = true;

		// Create unlinked NFSM

		unodes.resize(GetSize(nodes));

		for (int node = 0; node < GetSize(nodes); node++)
			node_to_unode(node, node, SigSpec());

		mark_reachable_unode(startNode);

		// Create DFSM

		create_dnode(vector<int>{startNode}, firstmatch, condaccept);
		dnodes.sort();

		// Create DFSM Graph

		for (auto &it : dnodes)
		{
			SvaDFsmNode &dnode = it.second;
			dnode.outnode = output_fsm.createNode();

			if (it.first == vector<int>{startNode})
				output_fsm.createLink(output_start_node, dnode.outnode);

			if (output_accept_node >= 0) {
				vector<Const> accept_cond = dnode.accept;
				optimize_cond(accept_cond);
				for (auto &value : accept_cond)
					output_fsm.createLink(it.second.outnode, output_accept_node, make_cond_eq(dnode.ctrl, value));
			}

			if (output_reject_node >= 0) {
				vector<Const> reject_cond = dnode.reject;
				optimize_cond(reject_cond);
				for (auto &value : reject_cond)
					output_fsm.createLink(it.second.outnode, output_reject_node, make_cond_eq(dnode.ctrl, value));
			}
		}

		for (auto &it : dnodes)
		{
			SvaDFsmNode &dnode = it.second;
			dict<vector<int>, vector<Const>> edge_cond;

			for (auto &edge : dnode.edges)
				edge_cond[edge.first].push_back(edge.second);

			for (auto &it : edge_cond) {
				optimize_cond(it.second);
				for (auto &value : it.second)
					output_fsm.createEdge(dnode.outnode, dnodes.at(it.first).outnode, make_cond_eq(dnode.ctrl, value));
			}
		}
	}

	// ----------------------------------------------------
	// State dump for verbose log messages

	void dump_nodes()
	{
		if (nodes.empty())
			return;

		log("      non-deterministic encoding:\n");
		for (int i = 0; i < GetSize(nodes); i++)
		{
			log("        node %d:%s\n", i,
					i == startNode ? " [start]" :
					i == acceptNode ? " [accept]" :
					i == condNode ? " [cond]" : "");

			for (auto &it : nodes[i].edges) {
				if (it.second != State::S1)
					log("          edge %s -> %d\n", log_signal(it.second), it.first);
				else
					log("          edge -> %d\n", it.first);
			}

			for (auto &it : nodes[i].links) {
				if (it.second != State::S1)
					log("          link %s -> %d\n", log_signal(it.second), it.first);
				else
					log("          link -> %d\n", it.first);
			}
		}
	}

	void dump_unodes()
	{
		if (unodes.empty())
			return;

		log("      unlinked non-deterministic encoding:\n");
		for (int i = 0; i < GetSize(unodes); i++)
		{
			if (!unodes[i].reachable)
				continue;

			log("        unode %d:%s\n", i, i == startNode ? " [start]" : "");

			for (auto &it : unodes[i].edges) {
				if (!it.second.empty())
					log("          edge %s -> %d\n", log_signal(it.second), it.first);
				else
					log("          edge -> %d\n", it.first);
			}

			for (auto &ctrl : unodes[i].accept) {
				if (!ctrl.empty())
					log("          accept %s\n", log_signal(ctrl));
				else
					log("          accept\n");
			}

			for (auto &ctrl : unodes[i].cond) {
				if (!ctrl.empty())
					log("          cond %s\n", log_signal(ctrl));
				else
					log("          cond\n");
			}
		}
	}

	void dump_dnodes()
	{
		if (dnodes.empty())
			return;

		log("      deterministic encoding:\n");
		for (auto &it : dnodes)
		{
			log("        dnode {");
			for (int i = 0; i < GetSize(it.first); i++)
				log("%s%d", i ? "," : "", it.first[i]);
			log("}:%s\n", GetSize(it.first) == 1 && it.first[0] == startNode ? " [start]" : "");

			log("          ctrl %s\n", log_signal(it.second.ctrl));

			for (auto &edge : it.second.edges) {
				log("          edge %s -> {", log_signal(edge.second));
				for (int i = 0; i < GetSize(edge.first); i++)
					log("%s%d", i ? "," : "", edge.first[i]);
				log("}\n");
			}

			for (auto &value : it.second.accept)
				log("          accept %s\n", log_signal(value));

			for (auto &value : it.second.reject)
				log("          reject %s\n", log_signal(value));
		}
	}

	void dump()
	{
		if (!nodes.empty())
			log("      number of NFSM states: %d\n", GetSize(nodes));

		if (!unodes.empty()) {
			int count = 0;
			for (auto &unode : unodes)
				if (unode.reachable)
					count++;
			log("      number of reachable UFSM states: %d\n", count);
		}

		if (!dnodes.empty())
			log("      number of DFSM states: %d\n", GetSize(dnodes));

		if (verific_verbose >= 2) {
			dump_nodes();
			dump_unodes();
			dump_dnodes();
		}

		if (trigger_sig != State::S1)
			log("      trigger signal: %s\n", log_signal(trigger_sig));

		if (final_accept_sig != State::Sx)
			log("      accept signal: %s\n", log_signal(final_accept_sig));

		if (final_reject_sig != State::Sx)
			log("      reject signal: %s\n", log_signal(final_reject_sig));
	}
};

PRIVATE_NAMESPACE_END

YOSYS_NAMESPACE_BEGIN

pool<int> verific_sva_prims = {
	// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
	PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
	PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
	PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
	PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
	PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
	PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
	PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
	PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
	PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
	PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
	PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
	PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
	PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
	PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
	PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
	PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
	PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
	PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
	PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
};

struct VerificSvaImporter
{
	VerificImporter *importer = nullptr;
	Module *module = nullptr;

	Netlist *netlist = nullptr;
	Instance *root = nullptr;

	VerificClocking clocking;

	bool mode_assert = false;
	bool mode_assume = false;
	bool mode_cover = false;
	bool mode_trigger = false;

	Instance *net_to_ast_driver(Net *n)
	{
		if (n == nullptr)
			return nullptr;

		if (n->IsMultipleDriven())
			return nullptr;

		Instance *inst = n->Driver();

		if (inst == nullptr)
			return nullptr;

		if (!verific_sva_prims.count(inst->Type()))
			return nullptr;

		if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
				inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE ||
				inst->Type() == PRIM_SVA_PAST || inst->Type() == PRIM_SVA_TRIGGERED)
			return nullptr;

		return inst;
	}

	Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
	Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
	Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
	Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
	Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }

	// ----------------------------------------------------------
	// SVA Importer

	struct ParserErrorException {
	};

	[[noreturn]] void parser_error(std::string errmsg)
	{
		if (!importer->mode_keep)
			log_error("%s", errmsg.c_str());
		log_warning("%s", errmsg.c_str());
		throw ParserErrorException();
	}

	[[noreturn]] void parser_error(std::string errmsg, linefile_type loc)
	{
		parser_error(stringf("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc)));
	}

	[[noreturn]] void parser_error(std::string errmsg, Instance *inst)
	{
		parser_error(stringf("%s at %s (%s)", errmsg.c_str(), inst->View()->Owner()->Name(), inst->Name()), inst->Linefile());
	}

	[[noreturn]] void parser_error(Instance *inst)
	{
		std::string msg;
		if (inst->Type() == PRIM_SVA_MATCH_ITEM_TRIGGER || inst->Type() == PRIM_SVA_MATCH_ITEM_ASSIGN)
		{
			msg = "SVA sequences with local variable assignments are currently not supported.\n";
		}

		parser_error(stringf("%sVerific SVA primitive %s (%s) is currently unsupported in this context",
				msg.c_str(), inst->View()->Owner()->Name(), inst->Name()), inst->Linefile());
	}

	dict<Net*, bool, hash_ptr_ops> check_expression_cache;

	bool check_expression(Net *net, bool raise_error = false)
	{
		while (!check_expression_cache.count(net))
		{
			Instance *inst = net_to_ast_driver(net);

			if (inst == nullptr) {
				check_expression_cache[net] = true;
				break;
			}

			if (inst->Type() == PRIM_SVA_AT)
			{
				VerificClocking new_clocking(importer, net);
				log_assert(new_clocking.cond_net == nullptr);
				if (!clocking.property_matches_sequence(new_clocking))
					parser_error("Mixed clocking is currently not supported", inst);
				check_expression_cache[net] = check_expression(new_clocking.body_net, raise_error);
				break;
			}

			if (inst->Type() == PRIM_SVA_FIRST_MATCH || inst->Type() == PRIM_SVA_NOT)
			{
				check_expression_cache[net] = check_expression(inst->GetInput(), raise_error);
				break;
			}

			if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_INTERSECT ||
					inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT ||
					inst->Type() == PRIM_SVA_OR || inst->Type() == PRIM_SVA_AND)
			{
				check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error);
				break;
			}

			if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
			{
				const char *sva_low_s = inst->GetAttValue("sva:low");
				const char *sva_high_s = inst->GetAttValue("sva:high");

				int sva_low = atoi(sva_low_s);
				int sva_high = atoi(sva_high_s);
				bool sva_inf = !strcmp(sva_high_s, "$");

				if (sva_low == 0 && sva_high == 0 && !sva_inf)
					check_expression_cache[net] = check_expression(inst->GetInput1(), raise_error) && check_expression(inst->GetInput2(), raise_error);
				else
					check_expression_cache[net] = false;
				break;
			}

			check_expression_cache[net] = false;
		}

		if (raise_error && !check_expression_cache.at(net))
			parser_error(net_to_ast_driver(net));
		return check_expression_cache.at(net);
	}

	SigBit parse_expression(Net *net)
	{
		check_expression(net, true);

		Instance *inst = net_to_ast_driver(net);

		if (inst == nullptr) {
			return importer->net_map_at(net);
		}

		if (inst->Type() == PRIM_SVA_AT)
		{
			VerificClocking new_clocking(importer, net);
			log_assert(new_clocking.cond_net == nullptr);
			if (!clocking.property_matches_sequence(new_clocking))
				parser_error("Mixed clocking is currently not supported", inst);
			return parse_expression(new_clocking.body_net);
		}

		if (inst->Type() == PRIM_SVA_FIRST_MATCH)
			return parse_expression(inst->GetInput());

		if (inst->Type() == PRIM_SVA_NOT)
			return module->Not(NEW_ID, parse_expression(inst->GetInput()));

		if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR)
			return module->Or(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2()));

		if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND || inst->Type() == PRIM_SVA_INTERSECT ||
				inst->Type() == PRIM_SVA_WITHIN || inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_SEQ_CONCAT)
			return module->And(NEW_ID, parse_expression(inst->GetInput1()), parse_expression(inst->GetInput2()));

		log_abort();
	}

	bool check_zero_consecutive_repeat(Net *net)
	{
		Instance *inst = net_to_ast_driver(net);

		if (inst == nullptr)
			return false;

		if (inst->Type() != PRIM_SVA_CONSECUTIVE_REPEAT)
			return false;

		const char *sva_low_s = inst->GetAttValue("sva:low");
		int sva_low = atoi(sva_low_s);

		return sva_low == 0;
	}

	int parse_consecutive_repeat(SvaFsm &fsm, int start_node, Net *net, bool add_pre_delay, bool add_post_delay)
	{
		Instance *inst = net_to_ast_driver(net);

		log_assert(inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT);

		const char *sva_low_s = inst->GetAttValue("sva:low");
		const char *sva_high_s = inst->GetAttValue("sva:high");

		int sva_low = atoi(sva_low_s);
		int sva_high = atoi(sva_high_s);
		bool sva_inf = !strcmp(sva_high_s, "$");

		Net *body_net = inst->GetInput();

		if (add_pre_delay || add_post_delay)
			log_assert(sva_low == 0);

		if (sva_low == 0) {
			if (!add_pre_delay && !add_post_delay)
				parser_error("Possibly zero-length consecutive repeat must follow or precede a delay of at least one cycle", inst);
			sva_low++;
		}

		int node = fsm.createNode(start_node);
		start_node = node;

		if (add_pre_delay) {
			node = fsm.createNode(start_node);
			fsm.createEdge(start_node, node);
		}

		int prev_node = node;
		node = parse_sequence(fsm, node, body_net);

		for (int i = 1; i < sva_low; i++)
		{
			int next_node = fsm.createNode();
			fsm.createEdge(node, next_node);

			prev_node = node;
			node = parse_sequence(fsm, next_node, body_net);
		}

		if (sva_inf)
		{
			log_assert(prev_node >= 0);
			fsm.createEdge(node, prev_node);
		}
		else
		{
			for (int i = sva_low; i < sva_high; i++)
			{
				int next_node = fsm.createNode();
				fsm.createEdge(node, next_node);

				prev_node = node;
				node = parse_sequence(fsm, next_node, body_net);

				fsm.createLink(prev_node, node);
			}
		}

		if (add_post_delay) {
			int next_node = fsm.createNode();
			fsm.createEdge(node, next_node);
			node = next_node;
		}

		if (add_pre_delay || add_post_delay)
			fsm.createLink(start_node, node);

		return node;
	}

	int parse_sequence(SvaFsm &fsm, int start_node, Net *net)
	{
		if (check_expression(net)) {
			int node = fsm.createNode();
			fsm.createLink(start_node, node, parse_expression(net));
			return node;
		}

		Instance *inst = net_to_ast_driver(net);

		if (inst->Type() == PRIM_SVA_AT)
		{
			VerificClocking new_clocking(importer, net);
			log_assert(new_clocking.cond_net == nullptr);
			if (!clocking.property_matches_sequence(new_clocking))
				parser_error("Mixed clocking is currently not supported", inst);
			return parse_sequence(fsm, start_node, new_clocking.body_net);
		}

		if (inst->Type() == PRIM_SVA_FIRST_MATCH)
		{
			SvaFsm match_fsm(clocking);
			match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode);

			int node = fsm.createNode();
			match_fsm.getDFsm(fsm, start_node, node);

			if (verific_verbose) {
				log("    First Match FSM:\n");
				match_fsm.dump();
			}

			return node;
		}

		if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME)
		{
			const char *sva_low_s = inst->GetAttValue("sva:low");
			const char *sva_high_s = inst->GetAttValue("sva:high");

			int sva_low = atoi(sva_low_s);
			int sva_high = atoi(sva_high_s);
			log_assert(sva_low == sva_high);

			int node = start_node;

			for (int i = 0; i < sva_low; i++) {
				int next_node = fsm.createNode();
				fsm.createEdge(node, next_node);
				node = next_node;
			}

			return parse_sequence(fsm, node, inst->GetInput());
		}

		if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
		{
			const char *sva_low_s = inst->GetAttValue("sva:low");
			const char *sva_high_s = inst->GetAttValue("sva:high");

			int sva_low = atoi(sva_low_s);
			int sva_high = atoi(sva_high_s);
			bool sva_inf = !strcmp(sva_high_s, "$");

			int node = -1;
			bool past_add_delay = false;

			if (check_zero_consecutive_repeat(inst->GetInput1()) && sva_low > 0) {
				node = parse_consecutive_repeat(fsm, start_node, inst->GetInput1(), false, true);
				sva_low--, sva_high--;
			} else {
				node = parse_sequence(fsm, start_node, inst->GetInput1());
			}

			if (check_zero_consecutive_repeat(inst->GetInput2()) && sva_low > 0) {
				past_add_delay = true;
				sva_low--, sva_high--;
			}

			for (int i = 0; i < sva_low; i++) {
				int next_node = fsm.createNode();
				fsm.createEdge(node, next_node);
				node = next_node;
			}

			if (sva_inf)
			{
				fsm.createEdge(node, node);
			}
			else
			{
				for (int i = sva_low; i < sva_high; i++)
				{
					int next_node = fsm.createNode();
					fsm.createEdge(node, next_node);
					fsm.createLink(node, next_node);
					node = next_node;
				}
			}

			if (past_add_delay)
				node = parse_consecutive_repeat(fsm, node, inst->GetInput2(), true, false);
			else
				node = parse_sequence(fsm, node, inst->GetInput2());

			return node;
		}

		if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT)
		{
			return parse_consecutive_repeat(fsm, start_node, net, false, false);
		}

		if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT || inst->Type() == PRIM_SVA_GOTO_REPEAT)
		{
			const char *sva_low_s = inst->GetAttValue("sva:low");
			const char *sva_high_s = inst->GetAttValue("sva:high");

			int sva_low = atoi(sva_low_s);
			int sva_high = atoi(sva_high_s);
			bool sva_inf = !strcmp(sva_high_s, "$");

			Net *body_net = inst->GetInput();
			int node = fsm.createNode(start_node);

			SigBit cond = parse_expression(body_net);
			SigBit not_cond = module->Not(NEW_ID, cond);

			for (int i = 0; i < sva_low; i++)
			{
				int wait_node = fsm.createNode();
				fsm.createEdge(wait_node, wait_node, not_cond);

				if (i == 0)
					fsm.createLink(node, wait_node);
				else
					fsm.createEdge(node, wait_node);

				int next_node = fsm.createNode();
				fsm.createLink(wait_node, next_node, cond);

				node = next_node;
			}

			if (sva_inf)
			{
				int wait_node = fsm.createNode();
				fsm.createEdge(wait_node, wait_node, not_cond);
				fsm.createEdge(node, wait_node);
				fsm.createLink(wait_node, node, cond);
			}
			else
			{
				for (int i = sva_low; i < sva_high; i++)
				{
					int wait_node = fsm.createNode();
					fsm.createEdge(wait_node, wait_node, not_cond);

					if (i == 0)
						fsm.createLink(node, wait_node);
					else
						fsm.createEdge(node, wait_node);

					int next_node = fsm.createNode();
					fsm.createLink(wait_node, next_node, cond);

					fsm.createLink(node, next_node);
					node = next_node;
				}
			}

			if (inst->Type() == PRIM_SVA_NON_CONSECUTIVE_REPEAT)
				fsm.createEdge(node, node);

			return node;
		}

		if (inst->Type() == PRIM_SVA_SEQ_OR || inst->Type() == PRIM_SVA_OR)
		{
			int node = parse_sequence(fsm, start_node, inst->GetInput1());
			int node2 = parse_sequence(fsm, start_node, inst->GetInput2());
			fsm.createLink(node2, node);
			return node;
		}

		if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND)
		{
			SvaFsm fsm1(clocking);
			fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode);

			SvaFsm fsm2(clocking);
			fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode);

			SvaFsm combined_fsm(clocking);
			fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);
			fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode);

			int node = fsm.createNode();
			combined_fsm.getDFsm(fsm, start_node, -1, node);

			if (verific_verbose)
			{
				log("    Left And FSM:\n");
				fsm1.dump();

				log("    Right And FSM:\n");
				fsm1.dump();

				log("    Combined And FSM:\n");
				combined_fsm.dump();
			}

			return node;
		}

		if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN)
		{
			SvaFsm intersect_fsm(clocking);

			if (inst->Type() == PRIM_SVA_INTERSECT)
			{
				intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput1()), intersect_fsm.acceptNode);
			}
			else
			{
				int n = intersect_fsm.createNode();
				intersect_fsm.createLink(intersect_fsm.createStartNode(), n);
				intersect_fsm.createEdge(n, n);

				n = parse_sequence(intersect_fsm, n, inst->GetInput1());

				intersect_fsm.createLink(n, intersect_fsm.acceptNode);
				intersect_fsm.createEdge(n, n);
			}

			intersect_fsm.in_cond_mode = true;
			intersect_fsm.createLink(parse_sequence(intersect_fsm, intersect_fsm.createStartNode(), inst->GetInput2()), intersect_fsm.condNode);
			intersect_fsm.in_cond_mode = false;

			int node = fsm.createNode();
			intersect_fsm.getDFsm(fsm, start_node, node, -1, false, true);

			if (verific_verbose) {
				log("    Intersect FSM:\n");
				intersect_fsm.dump();
			}

			return node;
		}

		if (inst->Type() == PRIM_SVA_THROUGHOUT)
		{
			SigBit expr = parse_expression(inst->GetInput1());

			fsm.pushThroughout(expr);
			int node = parse_sequence(fsm, start_node, inst->GetInput2());
			fsm.popThroughout();

			return node;
		}

		parser_error(inst);
	}

	void get_fsm_accept_reject(SvaFsm &fsm, SigBit *accept_p, SigBit *reject_p, bool swap_accept_reject = false)
	{
		log_assert(accept_p != nullptr || reject_p != nullptr);

		if (swap_accept_reject)
			get_fsm_accept_reject(fsm, reject_p, accept_p);
		else if (reject_p == nullptr)
			*accept_p = fsm.getAccept();
		else if (accept_p == nullptr)
			*reject_p = fsm.getReject();
		else
			fsm.getFirstAcceptReject(accept_p, reject_p);
	}

	bool eventually_property(Net *&net, SigBit &trig)
	{
		Instance *inst = net_to_ast_driver(net);

		if (inst == nullptr)
			return false;

		if (clocking.cond_net != nullptr)
			trig = importer->net_map_at(clocking.cond_net);
		else
			trig = State::S1;

		if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
		{
			if (mode_cover || mode_trigger)
				parser_error(inst);

			net = inst->GetInput();
			clocking.cond_net = nullptr;

			return true;
		}

		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
		{
			Net *antecedent_net = inst->GetInput1();
			Net *consequent_net = inst->GetInput2();

			Instance *consequent_inst = net_to_ast_driver(consequent_net);

			if (consequent_inst == nullptr)
				return false;

			if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY)
				return false;

			if (mode_cover || mode_trigger)
				parser_error(consequent_inst);

			int node;

			SvaFsm antecedent_fsm(clocking, trig);
			node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
				int next_node = antecedent_fsm.createNode();
				antecedent_fsm.createEdge(node, next_node);
				node = next_node;
			}
			antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);

			trig = antecedent_fsm.getAccept();
			net = consequent_inst->GetInput();
			clocking.cond_net = nullptr;

			if (verific_verbose) {
				log("    Eventually Antecedent FSM:\n");
				antecedent_fsm.dump();
			}

			return true;
		}

		return false;
	}

	void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
	{
		Instance *inst = net_to_ast_driver(net);

		SigBit trig = State::S1;

		if (clocking.cond_net != nullptr)
			trig = importer->net_map_at(clocking.cond_net);

		if (inst == nullptr)
		{
			log_assert(trig == State::S1);

			if (accept_p != nullptr)
				*accept_p = importer->net_map_at(net);
			if (reject_p != nullptr)
				*reject_p = module->Not(NEW_ID, importer->net_map_at(net));
		}
		else
		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
		{
			Net *antecedent_net = inst->GetInput1();
			Net *consequent_net = inst->GetInput2();
			int node;

			SvaFsm antecedent_fsm(clocking, trig);
			node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
				int next_node = antecedent_fsm.createNode();
				antecedent_fsm.createEdge(node, next_node);
				node = next_node;
			}

			Instance *consequent_inst = net_to_ast_driver(consequent_net);

			if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
					consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH ||
					consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS))
			{
				bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;

				Net *until_net = nullptr;
				if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)
				{
					consequent_net = consequent_inst->GetInput();
					consequent_inst = net_to_ast_driver(consequent_net);
				}
				else
				{
					until_net = consequent_inst->GetInput2();
					consequent_net = consequent_inst->GetInput1();
					consequent_inst = net_to_ast_driver(consequent_net);
				}

				SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0;
				SigBit not_until_sig = module->Not(NEW_ID, until_sig);
				antecedent_fsm.createEdge(node, node, not_until_sig);

				antecedent_fsm.createLink(node, antecedent_fsm.acceptNode, until_with ? State::S1 : not_until_sig);
			}
			else
			{
				antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
			}

			SigBit antecedent_match = antecedent_fsm.getAccept();

			if (verific_verbose) {
				log("    Antecedent FSM:\n");
				antecedent_fsm.dump();
			}

			bool consequent_not = false;
			if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) {
				consequent_not = true;
				consequent_net = consequent_inst->GetInput();
				consequent_inst = net_to_ast_driver(consequent_net);
			}

			SvaFsm consequent_fsm(clocking, antecedent_match);
			node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net);
			consequent_fsm.createLink(node, consequent_fsm.acceptNode);

			get_fsm_accept_reject(consequent_fsm, accept_p, reject_p, consequent_not);

			if (verific_verbose) {
				log("    Consequent FSM:\n");
				consequent_fsm.dump();
			}
		}
		else
		{
			bool prop_not = inst->Type() == PRIM_SVA_NOT;
			if (prop_not) {
				net = inst->GetInput();
				inst = net_to_ast_driver(net);
			}

			SvaFsm fsm(clocking, trig);
			int node = parse_sequence(fsm, fsm.createStartNode(), net);
			fsm.createLink(node, fsm.acceptNode);

			get_fsm_accept_reject(fsm, accept_p, reject_p, prop_not);

			if (verific_verbose) {
				log("    Sequence FSM:\n");
				fsm.dump();
			}
		}
	}

	void import()
	{
		try
		{
			module = importer->module;
			netlist = root->Owner();

			if (verific_verbose)
				log("  importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(),
						LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));

			bool is_user_declared = root->IsUserDeclared();

			// FIXME
			if (!is_user_declared) {
				const char *name = root->Name();
				for (int i = 0; name[i]; i++) {
					if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) {
						is_user_declared = true;
						break;
					}
				}
			}

			RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID);

			// parse SVA sequence into trigger signal

			clocking = VerificClocking(importer, root->GetInput(), true);
			SigBit accept_bit = State::S0, reject_bit = State::S0;

			if (clocking.body_net == nullptr)
			{
				if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr ||  clocking.cond_net != nullptr)
					parser_error(stringf("Failed to parse SVA clocking"), root);

				if (mode_assert || mode_assume) {
					reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput()));
				} else {
					accept_bit = parse_expression(root->GetInput());
				}
			}
			else
			{
				Net *net = clocking.body_net;
				SigBit trig;

				if (eventually_property(net, trig))
				{
					SigBit sig_a, sig_en = trig;
					parse_property(net, &sig_a, nullptr);

					// add final FF stage

					SigBit sig_a_q, sig_en_q;

					if (clocking.body_net == nullptr) {
						sig_a_q = sig_a;
						sig_en_q = sig_en;
					} else {
						sig_a_q = module->addWire(NEW_ID);
						sig_en_q = module->addWire(NEW_ID);
						clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
						clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
					}

					// accept in disable case

					if (clocking.disable_sig != State::S0)
						sig_a_q = module->Or(NEW_ID, sig_a_q, clocking.disable_sig);

					// generate fair/live cell

					RTLIL::Cell *c = nullptr;

					if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q);
					if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q);

					importer->import_attributes(c->attributes, root);

					return;
				}
				else
				{
					if (mode_assert || mode_assume) {
						parse_property(net, nullptr, &reject_bit);
					} else {
						parse_property(net, &accept_bit, nullptr);
					}
				}
			}

			if (mode_trigger)
			{
				module->connect(importer->net_map_at(root->GetOutput()), accept_bit);
			}
			else
			{
				SigBit sig_a = module->Not(NEW_ID, reject_bit);
				SigBit sig_en = module->Or(NEW_ID, accept_bit, reject_bit);

				// add final FF stage

				SigBit sig_a_q, sig_en_q;

				if (clocking.body_net == nullptr) {
					sig_a_q = sig_a;
					sig_en_q = sig_en;
				} else {
					sig_a_q = module->addWire(NEW_ID);
					sig_en_q = module->addWire(NEW_ID);
					clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
					clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
				}

				// generate assert/assume/cover cell

				RTLIL::Cell *c = nullptr;

				if (mode_assert) c = module->addAssert(root_name, sig_a_q, sig_en_q);
				if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q);
				if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_q);

				importer->import_attributes(c->attributes, root);
			}
		}
		catch (ParserErrorException)
		{
		}
	}
};

void verific_import_sva_assert(VerificImporter *importer, Instance *inst)
{
	VerificSvaImporter worker;
	worker.importer = importer;
	worker.root = inst;
	worker.mode_assert = true;
	worker.import();
}

void verific_import_sva_assume(VerificImporter *importer, Instance *inst)
{
	VerificSvaImporter worker;
	worker.importer = importer;
	worker.root = inst;
	worker.mode_assume = true;
	worker.import();
}

void verific_import_sva_cover(VerificImporter *importer, Instance *inst)
{
	VerificSvaImporter worker;
	worker.importer = importer;
	worker.root = inst;
	worker.mode_cover = true;
	worker.import();
}

void verific_import_sva_trigger(VerificImporter *importer, Instance *inst)
{
	VerificSvaImporter worker;
	worker.importer = importer;
	worker.root = inst;
	worker.mode_trigger = true;
	worker.import();
}

bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net)
{
	VerificSvaImporter worker;
	worker.importer = importer;
	return worker.net_to_ast_driver(net) != nullptr;
}

YOSYS_NAMESPACE_END