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 realign_fifo spec and proof #940

Closed blaxill closed 3 years ago

blaxill commented 3 years ago

This splits fifo realign and realign_fifo into separate files for easier manipulation (as some of the proof terms are slow), and also adds a spec and proof for realign_fifo in terms of the fifo and realign specs.