Báo cáo khoa học: "ngữ nghĩa quan hệ của các chương trình tổ hợp"

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

Thêm vào BST

Báo xấu

53
lượt xem 4
download

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

Các thao tác của các thiết bị dùng để cài đặt cho hệ thống điều khiển có thể đ-ợc mô phỏng bởi ch-ơng trình, điều đó cho phép phần cứng đ-ợc kiểm chứng bằng các công cụ phần mềm chuẩn. Trong bài báo này chúng tôi hình thức hoá ngữ nghĩa sự kiện của ngôn ngữ mô tả phần cứng d-ới dạng các quan hệ và sử dụng các quan hệ đó để chứng minh một số tính chất của các ch-ơng trình tổ hợp, mà mỗi chu trình hoạt động của nó là một vòng lặp có điều...

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: "ngữ nghĩa quan hệ của các chương trình tổ hợp"

ng÷ nghÜa quan hÖ cña c¸c ch−¬ng tr×nh tæ hîp TS. trÇn v¨n dòng Bé m«n To¸n - §H GTVT Tãm t¾t: C¸c thao t¸c cña c¸c thiÕt bÞ dïng ®Ó cμi ®Æt cho hÖ thèng ®iÒu khiÓn cã thÓ ®−îc m« pháng bëi ch−¬ng tr×nh, ®iÒu ®ã cho phÐp phÇn cøng ®−îc kiÓm chøng b»ng c¸c c«ng cô phÇn mÒm chuÈn. Trong bμi b¸o nμy chóng t«i h×nh thøc ho¸ ng÷ nghÜa sù kiÖn cña ng«n ng÷ m« t¶ phÇn cøng d−íi d¹ng c¸c quan hÖ vμ sö dông c¸c quan hÖ ®ã ®Ó chøng minh mét sè tÝnh chÊt cña c¸c ch−¬ng tr×nh tæ hîp, mμ mçi chu tr×nh ho¹t ®éng cña nã lμ mét vßng lÆp cã ®iÒu kiÖn cña mét sè c¸c phÐp g¸n song song. Summary: The actual behaviour of hardware devices available for installation of a control system can be simulated by a program, and this allows the hardware to be proved correct by standard software techniques. In this paper we formalise event semantics of Hardware Description Language in the form of relations and use relation calculus to prove properties (including termination and stability and uniqueness of final state) of combined programs, each operational cycle of which is defined as a conditional loop of non-deterministic choices among generalised parallel assignments. 2. Ng«n ng÷ m« t¶ VERILOG 1. Më ®Çu C¸c ch−¬ng tr×nh VERILOG ®−îc sinh ra bíi Ch−¬ng tr×nh VERILOG [6] ®−îc sö dông c¸c qui t¾c có ph¸p sau: réng r·i ®Ó m« h×nh cÊu tróc vµ hµnh vi cña c¸c thiÕt bÞ phÇn cøng tõ c¸c thiÕt bÞ ®¬n gi¶n ®Õn c¸c 1. Mét ch−¬ng tr×nh tuÇn tù ®−îc t¹o nªn tõ m¹ng m¸y tÝnh. Ng÷ nghÜa m« pháng ®Þnh h−íng c¸c phÐp g¸n song song víi c¸c phÐp ghÐp, cña sù kiÖn ®· ®−îc ®Ò cËp nghiªn cøu trong [3], chän cã ®iÒu kiÖn, chän kh«ng tÊt ®Þnh: tuy nhiªn khi m« t¶ ho¹t ®éng kh«ng ®ång bé cña S ::= SKIP | v ::= E | S ; S | S S | S Π S hÖ thèng gåm nhiÒu thiÕt bÞ song song, nã rÏ nh¸nh dÉn ®Õn nhiÒu kÕt qu¶ kh¸c nhau. V× vËy trong ®ã v lµ vÐc t¬ c¸c biÕn Bool, E lµ vÐc t¬ ng÷ nghÜa ®ã kh«ng hç trî viÖc kiÓm chøng c¸c c¸c biÓu thøc Bool cã cïng ®é dµi víi v . thiÕt bÞ phÇn cøng. Do ®ã cÇn ph¶i cã ph−¬ng 2. C¸c hµm tuÇn tù ®ang xem xÐt ®−îc ®¸nh ph¸p h×nh thøc ho¸ ng÷ nghÜa sù kiÖn. Bµi b¸o sè thø tù. Gi¶ sö ta cã m c¸c ch−¬ng tr×nh tuÇn nµy tæng qu¸t ho¸ ng÷ nghÜa m« pháng b»ng tù: P1, P2,..., Pm, chóng cã thÓ cã c¸c biÕn chung. c¸ch ®−a ra m« h×nh quan hÖ cho VERILOG dùa Gi¶ sö index lµ hµm dïng ®Ó ®¸nh sè thø tù c¸c trªn quan hÖ cña c¸c tr¹ng th¸i kÕt thóc. Bµi b¸o ch−¬ng tr×nh. Mäi phÐp g¸n n»m trong ch−¬ng nµy xem xÐt ba líp ch−¬ng tr×nh m« t¶ ho¹t ®éng tr×nh tuÇn tù ®Òu cã chØ sè nh− ch−¬ng tr×nh ®ã. cña c¸c m¹ch tæ hîp. 3. BiÕn Bool tÝn hiÖu ~ x ®−îc dïng ®Ó ®¸nh Hai phÇn ®Çu cña Bµi b¸o h×nh thøc ho¸ ng÷ dÊu sù thay ®æi cña biÕn Bool x trong qu¸ tr×nh nghÜa sù kiÖn cña VERILOG. PhÇn sau cïng thùc hiÖn. NÕu biÕn Bool x thay ®æi, th× g¸n ~ x lµ dµnh cho viÖc nghiªn cøu c¸c ch−¬ng tr×nh tæ ttm (trong ®ã tt lµ h»ng ®óng, ff lµ h»ng sai). hîp.
Ch−¬ng tr×nh cã sè thø tù i ®−îc liªn kÕt víi thµnh Hµnh vi cña mét ch−¬ng tr×nh phÇn cøng phÇn thø i cña biÕn tÝn hiÖu (~x)[i]. ®−îc m« t¶ bëi mét d·y v« h¹n c¸c b−íc m« pháng sau 4. §iÒu khiÓn sù kiÖn g(S) ghi nhËn sù thay ®æi cña c¸c biÕn trong ch−¬ng tr×nh S ®−îc ®Þnh 1. T¹i thêi ®iÓm ban ®Çu cña mçi b−íc m« nghÜa nh− sau: pháng cho ®Çu vµo mét gi¸ trÞ x¸c ®Þnh. Gi¸ trÞ míi cña ®Çu vµo cã thÓ kÝch ho¹t mét sè c¸c ®iÒu • Gi¶ sö S lµ phÐp g¸n v := E cã sè thø tù i. khiÓn sù kiÖn. C¸c nh¸nh t−¬ng øng sÏ ®−îc kÝch NÕu x1, x2,..., xk lµ tÊt c¶ c¸c biÕn xuÊt hiÖn trong ho¹t vµ cã thÓ ho¹t ®éng. E , th× 2. M«i tr−êng sÏ chän kh«ng tÊt ®Þnh mét g(S) = df (~ x1)[i] ∨ (~ x2)[i] ∨...∨ (~ xk)[i] trong c¸c nh¸nh ®−îc kÝch ho¹t ®Ó thùc hiÖn. • NÕu S = P op Q, trong ®ã op ∈{ ;, ∩, }, 3. ViÖc thùc hiÖn mét nh¸nh ®−îc kÝch ho¹t th× Pi ®−îc gäi lµ mét b−íc c¬ së, nã bao gåm c¸c thao t¸c nhá sau: g(P op Q) = df g(P) ∨ g(Q) vµ • Thùc hiÖn ch−¬ng tr×nh Pi. index(P op Q) = df index(P) ∪ index (Q) • Xo¸ ®iÒu khiÓn sù kiÖn cña nh¸nh Pi ®Ó chØ nh¸nh ®ã ®· thùc hiÖn. • NÕu S = g(P) →P, th× g(S) = df g(P) vµ • TruyÒn sù thay ®æi cña c¸c biÕn t¹o nªn index(g(P) →P) = index(P) bëi sù thùc hiÖn ch−¬ng tr×nh Pi. • PhÐp ghÐp hai ch−¬ng tr×nh song song cã 4. Khi kh«ng cã nh¸nh nµo kÝch ho¹t n÷a, th× tËp index rêi nhau ®−îc ®Þnh nghÜa nh− sau: b−íc m« pháng ®ang xÐt dõng vµ chê nhËp gi¸ trÞ míi cho ®Çu vµo. NÕu lu«n lu«n cã mét nh¸nh P||Q = df (g(P) →P) Π (g(Q) →Q) ®−îc kÝch ho¹t sau mçi b−íc c¬ së th× b−íc m« PhÐp ghÐp song song cã tÝnh chÊt giao pháng ®ã kh«ng dõng. ho¸n, kÕt hîp vµ ph©n phèi víi phÐp chän kh«ng tÊt ®Þnh vµ phÐp chän cã ®iÒu kiÖn. 3. Ng÷ nghÜa quan hÖ •VERILOG ch−¬ng tr×nh cã d¹ng @ g(S) S, Hµnh vi cña mçi b−íc m« pháng cã thÓ m« ë ®ã S = P1|| P2||... || Pm vµ P1, P2,..., Pm lµ c¸c h×nh bëi mét phÐp lÆp cña mét phÐp ghÐp kh«ng ch−¬ng tr×nh tuÇn tù hoÆc c¸c ch−¬ng tr×nh tÊt ®Þnh mét sè c¸c nh¸nh song song kÕt hîp víi VERILOG cã c¸c tËp index nhau. mét sè thao t¸c phô sau mçi b−íc c¬ së nh− xãa • Ta ®Þnh nghÜa g(@ g(S) S) = df (g(S)) hoÆc ghi nhËn sù thay ®æi cña c¸c biÕn, §Þnh nghÜa 1 (Ng÷ nghÜa sù kiÖn). Gi¶ sö • Ch−¬ng tr×nh thµnh phÇn Pi ®−îc gäi lµ (@g(S) S) lµ mét ch−¬ng tr×nh VERILOG víi c¸c mét nh¸nh. NÕu sù thay ®æi cña biÕn x lµm cho biÕn v1, v2,..., vn vµ m chØ sè kh¸c nhau. Gi¶ sö g(Pi) thay ®æi gi¸ trÞ tõ ff sang tt, th× ta nãi ~ x ®· nh¸nh P cã tËp chØ sè lµ I. Ng÷ nghÜa sù kiÖn víi kÝch ho¹t ®iÒu khiÓn sù kiÖn g(Pi) vµ khi ®ã nh¸nh tËp chØ sè I ®−îc ®Þnh nghÜa nh− sau: Pi trë nªn cã thÓ ho¹t ®éng ®−îc. Bæ ®Ò 1 (g(P) →Pe,I) = df (g(I))T ; (P || DISevent(P, I) (a) g(P||Q) = g(P) ∨ g(Q) trong ®ã (b) index(P||Q) = df index(P) ∪ index (Q) 1. BiÓu thøc Bool g[I] nhËn ®−îc b»ng c¸ch thay thÕ c¸c biÕn ~ x trong g(S) víi chØ sè I b»ng (c) P||Q =(P||Q) < g(P||Q) > SKIP
thµnh phÇn thø I t−¬ng øng cña vÐc t¬ tÝn hiÖu 4. C¸c ch−¬ng tr×nh tæ hîp (~x)[i]. Trong phÇn nµy chóng ta nghiªn cøu c¸c 2. Ký hiÖu bT ký hiÖu gi¶ thiÕt SKIP T ch−¬ng tr×nh, mµ c¸c nh¸nh cña chóng lµ c¸c phÐp g¸n song song. §©y lµ líp c¸c ch−¬ng tr×nh 3. P || DIS Q biÓu diÔn phÐp ghÐp song song phÇn cøng m« t¶ ho¹t ®éng cña c¸c m¹ch tæ hîp, rêi nhau cña hai ch−¬ng tr×nh P vµ Q [5], ë ®ã trong ®ã mçi mét phÐp g¸n song song x := E chóng kh«ng cã ®Çu ra chung. biÓu diÔn mét thiÕt bÞ lÊy gi¸ trÞ E g¸n cho ®Çu 4. Ch−¬ng tr×nh event (P) ®−îc dïng ®Ó xo¸ ra cña d©y x . Ta gäi c¸c cÆp (xI, EI) lµ mét bæ c¸c ®iÒu khiÓn sù kiÖn ®· dïng khi P ®−îc thùc sung. hiÖn vµ truyÒn sù thay ®æi cña c¸c biÕn cho c¸c nh¸nh kh¸c trong ch−¬ng tr×nh. §Þnh nghÜa 3. Ch−¬ng tr×nh tæ hîp lµ mét ch−¬ng tr×nh VERILOG d¹ng @g(P) P, trong ®ã event(R,I) = df ∃ v1’,..., vn’• R ∧∀k : 1 ≤ k ≤ n • P = ( x := E ) ||... || ( z := F ) vµ kh«ng mét biÕn nµo xuÊt hiÖn nhiÒu h¬n mét lÇn ë vÕ tr¸i c¸c (~ vk’= (~vk ∧clear(I)) ∨ bool(vk ≠ vk’)m) phÐp g¸n. §Þnh nghÜa 4. (Tr¹ng th¸i æn ®Þnh). Cho Bæ ®Ò 2 ch−¬ng tr×nh tæ hîp nh− ®· ®Þnh nghÜa trong §Þnh 1. event (P Q,I) = event(P, I) nghÜa 3. Gi¶ sö VAR lµ tËp tÊt c¶ c¸c biÕn vµ event(Q, I) STATE: VAR → {0, 1} 2. event (P ΠQ,I) = event(P, I) Π event(Q, I) • Tr¹ng th¸i s ∈ STATE ®−îc gäi lµ æn ®Þnh ®èi víi Comb P nÕu víi mäi I ( s = s) = 3. event (v1,v2:= e1,e2,I) = true, trong ®ã (xI, EI) lµ mét bæ sung bÊt kú trong = event(v1:= e1,I) || DISevent(v2:= e2,I) Comb P vµ s ký hiÖu gi¸ trÞ cña biÓu thøc E 3. event (v:= e,I) = ∀k : 1≤ k ≤ n • t¹i tr¹ng th¸i s. • Hµm kiÓm tra tÝnh æn ®Þnh d(P) vµ ®iÒu (~ vk= (~vk ∧clear(I)); kiÖn æn ®Þnh c(P) cña c¸c tr¹ng th¸i cña ch−¬ng ⎛ if Δ x ≠ 1 ∧ e = 1 → ~ x :: tt m ⎞ tr×nh Comb P lµ c¸c hµm logic sau: ⎜ ⎟ ⎜ Δ x ≠ 0 ∧ e = 0 → ~ x :: tt m ⎟ ⎜ ⎟ d(P) = df( x := E ) ∧... ∧ ( z := F ) ⎜ Δ x = e → SKIP ⎟ fi ⎝ ⎠ c(P) = df(¬g[1]⇒ x := E ) ∧... ∧(¬g[m]⇒ z := F ), §Þnh nghÜa 2 (B−íc m« pháng). Gi¶ sö @ g(S) S lµ ch−¬ng tr×nh VERILOG, trong ®ã ë ®ã: g[1]= g( x := E ),..., g[m] = g( z := F ). S = P|| … || Q vµ v1, v2,..., vn lµ c¸c biÕn cña chóng. Gi¶ sö P, …, Q cã c¸c tËp chØ sè rêi nhau C¸c ch−¬ng tr×nh tæ hîp biÕn ®æi tõ tr¹ng I, …, J, t−¬ng øng. Ta ®Þnh nghÜa b−íc lÆp m« th¸i æn ®Þnh nµy sang tr¹ng th¸i æn ®Þnh kh¸c. pháng lµ b−íc lÆp sau: §Þnh lý 1. @ g(S) S = df var ~ v1,~v2,..., ~vn :=in(v1),....in(vn); c(P)T ; Comb P = c(P)T; Comb P; d(P)⊥ trong ®ã b⊥ ký hiÖu lµ kh¼ng ®Þnh SKIP ⊥ (g[I] ∨ g[J] * g[I] →Pe,I Π... Π g[J] →Qe,J) vµ ⊥ lµ ch−¬ng tr×nh ABORT. end ~ v1,~v2,..., ~vn Ta cã thÓ bæ sung viÖc kiÓm tra tÝnh æn ®Þnh trong ®ã in(vI) = ttm nÕu vI lµ ®Çu vµo mµ gi¸ trÞ vµo trong ®iÒu kiÖn cña phÐp lÆp mµ kh«ng ¶nh míi kh¸c víi gi¸ trÞ cò. h−ëng ®Õn hµnh vi cña ch−¬ng tr×nh.
§Þnh lý 2. 6. KÕt luËn c(P)T ; Comb P = c(P)T; (g(P) ∨¬ d(P)) * Pe, Bµi b¸o cung cÊp cho ng«n ng÷ m« t¶ phÇn cøng ng÷ nghÜa sù kiÖn dùa trªn m« h×nh quan trong ®ã Pe = g[1]⇒( x := E )e,1 Π... Π g[m]⇒ hÖ. Ban ®Çu c¸c ch−¬ng tr×nh tæ hîp ë tr¹ng th¸i ( z := F )e,m æn ®Þnh vµ ®−îc kÝch ho¹t bëi c¸c gi¸ trÞ míi cung cÊp cho c¸c thiÕt bÞ ®Çu vµo. C¸c nh¸nh kÝch ho¹t cña ch−¬ng tr×nh sÏ ®−îc lôa chän mét c¸ch 5. C¸c ch−¬ng tr×nh tæ hîp luü ®¼ng kh«ng tÊt ®Þnh ®Ó thùc hiÖn. Bµi b¸o chøng tá Trong môc nµy chóng ta nghiªn cøu mét líp r»ng mét ch−¬ng tr×nh phÇn cøng t−¬ng ®−¬ng c¸c ch−¬ng tr×nh con, mµ mçi phÐp g¸n cña nã víi mét phÐp lÆp cña phÐp lùa chän kh«ng tÊt lòy ®¼ng. ®Þnh cña mét sè c¸c ch−¬ng tr×nh tuÇn tù cã chung c¸c biÕn. NÕu ch−¬ng tr×nh ®−îc thiÕt kÕ §Þnh nghÜa 5. Ch−¬ng tr×nh P ®−îc gäi lµ tèt, th× chóng sÏ lu«n lu«n dõng vµ ®¹t tr¹ng th¸i lòy ®¼ng, nÕu P; P = P. kÕt thóc duy nhÊt. §èi víi mét líp c¸c ch−¬ng Bæ ®Ò 3. Mäi ch−¬ng tr×nh tæ hîp ®Òu lòy tr×nh lòy ®¼ng bµi b¸o ®−a ra thuËt to¸n h÷u hiÖu ®¼ng. xÐt tÝnh dõng cña nã. ViÖc nghiªn cøu c¸c tÝnh chÊt dõng vµ tr¹ng th¸i kÕt duy nhÊt cña mét sè §Þnh nghÜa 6. Ch−¬ng tr×nh tæ hîp ®−îc gäi líp ch−¬ng tr×nh kh¸c lµ ®Ò tµi nghiªn cøu tiÕp lµ lòy ®¼ng theo thµnh phÇn nÕu mäi nh¸nh cña theo. nã lµ lòy ®¼ng. B¾t ®Çu tõ mét tr¹ng th¸i æn ®Þnh mét ch−¬ng tr×nh tæ hîp lòy ®¼ng theo thµnh phÇn Tµi liÖu tham kh¶o gåm hai nh¸nh cã thÓ b¾t ®Çu tõ mét nh¸nh, sau ®ã thùc hiÖn nh¸nh kia vµ cø tiÕp tôc nh− vËy cho [1]. K. C. Davis. A denotational definition of the VHDL simulation Kernel. University of Cincinnati. ®Õn khi ®¹t ®−îc tr¹ng th¸i æn ®Þnh. [2]. M. Gordon. Why higher-order logic is a good §Þnh lý 3. NÕu P = Q || R vµ Q, R lµ hai formalsm for specifying and verifying hardware. ch−¬ng tr×nh lòy ®¼ng, th× Formal Aspect of VLSI Design, 153-177, (1986). c(P)T ; Comb P; end ~ x , ~ z = c(P)T; [3]. M. Gordon. Event and Cycle Semantics of Hardware Description Languages. University of Comb(Q;R Π R;Q);end ~ x , ~ z Cambridge Computer Laboratory, (1998). §Þnh nghÜa 7. Ch−¬ng tr×nh P ®−îc gäi lµ [4]. C. Delgado Kloos and P. T. Breuer. Formal kh«ng më réng, nÕu Pk+1 = Pk, trong ®ã Semantics for VHDL. Kluwer Academic Publisher, (1995). Xn+1= df(X;Xn) vµ X1= df X. [5]. C. A. R. Hoare and He Jifeng. Unifying Theory of Khi chu tr×nh m« pháng cña ch−¬ng tr×nh tæ Programing. Prentice – Hall, (1998). hîp kÕt thóc, tr¹ng th¸i cña nã th−êng kh«ng [6]. Open VERILOG International. VERILOG Hardware ®−îc x¸c ®Þnh mét c¸ch duy nhÊt. §èi víi ch−¬ng Description Language Reference Manual, Version tr×nh lòy ®¼ng cã thÓ dÔ dµng kiÓm tra tÝnh dõng 1.0. vµ tÝnh duy nhÊt cña tr¹ng th¸i kÕt. [7]. D. E. Thomas and P. R. Mooby. The VERILOG §Þnh lý 4. NÕu P = Q || R vµ Q, R lµ hai Hardware Description Language. Kluwer Academic Publishers, (1995) ch−¬ng tr×nh lòy ®¼ng, sao cho P;Q vµ Q;R lµ hai ch−¬ng tr×nh kh«ng më réng, th× khi ®ã Comb P [8]. Tran Van Dung and He JiFeng. A Theory of lu«n lu«n dõng khi xuÊt ph¸t tõ tr¹ng th¸i ban ®Çu Combinational Programs. UNU/IIST Report No tháa m·n ®iÒu kiÖn c(P). 162