aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Fix pretty printing bug in VerilogYann Herklotz2020-11-091-2/+2
|
* Fix printing of negative numbersYann Herklotz2020-11-091-1/+5
|
* Add html generation and clean Coq filesYann Herklotz2020-08-134-7/+3
|
* Finished all the proofsv1.0.0Yann Herklotz2020-08-133-39/+46
| | | | Removed support for case statements temporarily.
* Remove unnecessary commented proofYann Herklotz2020-08-121-23/+0
|
* Finish proof of conditionalsYann Herklotz2020-08-121-4/+11
|
* Nearly finished all proofsYann Herklotz2020-08-121-48/+228
|
* Remove alignment constraint during translation.James Pollard2020-08-112-67/+69
| | | | This is now inferred from the memory model.
* Remove last admits from istoreYann Herklotz2020-08-041-2/+3
|
* Finish istore and iload without any admitsYann Herklotz2020-08-042-119/+115
|
* No admitted in iload proofYann Herklotz2020-08-041-38/+72
|
* Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-08-041-5/+6
|\
| * Fix broken proof.James Pollard2020-08-041-5/+6
| |
* | Add expr_ok proofYann Herklotz2020-08-041-11/+25
|/
* Fix first part of istoreYann Herklotz2020-08-041-40/+43
|
* Fix iload proofYann Herklotz2020-08-042-43/+52
|
* Add proof of divisibilityYann Herklotz2020-08-041-21/+14
|
* Remove check mpassYann Herklotz2020-07-241-2/+0
|
* More renames to get it to compileYann Herklotz2020-07-244-6/+9
|
* Rename to VericertlibYann Herklotz2020-07-171-0/+0
|
* Change name to VericertYann Herklotz2020-07-1423-53/+52
|
* Fixes to operatorsYann Herklotz2020-07-074-6/+12
|
* Finished transl_condYann Herklotz2020-07-072-62/+45
|
* Only translate_cond leftYann Herklotz2020-07-074-17/+252
|
* No admitted in Deterministic proofYann Herklotz2020-07-073-14/+10
|
* A few operations leftYann Herklotz2020-07-071-30/+88
|
* Proof of TransfHTLLink DONEYann Herklotz2020-07-071-1/+14
|
* Rename asm to verilogYann Herklotz2020-07-061-9/+10
|
* Add top level backward simulationYann Herklotz2020-07-063-95/+191
|
* HTLgenproof compiles againYann Herklotz2020-07-064-22/+47
| | | | - Commented out Iload, Istore proofs for now
* Fix InopYann Herklotz2020-07-054-47/+58
|
* Fix HTLgenspecYann Herklotz2020-07-051-3/+4
|
* No addmitted in VeriloggenproofYann Herklotz2020-07-054-100/+245
| | | | However, there may have been breaking changes to HTLgenproof.
* Remove admitted in mis_stepp_VdeclYann Herklotz2020-07-053-9/+12
|
* Finish most of VeriloggenproofYann Herklotz2020-07-055-31/+205
|
* Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-07-042-12/+175
|\
| * Working on determinacy proof.James Pollard2020-07-042-12/+175
| |
* | Define ofbytesYann Herklotz2020-07-041-1/+72
| |
* | Make HTLgen compile againYann Herklotz2020-07-041-3/+11
|/
* Fixing HTLgenproofYann Herklotz2020-07-036-41/+67
|
* Add new value type to fix Iop proofYann Herklotz2020-07-035-67/+217
|
* Addition to int_add_v2Yann Herklotz2020-07-031-3/+13
|
* Updates to Iop proofYann Herklotz2020-07-033-92/+179
|
* Switch to uvalueToZ in lessdef.James Pollard2020-07-024-67/+87
|
* Complete ZToValue_valueToNat.James Pollard2020-07-022-31/+34
|
* Fix callstate proof.James Pollard2020-07-021-7/+7
|
* Stuck in Callstate proofYann Herklotz2020-07-021-20/+17
|
* Push current stateYann Herklotz2020-07-022-26/+46
|
* Remove all <> AdmittedYann Herklotz2020-07-022-23/+27
|
* Fix spec by adding details about reg valsYann Herklotz2020-07-022-36/+182
|
generated by cgit (git 2.34.1) at 2024-07-03 13:15:52 +0000