View
40
Download
0
Category
Preview:
DESCRIPTION
Modeling Dynamically Reconfigurable Systems via Rewriting-Logic (modeling and simulation of the FFT in Optimal Space). - PowerPoint PPT Presentation
Citation preview
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
1
C. Llanos2,4 ,M. Ayala-Rincón1,4, R. B. Nogueira2,4, R. P. Jacobi3,4 and R. W. Hartenstein5,6
1 Departamentos de Matemática, 2 Engenharia Mecânica e 3 Ciência da Computação 4 Universidade de Brasília
5 Fachbereich Informatik, 6 Kaiserslautern University of Technology
2nd Dagsthul Seminar on Dynamically Reconfigurable Architectures
Dagsthul, Germany, July 20-25, 2003
Modeling Dynamically Reconfigurable Systems via Rewriting-Logic (modeling and simulation of the FFT in Optimal Space)
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
2
Overview(Arvind aproach)
Applying rewriting techniques in hardware design [Arvind et al]• specification of correct processors• Cache protocols over memory systems• Specification of digital circuits • Specification and verification of network
protocols
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
3
rewriting is neither applied for simulation nor for verification
Proposal Translate to Verilog!
Characteristic of Arvind’s approach
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
4
•Bejesse et al use Haskell (a functional language) for circuit design, specification and verification
•These ideas are implemented in LAVA system
•This approach shows how the high level abstraction of functional languages is suitable for hardware design
Overview (using Haskell)
Lava approach takes advantage of high level abstraction provided by functional languages
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
5
Kapur has used his well-known Rewriting Rule Laboratory - RRL for verifying arithmetic circuits
RRL is used to verify automatically properties of arithmetic hardware circuits (adders, multipliers, SRT division circuits)
Overview (Kapur Approach)
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
6
Rewriting is the formal framework of all functional languages
This fact allows us to work in more abstract levels
Rewriting assistant environments help in the task of formal verification of hardware
Why Rewriting?
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
7
l r if C
Rewriting Rule
left side right side
Rewriting Rules
Premise to be hold
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
8
Rewriting rules:
l r if C
Operational semantics:
a rule is applied to a term, when its left-side matches a sub-term, replacing the matched sub-term with the corresponding right-side of the rule. All that, whenever the premise C of the rule holds.
Rewriting
Premise to be hold
Semantic: “l is replaced by r if C is true”
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
9
Specifying Processors(Arvind’s proposal)
+1
RegisterFile
Int MemPC ALU
Data Mem
PROC(ia,rf,prog)
SYS(mem,Proc)
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
10
Specifying Processors
• Basic Processor– Single cycle, non pipelined, in-order execution
• SYS := Sys(MEM,PROC)• PROC := Proc(ia, rf, prog)
• AX ArchitectureInstruction set:
r:=Loadc(v) r:=Loadpc
r:=Op(r1,r2) Jz(r1,r2)
r:=Load(r1) Store(r1,r2)
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
11
Jz-jump-rule:
[Jz(r1, r2)]
Proc(ia, rf, prog) Proc(rf[r2], rf, prog)
Defining Instruction of the processor by rewriting rules
if im[ia] = jz(r1, r2) and rf[r1] = 0
Conditional jump
Rewriting rules can implement state transitions in the processor
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
12
Example: Euclid’s Algorithm for greatest common divisor (GCD)
GCD Mod Rule
Gcd(a, b) Gcd(a-b, b) if (a b) (b 0)
GCD Flip Rule
Gcd(a, b) Gcd (b, a) if a < b The term Gcd(6,15) can be reduced by applying the Mod and Flip rules
Flip Gcd(15,6) Mod Gcd (9, 6) Mod Gcd(3, 6)
Flip Gcd (6, 3)
Gcd(6,15)
Mod Gcd(3,3) Mod Gcd(3,0) Result!
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
13
Characteristic of Rewriting
Rules are applied non-deterministically
Controlling the execution of rules can be accomplished by logic
Rewriting-Logic = Rewriting Rules + Strategies
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
14
Examples of Rewriting Oriented Environments
ELAN:
Maude: •It’s necessary to do more effort for description
•it provides model checking useful for hardware verification
it has great flexibility for defining types and ease manipulation of strategies
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
15
Address registerAddress
register
functional Units
R2
Op2
R1C1
Op1
Ar1Ar2
P1 P2
Constant Register
Example of a Reconfigurable Architecture
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
16
**
ANDAND11 100100
R2
Op2
R1C1
Op1
Ar1Ar2
P1 P2
011 100
Example of Reconfigurable Architecture
At some time the
configuration can be
specified
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
17
const(@) : ( complexUnit ) Const; port(@) : ( complexUnit ) Port; reg(@) : ( complexUnit ) Reg; addr(@) : ( int ) Addr; @,@,@,@,@ : ( int Port Port Reg Reg ) fixMAC; @,@,@,@,@ : ( Addr Addr Const OpUnit OpUnit ) recMAC; [ @ # @ ] : ( fixMAC recMAC ) MAC;
**
ANDAND11 100100
R2
Op2
R1 C1
Op1
Ar1Ar2
P1 P2
011 100
Problem: how can this architecture be described in ELAN
Using and defining types It’s possible to describe fixed parts and reconfigurable ones
Describing Architectures in ELAN
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
18
Describing more Complex Architectures
@,@,@,@,@ : ( int Port Port Reg Reg ) fixMAC; @,@,@,@,@ : ( Addr Addr Const OpUnit OpUnit ) recMAC; [ @ # @ ] : ( fixMAC recMAC ) MAC; < @ @ @ @ @ @ @ @ @ @ > : ( int rArrayStruct MAC MAC MAC MAC MAC MAC MAC MAC )Proc;
R2
Op2
R1
C1
Op1
Ar1Ar2
P1
P2
R2
Op2
R1
C1
Op1
Ar1Ar2
P1
P2
R2
Op2
R1
C1
Op1
Ar1Ar2
P1
P2
Processor
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
19
< [0,port(cPort1),port(cPort2),reg(cReg1),reg(cReg2)# addr1,addr2,const(cConst1),op1,op2] >
< [0,port(cPort1),port(cPort2),reg(cRegRes1),reg(cRegRes2) # addr1,addr2,const(cConst1),op1,op2] >
How the Execution Process is described in the ELAN system
where cRegRes1 :=() operate(cPort1,cPort2,op1) where cRegRes2 :=() operate(cReg1,cConst1,op2)
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
20
[] reconfigure(MACsArray( [ fix0 # rec0 ] )
MACsArray([ fix0 # getRecMAC(MAConfig0) ] )
How the Reconfiguration Process is described in ELAN system
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
21
strategies for Proc implicit [] process input; repeat*(reconfiguration;propagation;execution); output end endUsing strategies for guiding the application of the rules
Strategies in ELAN allow to separate execution and reconfiguration steps
This approach allows a closer specification to transference register description (RTL Description)
Using Strategies in ELAN
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
22
a0
a4
a2
a6
a1
a5
a3
a7
b0
b1
b2
b3
b4
b5
b6
b7
Reconfiguration for FFT
Number of reconfiguration = ln(n) + 1
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
23
Interconnections in reconfiguration step 3
0 2 3 4 5 6 71
FFT in Optimal Space
MAC0
MAC1
MAC2
MAC3
MAC4
MAC5
MAC6
MAC7
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
24
< [0,port(cPort1),port(cPort2),reg(cRegRes1),reg(cRegRes2) # addr1,addr2,const(cConst1),op1,op2] [1,port(cPort3),port(cPort4),reg(cRegRes3),reg(cRegRes4) # addr3,addr4,const(cConst2),op3,op4] >
An Execution Rule for a pair of MACs
[MAC01]
< [0,port(cPort1),port(cPort2),reg(cReg1),reg(cReg2)# addr1,addr2,const(cConst1),op1,op2]
[1,port(cPort3),port(cPort4),reg(cReg3),reg(cReg4)# addr3,addr4,const(cConst2),op3,op4]
>
where cRegRes1 := () operate( cPort1,cPort2,op1 )
where cRegRes2 := () operate( cRegRes1,cConst1,op2 )
where cRegRes3 := () operate( cPort3,cPort4,op3 )
where cRegRes4 := () operate( cRegRes3,cConst2,op4 )
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
25
A Reconfiguration Rule for a pair of MACs
< [ fix0 # addr(0),addr(2),const( < 1,0000 0,0000 > ), < + >,< * > ]
[ fix1 # addr(1),addr(3),const( < 1,0000 0,0000 > ), < + >,< * > ] >
[reconfiguration]
<
[ fix0 # rec0 ]
[ fix1 # rec1 ]
>
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
26
A Pipelined Reconfigurable FFT(eliminating the reconfiguration overhead)
Reconfigurable Interconnection Network
Reconfigurable Interconnection Network
While one Mac array is being reconfigured the other array is computing one step of FFT
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
27
ELAN has the advantage of an embedded inference engine
a flexible type definition mechanism (data and operators)
a powerful manipulation of typed expressions through rules
and meta-rules
the availability of logical strategies to control their
application.
Advantages of ELAN Environment
Modeling DRS via Rewriting-Logic, 2nd Dagstuhl Seminar on Dynamically Reconfigurable Systems
28
Conclusions
The high abstraction of Rewriting Environments makes design exploration easier
Using ELAN is possible to simulate the description of the architecture
Descriptions in ELAN are close to the physical architecture
Recommended