Báo cáo khoa học: "VỀ TÍNH DỪNG CỦA MẠCH KHÔNG ĐỒNG BỘ"

Chia sẻ: Nguyễn Phương Hà Linh Linh | Ngày: | Loại File: PDF | Số trang:6

Thêm vào BST

Báo xấu

44
lượt xem 3
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

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.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Báo cáo khoa học: "VỀ TÍNH DỪNG CỦA MẠCH KHÔNG ĐỒNG BỘ"

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 CNTT- CB 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]). 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 CNTT-CB không là đầu vào của P, thì ta luôn có 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: X; X = (X = C•X + D•Z); (X = C•X + D•Z) o = (X = C•(C•X + D•Z) + D•Z = (X = C•X + C•D•Z + D•Z) = (X = C•X + D•Z) =X Y; Y = (Y = C•X + Y•Z); (Y = C•X + Y•Z) o = (Y = C•X + (C•X + Y•Z)•Z = (Y = C•X + C•X•Z + Y•Z) = (Y = C•X + Y•Z) =Y CNTT- Z; Z = (Z = C•X + D•Z + C’); (Z = C•X + D•Z + C’) o CB = (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 X; Z = (X = C•X + D•Z); (Z = C•X + D•Z + C’) o = ((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’) Z; X = (Z = C•X + D•Z + C’); (X = C•X + D•Z) o = ((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)).
Tuy nhiên, trong ví dụ này dễ dàng thấy: X;Z;X = Z;X;Z = Z;X Ở đây, ta nhận thấy các đầu ra của Y không tham gia vào các đầu vào của Z và X. Đồng thời, X và Z tác động lẫn nhau và tham gia vào đầu vào của Y. Ở đây Y không phải là mạch không có bộ nhớ, vì Y có thông tin quay vòng. Tuy nhiên, vì C·(C·X + D·Z + D·C’) + (C·X + Y·Z)·(C·X + D·Z + C’) = C·(C·X + D·Z + D·C’) + C·X + C·X·D·Z + Y·Z·C·X +Y·D·Z +Y·Z·C’ = C·(C·X + D·Z + D·C’) + Y·C·X +Y·D·Z + Y·Z·C’ = C·(C·X + D·Z + D·C’) + Y·C·X +Y·D·Z + Y·Z·C’ = C·(C·X + D·Z + D·C’) + Y·(C·X +D·Z + Z·C’) Do đó, với Z =1 ở trạng thái xuất phát thì ta có Y; Z; X;Y = Z; X;Y Có hai trường hợp trạng thái ổn định ban đầu với Z = 0 là (C, D, X, Y, Z) = (1, 1, 0, 0, 0) và (C, D, X, Y, Z) = (1, 0, 0, 0, 0), ở đây X=0, Y=0, Z=0 và C=1. Dễ dàng thấy ở trạng thái ổn định (1, 1, 0, 0, 0) nếu thay đổi C=1 thành C=0, thì Y không thay đổi với X=1, Z=1, do đó hội tụ về trạng thái (0, 1, 1, 0, 1); ở trạng thái ổn định (1, 0, 0, 0, 0) nếu thay đổi D=0 thành D=1, thì X, Y, Z không thay đổi, do đó hội tụ về trạng thái (1, 1, 0, 0, 0); ở trạng thái ổn định (1, 0, 0, 0, 0) nếu thay đổi C=1 thành C=0, D=0 thành D=1, thì Y không thay đổi, X=1, Z = 1,do đó hội tụ về trạng thái (0, 1, 1, 0, 1); ở trạng thái ổn định (1, 0, 0, 0, 0) nếu thay đổi C=1 thành C=0, thì X, Y không thay đổi, Z = 1,do đó hội tụ về trạng thái (0, 0, 0, 0, 1); CNTT-CB Tóm lại trong mọi trường hợp ta đều có: Comb(X#Y#Z) = Comb((X#Z)#Y) = Comb (X#Z); Comb(Y) = Comb (X;Z + Z;X); Y = Z; X; Y IV. KẾT LUẬN Như vậy bằng việc dùng chương trình tổ hợp mô phỏng các mạch không đồng bộ, chúng ta đã có thể sử dụng một số kỹ thuật suy luận chương trình phần mềm để xét các tính chất của các mạch chẳng hạn như tính chất dừng và tất định. Điều đó cho phép kiểm tra tính chất của các mạch trước khi đưa vào sản xuất. Tài liệu tham khảo [1]. Tran Van Dung and He Jifeng: A Theory of Combinational Programs, Proceedings, APSEC 2001, Macao, Computer Society Press, pp. 325-329. [2]. Tran Van Dung: "On the Stability Semantics of Combinational Programs", Proceedings, ICTAC2005, LNCS 3722, pp. 180-194♦