aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog
Commit message (Expand)AuthorAgeFilesLines
* Add top level backward simulationYann Herklotz2020-07-061-8/+2
* HTLgenproof compiles againYann Herklotz2020-07-062-7/+11
* No addmitted in VeriloggenproofYann Herklotz2020-07-051-8/+12
* Remove admitted in mis_stepp_VdeclYann Herklotz2020-07-051-4/+3
* Finish most of VeriloggenproofYann Herklotz2020-07-053-7/+9
* Working on determinacy proof.James Pollard2020-07-041-2/+133
* Fixing HTLgenproofYann Herklotz2020-07-033-13/+20
* Add new value type to fix Iop proofYann Herklotz2020-07-034-65/+215
* Addition to int_add_v2Yann Herklotz2020-07-031-3/+13
* Updates to Iop proofYann Herklotz2020-07-031-1/+78
* Switch to uvalueToZ in lessdef.James Pollard2020-07-021-2/+2
* Complete ZToValue_valueToNat.James Pollard2020-07-021-9/+18
* Push current stateYann Herklotz2020-07-021-0/+2
* Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-07-011-28/+41
|\
| * Improve (?) automation.James Pollard2020-07-011-28/+41
* | Add HTL pretty printerYann Herklotz2020-06-301-0/+81
* | Add htl pretty printingYann Herklotz2020-06-302-1/+3
|/
* Add command line flags for initial blockYann Herklotz2020-06-301-0/+10
* Make the proofs more conciseYann Herklotz2020-06-301-17/+21
* Add equivalence between int add value addYann Herklotz2020-06-301-10/+54
* Work on addition proofYann Herklotz2020-06-291-1/+21
* Fix proof again with Verilog semantics changesYann Herklotz2020-06-281-0/+12
* Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-281-0/+53
|\
| * Work on proof.James Pollard2020-06-281-0/+53
* | Fix Verilog semantics and fix order of always blocksYann Herklotz2020-06-261-1/+1
* | Progress on proof of VeriloggenYann Herklotz2020-06-252-1/+5
* | Work on Veriloggen proofYann Herklotz2020-06-251-3/+4
|/
* Fixes to make develop compileYann Herklotz2020-06-241-5/+3
* More to proofYann Herklotz2020-06-231-7/+9
* Admit the value proofYann Herklotz2020-06-221-3/+5
* Merge branch 'arrays-proof' into developYann Herklotz2020-06-221-0/+5
|\
| * Finish structure of Aindexed2scaled ILoad proof.James Pollard2020-06-201-0/+5
* | Merge branch 'master' into developYann Herklotz2020-06-222-13/+28
|\ \
| * | Only print out main as everything is inlinedYann Herklotz2020-06-221-8/+10
| * | Add print for debug always block in moduleYann Herklotz2020-06-222-6/+19
* | | Add proof of nat equivYann Herklotz2020-06-201-2/+15
* | | Merge remote-tracking branch 'james/arrays-proof' into developYann Herklotz2020-06-204-40/+337
|\ \ \ | |/ / |/| / | |/
| * Tidy up proof.James Pollard2020-06-181-1/+1
| * Fix array semantics behaviour for undefined values.James Pollard2020-06-181-1/+1
| * Fix Inop proof to work with new array semantics.James Pollard2020-06-171-0/+8
| * Some (very) useful lemmas about arrays.James Pollard2020-06-171-3/+105
| * Fix array semantics merge granularity.James Pollard2020-06-173-30/+80
| * Array semantics now uses dependent Array type.James Pollard2020-06-142-39/+39
| * Add a basic length-indexed list type.James Pollard2020-06-131-0/+123
| * Merge branch 'master' into arrays-proofJames Pollard2020-06-125-188/+149
| |\
| * | Rough outline of stack address proofJames Pollard2020-06-111-4/+4
| * | Working on proof.James Pollard2020-06-112-6/+20
* | | Add more unproven instructions, Admitted equiv to specYann Herklotz2020-06-142-2/+5
| |/ |/|
* | Fix declaring function arguments correctlyYann Herklotz2020-06-121-3/+3
* | Fix printing of Verilog with new datatypesYann Herklotz2020-06-122-17/+27
generated by cgit (git 2.34.1) at 2024-07-03 01:08:49 +0000