aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'develop' into dev-nadesh-provendev-nadesh-provenYann Herklotz2020-07-074-8/+8
|\
| * Fixes to operatorsYann Herklotz2020-07-074-6/+12
| * Finished transl_condYann Herklotz2020-07-072-62/+45
* | Merge branch 'dev-nadesh-proven' of https://github.com/ymherklotz/coqup into ...Nadesh Ramanathan2020-07-0720-2211/+3552
|\ \
| * \ Merge branch 'dev-nadesh' into dev-nadesh-provenJames Pollard2020-07-0720-2211/+3552
| |\ \
| | * | Merge remote-tracking branch 'upstream/develop' into dev-nadeshJames Pollard2020-07-073-13/+57
| | |\|
| | | * Only translate_cond leftYann Herklotz2020-07-074-17/+252
| | * | Get Coqup compiling again on dev-nadesh.James Pollard2020-07-073-1937/+1938
| | * | Merge branch 'byte-addressing' into dev-nadeshJames Pollard2020-07-0725-2213/+3436
| | |\ \
| | | * | Merge branch 'develop' of github.com:ymherklotz/coqup into byte-addressingJames Pollard2020-07-075-124/+293
| | | |\|
| | | | * No admitted in Deterministic proofYann Herklotz2020-07-073-14/+10
| | | | * A few operations leftYann Herklotz2020-07-071-30/+88
| | | | * Proof of TransfHTLLink DONEYann Herklotz2020-07-071-1/+14
| | | | * Rename asm to verilogYann Herklotz2020-07-061-9/+10
| | | | * Add top level backward simulationYann Herklotz2020-07-063-95/+191
| | | * | Concatenation style loads.James Pollard2020-07-063-49/+54
| | | * | Reduce number of array addressing modes.James Pollard2020-07-062-6/+27
| | | * | Check chunk size during translation.James Pollard2020-07-062-19/+33
| | | * | Remove alignment requirement for lessdef.James Pollard2020-07-061-9/+3
| | | * | Merge branch 'develop' of github.com:ymherklotz/coqup into byte-addressingJames Pollard2020-07-067-2201/+2238
| | | |\|
| | | | * HTLgenproof compiles againYann Herklotz2020-07-064-22/+47
| | | | * Fix InopYann Herklotz2020-07-054-47/+58
| | | * | Fix HTLgenspec.James Pollard2020-07-062-476/+467
| | | * | Implemented algorithm for new byte-addressed stack.James Pollard2020-07-0611-2682/+2730
| | | |/
| | | * Fix HTLgenspecYann Herklotz2020-07-051-3/+4
| | | * No addmitted in VeriloggenproofYann Herklotz2020-07-054-100/+245
| | | * Remove admitted in mis_stepp_VdeclYann Herklotz2020-07-053-9/+12
| | | * Finish most of VeriloggenproofYann Herklotz2020-07-055-31/+205
| | | * Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-07-042-12/+175
| | | |\
| | | | * Working on determinacy proof.James Pollard2020-07-042-12/+175
| | | * | Define ofbytesYann Herklotz2020-07-041-1/+72
| | | * | Make HTLgen compile againYann Herklotz2020-07-041-3/+11
| | | |/
| | | * Fixing HTLgenproofYann Herklotz2020-07-036-41/+67
| | | * Add new value type to fix Iop proofYann Herklotz2020-07-035-67/+217
| | | * Addition to int_add_v2Yann Herklotz2020-07-031-3/+13
| | | * Updates to Iop proofYann Herklotz2020-07-033-92/+179
| | | * Switch to uvalueToZ in lessdef.James Pollard2020-07-024-67/+87
| | | * Merge branch 'develop' of github.com:ymherklotz/coqup into developJames Pollard2020-07-020-0/+0
| | | |\
| | | | * Typo fixYann Herklotz2020-07-021-1/+1
| | | * | Complete ZToValue_valueToNat.James Pollard2020-07-022-31/+34
| | | |/
| | | * Fix callstate proof.James Pollard2020-07-021-7/+7
| | | * Stuck in Callstate proofYann Herklotz2020-07-021-20/+17
| | | * Push current stateYann Herklotz2020-07-022-26/+46
| | | * Remove all <> AdmittedYann Herklotz2020-07-022-23/+27
| | | * Fix spec by adding details about reg valsYann Herklotz2020-07-022-36/+182
| | * | Merge branch 'develop' into dev-nadeshYann Herklotz2020-06-3010-39/+340
| | |\ \
| | * | | Remove checks for translate_eff_addressingYann Herklotz2020-06-293-17/+9
| | * | | Merge branch 'develop' into dev-nadeshYann Herklotz2020-06-2913-245/+2677
| | |\ \ \
* | | | | | added counter in testbenchNadesh Ramanathan2020-07-071-1/+4
* | | | | | remove const propNadesh Ramanathan2020-07-071-1/+1
|/ / / / /
generated by cgit (git 2.34.1) at 2024-05-21 22:29:22 +0000