Change device.run1 to use TL interface

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.

Apache License 2.0

123 stars 20 forks source link

Change device.run1 to use TL interface #942

Closed fshaked closed 2 years ago

fshaked commented 2 years ago

@samuelgruetter, I fixed everything you mentioned. Please take another look at the changes in InternalMMIOMachine.v, I used tactics to generate the get/set functions. The generated Galina looks reasonable (no crazy 'match'/'return').

fshaked commented 2 years ago

@samuelgruetter, I fixed everything. You can have another go before I merge.