Instead of Cadence's Verilog-XL, we will be using NC Verilog. NCV runs much faster than Verilog-XL and is similar to Synopsys' VCS; both spend more time compiling the source verilog code before executing it.
Section 2.3
Do not worry about the various port/wire/register combinations. We will not be using inout ports
Section 3.3.1
We in fact do want to design single-edge-triggered state machines.