aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/Verilog.v
Commit message (Expand)AuthorAgeFilesLines
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-893/+0
* Change name to VericertYann Herklotz2020-07-141-2/+2
* Fixes to operatorsYann Herklotz2020-07-071-3/+2
* Only translate_cond leftYann Herklotz2020-07-071-1/+3
* No admitted in Deterministic proofYann Herklotz2020-07-071-11/+7
* HTLgenproof compiles againYann Herklotz2020-07-061-5/+7
* Remove admitted in mis_stepp_VdeclYann Herklotz2020-07-051-4/+3
* Finish most of VeriloggenproofYann Herklotz2020-07-051-6/+4
* Working on determinacy proof.James Pollard2020-07-041-2/+133
* Fixing HTLgenproofYann Herklotz2020-07-031-1/+1
* Add new value type to fix Iop proofYann Herklotz2020-07-031-45/+48
* Fix Verilog semantics and fix order of always blocksYann Herklotz2020-06-261-1/+1
* Progress on proof of VeriloggenYann Herklotz2020-06-251-0/+2
* Work on Veriloggen proofYann Herklotz2020-06-251-3/+4
* Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-201-28/+45
|\
| * Fix array semantics behaviour for undefined values.James Pollard2020-06-181-1/+1
| * Fix array semantics merge granularity.James Pollard2020-06-171-22/+34
| * Array semantics now uses dependent Array type.James Pollard2020-06-141-26/+31
| * Merge branch 'master' into arrays-proofJames Pollard2020-06-121-69/+114
| |\
| * | Rough outline of stack address proofJames Pollard2020-06-111-4/+4
* | | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-141-1/+3
| |/ |/|
* | Generate Verilog from HTLYann Herklotz2020-06-121-69/+114
|/
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-091-6/+3
|\
| * Finished main proof with small assumptionsYann Herklotz2020-06-041-6/+3
* | Update HTL semantics to support arrays.James Pollard2020-06-021-5/+7
* | Paramterise associations type to avoid some duplication.James Pollard2020-06-021-44/+40
* | First draft of array semantics.James Pollard2020-06-011-112/+188
* | Merge branch 'develop' into arrays-proofJames Pollard2020-05-301-88/+247
|\|
| * Fix compilation moving to PTreeYann Herklotz2020-05-291-7/+7
| * Switch position of empty ruleYann Herklotz2020-05-201-4/+4
| * Add AssocMapYann Herklotz2020-05-081-39/+25
| * Use associations instead of stateYann Herklotz2020-05-071-70/+65
| * Rename assoclist to assocsetYann Herklotz2020-05-071-25/+25
| * Minimised manual simulationYann Herklotz2020-05-051-10/+10
| * Simplifications to proofYann Herklotz2020-05-051-2/+8
| * Add equality check for valueYann Herklotz2020-05-041-1/+1
| * Refine the semanticsYann Herklotz2020-05-041-42/+63
| * Change to StateYann Herklotz2020-05-031-21/+22
| * Add CompCert semantics for VerilogYann Herklotz2020-04-241-81/+152
| * Add stmnt_runp inductiveYann Herklotz2020-04-221-27/+106
* | (Tentatively) working stack array/memory support.James Pollard2020-05-261-0/+4
|/
* Use State in semantics instead of splitting it upYann Herklotz2020-04-221-95/+98
* Fix Verilog.vYann Herklotz2020-04-171-1/+1
* Add main module runYann Herklotz2020-04-171-50/+78
* Add Verilog semantics with new Verilog moduleYann Herklotz2020-04-151-33/+326
* Handle loops and conditionals correctlyYann Herklotz2020-04-021-7/+8
* Update compilationYann Herklotz2020-04-011-5/+36
* Add documentation and fix makefile for CompcertYann Herklotz2020-03-311-1/+1
* Add more operators and print themYann Herklotz2020-03-311-3/+10
* Improve Verilog error messagesYann Herklotz2020-03-311-1/+4
generated by cgit (git 2.34.1) at 2024-07-01 12:48:38 +0000