Hardware Reference
In-Depth Information
be assigned in another (see Sect.
2.2.1
). Nor can a variable be assigned by two
continuous assignments, according to general SystemVerilog rules.
8
Formal Semantics.
It is difficult to give a general definition of the formal semantics
of continuous and blocking assignments to regular checker variables because of
various constructs, such as task calls in procedures and general looping statements.
If we avoid these constructs and assume that there are no side effects for the
variables in question, that all the loops are statically unrollable, and that there are
no combinational loops, we can provide a formal semantics for continuous and
blocking assignments.
Consider the continuous assignment
assign
v=e;
where
v
is a regular variable and expression
e
does not depend on
v
.Itsformal
semantics is given by the assumption
assume property
(@$global_clock v === e);
Expression
e
may contain free variables.
In the notation of research literature, the assignment is written
v
e, and the
equivalent assumption is the invariant G.
v
D
e/. The transition relation for
v
is in
this case a function. This function is called the
current state function
, stressing that
it assigns the current, rather than the next, state value of
v
(cf. Sect.
23.2.2.1
).
It remains to provide a formal semantics for blocking assignments to regular
checker variables. This task is much more complicated and requires a thorough
consideration of many details beyond the scope of this topic. We provide only a
sketch. In the theory of compilation it is proven that any synthesizable program
can be represented in a Static Single Assignment (SSA) form [
31
](seealso[
51
]).
9
In SSA form each
always_comb
and
always_latch
procedure is represented
equivalently using only continuous assignments, whose semantics has been given.
But the situation is complicated by latch modeling, which introduces incomplete
assignments and NBAs. Detailed description of latch modeling is beyond the scope
of this topic. We will just illustrate the concept in the following example.
Example 23.17.
Consider the variable declarations
bit
c, i;
bit
q = 1'b0;
A simple latch may be defined either using an NBA, as in
always_latch
if
(c)q<=i;
or using a blocking assignment:
8
Multiple continuous assignments are allowed only for nets.
9
The program does not have to be synthesizable to be represented in SSA form. The synthesizabil-
ity is required for an efficient representation of the -function.
Search WWH ::
Custom Search