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

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...
Nội dung trích xuất từ tài liệu:
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¶ VERILOG1. 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¸cthiÕ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 < b > S | S Π ShÖ 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 ®¸nhph¸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Çnnµ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¸ctrª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−¬ngnµ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×nhnghÜ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øngphÇ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. ...