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
/
hls
Commit message (
Expand
)
Author
Age
Files
Lines
*
Check whether callee is internal for Icall
Michalis Pardalos
2021-08-02
2
-25
/
+24
*
Add "join state is <=Int.max_unsigned" to HTLgenspec
Michalis Pardalos
2021-06-10
2
-10
/
+13
*
Remove all Admitted from top-level Compiler.v
Michalis Pardalos
2021-06-10
5
-383
/
+588
*
Make externctrl application its own HTL pass
Michalis Pardalos
2021-06-06
3
-184
/
+225
*
Move HTL renaming pass to own file
Michalis Pardalos
2021-06-06
3
-240
/
+230
*
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
1
-14
/
+26
*
Progress on tr_module proof
Michalis Pardalos
2021-05-08
1
-52
/
+80
*
Fully clean up the iter_expand_instr_spec proof
Michalis Pardalos
2021-05-07
1
-146
/
+67
*
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
2
-43
/
+123
*
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
1
-105
/
+179
*
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
1
-49
/
+71
*
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
1
-41
/
+44
*
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
1
-2
/
+2
*
Handle declarations of externctrl regs in Verilog
Michalis Pardalos
2021-05-01
1
-24
/
+41
*
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
[next]