| ชื่อเรื่อง | : | Experiments in Automating Hardware Verification using Inductive Proof Planning |
| นักวิจัย | : | Cantu, Francisco , Bundy, Alan , Smaill, Alan , Basin, David |
| คำค้น | : | - |
| หน่วยงาน | : | Edinburgh Research Archive, United Kingdom |
| ผู้ร่วมงาน | : | - |
| ปีพิมพ์ | : | 2539 |
| อ้างอิง | : | 3-540-61937-2 , http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.8663 , http://hdl.handle.net/1842/4527 |
| ที่มา | : | - |
| ความเชี่ยวชาญ | : | - |
| ความสัมพันธ์ | : | - |
| ขอบเขตของเนื้อหา | : | - |
| บทคัดย่อ/คำอธิบาย | : | We present a new approach to automating the verification of hardware designs based on planning techniques. A database of methods is developed that combines tactics, which construct proofs, using specifications of their behaviour. Given a verification problem, a planner uses the method database to build automatically a specialised tactic to solve the given problem. User interaction is limited to specifying circuits and their properties and, in some cases, suggesting lemmas. We have implemented our work in an extension of the Clam proof planning system. We report on this and its application to verifying a variety of combinational and synchronous sequential circuits including a parameterised multiplier design and a simple computer microprocessor. |
| บรรณานุกรม | : |
Cantu, Francisco , Bundy, Alan , Smaill, Alan , Basin, David . (2539). Experiments in Automating Hardware Verification using Inductive Proof Planning.
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Cantu, Francisco , Bundy, Alan , Smaill, Alan , Basin, David . 2539. "Experiments in Automating Hardware Verification using Inductive Proof Planning".
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom . Cantu, Francisco , Bundy, Alan , Smaill, Alan , Basin, David . "Experiments in Automating Hardware Verification using Inductive Proof Planning."
กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom , 2539. Print. Cantu, Francisco , Bundy, Alan , Smaill, Alan , Basin, David . Experiments in Automating Hardware Verification using Inductive Proof Planning. กรุงเทพมหานคร : Edinburgh Research Archive, United Kingdom ; 2539.
|
