MattHsu DAC SynthesizableConstra intSolver

Synthesizable Testbench Constraint Solver: Let’s See You Simulate This! : 

Synthesizable Testbench Constraint Solver: Let’s See You Simulate This! Matthew A. Hsu Consulting consulting@mhsu.com www.mhsu.com 408-439-8798

The Design: Synthesizable Constraint Solver : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 The Design: Synthesizable Constraint Solver The synthesizable constraint solver is a synthesizable testbench block that solves this problem: 25% of the time generate: 0 25% of the time generate: random( 10, 1) 50% of the time generate: random( 100, 11)

Algorithm: Two Randomizations Required : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 Algorithm: Two Randomizations Required First we must randomize a bin Use tables with locations 0 to 7 minTable and maxTable hold minimum and maximum values for each bin Randomize address from 1 to numValidEntries Next, must randomize between minimum and maximum value from tables Both randomizations require this solution random( M, N ) where M ≥ N Hard part is random is non-even power of 2

Block Diagram : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 Block Diagram 100 100 0 10 X X X X 11 11 0 1 X X X X address/data bus 3 minTable maxTable numValidEntries 0 LFSR LFSR Csolved

Random Core Inputs and Outputs : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 Random Core Inputs and Outputs Constraint Maximum Constraint Minimum Random Value Solution 16 16 16 16

The Math : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 The Math Csolved = (Cmax – Cmin) * $random / 2^16 + Cmin Where: Cmax – Cmin normalizes range to 0 $random / 2^16 is a fraction between 0 and 1 + Cmin shifts value back up within Cmax and Cmin Multiplier implemented with shift-accumulator Block takes number of cycles = highest set bit of Cmax – Cmin plus constant

How to Verify With Simulation? : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 How to Verify With Simulation? Given Cmax ≥ Cmin For all values of random all minimum constraint values all maximum constraint values Want to simply prove that Cmin ≤ Csolution ≤ Cmax

Problems with Simulation : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 Problems with Simulation It will take too long 2^16 * 2^ 16 * 2^16 combinations of inputs Even if you wrote a ‘C’ algorithm it would take too long The conditionals as easy, it’s the LFSR that gets you Then the multiplier gets you

Using Jasper : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 Using Jasper With default engines took overnight Finding the right engine, solved problem in 2 hours Found other problems while constructing constraints Needed to latch constraints Problem with reset

The Magic Constraint : 

DAC 2010 Matthew A. Hsu Consulting consulting@mhsu.com 408-439-8798 The Magic Constraint // hold valid until solve reg pending_valid; always @( posedge clock ) begin if ( reset ) pending_valid <= 1'b0; else if ( constraint_solve ) pending_valid <= 1'b1; else if ( constraint_valid ) pending_valid <= 1'b0; end // hold constraints constant reg [15:0] constraint1_reg; reg [15:0] constraint2_reg; always @( posedge clock ) begin if ( constraint_solve & ( ~pending_valid | constraint_valid ) ) begin constraint1_reg <= constraint1; constraint2_reg <= constraint2; end end // the property property value_within_constraints_P; @( posedge clock ) disable iff ( reset ) ( constraint_valid |-> ( ( constraint_value <= constraint2_reg && constraint_value >= constraint1_reg ) || ( constraint_value <= constraint1_reg && constraint_value >= constraint2_reg ) ) ); endproperty value_within_constraints_A : assert property( value_within_constraints_P );