project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
124 stars 20 forks source link

Add HMAC registers to circuit needed by software: #961

Closed blaxill closed 3 years ago

blaxill commented 3 years ago
blaxill commented 3 years ago

Shaked has identified an additional needed blocking condition, which I will shortly add to this PR.

fshaked commented 3 years ago

A bit too late but, seems to me like the was_fifo_full field is not really needed, instead apply mask_ready to tl_o inside the let/dealy. I will do this change if you don't see anything wrong with it.