Transcription
3. Finite StateMachinesGisselquistTechnology, LLCDaniel E. Gisselquist, Ph.D.
Lesson OverviewŹ Lesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionWhat is a Finite State Machine? Why do I need it? How do I build one? ObjectivesLearn the concatenation operator Be able to explain a shift register To get basic understanding of Finite State Machines To learn how to build and use Finite State Machines 2 / 51
Shift RegisterLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹThe concatenation operatoralways @ ( posedge i clk )o led { o led [ 6 : 0 ] , o led [ 7 ] } ;Composes a new bit-vector from other pieces3 / 51
Shift RegisterLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹThe concatenation operatoralways @ ( posedge i clk )o led { o led [ 6 : 0 ] , o led [ 7 ] } ;Simplifies what otherwise would be quite painfulalways @ ( posedgebegino led [ 0 ]o led [ 1 ]o led [ 2 ]o led [ 3 ]o led [ 4 ]o led [ 5 ]o led [ 6 ]o led [ 7 ]endi clk ) o led [ 7 ] ;o led [ 0 ] ;o led [ 1 ] ;o led [ 2 ] ;o led [ 3 ] ;o led [ 4 ] ;o led [ 5 ] ;o led [ 6 ] ;4 / 51
Shift RegisterLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionA shift register shifts bits through a registerŹ Can shift from LSB to MSBalways @ ( posedge i clk )o led { o led [ 6 : 0 ] , i input } ; or from MSB to LSBalways @ ( posedge i clk )o led { i input , o led [ 7 : 1 ] } ;5 / 51
Shift RegisterLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionYou can use this to create a neat LED display as wellŹ You just need to mix the shift registeri n i t i a l o led 8 ’ h1 ;always @ ( posedge i clk )i f ( stb )o led { o led [ 6 : 0 ] , o led [ 7 ] } ; With a counter to slow it downreg[ 2 6 : 0 ] counter ;regstb ;i n i t i a l { stb , counter } 0 ;always @ ( posedge i clk ){ stb , counter } counter 1 ’ b1 ; stb here is a strobe signal. A strobe signal is true for oneclock only, whenever an event takes place6 / 51
Shift RegisterLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionYou can use this to create a neat LED display as wellŹ You just need to mix the shift registeri n i t i a l o led 8 ’ h1 ;always @ ( posedge i clk )i f ( stb )o led { o led [ 6 : 0 ] , o led [ 7 ] } ; With a counter to slow it downreg[ 2 6 : 0 ] counter ;regstb ;i n i t i a l { stb , counter } 0 ;always @ ( posedge i clk ){ stb , counter } counter 1 ’ b1 ; Note that you can assign to a concatenation as well7 / 51
WavedromLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹIf you’ve never seen Wavedrom, it is an awesome tool!Here’s a waveform description of our shift registeri n i t i a l o led 8 ’ h1 ;always @ ( posedge i clk )o led { o led [ 6 : 0 ] , o led [ 7 ] } ;What would it take to make the LED’s go back and forth?8 / 51
LED WalkerLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹLet’s build an LED walker! Active LED should walk across valid LED’s and backWe’ll assume 8 LEDsShift registers don’t naturally go both waysOnly one LED should be active at any time One LED should always be active at any given time Most of this project can be done in simulation9 / 51
WavedromLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionHere’s a waveform description of what I want this design to doŹ This “goal” diagram can help mitigate complexity10 / 51
Tikz-TimingLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionTikz-timing also works nicely for LATEX usersŹooooooooi ]Our goal will be to create a design with these outputs If successful, you’ll see this in GTKwave 11 / 51
The NeedLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹWere we building in C, this would be our programw h i l e (1) {o led o led o led // .o led o led // .o led o led }0 x01 ;0 x02 ;0 x04 ;0 x80 ;0 x40 ;0 x04 ;0 x02 ;How do we turn this code into Verilog?12 / 51
Case StatementLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹWe could use a giant cascaded if statementalways @ ( posedge i clk )i f ( o led 8 ’ b0000 0001 )o led 8 ’ h02 ;e l s e i f ( o led 8 ’ b0000 0010 )o led 8 ’ h04 ;e l s e i f ( o led 8 ’ b0000 0100 )o led 8 ’ h08 ;e l s e i f ( o led 8 ’ b0000 1000 )o led 8 ’ h08 ;// . . .// Don ’ t f o r g e t a f i n a l e l s e !e l s e // i f ( o l e d 8 ’ b 0 0 0 0 0 0 1 0 )o led 8 ’ h0113 / 51
Case StatementLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹWe could use a giant case statementalways @ ( posedge i clk )case ( o led )8 ’ b0000 0001 : o led 8 ’ h02 ;8 ’ b0000 0010 : o led 8 ’ h04 ;// . . .8 ’ b0010 0000 : o led 8 ’ h40 ;8 ’ b0100 0000 : o led 8 ’ h80 ;8 ’ b1000 0000 : o led 8 ’ h40 ;// . . .8 ’ b0000 0100 : o led 8 ’ h02 ;8 ’ b0000 0010 : o led 8 ’ h01 ;d e f a u l t : o led 8 ’ h01 ;endcaseCan anyone see a problem with these two approaches?14 / 51
The NeedLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹA better way: Let’s assign an index to each of these outputs// . . . u s i n g C n o t a t i o n a g a i no led 0 x01 ;// 1o led 0 x02 ;// 2o led 0 x04 ;// 3// . . .o led 0 x80 ;// 8o led 0 x40 ;// 9// . . .o led 0 x04 ;// 13o led 0 x02 ;// 14In software, you might think of this as an instruction address15 / 51
Tikz-TimingLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionHere’s what an updated waveform diagram might look likeooooooooŹi led[7]0123456789101112130123Our goal will be to create a design with these outputs If successful, you’ll see this in GTKwave 16 / 51
The NeedLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹWe can now set the result based upon the instruction addressalways @ ( posedge i clk )case ( led index )4 ’ h0 :o led 8 ’ h01 ;4 ’ h1 :o led 8 ’ h02 ;4 ’ h2 :o led 8 ’ h04 ;// . . .4 ’ h7 :o led 8 ’ h80 ;4 ’ h8 :o led 8 ’ h40 ;// . . .4 ’ hc :o led 8 ’ h02 ;4 ’ hd :o led 8 ’ h01 ;d e f a u l t : o led 8 ’ h01 ;endcase This is an example of a finite state machine17 / 51
The addressesLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹAll we need now is something to drive the instruction address This is known as the state of our finite state machinei n i t i a l led index 0 ; // Our ” s t a t e ” v a r i a b l ealways @ ( posedge i clk )i f ( led index 4 ’ d13 )led index 0 ;elseled index led index 1 ’ b1 ;18 / 51
SimulationLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionGo ahead and simulate this designDoes it work as intended? Did we miss anything? Ź19 / 51
Finite State MachineLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite StateMachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionA finite state machine consists of. . .Inputs State Variable, Finite means there are a limited number of states OutputsŹ20 / 51
Finite State MachineLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite StateMachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹA finite state machine consists of. . .Inputs // we didn’t have any State Variable, // led index , or addr Finite means there are a limited number of states Outputs // o ledKeep it just that simple.20 / 51
SimpleLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹState machines are conceptually very simple We’ll ignore the excess math here Two classical FSM formsMealy Moore Two implementation approachesOne process Two process 21 / 51
MealyLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹOutputs depend upon the current state plus inputsalways @ ( )i f ( ! i display enable )o led 0 ;elsecase ( led index )4 ’ h1 : o led 8 ’ h01 ;4 ’ h2 : o led 8 ’ h02 ;4 ’ h3 : o led 8 ’ h04 ;4 ’ h4 : o led 8 ’ h08 ;// . . .endcase22 / 51
MooreLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹOutputs depend upon the current state only// Update t h e s t a t ealways @ ( posedge i clk )enabled i display enable ;// C r e a t e t h e o u t p u t salways @ ( )i f ( ! enabled )o led 0 ;elsecase ( led index )4 ’ h1 : o led 8 ’ h01 ;4 ’ h2 : o led 8 ’ h02 ;// . . .endcaseThe inputs are then used to determine the next state23 / 51
One Process FSMLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne ProcessFSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionA one process state machine Created with synchronous always block(s)i n i t i a l led index 0 ; // Our ” s t a t e ” v a r i a b l ealways @ ( posedge i clk )begini f ( led index 4 ’ he )led index 0 ;elseled index led index 1 ’ b1 ;Źcase ( led index )4 ’ h0 : o led 8 ’ h01 ;// . . .endcaseend24 / 51
Two Process FSMLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo ProcessFSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹTwo Process FSM uses both synchronous and combinatorial logicalways @ ( )begini f ( led index 4 ’ he )next led index 0 ;elsenext led index next led index 1 ’ b1 ;case ( led index )4 ’ h0 : o led 8 ’ h01 ;// . . .endcaseendalways @ ( posedge i clk )led index next led index ;25 / 51
Which to use?Lesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionPick whichever finite state machine form . . . . . . you are most comfortable withThere is no right answer hereŹ26 / 51
Which to use?Lesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionPick whichever finite state machine form . . . . . . you are most comfortable withThere is no right answer herebut people still argue about it! Tastes great Less FillingI tend to use one process FSM’sŹ26 / 51
Formal VerificationLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?FormalVerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionFormal Verification is a process to prove your design “works”Fairly easy to use Can be faster and easier than simulation Most valuable ––Early in the design processFor design components, and not entire designsŹ27 / 51
Formal VerificationLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?FormalVerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionFormal VerificationYou specify properties your design must have A solver attempts to prove if your design has them If the solver fails –– It will tell you what property failedBy line numberIt will generate a trace showing the failureThese traces tend to be much shorter than simulation failuretracesŹ28 / 51
AssertionLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionThe free version of Yosys supports immediate assertionsTwo types Clocked – only checked on clock edges// Remember how we o n l y// u s e d some o f t h e s t a t e s ?always @ ( posedge i clk )a s s e r t ( led state 4 ’ d13 ) ; Combinational – always checkedalways @ ( )a s s e r t ( led state 4 ’ d13 ) ;Ź29 / 51
SymbiYosysLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹTo verify this design using SymbiYosys, You’ll need a script[ options ]mode prove[ engines ]smtbmc[ script ]read formal ledwalker . v# . . . o t h e r f i l e s would go h e r eprep top ledwalker[ files ]# L i s t a l l f i l e s and r e l a t i v e p a t h s h e r eledwalker . v30 / 51
Three Basic FV ModesLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusion1.BMC (Bounded Model Checking)[ options ]mode bmcdepth 20Examines the first N steps (20 in this case) . . . looking for a way to break your assertion(s) Can find property (i.e. assert) failures An assert is a safety property –Succeeds only if no trace can be found that makesany one of your assertions failŹ31 / 51
Three Basic FV ModesLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹ1.2.BMC (Bounded Model Checking)Cover[ options ]mode coverdepth 20Examines the first N steps (20 in this case) . . . looking for a way to make any cover statement pass always @ ( posedge i clk )cover ( led state 4 ’ he ) ;No trace will be generated if no way is found cover is a liveness property Succeeds if one trace, any trace, can be found tomake the statement true32 / 51
Three Basic FV ModesLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusion1.2.3.BMC (Bounded Model Checking)CoverFull proof using k-induction[ options ]mode provedepth 20Examines the first N steps (20 in this case) Also examines an arbitrary N stepsstarting in an arbitrary state The induction step will ignore your initial statementsCorrect functionality must be guaranteed using assertstatementsŹCan prove your properties hold for all time This is also a safety property check 33 / 51
Example propertyLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹAssert the design can only contain one of eight outputsalways @ ( )beginf valid output 0 ;case ( o led )8 ’ h01 : f valid output 8 ’ h02 : f valid output 8 ’ h04 : f valid output 8 ’ h08 : f valid output 8 ’ h10 : f valid output 8 ’ h20 : f valid output 8 ’ h40 : f valid output 8 ’ h80 : f valid output endcasea s s e r t ( f valid output ) ;end1 ’ b1 ;1 ’ b1 ;1 ’ b1 ;1 ’ b1 ;1 ’ b1 ;1 ’ b1 ;1 ’ b1 ;1 ’ b1 ;34 / 51
It doesn’t workLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionIf you try implementing this design as it is now,You’ll be disappointed All the LED’s will light dimlyThe LED’s will toggle so fast you cannot see them change We need a way to slow this down.Ź35 / 51
Integer Clock DividerLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹYou may remember the integer clock divider Let’s use it herealways @ ( posedge i clk )i f ( wait counter 0 )wait counter CLK RATE HZ 1;elsewait counter wait counter 1 ’ b1 ;always @ ( posedge i clk )beginstb 1 ’ b0 ;i f ( wait counter 0 )stb 1 ’ b1 ;end36 / 51
Integer Clock DividerLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹThis wait counter is limited in rangeIt will only range from 0 to CLK RATE HZ 1 Don’t forget the assertion that wait counter remains inrange! always @ ( posedge i clk )a s s e r t ( wait counter CLK RATE HZ 1);If your state variable can only take on some values, alwaysmake an assertion to that affect Let’s also make sure the stb matches the wait counter tooalways @ ( posedge i clk )a s s e r t ( stb ( wait counter 0 ) ) ;37 / 51
Integer Clock DividerLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionNow we can use stb to tell us when to adjust our statei n i t i a l led index 0 ;always @ ( posedge i clk )i f ( stb )begin// The l o g i c i n s i d e i s j u s t//what i t was b e f o r e// Only t h e i f ( s t b ) changedi f ( led index 4 ’ d13 )led index 0 ;elseled index led index 1 ’ b1 ;end // e l s e n o t h i n g c h a n g e s// w a i t f o r s t b t o be t r u e b e f o r e c h a n g i n g s t a t eŹ38 / 51
ExerciseLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionTry out the tools1.Recreate this waveform using WavedromŹ39 / 51
ExerciseLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionTry out the tools1.2.Recreate this waveform using WavedromSimulate this design printf o led anytime it changes Look at the trace in gtkwaveDoes it match our design goal?Don’t forget to slow it down!Ź39 / 51
ExerciseLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionTry out the tools1.2.3.Recreate this waveform using WavedromSimulate this designRun SymbiYosysDoes this design pass?If it passes, try assert(led index 4);Examine the resulting waveformŹ40 / 51
ExerciseLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionTry out the tools1.2.3.Recreate this waveform using WavedromSimulate this designRun SymbiYosysDoes this design pass?If it passes, try assert(led index 4);Examine the resulting waveformLet’s do this one togetherŹ40 / 51
Running VerilatorLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusion% verilator - Wall - cc ledwalker . v% Error : ledwalker . v :61: Can ’ t find definitionof variable : o leed% Error : Exiting due to 1 error ( s )% Error : Command Failed / usr / bin / verilator bin- Wall - cc ledwalker . v%Oops, we misspelled o led in our case statement We also forgot to start our file with ‘default nettype none Once fixed, we pass the Verilator check % verilator - Wall - cc ledwalker . v%Ź41 / 51
Running SymbiYosysLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusion% sby -f ledwalker . sbyAnother syntax error, mislabeled led index as led state Let’s try again Ź42 / 51
Running SymbiYosysLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹ% sby -f ledwalker . sbyIt failed, but how? Need to scroll up for the details43 / 51
Running SymbiYosysLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionFail in line 96 Trace file in ledwalker/engine 0/trace.vcd Open this in GTKWave, compare to line 96 Ź44 / 51
Running SymbiYosysLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusion See the bug?Ź45 / 51
Running SymbiYosysLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionSee the bug? o led starts at 8’h00 We never initialized o led to a valid value initial o led 8’h01; fixes this Ź45 / 51
Running SymbiYosysLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionŹSame trace file name Assertion failed in line 72 46 / 51
Running SymbiYosysLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusion if (led index 4’d12) in line 39 fixes thisŹ47 / 51
Cover PropertyLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionLet’s add a quick cover propertyalways @ ( )cover ( ( led index 0)&&(o led 4 ’ h2 ) ) ;Ź48 / 51
ExerciseLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionYour turn! Use the tools to modify the design1.2.3.4.Recreate this waveform using WavedromSimulate this designRun SymbiYosysRun your device’s Synthesis tool Make sure your design . . .––5.Passes a timing checkFits within your deviceNow repeat with the clock dividerŹ49 / 51
BonusLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionBonus: If you have hardware and more than one LEDAdjust this design for the number of LEDs you have Implement this on your hardwareDoes it work? Ź50 / 51
ConclusionLesson OverviewShift RegisterWavedromLED WalkerWavedromThe NeedCase StatementThe NeedThe addressesSimulationFinite State MachineSimpleMealyMooreOne Process FSMTwo Process FSMWhich to use?Formal VerificationAssertionSymbiYosysInteger ClockDividerExerciseConclusionWhat did we learn this lesson? What a Finite State Machine (FSM) isWhy FSM’s are necessaryVerilog case statementVerilog cascaded ifFormal assert statementHow to run SymbiYosysHow to run slow down an FSMVerilog is fun!Ź51 / 51
Finite State Machine Lesson Overview Shift Register Wavedrom LED Walker Wavedrom The Need Case Statement The Need The addresses Simulation Ź Finite State Machine Simple Mealy Moore One Process FSM Two Process FSM Which to use? Formal Verification Assertion SymbiYosys Integer Clock Divider Exercise Conclusion 20 / 51 A finite state machine .
