Not quite. posedge detects these transitions (from the LRM):
Table 43—Detecting posedge and negedge
To 0 1 x z
From
0 No edge posedge posedge posedge
1 negedge No edge negedge negedge
x negedge posedge No edge No edge
z negedge posedge No edge No edge
So, 0->x is a posedge, for example. Your second example only detects cases where CLK ends up as 1, so misses 0->x and 0->z.
The IEEE Std. 1364.1(E):2002 (IEC 624142(E):2005), the Verilog register transfer level synthesis standard, states in Sec. 5.1 that an always block without any posedge/negedge events in the sensitivity list is combinational logic. I.e. the signals in the event list are ignored and the block is synthesized as if an implicit expression list (@(*), @*) was used. The following example is given in the standard ("Example 4" on page 14):
always @ (in)
if (ena)
out = in;
else
out = 1’b1;
// Supported, but simulation mismatch might occur.
// To assure the simulation will match the synthesized logic, add ena
// to the event list so the event list reads: always @ (in or ena)
(the comment is also copied from the standard document)
I.e. for a synthesis tool your second block is effectively:
always @*
begin
case(CLK)
1'b1:
state <= next_state;
1'b0:
state <= state;
end
which is just a multiplexer with CLK as select input, next_state as active-1 input and the output (state) fed back as active-0 input. A smart synthesis tool might detect that this is identical to a d-type latch with CLK as enable-input and create a d-type latch instead of a combinational loop. Note that the synthesis tool is not required to detect this latch because the code explicitly assigns state in all branches (compare Sec. 5.3. of the standard).
Either way this is different from the d-type flip-flop your first code example would synthesize to. This is one of many cases where Verilog-code has different meaning in simulation and synthesis. Therefore it is important to (1) write synthesizeable Verilog code in a way that avoids this cases and (2) always run post-synthesis simulations of your design (even if you are also using formal verification!) to make sure you have successfully avoided this pitfalls.
Functionally, those two circuits describe the same behavior in verilog, so I think there should be no difference.
However you should generally use the first style, as that is the one that is standard for writing synthesizable code, and most understandable by anyone else reading your code. The latter style, while describing the correct behavior, may confuse some synthesizers that don't expect to see clocks that are both sensitive to positive and negative edge.
The two blocks are VERY different.
The top one gives you a flip-flop while the bottom one gives you a latch with a multiplexer with the CLK as the select signal.
The critical difference between the two blocks is that the top one is a synchronous block i.e. the posedge clk part while the bottom one is asynchronous with the CLK level, not edge.
A verilog simulator could do left-hand sampling of CLK, effectively making the the case(CLK) version the same as a negedge CLK flop. Otherwise the simulator will treat it like a posedge CLK flop. It really depends how it is handled in the scheduler of specific simulator (or how a particular synthesizer will process it).
The most common codding styles all use the first condition. It is explicitly clear to the synthesizer and anyone reading the code that state is intended to be a flip-flop with a positive edge clocking trigger.
There is also a simulation performance differences. The posedge CLK performances 2 CPU operations every clock period, while the case(CLK) will perform 6 CPU operations every clock period. Granted in this example the differences is insignificance, but in large designs the poor coding used everywhere will add up to hours of simulation time wasted.
