project-oak / silveroak

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

Increment device with TLUL #939

Closed fshaked closed 3 years ago

fshaked commented 3 years ago

At the end I didn't use any spec. I suspect both [tlul_adapter_reg] and [incr] are just too simple to justify the overhead of a spec. Also, I can't think of a spec that is any different than the implementation.