aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* 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
| | | | | 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
|
* 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
| | | | | | | | | | 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
|/
* 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
|
* Update compcert dependencyYann Herklotz2020-04-022-0/+2
|
* Update readmeYann Herklotz2020-04-021-1/+1
|
* Handle loops and conditionals correctlyYann Herklotz2020-04-024-114/+183
|
* Update makefile for testsYann Herklotz2020-04-021-1/+4
|
* Add testsYann Herklotz2020-04-024-0/+68
|
* Complete translation from simple RTL to VerilogYann Herklotz2020-04-011-101/+162
|
* Update compilationYann Herklotz2020-04-015-17/+84
|
* Add necessary dependenciesYann Herklotz2020-04-011-1/+1
|
* Convert from RTL to Verilog directlyYann Herklotz2020-03-313-21/+45
|
generated by cgit (git 2.34.1) at 2024-07-10 21:24:46 +0000