I am reading the IEEE Standard Verilog Hardware Description Language (specifically IEEE Std 1364-2001) which unambiguously defines and discusses simulatable Verilog. Unfortunately, the document does not touch upon the notion of synthesis.

I haven't been able to find a similar reference for synthesisable Verilog. All I find is vague rules, or unnecessarily restrictive ones.

Where can I learn the formal language of synthesisable Verilog?

• verilog

IEEE 1364.1 is an adjunct to the 1364 Verilog standard titled Verilog Register Transfer Level Synthesis, which attempts to define a common synthesizable subset. However, as Jerry points out, different tools support different constructs, and to determine tool-specific behavior, you need to consult the tool documentation.

There isn't a formal (BNF-style) syntax definition for synthesizable Verilog. Whether code is synthesizable depends on usage as well as syntax. For example, the behavior described by an always construct with incomplete sensitivity, like always @(a) o = a || b, isn't synthesizable. (Most tools will synthesize that code as if the sensitivity list were complete, resulting in a possible simulation/synthesis mismatch.)

Circuit constructs like latches and multiply-driven nets can be synthesized from a Verilog description, but are disallowed or discouraged under most design rules. There are also synthesizable constructs that are unsupported or inadvisable given the choice of target library. For example, describing a RAM that's larger than the maximum supported by a chosen FPGA technology, or describing tri-state drivers when they aren't present in the target library.

The general constructs to stick to for synthesizable Verilog are:

• Combinational logic modeled with continuous assignments (assign statements)
• Combinational logic modeled with always blocks, which should use blocking assignments, and either have a complete sensitivity list or use always @*
• Sequential logic (flip-flops) modeled with always blocks, which should use non-blocking assignments, and have either posedge clock alone (for sync reset or non-reset flops) or posedge clock and posedge or negedge reset (for async reset flops) in the sensitivity list.

The safest coding style for sequential logic is to code only reset logic in the sequential always block:

always @(posedge clk or posedge reset)
  if (reset)
    q <= reset_value;
  else
    q <= next_value;

However, if you're careful, you can code additional combinational logic in the sequential block. A common case where it may make sense to do this is a mux in front of a flop:

always @(posedge clk)
  if (!sel)
    q <= sel0_value;
  else if (sel)
    q <= sel1_value;
  else
    q <= 'bx;