index
:
vericert
debug/unhashed
dev-michalis
dev/asplos
dev/div
dev/divider
dev/full-nix-build
dev/mac-op
dev/michalis
dev/scheduling
dev/value
exp/inl-cse-const
master
stable
Vericert is a formally verified high-level synthesis tool.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
src
Commit message (
Expand
)
Author
Age
Files
Lines
*
Get top-level (Compiler) proof closer to Qed
Michalis Pardalos
2021-06-08
1
-3
/
+27
*
Make externctrl application its own HTL pass
Michalis Pardalos
2021-06-06
4
-185
/
+229
*
Move HTL renaming pass to own file
Michalis Pardalos
2021-06-06
5
-242
/
+249
*
Add explanations for axioms
Michalis Pardalos
2021-05-18
1
-11
/
+13
*
Add axiom that only the main contains stores
Michalis Pardalos
2021-05-18
1
-4
/
+10
*
Qed on top-level correctness lemma
Michalis Pardalos
2021-05-18
1
-2
/
+2
*
Update lemmata broken by changes to semantics
Michalis Pardalos
2021-05-18
1
-42
/
+35
*
Get Icall translation lemma *statement* passing
Michalis Pardalos
2021-05-18
1
-15
/
+17
*
Add "internal calls only" into translation spec
Michalis Pardalos
2021-05-18
2
-70
/
+94
*
Get Ireturn proof to pass again
Michalis Pardalos
2021-05-18
1
-11
/
+8
*
Callstate proof with holes regarding stack
Michalis Pardalos
2021-05-18
1
-129
/
+97
*
Complete Returnstate proofs
Michalis Pardalos
2021-05-18
1
-19
/
+3
*
Complete Returnstate proofs
Michalis Pardalos
2021-05-17
2
-78
/
+173
*
Elaborate how stackframes match (match_frames)
Michalis Pardalos
2021-05-17
1
-3
/
+29
*
Add module idents to the semantics
Michalis Pardalos
2021-05-17
2
-51
/
+66
*
Most of Ireturn proof
Michalis Pardalos
2021-05-16
4
-17
/
+80
*
Update HTL proof for resource sharing (WIP)
Michalis Pardalos
2021-05-14
2
-242
/
+307
*
Give new semantics for HTL
Michalis Pardalos
2021-05-13
1
-15
/
+41
*
Get HTLgenproof passing again (with admits)
Michalis Pardalos
2021-05-13
1
-230
/
+172
*
Remove "active_call" from HTL semantics
Michalis Pardalos
2021-05-13
2
-28
/
+24
*
Remove reverse matching from monad_crush
Michalis Pardalos
2021-05-12
1
-2
/
+2
*
Change tr_module to show registers are different
Michalis Pardalos
2021-05-12
1
-6
/
+6
*
Fix added tr_code constructors
Michalis Pardalos
2021-05-10
1
-12
/
+19
*
Clean up HTLgenspec
Michalis Pardalos
2021-05-10
1
-127
/
+130
*
Remove unused lemmas in HTLgenspec
Michalis Pardalos
2021-05-10
1
-414
/
+33
*
Delete inv_incr tactic (unused)
Michalis Pardalos
2021-05-10
1
-51
/
+0
*
Get entire HTLgenspec proof passing
Michalis Pardalos
2021-05-10
2
-14
/
+36
*
Progress on tr_module proof
Michalis Pardalos
2021-05-08
2
-52
/
+82
*
Fully clean up the iter_expand_instr_spec proof
Michalis Pardalos
2021-05-07
2
-146
/
+80
*
Complete iter_expand_instr_spec proof
Michalis Pardalos
2021-05-07
1
-14
/
+23
*
Prove a spec for the mapping of function params
Michalis Pardalos
2021-05-06
3
-49
/
+128
*
Solve easier branches of the transf_instr proof
Michalis Pardalos
2021-05-06
1
-29
/
+64
*
Define map_incr to clarify st_incr
Michalis Pardalos
2021-05-05
1
-9
/
+13
*
Clean up iter_expand_instr_spec proof
Michalis Pardalos
2021-05-05
1
-21
/
+10
*
Solve iter_expand_instr_spec by tactic (not Icall)
Michalis Pardalos
2021-05-05
2
-107
/
+182
*
Rewrite transf_instr, move complicated part up
Michalis Pardalos
2021-05-03
1
-6
/
+6
*
Add lemmas relating to new HTLgen operations
Michalis Pardalos
2021-05-03
2
-51
/
+73
*
Add some statements about externctrl to tr_code
Michalis Pardalos
2021-05-03
1
-9
/
+13
*
Add externctrl props to HTLgen's st_prop
Michalis Pardalos
2021-05-03
2
-41
/
+51
*
Use ltac:() instead of Program in HTLgen
Michalis Pardalos
2021-05-03
1
-140
/
+116
*
Use Defined for obligations in Program Definitions
Michalis Pardalos
2021-05-02
1
-12
/
+12
*
Give a (questionable) translation spec for HTLgen
Michalis Pardalos
2021-05-02
2
-39
/
+61
*
Simplify some HTLgenspec proofs
Michalis Pardalos
2021-05-02
2
-2
/
+7
*
Handle declarations of externctrl regs in Verilog
Michalis Pardalos
2021-05-01
2
-24
/
+48
*
Remove some dead code from Veriloggen
Michalis Pardalos
2021-05-01
1
-17
/
+0
*
Fix HTLgen using wrong register in call wait state
Michalis Pardalos
2021-05-01
1
-2
/
+3
*
Fix typo bug in applying externctrl
Michalis Pardalos
2021-05-01
1
-2
/
+2
*
Print externctrl in HTL debug output
Michalis Pardalos
2021-05-01
2
-6
/
+31
*
Apply externctrl mapping in HTL->Verilog stage
Michalis Pardalos
2021-04-30
1
-22
/
+147
*
Tie all modules' clock to main
Michalis Pardalos
2021-04-30
4
-16
/
+47
[next]