Assignment III (Synthesis)

Consider the following subset of Verilog called V0 (from Mike Gordon's notes)

Programs     P ::= always S
Statements   S ::= x = exp                          Blocking assignment
                |  x <= exp                         Non-blocking assignment
                |  begin {:label} S; ...; S end     Blocks
                |  disable label                    Jumps
                |  if (exp) S {else S}              Conditionals
                |  while (exp) S                    Loops
                |  forever S                        Infinite Loops
                |  @ S                              Timing Control

Programs     P ::= forever C
Commands     C ::= x1 := E1, x2 := E2, ...
Expressions  E ::= usual expressions 
                |  E -> E1 | E2

always
  begin
   @ x = 3;
   @ y = x + 4;
  end

forever
  pc := (pc=0 -> 1 | pc=1 -> 0);
  x  := (pc=0 -> 3 | pc=1 -> x);
  y  := (pc=0 -> y | pc=1 -> x+4);