Production RTL is parameterized, lint-clean, and verifiable. This section covers generate loops, IP boundaries, synthesis constraints, coding rules, assertions, and when formal helps.
Topic | Lessons | After it you can… | Study time |
|---|---|---|---|
3 | Write parameterized modules with generate loops and named overrides. | 25 min | |
3 | Structure hierarchy with clean ports and propagated parameters. | 25 min | |
4 | Write inference-friendly RTL without latches or banned pragmas. | 25 min | |
3 | Apply style rules and run lint with disciplined waivers. | 25 min | |
4 | Bind immediate and concurrent assertions with cover and assume. | 25 min | |
4 | Scope bounded proofs with sound assumptions on the right targets. | 25 min | |
7 | Use packages, packed types, parameter types, functions, and interfaces in portable RTL. | 2 h |
Study time covers reading each lesson and running its examples. The section's hands-on project takes extra hours on top.
The testbench samples behaviors while lint checks every path for width, latch, and rule violations. The Coding Style and Lint topic shows the rule table and waiver discipline.
Use these four questions to decide whether you are ready to move on: explain, predict, implement and debug. If one is shaky, each answer names the lesson to revisit. New readers can skip this until they finish the section.
parameter and when localparam?A parameter can be overridden per instance, so it is the module's configuration interface. A localparam cannot be overridden; use it for values derived from parameters (widths, depths) so nobody can set them inconsistently. Revisit Parameters vs localparams.
assert property (@(posedge clk) req |-> ##[1:3] gnt); and req is high at cycle 0, with gnt first high at cycle 4. Pass or fail?Fail. The property needs gnt one to three cycles after req, that is at cycle 1, 2 or 3; cycle 4 is outside the window, so the assertion fails at cycle 3 when the window closes. Revisit Common RTL property templates.
for generate loop. Why name the generate block?for (genvar i = 0; i < N; i++) begin : gen_stage ... end. The name gives each copy a stable hierarchical path (gen_stage[2].q) for waveforms, assertions, constraints and debugging. Revisit Generate loops and conditionals.
An over-constraining assumption: for example, assuming a request never arrives while busy removes exactly the case with the bug, so the proof is vacuous. Check that cover properties for the interesting scenarios are reachable, and review every assume against the interface spec. Revisit Assumption discipline.