diff options
| author | James Pollard <james@pollard.dev> | 2020-06-28 22:22:17 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-28 22:22:17 +0100 |
| commit | 2f71ed762e496545699ba804e29c573aa2e0b947 (patch) | |
| tree | c2f6f2b8f7ca5b51df78ddd1c4d82ccd5b4bdf0b /src/verilog | |
| parent | b988e11ff068e6c27a5252ed39113ca2bebf35e8 (diff) | |
| download | vericert-2f71ed762e496545699ba804e29c573aa2e0b947.tar.gz vericert-2f71ed762e496545699ba804e29c573aa2e0b947.zip | |
Finish store proof modulo:
* EXPR_OK proofs (Yann).
* Trivial register size proof (i.e. register values < 2^32).
* Read bounds (to be extracted from RTL semantics).
* Stack frame proof issues.
Diffstat (limited to 'src/verilog')
0 files changed, 0 insertions, 0 deletions