aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog
Commit message (Expand)AuthorAgeFilesLines
* Add lessdef for valuesYann Herklotz2020-05-081-3/+10
* Add AssocMapYann Herklotz2020-05-084-47/+93
* Redefine HTL for intermediate Verilog languageYann Herklotz2020-05-071-76/+69
* Use associations instead of stateYann Herklotz2020-05-072-70/+69
* Rename assoclist to assocsetYann Herklotz2020-05-072-28/+28
* 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-042-16/+22
* Refine the semanticsYann Herklotz2020-05-043-56/+130
* Add code to debug execution of HLSsave/old-stepYann Herklotz2020-05-031-0/+73
* Add hex notation to valuesYann Herklotz2020-05-031-0/+9
* Change to StateYann Herklotz2020-05-031-21/+22
* 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
* 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
* 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
* Add Verilog semantics with new Verilog moduleYann Herklotz2020-04-151-33/+326
* Create Value module for bitvectorsYann Herklotz2020-04-151-0/+217
* Handle loops and conditionals correctlyYann Herklotz2020-04-022-12/+53
* Update compilationYann Herklotz2020-04-013-14/+81
* Add documentation and fix makefile for CompcertYann Herklotz2020-03-312-1/+26
* Add more operators and print themYann Herklotz2020-03-312-4/+15
* Improve Verilog error messagesYann Herklotz2020-03-311-1/+4
* Fix Verilog printingYann Herklotz2020-03-312-33/+35
* Change Verilog AST back to more traditional ASTYann Herklotz2020-03-291-30/+44
* Remove unnecessary examples from HTLYann Herklotz2020-03-291-4/+4
* Update AST and value representationsYann Herklotz2020-03-291-213/+42
* Rename Verilog AST filesYann Herklotz2020-03-293-0/+0
* Update printingYann Herklotz2020-03-253-38/+52
* Remove dunes and make the build recursiveYann Herklotz2020-03-251-4/+0
* Rename to HTLYann Herklotz2020-03-231-18/+28
* Create intermediate VTL languageYann Herklotz2020-03-221-0/+63
* Add compcert library to coquplibYann Herklotz2020-03-221-8/+9
* Lower case foldersYann Herklotz2020-03-194-0/+341