Convert to parallel form with blocking assign present:
------------------------------------------------------
NB: Not examinable for SoCDAM course but useful to know!
Peform symbolic evaluation: evaluate imperative code in an environment sigma.
Sigma is a mapping from variable name to expression already assigned.
Expressions:
[ n ]_sigma = n
| [ v ]_sigma = sigma(v)
| [ e1+e2 ]_sigma = gen_plus( [e1]_sigma, [e2]_sigma)
| [ e1?et:ef ]_sigma = gen_mux2([e1]_sigma, [et]_sigma, [ef]_sigma))
| and so on
Note: the notation [ ] is here used for semantics-style interpretation, not ML-style lists!
The function 'gen_plus' generates a tree node unless its args are compile-time
constants in which case it evauates the addition.
sigma(v) where v is not in sigma just returns v.
Assignment Command:
[ v := e ]_sigma = sigma augmented with [ e ]_sigma
For example : start with empty sigma
[ v1 := 7; v2 := v1 + v2 ]_sigma
gives [ ("v1", 7), ("v2", plus(7, v3)) ]
Sequencing Command:
[ C1; C2 ]_sigma = let val sigma' = [ C1 ]_sigma in [ C2 ]_sigma' end
If command:
[ if e then CT else CF ]_sigma =
let val g = [ e ]_sigma // no side effects
val st = [ C1 ]_sigma
val sf = [ C2 ]_sigma
val updated = union(map fst st, map fst sf)
fun envmux v = (v, gen_mux2(g, [ v ]_st, [ v ]_sf))
or equally:
fun envmux v = (v, gen_mux2(g, st(v), sf(v)))
in map envmux updated end
// Can optimise if g is a compile time constant!
It's just pure Denotational Semantics!
Convert to parallel form, with non-blocking assigns:
----------------------------------------------------
Same as with blocking assigns except that r.h.s. expressions do not
have to be looked up in sigma.
Convert to parallel form, with both styles of assign present:
-------------------------------------------------------------
Need to keep two environments: one for each type of assignment.
Rhs values are only looked up in the blocking assignment list.
On exit, need to merge lists: if a net appears twice,
Verilog gives precedence to the non-blocking assign.
-----------------------
Code generation:
The environment list is a query tree for each variable.
For instance:
reg z;
reg [2:0] q;
always @(posedge ck) begin
z <= ~z;
if (z) q <= q + 3'd1;
end
Generates, for the clock domain 'ck', the list:
[ (Net "z", Inv(Net "z")),
(Net "q", Query(Net "z", Diadic(D_plus, Net "q", Num 1), Net "q"))
]
And to make the gates we need to call
app (fn (l, r)=>build_cmd(Assign(l, r))) sigma
-------------------------
Adding Arrays:
When we have arrays, the env list needs to either have a modified
form,
(lhs, [(guard, subscript, value), ... ])
or else we can use 'functional arrays'. Either way, code can get
quite complex when subscript equality cannot be determined at compile time.
END