FYI OpenCPI is designed around an RTL (VHDL/Verilog) language-neutral platform for FPGA and ASIC. This approach does not impede innovation to produce high-trust, provably-correct RTL codes for implementation and application in any language. We will be at a seminar tomorrow at Bluespec in Waltham, MA to discuss this. The two links at the bottom may be of interest.
-Shep Siegel, CTO www.atomicrules.com * Automated Reasoning for Bluespec SystemVerilog* Dominic Richards, The University of Manchester Automated reasoning is a hot topic in the IC industry; currently, around 10% of design errors are identified with formal methods, and this is projected to increase to 45% over the next 15 years. BSV has an elegant semantics, and supports design by refinement; these properties make particularly it well suited for formal reasoning, in stark contrast to C/SystemC or VHDL/Verilog. However, little work has been done on the application automated reasoning to BSV designs. We present our experience of verifying BSV code with the PVS theorem prover and the SAL model checker, highlighting the natural advantages that BSV offers, compared to mainstream RTL/ESL languages. We also survey more mature automated reasoning tools for other languages, showing that automated reasoning can be successfully applied to large scale systems. The material in this presentation has been published in two papers: NFM 2010: http://shemesh.larc.nasa.gov/NFM2010/papers/nfm2010_139_148.pdf DCC 2010: http://web.comlab.ox.ac.uk/dcc2010/dcc.pdf
_______________________________________________ opencpi_dev mailing list [email protected] http://lists.opencpi.org/listinfo.cgi/opencpi_dev-opencpi.org
