aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
...
| * Add proof of translation correctnessYann Herklotz2020-05-202-17/+200
| | | | | | | | Modified-by: Yann Herklotz <git@yannherklotz.com>
| * Fix the semantics to properly evaluate the stateYann Herklotz2020-05-201-2/+4
| |
| * Switch position of empty ruleYann Herklotz2020-05-201-4/+4
| |
| * Fix definitions in Value and add lemmasYann Herklotz2020-05-201-7/+35
| |
| * Add theorems about mergeYann Herklotz2020-05-201-2/+12
| |
| * Add simulation diagramYann Herklotz2020-05-081-5/+53
| |
| * Add lessdef for valuesYann Herklotz2020-05-081-3/+10
| |
| * Add AssocMapYann Herklotz2020-05-084-47/+93
| |
| * Add match_states InductiveYann Herklotz2020-05-071-0/+29
| |
| * Remove HTLgen and create the specificationYann Herklotz2020-05-072-163/+92
| |
| * Redefine HTL for intermediate Verilog languageYann Herklotz2020-05-072-76/+87
| |
| * Use associations instead of stateYann Herklotz2020-05-072-70/+69
| |
| * Rename assoclist to assocsetYann Herklotz2020-05-072-28/+28
| |
| * Remove Admitted Maps LemmaYann Herklotz2020-05-071-6/+0
| |
| * Add changes to valueYann Herklotz2020-05-061-2/+9
| |
| * Refine test fileYann Herklotz2020-05-051-5/+2
| |
| * Minimised manual simulationYann Herklotz2020-05-052-45/+14
| |
| * Simplifications to proofYann Herklotz2020-05-053-18/+15
| |
| * Finish manual simulationYann Herklotz2020-05-052-5/+68
| |
| * Add equality check for valueYann Herklotz2020-05-047-21/+27
| |
| * Refine the semanticsYann Herklotz2020-05-043-56/+130
| |
| * Add code to debug execution of HLSYann Herklotz2020-05-031-0/+73
| |
| * Add proofs and specification of Verilog conversionYann Herklotz2020-05-032-0/+158
| |
| * Add state transition conversion functionsYann Herklotz2020-05-031-2/+14
| |
| * Add hex notation to valuesYann Herklotz2020-05-031-0/+9
| |
| * Change to StateYann Herklotz2020-05-031-21/+22
| |
| * Add documentation and conform to specificationYann Herklotz2020-04-291-24/+41
| |
| * Add CompCert semantics for VerilogYann Herklotz2020-04-241-81/+152
| |
| * Add valueToInt functionYann Herklotz2020-04-241-0/+3
| |
| * Add stmnt_runp inductiveYann Herklotz2020-04-221-27/+106
| |
* | Stop using tuples for register declarationsJames Pollard2020-05-301-37/+39
| | | | | | | | We use a proper record type now.
* | Fix addressing to add support for arbitraty pointer operationsJames Pollard2020-05-271-10/+19
| | | | | | | | | | | | Currently cannot guarantee alignment in some cases (single reg addressing); will need to fix this in order to prove correctness, perhaps by keeping track of alignment from LEA onwards using AbsInt?
* | Bug fix: stack address normalisationJames Pollard2020-05-261-1/+1
| |
* | (Tentatively) working stack array/memory support.James Pollard2020-05-263-37/+62
| |
* | Add pattern matches and plumb through stack regJames Pollard2020-05-251-5/+21
| |
* | Start work on array supportJames Pollard2020-05-251-0/+1
|/ | | | Try to add a verilog register to represent the stack.
* Return the actual result of the moduleYann Herklotz2020-04-221-2/+5
|
* Remove unnecessary LemmaYann Herklotz2020-04-221-8/+1
| | | | | Still cannot run these functions inside Coq itself, however, they work when they are extracted to Caml.
* Use State in semantics instead of splitting it upYann Herklotz2020-04-221-95/+98
|
* Improve printing of resultsYann Herklotz2020-04-222-7/+13
|
* Fix Verilog.vYann Herklotz2020-04-171-1/+1
|
* Add main module runYann Herklotz2020-04-172-51/+79
|
* Fix printing with new Verilog ASTYann Herklotz2020-04-172-26/+54
|
* Only generate clocked always blocksYann Herklotz2020-04-171-13/+13
|
* Extract simulatorYann Herklotz2020-04-172-5/+5
|
* Add Simulator.vYann Herklotz2020-04-171-0/+32
|
* Add do notation for optionYann Herklotz2020-04-151-0/+11
|
* Make proofs simpler using autoYann Herklotz2020-04-151-59/+45
| | | | | This makes changes to theorems easier, as the proofs will likely not have to be fixed. The runtime is also not much slower.
* Add Verilog semantics with new Verilog moduleYann Herklotz2020-04-151-33/+326
|
* Create Value module for bitvectorsYann Herklotz2020-04-151-0/+217
|
generated by cgit (git 2.34.1) at 2024-07-15 21:13:38 +0000