A semantics for SVA local variables that preserves the distributivity of intersection

According to Eisner and Fisman

The semantics of temporal logic is usually defined with respect to a word representing a computation path over a set of atomic propositions. A temporal logic formula does not control the behavior of the atomic propositions, it merely observes their behavior. Local variables are a twist on this approach, in which the user can declare variables local to the formula and control their behavior from within the formula itself.

Local variables were introduced in 2002, and a formal semantics was given to them in the context of SVA, the assertion language of SystemVerilog, in 2004. That semantics suffers from several drawbacks. In particular, it breaks distributivity of the operators corresponding to intersection and union. In this paper we present a formal semantics for local variables that solves that problem and others, and compare it to the previous solution.

More …


Tell me (anonymous OK)

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s