Lab: verify counter reset, wraparound and invariants

The circuit and observation conditions

Initialize to 3 and reset^{iReset A control that returns state to a specified initial value. Define whether it is synchronous or asynchronous and whether it has priority over other controls. Learn more} at the first rising edge^{iRising edge The instant at which the clock changes from 0 to 1. Distinguish it from a level, which refers to the entire interval during which CLK=1. Learn more}. The counter then follows 0, 1, 2, 3, 0. Even with reset asserted, the value remains unchanged before the clock edge.

Before starting

Prepare a Digital Design Studio Desktop project with normal execution permission. Save each example as rtl/top.sv in a separate folder.

SystemVerilog source

module top (
    input logic clk,
    input logic rst,
    output logic [1:0] count
);
    // Active-high synchronous reset: sampled only at the rising clock edge.
    always_ff @(posedge clk)
        if (rst) count <= 2'b00;
        else count <= count + 2'b01;
endmodule

Running the lab

In New analysis, choose Two-state single-clock v1. Clock port is clk, with period 1000ps. Use the settings below, run Preflight and Run RTL simulation, then compare results.

Input stimulus

[
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  },
  {
    "inputs": {}
  }
]

Each column below records one rising edge. Inputs are pre-edge; states labeled “after” are post-update. Alignment indicates sampling order, not physical propagation delay^{iPropagation delay The time from an input change until the output settles to the correct value. Logical equivalence and timing behavior are separate properties. Learn more}. E0–E4 are the rising edges at 500, 1500, 2500, 3500 and 4500ps. Compare every intermediate count column as well as the final value.

Compare results

5 cycles · count=00. Confirm 00 → 01 → 10 → 11 → 00 at 500, 1500, 2500, 3500 and 4500ps.

This lab uses 0/1 single-clock RTL and does not include #delay, initial or X/Z testbenches. A lesson-completion mark records learning progress, not an actual simulation result.

Calculate expected state edge by edge

The initial register^{iRegister A circuit that stores multiple bits of state. The synchronous registers in this course store their specified inputs at a clock edge. Learn more} value is 3, but reset wins at the first rising edge. Do not treat initialization and reset as the same thing.

At every edge without reset,

Checking only the final 00 can pass even after incorrect intermediate states. Check the entire state sequence and reset priority separately.

Change one experimental condition at a time

• Setting the initial value to 00 should leave the post-reset sequence unchanged. Use this to check that reset does not depend on the initial value.
• With Reset cycles=2, count must be 00 after both first rising edges. Incrementing then starts one edge later.
• Widening to three bits gives a wrap period of eight increments. Review constant widths, the initial register array and run length as well as the declaration.

Generalize to modulo-10

Four-bit storage represents 0–15, so simple incrementing does not wrap 9 to 0. Specify the next-state function separately:

This definition returns unused states 10–15 to 0 when enable is active. Other recovery policies are possible, but the specification and verification model must use the same policy.