Comments (4)
Hi, I'd be interested in picking this issue up. I've been looking around for how to do this and it seems pono has a few APIs:
- C++: seems least desirable as I reckon C++ interop will be painful.
- Python: The API seems nice and could potentially be interacted with using scalapy.
- BTOR2: Potentially the easiest way of integrating the engine as chiseltest seems to already be able to emit
.btor2
s.
I don't think pono uses an smt-lib interface as the other engines in chiseltest do. So, given these options, I'm leaning towards using the python API but do let me know if you disagree! The formal verification world is certainly a new thing to me!
Let me know if I'm leaving out anything! I'm super keen to help :^).
from chiseltest.
From what I've seen so far, the API can only describe safety properties (please correct if I'm wrong), so it seems like at least implementing k-induction isn't that far away from what's currently there for BMC.
k-induction would totally be doable to implement. We could also try to interface with model checkers that implement PDR (like pono). However, currently no one is working on this.
from chiseltest.
Thanks for the info!
from chiseltest.
- BTOR2: Potentially the easiest way of integrating the engine as chiseltest seems to already be able to emit
.btor2
s.
That would be the way to go.
I don't think pono uses an smt-lib interface as the other engines in chiseltest do.
There is one engine, btormc
which already consumes btor
for BMC.
As a first step I would recommend that you try adding pono
as a BMC backend. You can look at the code for btormc
as a template. There will probably be some peculiarities about pono that you will have to add some code for. Then you could make a PR with your changes and after that you could investigate how to use pono
in "proof-mode" instead of only doing BMC.
from chiseltest.
Related Issues (20)
- JRE detects `EXCEPTION_ACCESS_VIOLATION` when trying to use Verilator as Chiseltest's backend HOT 2
- Report assert message with `FailedBoundedCheckException` HOT 1
- Generate waveform file in real-time HOT 1
- chiseltest gets the signal name wrong when trying to peek, poke, or expect an OpaqueType HOT 3
- Solver Chosen Constants for Formal Verification HOT 3
- scala.NotImplementedError: TODO: convert ThrowOnFirstErrorAnnotation HOT 3
- Bundle literal construction outside test() is not allowed in Chiseltest 5.0.0 (works in 0.5.4) HOT 2
- assertion failed: The Chisel compiler plugin is now required for compiling Chisel code HOT 1
- The waveform doesn't reflect changes in the input port until io.clock.peek HOT 1
- scala.NotImplementedError: TODO: convert DecodeTableAnnotatio HOT 7
- Will there be a chiseltest 6.0.0? HOT 16
- Frequent crash on macOS with the threaded Verilator backend HOT 6
- AXI4RAM test failed on chiseltest 5.0.2 HOT 2
- Cant ```import chiseltest._``` HOT 1
- Bitwuzla has changed it's command line argument format HOT 1
- [WARNING] Unsupported annotation: SRAMAnnotation
- [Help]A TLRAM test failed log HOT 8
- What are the future use cases of ChiselTest if it is replaced by ChiselSim? HOT 4
- Who is the copyright holder of chiseltest and what is the license? HOT 1
- one step takes extremely long time to complete HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from chiseltest.