aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/HTL.v
Commit message (Expand)AuthorAgeFilesLines
* Change name to VericertYann Herklotz2020-07-141-3/+3
* HTLgenproof compiles againYann Herklotz2020-07-061-2/+4
* No addmitted in VeriloggenproofYann Herklotz2020-07-051-8/+12
* Finish most of VeriloggenproofYann Herklotz2020-07-051-0/+4
* Fixing HTLgenproofYann Herklotz2020-07-031-6/+4
* Progress on proof of VeriloggenYann Herklotz2020-06-251-1/+3
* Fix array semantics merge granularity.James Pollard2020-06-171-8/+8
* Array semantics now uses dependent Array type.James Pollard2020-06-141-13/+8
* Merge branch 'master' into arrays-proofJames Pollard2020-06-121-1/+6
|\
| * Remove Verilog proofsYann Herklotz2020-06-121-1/+6
* | Working on proof.James Pollard2020-06-111-6/+15
|/
* Merge branch 'develop' into arrays-proofJames Pollard2020-06-091-13/+48
|\
| * Finished main proof with small assumptionsYann Herklotz2020-06-041-13/+47
* | HTLgenspec status in line with developJames Pollard2020-06-031-0/+1
* | Merge branch 'develop' into arrays-proofJames Pollard2020-06-031-2/+2
|\|
| * Add proof to final_statesYann Herklotz2020-06-021-2/+2
* | Update HTL semantics to support arrays.James Pollard2020-06-021-14/+25
|/
* Copy over RTL global stateYann Herklotz2020-06-011-8/+15
* Fix compilation moving to PTreeYann Herklotz2020-05-291-4/+3
* Fix the semantics to properly evaluate the stateYann Herklotz2020-05-201-2/+4
* Add AssocMapYann Herklotz2020-05-081-5/+5
* Redefine HTL for intermediate Verilog languageYann Herklotz2020-05-071-76/+69
* Add documentation and fix makefile for CompcertYann Herklotz2020-03-311-0/+25
* Remove unnecessary examples from HTLYann Herklotz2020-03-291-4/+4
* Update printingYann Herklotz2020-03-251-35/+41
* Rename to HTLYann Herklotz2020-03-231-0/+73