Loading...
Please wait, while we are loading the content...
Similar Documents
A prototype embedding of bluespec system verilog in the pvs theorem prover
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Richards, Dominic Lester, David |
| Copyright Year | 2010 |
| Description | Bluespec SystemVerilog (BSV) is a Hardware Description Language based on the guarded action model of concurrency. It has an elegant semantics, which makes it well suited for formal reasoning. To date, a number of BSV designs have been verified with hand proofs, but little work has been conducted on the application of automated reasoning. We present a prototype shallow embedding of BSV in the PVS theorem prover. Our embedding is compatible with the PVS model checker, which can automatically prove an important class of theorems, and can also be used in conjunction with the powerful proof strategies of PVS to verify a broader class of properties than can be achieved with model checking alone. |
| File Size | 783083 |
| Page Count | 10 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20100018540 |
| Archival Resource Key | ark:/13960/t8kd6w79x |
| Language | English |
| Publisher Date | 2010-04-01 |
| Access Restriction | Open |
| Subject Keyword | Mathematical And Computer Sciences (general) Embedding Hardware Description Languages Semantics Prototypes Proving Program Verification Computers Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
