Mar02 Workshop Sakallah

Category: Education

Presentation Description

No description available.


Presentation Transcript


Maher Mneimneh and Karem Sakallah EECS Department University of Michigan - Ann Arbor Design for Verifiability


Outline Automatic abstraction of HDL models Sequential equivalence checking

Microprocessor Design Verification: 

Microprocessor Design Verification Extensive research on decidable formal models Logic of Equality with uninterpreted functions (Burch, Dill, Miroslav, and Bryant) Superior because it automates verification once the models are available Extensive research on decision procedures Efficient conversion from LEUF formulas to Boolean formulas (Miroslav, and Bryant) Little research on the rigorous construction of formal models from HDL descriptions Most often manual construction

Hand-Crafted Verification Models: 

Hand-Crafted Verification Models Require substantial human effort (time consuming) Are error-prone Introduce new errors Miss present ones Do not scale well to large designs Need to be modified with RTL changes Might lack aggressive optimizations that simplify the verification

Consequences …: 

Consequences … No integration in early stages of HDL design cycle Desirable: bugs are common in these early stages Difficulty: design is constantly changing Verification results might be unsound Bug might have been injected during modeling Bug might no more exist in the modified RTL model Generally designs formally verified late in the cycle even after tape-out

Solution …: 

Solution … Automatically construct a faithful formal model from the HDL description Verify the model against the specification Map counter examples (if any) back to the HDL description Automatic Abstraction HDL Model Abstract Formal Model Specification Model Automatic Verification

Some Software Abstraction Tools: 

Some Software Abstraction Tools C2BP (C to Bebop): Automatic abstraction to Boolean programs (Ball, Rajamani, Microsoft Research) Bandera user-guided abstraction (Java to SMV/PVS/SPIN) (Dwyer, Hatcliff, Kansas State University) Others: Feaver (Bell Labs) Java PathFinder (NASA) We are unaware of similar tools for Verilog or VHDL

Abstraction Tool: 

Abstraction Tool Abstracts datapath: Most errors are in the control: abstract datapath units Ex: abstract an adder with an uninterpreted function Performs rigorous analysis of HDL description to detect further structure (eg. symmetries) Can be viewed as an optimizing compiler

Issues To Be Addressed: 

Issues To Be Addressed What is the HDL language used and what subset is supported? Use synthesizable Verilog subset What is the formal modeling language used? UCLID (CMU) Is the abstraction user-guided (annotated HDL) or totally automatic? Automatic abstraction Is the constructed abstraction faithful to the original model? Prove (in)validity of abstraction

Verilog to Uclid: A Simple Example: 

Verilog to Uclid: A Simple Example input [7:0] a, b; input op; output [7:0] result; assign result = (op) ? a+b : a-b; a : TERM; b : TERM; op : TRUTH; result : TERM; funcAdd : FUNC[2]; funcSub : FUNC[2]; result := case op : funcAdd(a,b); default : funcSub(a,b); esac;


Accomplishments Established mappings from Verilog constructs to UCLID Arithmetic, equality, relational, and reduction operators Conditional operators Bit selectors and part selectors Implemented a simple abstraction tool Accepts limited subsets of Verilog and converts to UCLID Applied to the verification of DIVA Verilog model against ALPHA ISA

Sequential Equivalence Checking: 

Sequential Equivalence Checking Detailed study of the semantics of sequential equivalence Classical notion of machine equivalence Equivalence when the initial state is known Sequential Hardware Equivalence (Pixley) Safe replaceability and 3-valued safe replaceability Detailed study of BDD-based and SAT-based sequential equivalence checking techniques A survey paper on sequential equivalence checking

Work in Progress: 

Work in Progress Detect functional symmetries of finite-state machines Previous research: use state transition graph to extract symmetries Our approach: use net-list to extract symmetries Use symmetries to simplify sequential equivalence checking Work is still in its early phases

Future Work: 

Future Work Incorporate automatic abstraction of datapath through control-flow graph analysis Add symmetry detection algorithms to the abstraction tool Design an internal representation language that facilitates translation to different formal models (PVS, ACL2, …) Build a rigorous abstraction framework that checks the faithfulness of the generated abstraction to the original model provides suitable refinements to the abstraction model if needed Enhance SAT-based sequential equivalence checking techniques Incremental satisfiability Learning methods

authorStream Live Help