aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * Finish manual simulationYann Herklotz2020-05-052-5/+68
| * Add equality check for valueYann Herklotz2020-05-047-21/+27
| * Move Verilog to .svYann Herklotz2020-05-041-3/+1
| * Refine the semanticsYann Herklotz2020-05-043-56/+130
| * Add code to debug execution of HLSYann Herklotz2020-05-033-0/+137
| * 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 OS detection to makefileYann Herklotz2020-04-232-16/+13
| * Add stmnt_runp inductiveYann Herklotz2020-04-221-27/+106
* | Stop using tuples for register declarationsJames Pollard2020-05-301-37/+39
* | Fix addressing to add support for arbitraty pointer operationsJames Pollard2020-05-271-10/+19
* | 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
* | Merge pull request #4 from ymherklotz/developYann Herklotz2020-04-2212-158/+804
|\|
| * Improve the printing of resultsYann Herklotz2020-04-221-4/+5
| * Return the actual result of the moduleYann Herklotz2020-04-221-2/+5
| * Remove unnecessary LemmaYann Herklotz2020-04-221-8/+1
| * Use State in semantics instead of splitting it upYann Herklotz2020-04-221-95/+98
| * Improve printing of resultsYann Herklotz2020-04-222-7/+13
| * Merge branch 'master' into developYann Herklotz2020-04-191-0/+24
| |\ | |/ |/|
* | Add travis urlYann Herklotz2020-04-171-1/+1
* | Fix examples for current version of coqupYann Herklotz2020-04-171-3/+3
* | Add information about downloading compcertYann Herklotz2020-04-171-0/+14
* | Add examples on how to run HLS toolYann Herklotz2020-04-171-0/+10
* | [#1 #2] Update README for installationYann Herklotz2020-04-171-8/+14
| * Add travis urlYann Herklotz2020-04-171-1/+1
| * 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
| * Update driver to support simulatorYann Herklotz2020-04-171-15/+60
| * Add Simulator.vYann Herklotz2020-04-172-1/+33
| * [#1 #2] Update README for installationYann Herklotz2020-04-171-8/+14
| * Add do notation for optionYann Herklotz2020-04-151-0/+11
| * Make proofs simpler using autoYann Herklotz2020-04-151-59/+45
| * Add Verilog semantics with new Verilog moduleYann Herklotz2020-04-151-33/+326
| * Create Value module for bitvectorsYann Herklotz2020-04-151-0/+217
|/
* Add proof about state wfYann Herklotz2020-04-081-40/+193
* Add partial proof of well formed stateYann Herklotz2020-04-061-24/+136
* Update the readmev0.1.0Yann Herklotz2020-04-031-1/+47
* Fix extraction on linuxYann Herklotz2020-04-021-1/+1
* Add gcc to build dependenciesYann Herklotz2020-04-021-1/+3
generated by cgit (git 2.34.1) at 2024-07-15 18:27:16 +0000