ON THE REUSE OF RTL ASSERTIONS IN SYSTEMC TLM VERIFICATION Nicola Bombieri 1,2
Franco Fummi1,2, Graziano Pravadelli1,2, Valerio Garnieri1, Francesco Stefanni1, Tara
Ghasempouri2, Michele Lora2, Giovanni Auditore3, Mirella Negro Marcigaglia3
EDALab s.r.l.
Dip. Informatica, Università di Verona
3 STMicroelectronics s.r.l.
1
2
Mo#va#ons RTL IP reuse in SystemC TLM pla6orms • SystemC and TLM – SystemC is the de-‐facto reference standard language for design and verifica@on of Embedded Systems at system level – Transac@on-‐level Modeling is the key paradigm for design and verifica@on at high abstrac@on levels • RTL IP reuse – Libraries of RTL IPs are available today, already stressed and verified – RTL IPs are mainly implemented in Hardware Descrip@on Language (HDL), such as VHDL or Verilog • Design teams cannot oKen maintain double and equivalent implementa@ons of IPs (RTL and TLM) – IP models oKen undergo manual interven@ons for op@miza@on – Today, actually, op@miza@ons are done at RTL – Op@miza@ons over exis@ng and already verified IPs are s@ll expensive Automa7c RTL-‐TLM abstrac7on Mo#va#ons (contd.) IP verifica@on aKer abstrac@on • Exis@ng tools for automa@c RTL-‐TLM abstrac@on! • Exis@ng methodologies for verifying: – The abstracted TLM IP model – The TLM IP correct integra@on • Asser@on-‐based Verifica@on (ABV) What about exis#ng RTL IP asser#ons? CPU MEM Bus/NoC SystemC wrapper Checkers (C++) TLM IP (SystemC) Asser@on synthesis (IBM FoCs) RTL-‐TLM abstrac@on (Carbon Design, HIFSuite A2T) RTL IP (VHDL, Verilog) TLM pla6orm (SystemC) RTL asser@ons TLM asser@ons (ex-‐novo defini@on) Exis@ng IP and asser@on libraries 3 Goal: RTL asser@on reuse in SystemC TLM pla6orms CPU MEM Bus/NoC TLM IP RTL-‐TLM Abstrac@on (Carbon Design, HIFSuite A2T) RTL IP (VHDL, Verilog) TLM pla6orm (SystemC) SystemC wrapper Checkers (C++) Asser@on synthesis and integra@on (Proposed approach) RTL asser@ons Exis@ng IP and asser@on libraries Checkers (C++) Asser@on synthesis (IBM FoCs) TLM asser@ons (ex-‐novo defini@on) With the aim of: 1. Avoid error-‐prone, @me-‐consuming asser@on re-‐defini@on 2. Reuse verifica@on effort spent at RTL (for RTL asser@on defini@on) What happens to the TLM performance? 4 Limits of related work: Asser@on-‐based Verifica@on in SystemC TLM • ABV in SystemC TLM: – [Habibi-‐IEEE Trans.VLSI’06] First contribu@on for cycle-‐accurate TLM – [Ecker-‐IEEE ICCD’06,MEMOCODE’06,DATE’07] Proposal of specific asser@on language for SystemC TLM – [Lahbib-‐IEEE DTIS’06] IBM FoCs asser@on synthesis into SystemC TLM • Automa@c genera@on of checkers for ABV in SystemC TLM: – [Ferro-‐IEEE IDTL’08,FDL’09] • Formal tools for ABV in SystemC TLM: – [Grosse-‐IEEE MEMOCODE’10] • TLM asser@on reuse at RTL – [Bombieri-‐IEEE DATE’07, Kasuya-‐DAC’07, Pierre-‐CODES’13] No work for reusing RTL assertions in SystemC TLM
5 Methodology: genera7on of checkers from asser7ons and integra7on in the TLM model • Two ways: 1. Genera@on of HDL checkers, integra@on, and abstrac@on Checker #1 PSL RTL asser@ons Checker #2 TLM IP model with integrated checkers 3
1
Genera@on of HDL checkers RTL-‐to-‐TLM abstrac@on RTL IP model 2
Checker integra@on 2. Genera@on of C++ checkers, abstrac@on, and integra@on PSL RTL asser@ons cp1 1
Genera@on of C++ checkers RTL IP model TLM IP model with integrated checkers 2
RTL-‐to-‐TLM abstrac@on cp2 3
Checker integra@on 6 2: Automa#c RTL-‐to-‐TLM abstrac#on of IPs in1 ps1 in2 sig1 pa1 sig2 ps3 RTL model Clock Cycle i ps2 (δ-‐cycle 1) Falling edge (δ-‐cycle 0) sig3 ps4 Rising edge (δ-‐cycle 0) out2 Synchronous process Rising edge (δ-‐cycle 0) Asynchronous process Clock Cycle (δ-‐cycle 1) i+1 … Falling edge (δ-‐cycle 0) … “Synchronous” func@on Scheduling: ps1, ps2, ps3 , ps4 Execu@on: ps1, ps2, ps3 , ps4 Scheduling: pa1 Execu@on: pa1 … Scheduling: ps1, ps2, ps3 , ps4 Execu@on: ps1, ps2, ps3 , ps4 Scheduling: pa1 Execu@on: pa1 How the TLM scheduling works … Simula@on @me “Asynchronous” func@on fa1() fs4() fs3() How the HDL scheduling works fs2() fs1() scheduler{ rising_edge(); while(events_triggered) { delta_cycle(); } falling_edge(); while(events_triggered) { delta_cycle(); } TLM model 7 1. Genera#on of C++ checkers • Example of RTL assertion: An input A or B high is always followed
by output C high
-‐-‐ psl P1: assert always A or B -‐> next C@(clk’event and clk=‘1’); Generally clocked asser@ons A if then B if then if then C clk P1(){ … } Checker invoca@ons 8 3: C++ checkers integra#on in the TLM model TLM model fa1() fs4() P1() P2() fs3() fs2() fs1() Integra@on of checkers Genera@on of C++ checkers PSL asser@ons P1() P2() C++ checkers scheduler{ rising_edge(); while(events_triggered) { delta_cycle(); } falling_edge(); while(events_triggered) { delta_cycle(); } Less @me-‐
consuming than HDL checkers integra@on Less overhead introduced than HDL checkers 9 Some experimental results: 10 Some experimental results IP model Checkers (#) 0 UART 2 40 0 Root 2 40 0 Div 2 40 0 FDCT 2 40 0 QNR 2 40 0 RLE 2 40 0 JPEG 2 40 0 Error_corr. 2 40 0 Lambda_err 2 40 0 Omega-‐phy 2 June 6th 2013 40 RTL (s) 24,19 54,69 588,71 22,75 97,44 1.422,16 46,03 125,43 1.528,48 105,59 209,65 2.250,88 94,54 202,46 2.110,55 96,12 219,80 2.207,52 307,83 622,94 6.257,01 197,56 386,73 3.971,00 487,54 791,15 7.406,19 487,54 935,10 8.945,88 Overhead (%) TLM (s) Overhead (%)2 -‐ 11,61 -‐ 126,13 23,71 104,22 976,42 458,94 1.835,64 -‐ 19,94 -‐ 328,32 37,00 85,55 1.359,55 1.203,10 3.151,79 -‐ 20,79 -‐ 172,51 23,05 10,87 1.118,61 665,41 2.787,44 -‐ 18,57 -‐ 98,55 34,58 86,24 973,65 1.054,86 2.950,75 -‐ 12,09 -‐ 114,15 25,45 110,57 942,43 950,84 3.635,83 -‐ 12,99 -‐ 128,66 28,19 117,12 904,35 985,70 3.396,25 -‐ 42,02 -‐ 102,37 82,96 97,42 904,43 3.084,88 3.618,47 -‐ 34,77 -‐ 95,76 70,02 101,38 926,80 2.603,49 3.618,47 -‐ 69,13 -‐ 62,27 121,79 76,18 836,13 3.568,10 2.829,69 -‐ 80,94 -‐ 91,80 Automa@on 144,80 78,91 -‐ Design Conference (DAC) 856,67 3.978,45 2.647,53 2013 Speedup (x) 2,08 2,31 1,28 1,14 2,63 1,18 2,21 5,44 2,30 5,69 6,06 2,13 7,82 7,95 2,22 7,40 7,80 2,24 7,33 7,51 2,03 5,68 5,52 1,53 7,05 6,50 2,08 6,02 6,46 2,25 11 Conclusions • Key idea of the proposed method: – to recover RTL IP asser@ons and make them suitable for ABV in SystemC TLM pla6orms • Main contribu@ons: a two steps methodology – A checker generator is adopted to automa@cally generate run-‐@me checkers from exis@ng RTL asser@ons – Checkers are integrated in the TLM IP models • Observed results: – The overhead introduced by asser@ons (checkers) automa@cally generated through the proposed approach is comparable to the overhead introduced by asser@ons (checkers) manually defined. – The best results have been obtained with a limited number of asser@ons checked at TLM (10-‐15 per IP). More details and results offline. Thank you! 12
© Copyright 2024 ExpyDoc