Verification Methodology Based on Algorithmic State

Report
Verification Methodology Based on
Algorithmic State Machines and
Cycle-Accurate Contract Specifications
Sergey Frenkel1 and Alexander Kamkin2
1Institute
of Informatics Problems of the Russian Academy of Sciences
E-mail: [email protected]
2Institute for System Programming of the Russian Academy of Sciences
E-mail: [email protected]
Design Steps

Architectural and RTL Design
Input: architectural (behavioral) description in HDL (Verilog,
VHDL) or system-level language (SystemC, SystemVerilog)
Output: RTL description of the design:
 data path (interconnection of adders, multipliers, etc.)
 control logic (FSM model of a control unit)

Logic Synthesis
Input: RTL description of the design
Output: gate-level description of the design

Physical Design
Out of our consideration
2
General Scheme of Design Verification
Design
Specification
Implementation
Verifier
Yes
Correct
Implementation
No
Incorrect
Implementation
3
Challenges of Design Verification
50-80% of ASIC / IP / SoC design effort goes to verification,
what has effects on Schedule, Cost, Quality




computational complexity of formal verification is prohibited for
many real-life designs
simulation is slow, requires billions of vectors for large designs, and
exhaustive simulation is infeasible
the verification tools and methods need to scale well, and be able to
support efficient debugging, have to allow for ongoing changes in
the specification and the design
the methodology must be flexible enough to permit new design
features, such as soft error detection, including fault latency and
self-healing analysis
4
Total Design Cost Reducing
A work of a designer is resulted in two or three activities
and human/equipment resources which have been spent
for one of them should be kept back in another
5
Two Ways of Design Verification (RTL)
Formal Verification
Verification Via Simulation
Formal Verification
Verification
Verification via Simulation
6
Possible Combination of the Verification
Approaches

a “mechanical” combination of the verification techniques:
part of design is verified by simulation, while another by a
formal method

by using of formal specification for simulation verification

by using a semi-formal specification
7
Semi-Formal Verification
Informal Specification
Formal Specification
Formal Verification
Verification via Simulation
Verdict: Pass or Fail
8
Cycle-Accurate Contract Specifications
Operation
Operations
pre(A)
Contracts of stages
AAA111
pre(A, 1)
post(A, 1)
…
…
…
…
…
…
AAANNN
pre(A, N)
post(A, N)
Contract
Contractsofof
operation
operations
9
Idea of the Method
A2
…
AN
Operation B
B1
B2
…
BN
Test Oracle
post(A, 2)  post(B, 1)
…
Time
Operation A
A1
1
2
3
10
Branching and Other Features
A
— stage
— branch
B
— fork
— join
C
11
Algorithmic State Machine (ASM)
An Algorithmic State Machine (ASM) is the directed connected graph
containing an initial vertex (Begin), a final vertex (End) and a finite set of
operators and conditional vertices.
The operators and conditional vertices have only one input, the initial vertex
has no input. Initial and operator vertices have only one output, a conditional
vertex has two outputs marked by “1” and “0”. A final vertex has no outputs.
Each operator include some body in a pseudo-code, and its execution takes a
clock of the target system time
The following are the major steps in the ASM methodology:
 Describe the target system algorithm by ASM chart (using a pseudo-code)
 Design the data path based on the ASM chart
 Design the control logic based on the detailed ASM chart
12
ASM Example

Let us an operator Yb be implemented. The sequence of the actions after Yb can be
represented by ASM as following:

