VỀ TÍNH DỪNG CỦA MẠCH KHÔNG ĐỒNG BỘ
TS. TRẦN VĂN DŨNG
Bộ môn Khoa học máy tính
Khoa Công nghệ thông tin
Trường Đại học Giao thông Vận tải
Tóm tắt: Bài báo sử dụng ngữ nghĩa quan hệ của chương trình tổ hợp [1, 2] để mô
phỏng và chứng minh tính dừng của các mạch không đồng bộ có một số tính chất xác định.
Điều đó cho phép dùng các kỹ thuật phần mềm chuẩn để kiểm chứng các hành vi của các
mạch tổ hợp.
Summary: This paper using relational semantics of combinational programs [1,2] to
simulate and prove a termination of some sequential circuits with determined properties. It
allows to use standard software verification techniques to verify behaviours of some kinds of
sequential circuits.
I. MỞ ĐẦU
Mục đích của bài báo nhằm đưa ra phương pháp hình thức để nghiên cứu một số tính chất
quan trọng của các mạch không đồng bộ, tức là mạch xử lý thông tin mà ngoài đầu vào và đầu
ra có thể cho phép quay vòng một số thông tin bên trong mạch. Các mạch không tuần tự là cơ sở
phần cứng cho các mô hình máy tính, chính vì vậy việc tìm hiểu và suy luận về các hành vi của
mạch có ý nghĩa quan trọng và thu hút sự quan tâm nghiên cứu của nhiều tác giả (xem [1,2]).
CNTT-
CB
Trong bài này ta xét mạch tuần tự không đồng bộ theo trình tự các bước như sau:
* Bổ sung biến delay vào các vị trị cần thiết
* Biểu diễn các biến bổ sung thông qua đầu vào, đầu ra và thông tin quay vòng
* Tìm mối liên hệ giữa các biến xem có thoả mãn các điều kiện cần thiết không
* Xét mạch có cho kết quả về hành vi duy nhất không.
Ở đây ta xét chế độ thao tác cơ bản mở rộng theo nghĩa sau: các tín hiệu vào có thể đồng bộ
thay đổi, nhưng sau đó mọi tín hiệu vào đều chờ đợi cho đến khi mạch đạt đến trạng thái cân
bằng tiếp theo.
Khi ghép nối các mạch, nếu các mạch thành phần là lũy đẳng (tức là nếu thực hiện thêm
một lần thứ hai thì không đem lại kết quả gì mới) hoặc bản thân nó là mạch tổ hợp, thì nguyên
tắc hoạt động trên được đảm bảo.
II. MÔ PHỎNG MẠCH KHÔNG ĐỒNG BỘ
Bây giờ chúng ta xét các mạch không đồng bộ, đó là các mạch có phản hồi nhưng không có
đồng hồ đồng bộ. Ở đây các tín hiệu đầu vào có thể thay đổi, sau đó chờ cho mạch hoạt động
cho đến khi mọi giá trị đầu ra và thông tin quay vòng không thay đổi, nữa, đến lúc đó giá trị đầu
vào mới lại có thể thay đổi.
Trong [1, 2] chúng ta đã đưa ra định nghĩa chương trình tổ hợp Comb để mô phỏng hoạt
động của mạch không đồng bộ. Trong mạch có thể có nhiều luồng thành phần, chúng thay nhau
thực hiện một cách tùy ý, cho đến khi mọi việc thực hiện sẽ không đem lại kết quả mới nữa. Lúc
đó ta nói mạch ở trạng thái ổn định và dừng.
Chúng ta mong muốn tìm hiểu các điều kiện ràng buộc đối với các mạch mà kết quả cuối
cùng khi thực hiện chúng là tất định, không phụ thuộc vào thứ tự thực hiện của các luồng.
Ví dụ 1: Cho mạch không đồng bộ sau
* Đầu vào S, R
* Đầu ra Q. Vì Q có feedback, nên coi Q là biến trung gian (delay)
* Biến trung gian delay tác động bên trong X
* Vậy ta có hai mạch sau:
Q = X’ · R’ (1)
X = S’ · Q’ (2)
CNTT-CB
Ở đây để đơn giản ký hiệu A’ là phủ định của A và · là phép hội logic hai mệnh đề. Mạch
không đồng bộ được xem như chương trình tổ hợp (xem [1,2]):
Comb (Q # X)
Điều đó cho ta biết, hai phép gán (1) và (2) thay nhau thực hiện cho đến khi giá trị của hai
vế các phương trình đó đồng nhất.
Dễ dàng kiểm chứng thấy các trạng thái ổn định (R, S, X, Q) của chương trình tổ hợp trên
bao gồm các trạng thái sau:
(0, 0, 0, 1); (0, 0, 1, 0); (0, 1, 0, 1); (1, 0, 1, 0); (1, 1, 0, 0).
* Xét trạng thái (0, 0, 0, 1) với R = 0, S = 0, X = 0, Q = 1:
Giả sử R tăng giá trị lên 1, khi đó nó kích hoạt Q:
+ Q = X’ · R’ = 1 · 0 = 0. Q thay đổi kích hoạt X.
+ X = S’ · Q’ = 1 · 1 = 1. X thay đổi kích hoạt Q.
+ Q = X’ · R’ = 0 · 0 = 0. Q không thay đổi.
+ Dừng do không có biến nào thay đổi. Trạng thái ổn định đạt được (1, 0, 1, 0).
Giả sử S tăng giá trị lên 1, khi đó nó kích hoạt X:
+ X = S’ · Q’ = 0 · 0 = 0. X không thay đổi.
+ Dừng do không có biến nào thay đổi, vẫn ở trạng thái ổn định (0, 1, 0, 1).
Giả sử S và R cùng tăng giá trị lên 1, khi đó nó kích hoạt đồng thời Q và X:
• Giả sử Q thực hiện trước:
+ Q = X’ · R’ = 1 · 0 = 0. Q thay đổi kích hoạt X.
+ X = S’ · Q’ = 0 · 1 = 0. X không thay đổi.
Dừng do không có biến nào thay đổi. Trạng thái ổn định đạt được (1, 1, 0, 0).
• Giả sử X thực hiện trước:
+ X = S’ · Q’ = 0 · 0 = 0. X không thay đổi.
+ Q = X’ · R’ = 1 · 0 = 0. Q thay đổi kích hoạt X.
+ X = S’ · Q’ = 0 · 1 = 0. X không thay đổi.
+ Dừng do không có biến nào thay đổi. Trạng thái ổn định đạt được (1, 1, 0, 0).
+ Ta nhận thấy Q và X là hai chương trình lũy đẳng, vì vế phải (1) và (2) không có
feedback trong mỗi một chương trình tổ hợp đó.
+ Sau đây ; là phép ghép hai chương trình. Xét các phép ghép sau:
Q; X; Q = (Q = X’ · R’); (X = S’ · Q’); (Q = X’ · R’) =
= (X = S’ · (X’ · R’)’); (Q = X’ · R’) =
= (X = (S’· X + S’· R); (Q = R’· (S +X’· R’)) =
= ((X, Q) = (S’· X + S’· R, R’· S + R’· X’)) (3)
X; Q; X = (X = S’ · Q’); (Q = X’ · R’); (X = S’ · Q’) =
= (Q = (S + Q) · R’); (X = S’ · Q’) =
= (Q = (S · R’ + Q · R’); (X = S’ · ((S’ + R) · (Q’ + R) =
= ((Q, X) = (S · R’ + Q · R’, S’ · ((S’· Q’) + R)) =
CNTT-
CB
= ((Q, X) = (S · R’ + Q · R’, S’·Q’ + S’· R)
= ((X, Q) = (S’·Q’ + S’· R, S · R’ + Q · R’)) (4)
Từ (3) và (4) dễ dàng thấy nếu X = Q’, thì hai biểu thức trên là như nhau. Như vậy chỉ có
trạng thái ổn định (1, 1, 0, 0) với X = Q = 0 là không thoả mãn điều kiện X = Q’, nhưng trong
truờng hợp này R’ = S’ = 0, do đó hai biểu thức vẫn trùng nhau Q; X; Q = X; Q; X.
Do đó chương trình tổ hợp trên là tất định và nếu các chương trình luôn bắt đầu từ các
trạng thái ổn định, thì
Comb (Q # X) = ((X, Q) = (S’·X + S’· R, R’· S + R’·X’)) hoặc
Comb (Q # X) = ((X, Q) = (S’·Q’ + S’· R, S · R’ + Q · R’))
III. MỘT SỐ KẾT QUẢ VỀ TÍNH DỪNG
Ta có thể phát biểu và chứng minh Định lý sau, xem [1,2]:
Định lý 1: Nếu P và Q là hai chương trình lũy đẳng và
C┬; P; Q; P; Q = C┬;Q; P; Q; P; C┴ thì
C┬; Comb (P#Q) = C┬; P; Q; P; Q; C┴
trong đó C┬ = if C then skip else stop và C┴ = if C then skip else chao, với C là điều kiện
ổn định của trạng thái xuất phát và skip, stop, chao tương ứng là các chương trình bỏ qua, dừng
và có hành vi tùy ý.
Chứng minh:
C┬; Comb (P#Q) = C┬; Comb (P;Q + Q;P)
= C┬; C┴; (P;Q + Q;P)*
= C┬; (P;Q Π + Q;P); (P;Q + Q;P); (P;Q + Q;P); (P;Q + Q;P)*
= C┬; (P; Q; P; Q + Q;P;Q;P); C┴; (P;Q + Q;P)*
= C┬; (P;Q;P;Q); C┴; (P;Q + Q;P)*; C┴
= C┬; P; Q; P; Q; C┴
Định lý trên nói lên nếu xuất phát từ trạng thái ổn định, chương trình không đồng bộ sẽ
dừng ở trạng thái ổn định sau khi thực hiện lặp lần lượt hai chương trình thành phần.
Từ Định lý 1 ta thấy trong trường hợp P, Q lũy đẳng và P; Q = Q; P thì kéo theo: Q; P; Q;
P; Q = Q; P; Q; P = P; Q = Q; P. Do đó ta có
Hệ quả 2. Giả sử P, Q là hai chương trình lũy đẳng và P; Q = Q; P. Khi đó
Comb (P#Q) = P; Q
Định lý 3. Giả sử đầu ra của Q không tham gia vào đầu vào của P và Q là mạch không có
bộ nhớ. Khi đó
Comb (P#Q) = Comb P; Comb Q
Chứng minh. Thực vậy, trong trường hợp Q là mạch không bộ nhớ và mọi đầu ra của Q
không là đầu vào của P, thì ta luôn có CNTT-CB
Q j; P i; Q k = P i; Q j+k
Ví dụ 2. Cho mạch không đồng bộ sau:
Ta xét bổ sung ba biến trạng thái trong X, Y, Z với delay thời gian không xác định. Ở đây
ta coi X, Y, Z là các luồng thành phần.
Như vậy mỗi bộ giá trị của các biến (C, D, X, Y, Z) sẽ xác định một trạng thái của chương
trình. Ta có thể coi mạch trên là kết nối song song của ba mạch thành phần như sau:
• X = C·X + D·Z
• Y = C·X + Y·Z
• Z = C·X + D·Z + C’
• Gọi S = Comb (X#Y#Z)
• Dễ dàng thấy các trạng thái ổn định của S là:
(1, 1, 0, 0, 0) ; (1, 0, 0, 0, 0); (0, 0, 0, 0, 1); (0, 0, 0, 1, 1);
(0, 1, 1, 0, 1); (0, 1, 1, 1, 1); (1, 1, 1, 1, 1); (1, 0, 1, 1, 1)
• Dùng cách lập luận trên chương trình tổ hợp ta chứng minh một số tính chất của
mạch đã cho. Trước hết ta chứng tỏ rằng X, Y, Z là 3 chương trình lũy đẳng:
o X; X = (X = C•X + D•Z); (X = C•X + D•Z)
= (X = C•(C•X + D•Z) + D•Z
= (X = C•X + C•D•Z + D•Z)
= (X = C•X + D•Z)
= X
o Y; Y = (Y = C•X + Y•Z); (Y = C•X + Y•Z)
= (Y = C•X + (C•X + Y•Z)•Z
= (Y = C•X + C•X•Z + Y•Z)
= (Y = C•X + Y•Z)
= Y
CNTT-
CB o Z; Z = (Z = C•X + D•Z + C’); (Z = C•X + D•Z + C’)
= (Z = C•X + D•(C•X + D•Z + C’) + C’
= (Z = C•X + D•C•X + D•Z + D•C’ + C’)
= (Z = C•X + D•Z + C’)
= Z
o X; Z = (X = C•X + D•Z); (Z = C•X + D•Z + C’)
= ((X, Z) = (C•X + D•Z, C•(C•X + D•Z) + D•Z + C’)
= ((X, Z) = (C•X + D•Z, C•X +C•D•Z + D•Z + C’)
= ((X, Z) = (C•X + D•Z, C•X + D•Z + C’)
o Z; X = (Z = C•X + D•Z + C’); (X = C•X + D•Z)
= ((Z, X) = (C•X + D•Z + C’, C•X + D•(C•X + D•Z + C’))
= ((Z, X) = (C•X + D•Z + C’, C•X + D•C•X + D•Z + D•C’))
= ((Z, X) = (C•X + D•Z + C’, C•X + D•Z + D•C’))
= ((X, Z) = (C•X + D•Z + D•C’, C•X + D•Z + C’)
Z; X = X; Z trừ trường hợp (C, D, X, Z) = (0, 1, 0, 0), vì khi đó
X;Z = ((X,Z) = (0,1)), còn Z;X = ((X,Z) = (1,1)).
