Skip to main content

Using Non-Determinism with Formal

Conference: Verification Futures 2023 (click here to see full programme)
Speaker: Doug Smith
Presentation Title: Using Non-Determinism with Formal

The use of non-determinism with formal is how formal is able to manage large state spaces and still arrive at a quick solution. Non-determinism plays a part in writing our formal constraints, formal targets, and formal abstractions. In this formal tutorial session, we'll explain what non-determinism is, how it's used, and show lots of examples so you can take advantage of non-determinism in verifying your designs.

Speaker Bio:

Doug Smith is a verification engineer and instructor for Doulos based in the Austin Texas area with expertise in UVM and formal technologies. He has been using formal technology for several decades, performing formal verification on many kinds of designs and formal applications. Likewise, he has provided formal application support at both Jasper and Mentor/Siemens EDA. At Mentor/Siemens EDA, he served as a formal specialist and

verification consultant, where he provided both formal consulting and developed an automotive functional safety formal app for performing formal fault campaigns. At Doulos, he delivers training in verification methodologies like UVM, SystemVerilog, and formal technology.

Doug holds a masters degree in Computer Engineering from the University of Cincinnati and a bachelors degree in Physics and Biology from Northern Kentucky University. Currently, he resides in Paige Texas with his wife and family on a small farm where he raises bees, cows, horses, chickens, and pigs and loves driving a tractor.

Key Points:
  • Non-determinism helps you exhaustively verify design behaviors
  • Non-determinism is used in formal modeling like abstractions
  • A simple technique like non-determinism makes formal more effective
  • Close Menu