Description
Turn the three next-state equations into RTL, then account for its state bits.
Implement three toggle stages using nonblocking assignments. Reset clears all three; en toggles t0, en with old t0 toggles t1, and en with old t0 and t1 toggles t2. Report the bare transition model’s latch count.
Pinned interface
| Port | Direction | Bits |
|---|---|---|
| clk | input | 1 |
| rst | input | 1 |
| en | input | 1 |
| t0 | output | 1 |
| t1 | output | 1 |
| t2 | output | 1 |
Full specification
Write a three-stage toggle chain. With reset low, t0 toggles on en; t1 toggles on en && old t0; t2 toggles on en && old t0 && old t1. Otherwise each bit holds. Reset clears all three. Initialize the state to zero as in the starter.
Use nonblocking updates so every right-hand side reads the same current state. Report the latch count for the bare three-bit transition system after write_aiger, before assertion monitors or initialization conversion are added. The judge counts the submitted model before adding its checker; the qualification script independently measures the reference.
| Execution rule | Meaning |
|---|---|
| Interface | Use the pinned port names, directions and bit widths shown above. Observed state and tracker outputs are not environment inputs. |
| Sampling | One positive edge of clk; binary values. Non-overlapping implication observes the next sample. Reset and initialization follow the source and contract above. |
| Submission | Submit RTL using the starter’s format. The checks apply to this stated model and scope. |
| How this is graded | The reference obligations, independent reachability checks and fault checks must all succeed. An unresolved proof or resource limit is inconclusive and is never a rated miss. |
Measured Counterexample
FAIL · prove · depth 8 · smtbmc yices · 494 ms
This measured failing run uses the published interface. Follow the sampled violation back to the preceding inputs and state. The worked solution below explains the required behaviour and the failure mechanisms.
Samples from the measured run. Free input lanes are shaded; the terminal VCD record is omitted.
Sample 2: t2=0, t1=1, t0=1. Previous sample: rst=0, en=0, t2=0, t1=0, t0=1. All toggles use the old state. With en high, t1 toggles only if old t0 is one, and t2 only if both lower old bits are one.
Examples
Three Enabled Edges
State (t2,t1,t0)=000; rst=0; en=1 for three edges.
001, 010, 011
The carry uses the old lower-stage bits.
Requirements
- Use the published ports and widths. The checker and the DUT variants are owned by the judge.
- Do not add assumptions unless the statement explicitly asks for one. A passing assertion without a reachable trigger is insufficient.
Hints
Hint 1
Draw one D-input cone for each state bit.
Hint 2
All right-hand sides use the state before the edge.
Hint 3
Use the state / input / next-state table in F2.1.
Single clock, binary values, synchronous reset. The judge checks the pinned interface, reachability and the declared proof or bound. UNKNOWN, resource limits and timeouts remain inconclusive.
INCONCLUSIVE never counts as acceptance or a rated miss. Run previews the same checks that Submit uses.
More problems on this topic