18 / 37 · Kiểm tra

Kiểm tra thiết kế: biên độ rộng, ưu tiên và quay vòng

Dùng đặc tả chuyển trạng thái để quyết định giá trị biên và điều khiển đồng thời.

Quy ước bộ đếm modulo-10

Với count unsigned^{unsigned Quy tắc diễn giải chuỗi bit là số nguyên không âm. Phạm vi n bit là 0 đến 2^n−1 và có thể khác diễn giải signed của cùng chuỗi bit. Tìm hiểu thêm} bốn bit, ưu tiên reset, enable, hold. reset=1 thì về 0; nếu enable=1 thì count≥9 về 0, trạng thái khác tăng 1.

N=\lceil\log_2 10\rceil=4

Bốn bit chỉ nghĩa có thể lưu 16 trạng thái, không tự thực hiện đặc tả dùng mười trạng thái. Đặc biệt count=9, enable=0 không được về 0.

Mỗi cột ghi lại quan sát tại một cạnh lên^{Cạnh lên Khoảnh khắc clock chuyển 0 sang 1, khác với mức cao chỉ cả khoảng CLK=1. Tìm hiểu thêm}. Đầu vào là giá trị ngay trước cạnh, còn trạng thái có tên chứa after là giá trị ngay sau cập nhật. Cách căn cột thể hiện thứ tự lấy mẫu, không mô tả độ trễ lan truyền^{Độ trễ lan truyền Thời gian từ khi đầu vào đổi đến khi đầu ra ổn định ở giá trị đúng. Tương đương logic và đặc tính thời gian là hai vấn đề riêng. Tìm hiểu thêm} vật lý. Ban đầu count=9. Cột đầu không reset, enable=0 giữ 9; chỉ cột sau enable=1 mới về 0.

Tại giá trị biên, hold vẫn phải giữ

Xem dữ liệu dạng sóng

Dữ liệu dạng sóng: mỗi ký tự là một khoảng; dấu chấm giữ trạng thái trước; p là một chu kỳ đồng hồ.
Tín hiệu	Dạng sóng	Giá trị bus
edge	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
count after	`23.4`	9 → 0 → 1

Câu hỏi thiết kế bổ sung

Tìm giá trị sau khi count=9, reset=0, enable=0.
Giải thích phục hồi khi count=15, enable=1.
Quy định có tạo xung kết thúc khi count=9, reset=1, enable=1 không. Giả sử đầu ra trong reset^{Reset Điều khiển đưa trạng thái về giá trị đầu đã định. Phải quy định đồng bộ hay bất đồng bộ và ưu tiên so với các điều khiển khác. Tìm hiểu thêm} được định nghĩa 0.

Tự thử

Cần bao nhiêu chuyển một bước để kiểm tra mọi count 0~15 và tổ hợp reset, enable? Chỉ kiểm tra này có tự chứng minh toàn bộ yêu cầu chuỗi dài không?

Đọc giải thích

Có $16\times2\times2=64$ trường hợp. Nếu count biểu diễn đầy đủ trạng thái như thiết kế này và đặc tả trạng thái sau/đầu ra chính xác, kiểm tra một bước cho bằng chứng mạnh. Nhưng không chứng minh yêu cầu bị bỏ sót như khởi tạo, giả thiết đầu vào, trạng thái riêng của pulse hoặc thời gian thực.

Tại count=9, lấy mẫu reset=1 và enable=1 cùng lúc. count sau và pulse nào đúng đặc tả reset ưu tiên?

Chọn đáp áncount=0, pulse kết thúc=1: xử lý như quay bình thường.count=10, pulse kết thúc=0: enable ưu tiên.count=0, pulse kết thúc=0: reset khởi tạo trạng thái và pulse.