SVA assume/assertions for continuous data input
<p>I am an assertion based verification newbie trying to learn how it's supposed to be done properly. I have found a lot of information about the structure and technical details about the systemverilog + assertions but I still have not found somekind of a "cookbook" material of how things are really done in real world.</p>

<p>The question and constraints:</p>

<ul>
<li>Design has a data input bus with <em>data, valid</em> and <em>id</em> inputs</li>
<li>One data "package" is 3 samples</li>
<li>After channel <em>n</em> there will always be data from channel <em>n+1</em>

<ul>
<li>channel IDs will wrap after the largest ID has been sent</li>
</ul></li>
<li>There can be any number of clk ticks between data bytes</li>
<li><p>Below is a simple and hopefully correct timing diagram with channel IDs:</p>

<p><a href="https://i.stack.imgur.com/qz8XS.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/qz8XS.png" alt="enter image description here"></a></p></li>
</ul>

<p><strong>So how do you do this with least ammount of code?</strong> Nice and clean. Previously I have build dummy verilog modules to drive the data. But surely one could just use some <em>assume property</em> to just constrain the channel IDs but otherwise leave free hands for the formal tool to try to brake my design?</p>

<p>Simple template for starters could be:</p>

<pre><code>data_in : assume property (
  &lt;data with some ID&gt;[=3]
  |=&gt;
  &lt;data with the next id after any clk tick&gt;
);
</code></pre>

<p>I guess the problem is that assumes/assertions like above tend to trigger on every data sample and create parallel threads which overlap in time.</p>