Formal Techniques for
Hardware/Software Co-Verification

Materials

• Slides (PDF)
• demo1.zip – binary search
• demo2.zip – RTL vs C
• demo3.zip – k-induction
• demo4.zip – State Charts

Related Papers

• Verification of SpecC using Predicate Abstraction
• Formal Verification of SystemC by Automatic Hardware/Software Partitioning
• Checking Consistency of C and Verilog using Predicate Abstraction and Induction
• Hardware Verification using ANSI-C Programs as a Reference
• Behavioral Consistency of C and Verilog Programs Using Bounded Model Checking