Pipeline Design and Verification in Bluenose II
Ca Bol Chan, Vlad Ciubotariu, Mark D. Aagaard · 2007
As digital hardware circuits get more complex, it becomes more difficult and time consuming to verify a design. Although time to market is crucial, adequate time should be spent on verification since a bug found after manufacturing is expensive to fix and will cause further delay to market. Techniques in formal methods such as model checking allow the discovery of subtle design bugs. However, formal verification usually requires specialized expertise. Bluenose II aims to address these issues by raising design abstraction to increase productivity and reduce verification effort, focusing on pipelined circuits in particular.