Skip to content
code0.HDL

08Verification

Guard a method with a private constant

Diagnose the starter

Intended behavior. capacity is a package-level constant that no caller can see. It is the single place that decides how many admissions mkGate allows, so admit must stop being ready once seated reaches it.

Current behavior. The method's readiness condition compares seated against a literal 6 instead of capacity. The gate admits six callers, so the private constant no longer governs the public method and changing capacity has no effect.

Fix. Make the readiness condition depend on the package-level constant. Keep the bound on the method itself rather than in the rule that calls it.

Read the package-level declarations before the module. Then compare the constant with the method header and predict the public run: how many calls does the literal allow, and what value should the package policy allow?

Repair path

Edit only the readiness expression. The caller should not need to know the private capacity, so do not move this condition into drive. Run after the change and confirm that the final observation follows the private constant.

Completion contract

  • Stop admit once seated reaches capacity.
  • Derive the bound from the package-level constant, not a repeated literal.
  • Keep the bound in the method's readiness condition.
  • Block further caller progress at the same boundary; matching one final display while accepting extra calls does not satisfy the contract.

Progressive hints

Hint 1

The readiness condition is the expression between if ( and ) in the method header. Compare every name in that expression with the package policy.

Hint 2

A package-level constant is in scope inside every module of the package, so the method can name capacity directly.

Concept

A private package-level definition is still usable everywhere inside its package. Naming it once and referring to it keeps the public method's behavior tied to a value callers cannot see or depend on.

Transfer experiment

After the repair, change capacity to another value from 1 through 7 without touching the method or caller. Predict the accepted-call count and final display. This checks that one private declaration controls the whole behavior.

Review this concept
Ready
Main.bsv