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