aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Fix equivalence checkingYann Herklotz2021-10-012-5/+2
| | | | Do not compare memories in standard operations
* Add printers for expressions and RTLParYann Herklotz2021-10-012-0/+114
|
* Fix compilation of new intermediate languagesYann Herklotz2021-10-014-7/+12
|
* Improve equivalence checking using SATYann Herklotz2021-10-011-15/+22
|
* Fix scheduler for operation chainingYann Herklotz2021-10-011-8/+22
|
* Make all OCaml files compileYann Herklotz2021-09-292-4/+4
| | | | Reverted commit to get back the scheduling and pretty printing files.
* Revert "Remove more OCaml files to compile successfully without admits."Yann Herklotz2021-09-274-0/+1084
| | | | This reverts commit 9a4122dba9bdc33a8e912d5a45bae35e05afb229.
* Add dependencies for Alectryon documentationYann Herklotz2021-09-272-6/+6
| | | | Update README on the status of Vericert
* Compile HTLPargen againYann Herklotz2021-09-242-6/+5
|
* Fix scopingYann Herklotz2021-09-241-12/+10
|
* Add back top-level functionsYann Herklotz2021-09-241-40/+157
|
* RTLpargen passes compilation againYann Herklotz2021-09-222-10/+18
|
* Fix the comparison of predicated expressionsYann Herklotz2021-09-221-138/+174
|
* Change Inductive to recordYann Herklotz2021-09-223-18/+17
|
* Start adding hashing to RTLPargenYann Herklotz2021-09-202-7/+51
|
* Merge branch 'master' into developYann Herklotz2021-09-1812-1109/+71
|\
| * Merge remote-tracking branch 'origin/master'Yann Herklotz2021-09-171-0/+19
| |\
| | * Move license to the SoftwarePipelining directoryYann Herklotz2021-09-151-0/+19
| | |
| * | Fix compilation with new CompCert versionYann Herklotz2021-09-171-8/+8
| |/
| * Fix proofs for SATYann Herklotz2021-08-121-6/+27
| |
| * Fix pretty printing issue in VerilogYann Herklotz2021-08-121-1/+1
| |
| * Remove more OCaml files to compile successfully without admits.Yann Herklotz2021-07-114-1084/+0
| |
| * Remove unnecessary files and proofsYann Herklotz2021-07-116-15/+18
| |
| * Add legup scriptYann Herklotz2021-07-111-1/+1
| |
| * Add docker file and some commentsYann Herklotz2021-07-091-0/+2
| |
* | Add predicate semantics to abstractdev/ioYann Herklotz2021-05-261-69/+296
| |
* | Add predicate semantics to RTLParYann Herklotz2021-05-261-7/+8
| |
* | Add predicate semantics to RTLBlockYann Herklotz2021-05-261-7/+8
| |
* | Fix if-conversion pass with positivesYann Herklotz2021-05-261-1/+1
| |
* | Change naturals to positive in predicatesYann Herklotz2021-05-262-45/+79
| |
* | Add very top-level proofYann Herklotz2021-05-231-0/+33
| |
* | Fix admitted in last theoremYann Herklotz2021-05-211-3/+8
| |
* | Finish top-level of proofYann Herklotz2021-05-212-22/+23
| |
* | Minimise the proof a bitYann Herklotz2021-05-161-18/+12
| |
* | Finish up step_cf_instr_correct againYann Herklotz2021-05-162-19/+43
| |
* | Fix the top-level proofs with new state_matchYann Herklotz2021-05-152-27/+164
| |
* | Finish abstract interpretationYann Herklotz2021-05-121-75/+199
| |
* | Fix admitted in first proof of sem. preservationYann Herklotz2021-05-101-19/+68
| |
* | Finish correctness of semantics wrt. RTBlockYann Herklotz2021-05-061-84/+327
| |
* | Add admitted proof of translations in RTLPargenYann Herklotz2021-05-031-27/+177
|/
* Clean up Memorygen fileYann Herklotz2021-04-071-219/+1
|
* Remove Admitted in the highest of top-levelsv1.2.0Yann Herklotz2021-04-071-5/+10
|
* No admitted theorems in Memorygen proof (~‾▿‾)~Yann Herklotz2021-04-071-76/+99
|
* Basically done with proofYann Herklotz2021-04-076-18/+62
|
* Let everything compile againYann Herklotz2021-04-061-7/+18
|
* Finish load and store proof, but broke top-levelYann Herklotz2021-04-067-289/+317
|
* Finish Veriloggenproof completelyYann Herklotz2021-04-044-57/+339
|
* Prove all admit in load but oneYann Herklotz2021-04-041-162/+183
|
* Finish most of load proofYann Herklotz2021-04-041-21/+167
|
* Finish store proof without admitYann Herklotz2021-04-042-189/+533
|
generated by cgit (git 2.34.1) at 2024-06-26 17:25:37 +0000