The operator Y3 is executed after Yb when x1x4x3=1,Y1 is executed afterYb when
x1x’3=1, Y5 is excuted after Yb when x1x4x’3=1 or x’1=1, that is:
Yb→ x1x4x3Y3 + x1x4x'3Y5 + x1x'4Y1 + x'1Y5
Yb
Begin
0
x1
1
x4
1
Y5
y1 y 3
0
0
x3
1
x3
1
x1
1
Y1
Y4
y8 y9
0
0
y5 y6 y7
x5
1
y1 y2
x2
1
Y3
0
Y2
0
Y6
y6 y7
y4
x6
1
0
Ye
End
13
System/Logic Design by Abelite
(Prof. Samary Baranov, Holon Institute of Technology, Israel)
ASM-description
I1
I2
In
Micro
operations
FSM
FSM
Joint ASM
Flow Chart
RTL (VHDL)
Design Tools
(SYNOPSIS,CADENCE)
14
About ASM Formalities
A possibility to use some ASM-based formalized verification is due to
some formal rules, used for ASM flowchart construction. Namely, to
provide this unique correspondence between the ASM flowchart and a
target data path and control unit it is enough that a synthesis algorithm
would obey the following rules:





State boxes should contain only register statements, control signals in
parentheses
All operations within a state box should be concurrently executable in one
clock cycle
If the operations in two consecutive state boxes can be executed in the
same clock cycle, then these two state boxes can be combined into one
state box
For each register-transfer statement, there must be a path between the
source and destination registers
The description contains the ordering of microoperations, namely, each of
rectangle take one clock for its execution
15
Suggested Design Verification Methodology
No
Properties
(CTL)
Model
Checking
OK?
FSM
Informal Specification
of the Design
Yes
ASM Flowcharts
HDL
Model
Contract
Specifications
CTESK Testbench
Simulation
16
Design Verification Methodology (cont.)
Formal Verification
Behavioral Description
in a verification language (SMV)
Temporal properties
of the system to verify
RUN
17
Temporal Logic (CTL)
Temporal logic expresses the ordering of events in time by
means of operators that specify properties






“E”
“A”
“X”
“F”
“G”
“U”
existential path quantifier
universal path quantifier
next time
eventually
globally
until
18
Verification via Model Checking
FINITE-STATE
SYSTEM
PROPERTY
TO VERIFY
MODEL
CHECKING
PROGRAM
propagates sets
of states, not
individual
trajectories
PROPERTY IS TRUE OR
A COUNTER EXAMPLE
19
A Fragment of ASM Operation Hierarchical Description
20
ASM-Specified Model Checking (3-bit counter)
a1
a2
a3
a4
a5
a6
a7
a8
a9
a10
a10
a3
a1
a2
a4
a7
a8
a5
a6
a9
1
1
1
1
1
1
1
1
1
1
y7y8y9y10y11y12
y2y3
y4
y1
y4
y4
y1
y5y3
y6y3
y1
Micro Instructions:
Y1 = y1
Y2 = y2 y3
Y3 = y4
Y4 = y5 y3
Y5 = y6 y3
Y6 = y7 y8 y9 y10 y11 y12
Micro Operations:
y1 : v:=(v+c_in)mod 2
y3 : c_out:=v&c_in
y4 : c_in:=c_out
y5 : b1:=v
y6 : b0:=v
y7 : b0:=0
y8 : b1:=0
y9 : b2:=0
y10 : c_in:=1
y11 : c_out:=0
y12 : v:=0
21
Model Checking (cont.)
Conditions of Natural Ordering of Counting
SPEC AG (((bit0=0)&(bit1=1) &(bit2=0)) ->AX((bit0=1)&(bit1=1)&(bit2=0)))
SPEC AG (((bit0=0)&(bit1=1) &(bit2=0)) ->AX((bit0=1)&(bit1=1)&(bit2=1)))
22
Conclusion

An approach that is a combination of ASM-based and contractbased approaches to hardware designs semi-formal verification is
introduced

The approach allows to unify benefits of both formal and simulationbased methods for complex digital hardware designs verification at
early designing stages

Presently there are some examples of this approach application to
verification tests designing for one of unit of MIPS64-compatible
microprocessor

The approach allows to describe complex digital hardware with
pipelining, interlocks, branching, etc.
23
Thank You!
24

similar documents