ASIC Point Explore

Silicon Lab

Formal Verification Problems

Build a design, hunt its bugs, or repair what fails. Every answer runs on a real simulator.

Build starts from a specification: make it work, then make it small or fast. Bug Hunt asks for the checker or the test that catches broken designs. Repair hands you a failure: find the cause, then fix the design.

Formal Verification · F1

  1. F1.2.1 Retire the Response, Including Errors 1200 Verify Medium Verilator
  2. F1.4.1 The Acknowledgement After Cancellation 900 Debug Easy Verilator
  3. F1.4.2 A Failure Before the First Request 900 Debug Easy Verilator
  4. F1.5.1 How Deep Is the Expiry Corner? 1200 Verify Medium Verilator
  5. F1.6.1 Reset the Mode as Well as the Count 1200 Fix Medium Verilator

Formal Verification · F2

  1. F2.1.1 Write the Third Toggle Stage 900 Implement Easy Verilator
  2. F2.3.1 Three Bytes Before the Bad State 1200 Verify Medium Verilator
  3. F2.4.2 A Counterexample to Which Question? 1200 Debug Medium Verilator
  4. F2.4.1 Close the Induction with a Helper 1500 Optimize Hard Verilator
  5. F2.5.1 Let the Engine Find the Invariant 1200 Optimize Medium Verilator
  6. F2.6.1 Read the Timeout Without Inventing a Bug 1200 Debug Medium Verilator

Formal Verification · F3

  1. F3.1.1 Build the Register-Slice Checker 1200 Implement Medium Verilator
  2. F3.1.2 Check the Transformed Payload 1200 Verify Medium Verilator
  3. F3.2.2 Restrict Is Still a Promise 1200 Break It Medium Verilator
  4. F3.2.1 The Assumption That Hides the Overflow 1500 Break It Hard Verilator
  5. F3.3.1 Four Traces, Four Causes 1500 Debug Hard Verilator
  6. F3.3.2 One Promise for Speculative Capture 1500 Verify Hard Verilator
  7. F3.4.1 Prove the Data, Not Just the Pointers 1500 Verify Hard Verilator
  8. F3.5.1 Ask for Three Directed Tests 1200 Implement Medium Verilator
  9. F3.5.2 The Overflow That Cannot Be Reached 1200 Debug Medium Verilator
  10. F3.6.1 Make the Tracker a Claim 1200 Fix Medium Verilator
  11. F3.7.1 An Environment That Never Serves 1200 Break It Medium Verilator

Formal Verification · F4

  1. F4.1.1 Cut the Watchdog Cone 1500 Optimize Hard Verilator
  2. F4.2.2 The Cut That Removed the Bug 1200 Debug Medium Verilator
  3. F4.2.1 A Free CRC Cut 1500 Optimize Hard Verilator
  4. F4.3.1 An Exhaustive Address Case Split 1200 Implement Medium Verilator
  5. F4.3.2 Break the Circular Guarantee 1500 Break It Hard Verilator
  6. F4.4.1 Implement the Symbolic Packet Tracker 1500 Implement Hard Verilator
  7. F4.4.2 Identity Before Payload Equality 1500 Verify Hard Verilator
  8. F4.5.2 Qualify a Smaller Parameter Instance 1200 Optimize Medium Verilator
  9. F4.5.1 Abstract the Million-Cycle Watchdog 1500 Optimize Hard Verilator
  10. F4.6.2 Conserve the Credits 1200 Implement Medium Verilator
  11. F4.6.1 Two Relations for Two Enables 1500 Optimize Hard Verilator

Formal Verification · F5

  1. F5.2.1 Generate the Automatic Safety Checks 1200 Verify Medium Verilator
  2. F5.3.1 Turn the Connection Table into Claims 1200 Implement Medium Verilator
  3. F5.3.2 The Swapped Pair in the Table 1200 Debug Medium Verilator
  4. F5.4.2 Repair Write-One-to-Clear Priority 1200 Fix Medium Verilator
  5. F5.4.1 Check the Register Policy Table 1500 Verify Hard Verilator
  6. F5.5.1 Reset the Free Mode Bit 1200 Fix Medium Verilator
  7. F5.5.2 Keep an Unknown from Enabling the Block 1200 Verify Medium Verilator
  8. F5.6.1 Check a Scheduled Clock Crossing 1500 Verify Hard Verilator
  9. F5.7.1 Prove the Dead Bins and Reach the Live One 1200 Verify Medium Verilator
  10. F5.8.1 Compare All Forbidden Sinks 1500 Implement Hard Verilator
  11. F5.9.1 Read the Lab Constraint Experiment 1200 Debug Medium Verilator

Formal Verification · F6

  1. F6.1.1 Compare RTL with a Structural Implementation 1200 Verify Medium Verilator
  2. F6.2.1 Align a Two-Stage Adder 1500 Verify Hard Verilator
  3. F6.3.1 Partition the Multiplier Question 1500 Optimize Hard Verilator
  4. F6.4.1 Constrain the Scope of a WRAP Fix 1500 Verify Hard Verilator
  5. F6.5.2 Explain the Surviving Mutation 1200 Debug Medium Verilator
  6. F6.5.1 Kill the Data-Path Survivors 1500 Implement Hard Verilator

Formal Verification · F7

  1. F7.1.1 Map the Registers Each Property Can See 1200 Implement Medium Verilator
  2. F7.2.1 Close the FIFO Coverage Argument 1500 Verify Hard Verilator
  3. F7.3.1 Expose the Hidden Sign-Off Constraint 1500 Break It Hard Verilator
  4. F7.5.1 Review the Missing Depth Argument 1200 Debug Medium Verilator

Formal Verification · F8

  1. F8.1.1 Sign off a Four-Entry FIFO 1500 Verify Hard Verilator
  2. F8.1.2 Strengthen the FIFO Induction 1500 Optimize Hard Verilator
  3. F8.2.2 Find the Unfair Downstream 1200 Break It Medium Verilator
  4. F8.3.1 Implement a Sound Expiry Abstraction 1500 Implement Hard Verilator
  5. F8.4.1 Locate the Circular Handshake Wait 1200 Debug Medium Verilator
  6. F8.4.2 Repair the Four-Phase Handshake 1200 Fix Medium Verilator
  7. F8.5.1 One APB Contract on Both Sides 1500 Verify Hard Verilator
  8. F8.6.1 Forward the Newest Buffered Write 1500 Verify Hard Verilator
  9. F8.7.1 Check the Retired Register Value 1500 Implement Hard Verilator

Formal Verification · F9

  1. F9.1.1 Sign off the AXI4-Lite Register Block 1500 Verify Hard Verilator
  2. F9.1.2 Unmask the Capstone Response Bug 1500 Break It Hard Verilator
  3. F9.2.1 Prove Packet Routing End to End 1500 Verify Hard Verilator
  4. F9.2.2 Build the Router Packet Tracker 1500 Implement Hard Verilator
  5. F9.4.1 Five Traces at the Interview 1500 Debug Hard Verilator