title: What does it mean for hardware synthesised from Verilog code to be correct
body: <p>I have read "Nonblocking Assignments in Verilog Synthesis, Coding Styles that Kill!" by Clifford Cummings. He says that the code at the bottom of this question is "guaranteed" to be synthesised into a three flip-flop pipeline, but it is not guaranteed to simulate correctly (example pipeb3, page 10; the "guaranteed" comment is on page 12). The document won a best paper award, so I assume the claim is true. <a href="http://www.sunburst-design.com/papers/CummingsSNUG2000SJ_NBA.pdf" rel="nofollow">http://www.sunburst-design.com/papers/CummingsSNUG2000SJ_NBA.pdf</a></p>
  
  <p>My question: How is the correctness of Verilog synthesis defined if not by reference to the simulation semantics? Many thanks. </p>
  
  <p>I suppose the bonus points question is: give the simplest possible Verilog program that has well-defined synthesis semantics and does not have well defined simulation semantics, assuming it is not the code below. Thanks again.</p>
  
  <p>In fact, can someone give me a piece of Verilog thatis well defined when both simulated and synthesised, yet the two produce different results?</p>
  
  <p>The code:</p>
  
  <pre><code>module pipeb3 q3, d, clk);
    output [7:0] q3;
    input [7:0] d;
    input clk;
    reg [7:0] q3, q2, q1;
  
    always @(posedge clk) q1=d;
    always @(posedge clk) q3=q2;
    always @(posedge clk) q1=d;
  endmodule
  </code></pre>
  
  <p>PS: in case anyone cares, I though a plausible definition of a correct synthesis tool might be along the lines of "the synthesised hardware will do something that a correct simulator could". But this is inconsistent with the paper.</p>
  
  <p>[I now think the paper is not right. Section 5.2 of the 1364-2001 standard clearly says that the meaning of a Verilog program  is defined by its simulation that the standard then proceeds to define (non-determinism and all). There is no mention whatsoever of any "guarantees" that synthesis tools must provide over and above simulators.</p>
  
  <p>There is another standard 1364.1-2002 that describes the synthesisable subset. There is no obvious mention that the semantics of synthesised hardware should somehow differ from simulation. Section 5.2.2 "Modelling edge-sensitive storage devices" says that non-blocking assignments should be used to model flip-flops. In standard-speak that means that the use of anything else is unsupported. </p>
  
  <p>As a final note, the section referred to in the previous paragraph says that blocking assignments can be used to calculate the RHS of the non-blocking assignment. This appears to violate Cummings' recommendation #5. </p>
  
  <p>Cliff Cummings is listed as a member of the working group of the 1364.1-2002 standard. This standard is listed as replaced on the IEEE website but I cannot tell what it was replaced by.]</p>