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
/
HTLgen.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
Merge branch 'oopsla21' into sharing-merge
Michalis Pardalos
2021-08-26
1
-24
/
+53
|
\
|
*
Basically done with proof
Yann Herklotz
2021-04-07
1
-4
/
+6
|
*
Finish load and store proof, but broke top-level
Yann Herklotz
2021-04-06
1
-24
/
+24
|
*
Add RAM to HTL
Yann Herklotz
2021-03-02
1
-0
/
+1
*
|
Find called module in Icall proof
Michalis Pardalos
2021-08-19
1
-7
/
+1
*
|
Complete HTLspec (mostly)
Michalis Pardalos
2021-08-12
1
-34
/
+64
*
|
Tie clocks in the ApplyExternctrl pass
Michalis Pardalos
2021-08-12
1
-1
/
+0
*
|
Correct lookup for called funcs, simplify tr_module
Michalis Pardalos
2021-08-04
1
-8
/
+24
*
|
Check whether callee is internal for Icall
Michalis Pardalos
2021-08-02
1
-19
/
+24
*
|
Add "join state is <=Int.max_unsigned" to HTLgenspec
Michalis Pardalos
2021-06-10
1
-9
/
+11
*
|
Move HTL renaming pass to own file
Michalis Pardalos
2021-06-06
1
-240
/
+0
*
|
Most of Ireturn proof
Michalis Pardalos
2021-05-16
1
-11
/
+17
*
|
Prove a spec for the mapping of function params
Michalis Pardalos
2021-05-06
1
-5
/
+12
*
|
Define map_incr to clarify st_incr
Michalis Pardalos
2021-05-05
1
-9
/
+13
*
|
Rewrite transf_instr, move complicated part up
Michalis Pardalos
2021-05-03
1
-6
/
+6
*
|
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
1
-27
/
+37
*
|
Fix HTLgen using wrong register in call wait state
Michalis Pardalos
2021-05-01
1
-2
/
+3
*
|
Tie all modules' clock to main
Michalis Pardalos
2021-04-30
1
-6
/
+6
*
|
Fix map_externctrl double-incrementing freshreg
Michalis Pardalos
2021-04-30
1
-3
/
+2
*
|
Delete unused get_main_clk function from HTLgen
Michalis Pardalos
2021-04-30
1
-11
/
+0
*
|
Map clock correctly in RTL->HTL
Michalis Pardalos
2021-04-29
1
-15
/
+9
*
|
Renumber AssocMaps in HTL modules too
Michalis Pardalos
2021-04-20
1
-7
/
+24
*
|
Move renumbering to be HTL->HTL
Michalis Pardalos
2021-04-20
1
-0
/
+213
*
|
[WIP] Re-implement translation of calls.
Michalis Pardalos
2021-04-19
1
-33
/
+67
*
|
[WIP] Use Program instead of state_incr lemmas
Michalis Pardalos
2021-04-18
1
-165
/
+40
*
|
[WIP] Generate calling verilog in RTL->HTL
Michalis Pardalos
2021-04-18
1
-15
/
+40
*
|
[WIP] Remove extra statements from HTL.
Michalis Pardalos
2021-04-18
1
-17
/
+14
*
|
Fix merge error in oshrximm
Michalis Pardalos
2021-04-09
1
-1
/
+3
*
|
Add idle state after return
Michalis Pardalos
2021-03-01
1
-6
/
+7
*
|
Add changes to HTL as they weren't merged
Yann Herklotz
2021-02-16
1
-53
/
+122
*
|
Merge branch 'michalis' of https://github.com/mpardalos/vericert into michali...
Yann Herklotz
2021-02-16
1
-2
/
+2
|
/
*
Fix imports to remove warnings when compiling
Yann Herklotz
2021-01-22
1
-9
/
+20
*
Add correct copyright notices in files
Yann Herklotz
2021-01-10
1
-0
/
+1
*
Change and add back HTLgen
Yann Herklotz
2020-11-09
1
-4
/
+4
*
Add RTLBlock intermediate language
Yann Herklotz
2020-08-30
1
-0
/
+654