Model-Based Design for Embedded Systems- P14

Chia sẻ: Cong Thanh | Ngày: | Loại File: PDF | Số trang:30

Thêm vào BST

Báo xấu

72
lượt xem 4
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Model-Based Design for Embedded Systems- P14:The unparalleled flexibility of computation has been a key driver and feature bonanza in the development of a wide range of products across a broad and diverse spectrum of applications such as in the automotive aerospace, health care, consumer electronics, etc.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Model-Based Design for Embedded Systems- P14

366 Model-Based Design for Embedded Systems PLB bus LocalLink PLB Slave write buffer PLBv46 bus PLBv46 buffer master Slave Control bus interface LocalLink burst read buffer Interrupt request Bridge control Reset Interrupt Control logic Control logic generation bus bus DCR Bridge status signals bus Reset Reset request DCR Bus macro enable Reconfigured region slave Reconfigurable socket FIGURE 12.7 Reconfigurable socket abstraction based on the “PLBv46 PLBv46 bridge” architecture. The “PLBv46 slave” and “PLBv46 master burst” blocks are stan- dard IP components and all blocks except the DCR slave block are part of the bridge. Bus macros are implicitly present on all signals crossing the bound- ary of the reconfigured region. An alternative is to architect the interface around a bus bridge, with inde- pendent busses in the static region and in the reconfigurable region. The design of the socket is based on partitioning the Xilinx “PLBv46 PLBv46 bridge” IP [23], as shown in the block diagram in Figure 12.7. Internally this core is based around 32-bit fixed-width data FIFOs and a small number of control signals. Most of the bridge is treated as part of the static region, with only a small amount of logic required in the reconfigurable region to com- plete the bridge. In addition to the bus interface, which is primarily used to interface to the reconfigured region, the socket core also contains a control interface (based on the DCR protocol [7]) which is used to generate an inde- pendent reset signal to the reconfigurable region and to force signals driven by the reconfigurable module to stable values during reconfiguration. 12.5.3 Direct Memory Access Interfaces The bus interface above is a generic and flexible interface, which can be used to communicate with the reconfigured portion of the system in different ways. For instance, it may be used by the processor to both send and receive data from the reconfigured region or as a control interface to set parame- ter values of IP cores executing in the reconfigured region. However, it does have several disadvantages. Primarily, the bandwidth of data to or from the
FPGA Platforms for Embedded Systems 367 processor is limited because of the overhead of bus arbitration and the fact that the memory range is treated as uncached I/O transactions. Although performance could be improved somewhat for large transactions by using DMA engines or treating data transfer regions as cached and manually man- aging cache coherency, this would significantly increase the complexity of the processor software. Secondly, many FPGA algorithms require access to external memory for buffering data until it can be processed. For instance, in a network router, packet data may need to be stored until a routing decision can be made, or in a streaming video system, several frames of video data may need to be stored to analyze object motion between frames. Because of these limitations, it is best to consider the bus interface above as primarily an interface used for low-bandwidth control and configuration information. In systems that require higher bandwidth communication, or direct access to external memory, the control interface can be augmented with additional interfaces to memory. Although it may seem straightforward to include a complementary bus bridge that can be driven by the reconfig- ured region to provide this functionality, this tends not to be the highest bandwidth option since performance can be limited by the arbitration logic of the PLB bus. This logic is heavily pipelined in order to maximize the bus throughput under a wide variety of usage, typically incurring three cycles of latency before a slave can respond to a bus access. One solution is to provide an interface connected directly to the native port interface (NPI) of the Xilinx MPMC IP core, as shown in Figure 12.8. PIM PIM FIFO FIFO Arbiter Multiported memory Physical interface controller External memory (e.g., DDR/DDR2) FIGURE 12.8 Architecture of the Xilinx MPMC.
368 Model-Based Design for Embedded Systems Typically, this interface exhibits both lower latency and higher bandwidth than the PLB bus. Although the MPMC must still arbitrate between different ports attempting to use the memory controller, this arbitration can be per- formed locally within the memory controller and concurrently with the data being provided. The only disadvantage of connecting directly to the mem- ory controller is that other IP cores in the static region cannot be accessed from the reconfigured region. However, since in the SRP usage model these IP cores are likely being managed by device drivers in the operating system of the processor, it is questionable whether such access should be allowed anyway. 12.5.4 External Interfaces In addition to communicating with the static region, a reconfigurable mod- ule may also communicate with other interfaces external to the FPGA. In order to accomplish this, a reconfigurable region may include external I/O pins and/or high-speed serial transceivers. For the most part, these resources can be treated as any other FPGA primitives and can be placed and routed as usual. However, there is some complexity with regard to external I/O pins, since in many FPGA designs, the input/output buffer (IOB) primitives rep- resenting external I/O pins are not explicitly instantiated in a user design but are inferred in the synthesis process. Normally in a hierarchical design, the netlist can be synthesized using a special option to disable inference of these primitives, since they will be inferred or instantiated during synthesis of the toplevel design. However, when building a generic FPGA platform, relying on this may not be desirable, since the reconfigured region may require more control over the configuration of these primitives. In other cases, exactly which IOB primitives are explicitly instantiated in a reconfigurable module and which ones are not may not be known when the static design is synthe- sized and implemented. One way to solve this is to not expose any I/O pins of the reconfigurable region as external signals of the static region, implying that synthesis of the static design will never include IOB primitives for these pins. When a reconfigurable module is synthesized, signals interfacing with the static region are individually tagged with the constraint BUFFER_TYPE set to NONE, indicating that no IOB primitives should be inferred for those signals. High-speed serial transceivers also have additional design complexity, since each transceiver is associated with specialized clock resources in the FPGA. These clock resources typically include phase-locked loops for clock synchronization and dedicated clock distribution paths and may be shared between transceivers. From the perspective of building FPGA platforms, this resource sharing combined with how transceivers are grouped into configu- ration frames may need to be considered during the floorplanning stage in order to gain maximum usage of the available transceivers.
FPGA Platforms for Embedded Systems 369 Static design flow Module design flow EDK base Hand system builder design + hand design EDK .mhs .ucf .ucf hand design EDK Floor- UCF .mhs platgen planning merge EDK BSP EDK generator .ngc .ucf .ucf platgen .dts .ngc PR-enabled NGDBuild, PR-enabled Map, and PAR NGDBuild, .ncd static.used Map, and PAR Linux .ncd design PR-enabled PRMergeDesign + flow bitgen PR-enabled bitgen .elf Meta-information .bit C code partial.bit .bit EDK genace.tcl gcc + EDK objcopy genace.tcl static.ace configure.elf merged.ace FIGURE 12.9 Design flow for PR systems based on EDK. 12.5.5 Implementation Flow The implementation flow for the system is shown in Figure 12.9. The static design is implemented first, as shown in the left-hand side of the figure, using the EA PR tools. During this sequence, no netlist for the reconfigurable region is present, and the place and route tools only implement logic for the static region. Design constraints are provided in a .ucf file and must include the required floorplanning constraints for the PR flow. After routing is com- pleted, the routing resources used by the static logic are saved in the file static.used for later use. Since by default the interface with the reconfigured region is driven to an idle state, the resulting bitstream can be used in a sys- tem without programming the remainder of the FPGA. The device tree for a particular design is generated from the EDK design, and after being con- verted to a binary device tree blob, can be included in the Linux kernel image, or stored as the initial value of a BRAM in the bitstream. Lastly, EDK is used to package the FPGA bitstream with the Linux kernel binary in a bootable image that can be used with Xilinx SystemAce [24] to boot the kernel. The right-hand side of Figure 12.9 shows a second pass for the imple- mentation of a reconfigurable module. During this pass, the logic of the
370 Model-Based Design for Embedded Systems reconfigurable module is implemented together with a small portion of the static logic called the “context logic.” The context logic is necessary to pro- vide the context of the reconfigurable module, so that hierarchical names in the design and location constraints for clock signals and bus macros can be preserved. The design constraints for implementation are created by merging the design constraints from the static design with any additional design constraints specific to the reconfigurable module, such as pin loca- tion constraints. During this pass, the routing resources in the file static.used are excluded from use, since these resources are already used in the static design. The final bitstream for the reconfigurable module is generated by first merging the design database (contained in an .ncd file) from both passes, ensuring that the configuration bits used in the static design are pro- grammed correctly. In addition, design rule checks and timing analysis can be applied to the merged design database, to ensure that individual passes were implemented correctly. From the merged design database, it is possi- ble to generate both a partial bitstream that can be used after configuration with the static bitstream and a merged bitstream which can be used as an ini- tial configuration bitstream, with the reconfigurable module already loaded. To enable reconfiguration in a Linux system, the partial bitstream is encapsu- lated with the Linux code for performing PR and the meta-information about the reconfigurable module, to generate a Linux executable, as described in Section 12.6. 12.6 Managing Partial Reconfiguration in Linux Two device drivers are used to manage the reconfiguration process. Primar- ily, the device driver for the ICAP device performs the actual reconfigura- tion. When a partial bitstream is written to this device (for instance, using the cp command or the write() system call), the bytes are transferred to the ICAP. Since the device driver does not inspect or modify the stream of bytes, the data being written must include the appropriate control words, as expected by the configuration interface [26]. The device driver also includes simple locking of the ICAP resource, in order to prevent different processes from unexpectedly interleaving accesses to the ICAP. Readback is also possi- ble using this device driver by writing the correct readback request bitstream to the ICAP and subsequently reading data (using the read() system call). The second device driver used to manage reconfiguration is associated with the reconfigurable socket core. This driver exports a character interface to which meta-information about a reconfigurable module can be written. A simple way of representing this meta-information is in the form of an array of struct platform_device, a data structure which is used internally by Linux to represent devices. A more complex, but perhaps more robust
FPGA Platforms for Embedded Systems 371 Reconfigure FPGA Disable bus macros Reset reconfigurable module Enable bus macros Release devices Notify kernel of devices Unload kernel modules Processing Load kernel modules FIGURE 12.10 The reconfiguration process. representation of meta-information could be an additional device tree blob. This meta-information is parsed and checksummed and, if valid, is used to notify the Linux kernel of the presence of new devices, which can then be bound to other device drivers. An invalid checksum is interpreted as an indi- cation to unbind any previously loaded devices and release ownership of the reconfigured region. Secondarily, this device driver also enables and disables the bus macros between the static region and the reconfigured region, and controls the reset of the reconfigured region. As with the ICAP device driver, the socket device driver includes a simple locking mechanism in order to prevent a process from unexpectedly reconfiguring an active region in use by another process. The complete process of reconfiguration is shown in Figure 12.10. In the initial state, we assume no module is loaded in the reconfigured region. Next, a reconfigurable module is loaded into the FPGA through the ICAP device driver. Next, meta-information about the reconfigurable module is sent to the socket device driver, which registers the presence of any new devices, resets the newly loaded module, and enables the interface between the static region and the reconfigurable module. At this point, although Linux is aware of the presence of the reconfigured devices, it may not have device drivers appro- priate to those devices. Next, device drivers for new devices are provided by loading the appropriate kernel modules and the Linux kernel binds those device drivers to the reconfigured devices. At this point, application code may use the device drivers to communicate with the reconfigured region. A similar sequence of steps in reverse order occurs to unbind the device drivers and release the reconfigured region so that different processing may occur. Since the ICAP device and the control interface of the socket are exposed through device drivers, it is relatively straightforward to implement recon- figuration through a regular user process. One possibility for implementing
372 Model-Based Design for Embedded Systems this involves linking the bitstream and meta-information into a single exe- cutable along with the code for reconfiguration. The process created when this executable is executed can be controlled through any operating system mechanism (such as POSIX signals) to manage the life cycle of the module loaded in the FPGA. The executable can also be linked together with other application code, resulting in a familiar processor-centric usage model for the FPGA fabric. This approach is similar in spirit, but greatly different in implementation from that proposed in [18], which performs essentially the same processes using the Linux kernel’s ability to implement new executable formats. It is important to recognize that although the reconfiguration process is managed by a user process, it must be treated as a privileged opera- tion executed as the root user, since there are many places where both unintended errors and malicious attacks may result in unintended behav- ior. Some of these places are not specific to the PR process, such as loading kernel modules, whereas others are more subtle vulnerabilities. For instance, as noted before, partial bitstreams have significant constraints on how they are constructed and are specific to a particular implementation of the static system. More directly, it is possible to trigger reconfiguration of the FPGA through the ICAP interface, resulting in the loss of the current state of the system. If the bus macros are enabled during PR, then it is likely that glitch- ing on the interface signals will result in unintended behavior of the static system. One particularly common usage error is simply attempting to load a par- tial bitstream that does not correspond to the current implementation of the static design. This may happen during development when a modification is made to the static region, but a designer neglects to reimplement a recon- figured module. One way of avoiding such errors is to prepend each partial bitstream with a hash generated from the static design. This hash can also be stored in the static design, possibly in the device tree blob, and checked before being loaded into the FPGA. If the partial bitstream is not signed properly, then the reconfiguration process can be halted without affecting the operation of the static design. This technique can be simply applied to prevent unintended errors, or adapted using more cryptographically secure techniques to prevent malicious attacks [2,4]. 12.7 Putting It All Together This section illustrates a SRP design targeted at a variant of the WARP Software-defined Radio hardware built by Rice University [12]. Since the original hardware is based on an older Virtex 2 Pro FPGA, we present a design based on an updated Virtex 4 FX 100 device in order to better
FPGA Platforms for Embedded Systems 373 ICAP Interface Interrupt PPC405 (opb_hwicap v1.00b) controller (ppc_virtex4 v2.00.b) (using bridge) (xps_intc v1.00a) Reconfigurable socket PLB bus dcr (using bridge) RS232 Uart Ethernet MAC (xps_uartlite v1.00a) (xps_ll_temac v1.01a) Reconfigured region BRAM interface (xps_bram_if_cntlr v1.00a) plb plb sdma npi Multiported memory controller (mpmc v3.00b) FIGURE 12.11 Architecture of a reconfigurable platform. Some signals and standard cores have not been shown. represent the PR capabilities of newer FPGA architectures. In particular, we focus on a MIMO OFDM reference design for this board, which implements a bridge from Wired Ethernet to a two-radio MIMO system. The design uses a processor to manage the packet headers and to perform configuration man- agement of the radios, while packet payloads are communicated directly between the wired and wireless network interfaces using direct memory access to a processor-managed memory buffer. In the reference design, the packed payload buffer is implemened in BRAM and communicated through a PLB bus. In the reconfigurable design, we assume that the packet payload buffer is implemented in external DRAM, which must be accessed from the reconfigurable region through a separate port of the memory controller. As a nonreconfigurable system, this design uses approximately 50% of the device (21294 of 42176 slices). The design of the static subsystem is shown in Figure 12.11. This design is architected around the PowerPC 405 processor core and was largely gener- ated using the Base System Builder capability in Xilinx EDK. Standard serial port and ethernet IP cores provide external connectivity. Access to external 64 bit wide DDR2 SDRAM, including DMA access for the ethernet core, is provided by the Xilinx MPMC IP core. In this system, the processor, memory bus, and memory controller are designed to be “quasi-synchronous,” mean- ing that clocks must be edge-aligned. Based on the speeds of the individ- ual components, a design point was chosen targeting a slow speed grade FPGA (−10) with the memory bus clocked at 83.3 MHz, the memory con- troller clocked twice as fast (166.6 MHz), and the processor clocked three times as fast (250 MHz).
374 Model-Based Design for Embedded Systems Reconfigured region ICAP interface Utilized Control powerPC interface core bus macros Memory interface bus macros Static region FIGURE 12.12 Placed and routed design of an FPGA processor platform, targeting a Virtex 4 FX 100. The FPGA layout of the design is shown in Figure 12.12, overlaid with the PR floorplanning constraints. The static region is at the south of the chip, and is exactly two configuration frames tall. This layout provides approximately 8600 slices and 128 external I/O pins, which accommodates both the logic
FPGA Platforms for Embedded Systems 375 requirements of a simple processor design, and the I/O pins requirements of a 64-bit DDR2 memory interface. A significantly smaller region would fail to provide enough logic cells for the static design, while a larger region would allocate too many pins to the static region, which would be difficult to access from the reconfigurable region. Note that the majority of the routed signals are contained within the floor- planned area for the static region. The routes entering the top region connect primarily to external I/O pins and FPGA resources, such as clock buffers and the ICAP, located in the center column of the FPGA. Some routes into the top region also connect to the PowerPC cores. Although only one PowerPC is actually used in the static design, current versions of the EA PR tools do not allow PowerPC cores to be part of the reconfigured portion of the design. Hence, this design instantiates both PowerPC cores in the static region, in order to enable use of the JTAG chain, which is assumed to connect through both cores. The device tree for this design is shown in Figure 12.13. Since the targeted board includes Xilinx SystemACE, this is used to configure the FPGA and initialize external memory with the kernel image. The compressed device tree blob is initialized in the BRAM at address 0xfffff800 and decom- pressed by the Linux bootwrapper executing out of external memory. The root filesystem is stored on an external file server and loaded over the net- work interface using the NFS protocol. 12.8 Conclusion Although high-level algorithmic modeling offers significant promise for increasing design productivity, a common problem with many approaches is representing the environment in which a model exists in a system. A solu- tion to this problem is often to provide platforms that abstract lower level details, provide standardized interfaces, and can be targeted by a high-level design tool. Although this difficulty exists in any embedded system, it is par- ticularly apparent in FPGA systems, which include complex IP blocks, such as processor cores, and where physical interfaces to the rest of the system are highly flexible and incorporate many features that cannot be easily modeled even at the circuit and gate level. However, using the architectural features of some FPGAs, such as PR, higher level platforms can be constructed that abstract many of these details and are more appropriate for mapping from a high-level design tool. This chapter has particularly shown how this technique can abstract the complex- ities associated with including a control processor and operating system as part of an FPGA platform.
376 Model-Based Design for Embedded Systems /{ opb: opb@40000000 { #address−cells = ; #size−cells = ; #address−cells = ; #size−cells = ; compatible = "xlnx,virtex"; compatible = "xlnx,opb−v20−1.10.c"; DDR2_SDRAM: memory@0 { ranges = < 40000000 40000000 10000000 >; device_type = "memory"; opb_hwicap_0: opb−hwicap@41300000 { reg = < 0 10000000 >; compatible = "xlnx,opb−hwicap−1.00.b"; }; reg = < 41300000 10000 >; cpus { xlnx,family = "virtex4"; #address−cells = ; #size−cells = ; }; #cpus = ; }; ppc405_0: cpu@0 { plbv46_dcr_bridge_0: plbv46−dcr−bridge@80700000 { clock−frequency = ; compatible = "xlnx,plbv46−dcr−bridge−1.00.a"; compatible = "PowerPC,405", "ibm,ppc405"; dcr−access−method = "mmio"; d−cache−line−size = ; dcr−controller ; d−cache−size = ; dcr−mmio−range = < 80700000 1000 >; device_type = "cpu"; dcr−mmio−stride = ; i−cache−line−size = ; }; i−cache−size = ; rs232: serial@84000000 { model = "PowerPC,405"; clock−frequency = ; reg = ; compatible = "xlnx,xps−uartlite−1.00.a"; timebase−frequency = ; current−speed = ; }; device_type = "serial"; }; interrupt−parent = ; plb: plb@0 { interrupts = < 3 0 >; #address−cells = ; #size−cells = ; port−number = ; compatible = "xlnx,plb−v46−1.00.a"; reg = < 84000000 10000 >; ranges ; xlnx,baudrate = ; TriMode_MAC_GMII: xps−ll−temac@81c00000 { xlnx,data−bits = ; #address−cells = ; xlnx,odd−parity = ; #size−cells = ; xlnx,use−parity = ; compatible = "xlnx,compound"; }; ethernet@81c00000 { xps_bram_if_cntlr_1: xps−bram−if−cntlr@fffff000 { compatible = "xlnx,xps−ll−temac−1.01.a"; compatible = "xlnx,xps−bram−if−cntlr−1.00.a"; device_type = "network"; reg = < fffff000 1000 >; interrupt−parent = ; }; interrupts = < 2 2 >; xps_intc_0: interrupt−controller@81800000 { llink−connected = ; #interrupt−cells = ; local−mac−address = [ 02 00 00 00 00 00 ]; compatible = "xlnx,xps−intc−1.00.a"; reg = < 81c00000 40 >; interrupt−controller ; xlnx,phy−type = ; reg = < 81800000 10000 >; xlnx,temac−type = ; xlnx,num−intr−inputs = ; }; }; }; xps_socket_0: xps−socket@50000000 { mpmc@0 { compatible = "xlnx,xps−socket"; #address−cells = ; #size−cells = ; dcr−parent = ; compatible = "xlnx,mpmc−3.00.b"; dcr−reg = < c0 2 >; PIM2: sdma@84600100 { interrupt−parent = ; compatible = "xlnx,ll−dma−1.00.a"; interrupts = < 4 2 >; interrupt−parent = ; reg = < 50000000 10000000 >; interrupts = < 1 2 0 2 >; }; reg = < 84600100 80 >; }; }; }; }; FIGURE 12.13 Device tree.
FPGA Platforms for Embedded Systems 377 References 1. B. Blodget, P. James-Roxby, E. Keller, S. McMillan, and P. Sundararajaran. A self-reconfiguring platform. In Proceedings of the International Field Pro- grammable Logic and Applications Conference (FPL), Lisbon, Portugal, 2003. Lecture Notes in Computer Science, Vol. 2778, Springer-Verlag, September 2003. 2. J. Castillo, P. Huerta, V. Lopez, and J. Martinez. A secure self- reconfiguring architecture based on open-source hardware. In Inter- national Conference on Reconfigurable Computing and FPGAs (ReConFig), Puebla City, Mexico, September 2005. 3. J. Corbett, A. Rubini, and G. Kroah-Hartman. Linux Device Drivers. O’Reilly, Sebastopol, CA, 3rd edition, 2005. 4. R. Fong, S. Harper, and P. Athanas. A versatile framework for FPGA field updates: An application of partial self-reconfiguration. In Proceedings of the IEEE International Workshop on Rapid System Prototyping, San Diego, CA, June 2003. 5. R. Freeman. Configurable electrical circuit having configurable logic ele- ments and configurable interconnects. US Patent 4870302, September 1989. 6. D. Gibson and B. Herrenschmidt. Device trees everywhere. In Proceed- ings of linux.conf.au, Dunedin, New Zealand, January 2006. Available at http://ozlabs.org/people/dgibson/home/papers/dtc-paper.pdf, accessed April 28, 2008. 7. IBM. Device control register bus architecture specifications version 3.5, January 2006. 8. IBM. 128-bit processor local bus architecture specifications version 4.7, May 2007. 9. I. Kuon and J. Rose. Measuring the gap between FPGAs and ASICs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 26(2):203–215, February 2007. 10. E. A. Lee and S. Neuendorffer. Actor-oriented models for codesign: Bal- ancing re-use and performance. In S. Shukla and J.-P. Talpin (editors), Formal Methods and Models for System Design: A System Level Perspective, pp. 33–56, Kluwer, Norwell, MA, 2004. 11. M. Majer, J. Teich, A. Ahmadinia, and C. Bobda. The Erlangen slot machine: A dynamically reconfigurable FPGA-based computer. Journal of VLSI Signal Processing Systems, 47(1):15–31, March 2007.
378 Model-Based Design for Embedded Systems 12. P. Murphy, A. Sabharwal, and B. Aazhang. Design of WARP: A flexi- ble wireless open-access research platform. In Proceedings of the European Signal Processing Conference (EUSIPCO), Florence, Italy, 2006. 13. A. Parsons et al. A scalable correlator architecture based on modular FPGA hardware and data packetization. In Asilomar Conference on Sig- nals, Systems, and Computers, Pacific Grove, CA, November 2006. 14. A. Parsons et al. A scalable correlator architecture based on modu- lar FPGA hardware and data packetization. Submitted to IEEE Trans- actions on Signal Processing, available at http://casper.berkeley.edu/ papers/2008-02_parsons_et_al-correlator.pdf, February 2008. 15. Power.org. Power.org standard for embedded power architecture plat- form requirements (epapr), July 2008. Version 1.0. 16. A. Sangiovanni-Vincentelli. Defining platform-based design. EEDesign, February 2002. 17. P. Sedcole, B. Blodget, T. Becker, J. Anderson, and P. Lysaght. Modular dynamic reconfiguration in Virtex FPGAs. IEE Proceedings on Computers and Digital Techniques, 153(3):157–164, May 2006. 18. H. K.-H. So and R. W. Brodersen. Improving usability of FPGA-based reconfigurable computers through operating system support. In Proceed- ings of the International Field Programmable Logic and Applications Conference (FPL), Madrid, Spain, 2006. 19. Sun. Opensparc web page, available at http://www.opensparc. net, accessed on March 7, 2008. 20. Triscend. Triscend e5 configurable system-on-chip platform datsheet, July 2001, v1.06. 21. M. Uhm and J. Bezile. Meeting software defined radio cost and power targets: Making SDR feasible. in Military Embedded Systems, pp. 6–8, May 2005. 22. J. Williams and N. Bergmann. Embedded linux as a platform for dynami- cally self-reconfiguring systems-on-chip. In Proceedings of the International Multiconference in Computer Science and Computer Engineering (ERSA), Los Vegas, CA, June 2004. 23. Xilinx. PLBv46 to PLBv6 Bridge Data Sheet, ds618 edition. Ver- sion 1.00.a, available at http:/www.xilinx.com/bvdocs/ipcenter/data_ sheet/plbv46_plbv46_bridge.pdf, accessed on March 6, 2008. 24. Xilinx. Embedded System Tools Reference Manual, ug111 v9.2 edition, September 2007.
FPGA Platforms for Embedded Systems 379 25. Xilinx. PLBV46 Interface Simplifications, sp026 edition, October 2007. 26. Xilinx. Virtex-4 FPGA Confituration User Guide, ug071 v1.10 edition, April 2008. 27. Xilinx. Virtex-4 FPGA Guide, ug070 v2.40 edition, April 2008. 28. K. Yaghmour. Building Embedded Linux System. O’Reilly, Sebastopol, CA, 2003.
Part III Design Tools and Methodology for Multidomain Embedded Systems
13 Modeling, Veriﬁcation, and Testing Using Timed and Hybrid Automata Stavros Tripakis and Thao Dang CONTENTS 13.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 383 13.2 Modeling with Timed and Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 385 13.2.1 Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 386 13.2.2 Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 389 13.3 Exhaustive Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 391 13.3.1 Model Checking for Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 392 13.3.2 Verification of Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 396 13.3.2.1 Autonomous Linear Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 398 13.3.2.2 Linear Systems with Uncertain Input . . . . . . . . . . . . . . . . . . . . . . . 398 13.3.2.3 Nonlinear Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 401 13.3.2.4 Abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 403 13.4 Partial Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 404 13.4.1 Randomized Exploration and Resource-Aware Verification . . . . . . . . 406 13.4.2 RRTs for Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 408 13.4.2.1 Hybrid Distance . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410 13.5 Testing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 411 13.6 Test Generation for Timed Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 412 13.7 Test Generation for Hybrid Automata . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421 13.7.1 Conformance Relation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 422 13.7.1.1 Continuous Inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 422 13.7.1.2 Discrete Inputs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 422 13.7.2 Test Cases and Test Executions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 423 13.7.3 Test Coverage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 424 13.7.4 Coverage Guided Test Generation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 425 13.7.4.1 Coverage-Guided Sampling . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 425 13.8 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427 Acknowledgments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 427 13.1 Introduction Models have been used for a long time to build complex systems, in virtu- ally every engineering field. This is because they provide invaluable help 383
384 Model-Based Design for Embedded Systems in making important design decisions before the system is implemented. Recently, the term “model-based design” has been introduced to empha- size the use of models and place them in the center of the development process, especially for software-intensive systems. Traditionally, the fact that software is immaterial (contrary, say, to bridges or cars or hardware), has resulted in a software development process that largely blurs the line between design and implementation: a model of the software is the software itself, which is also the implementation. It is “cheap” to write software and test it, or so people used to believe. It is now becoming more and more clear that the costs for software development, testing and maintenance are non- negligible, in fact, they often outweigh the costs of the rest of the system. As a result of this and other factors, a more rigorous software develop- ment process based on formal, high-level models, is becoming widespread, especially in the “embedded software” domain. The term “embedded soft- ware” may generally include any type of software that runs on an embedded system. Embedded systems are computer-controlled systems that strongly interact with a physical environment, for example, “x-by-wire” systems for car control, cell phones, multimedia devices, medical devices, defense and aerospace, public transportation, energy and chemical plants, and so on. In all these systems, timing and other physical characteristics of the envi- ronment are essential for system correctness as well as for performance. For instance, in an engine-control system it is critical to ignite the engine at very precise moments in time (in the order of 1 ms). Moreover, the control logic depends on a number of continuously evolving variables that have to do with the combustion in the engine, exhaust, and so on. In order to cap- ture such timing and physical constraints, models of “timed automata” and “hybrid automata” have been developed in the early 1990s [5,9]. Since then, these models have been studied extensively and today there are a number of sophisticated analysis and synthesis methods and tools available for such models. We will discuss some of these methods in this chapter. Models, in general, play different roles and are used for different tasks, at different phases of the design process. For instance, sometimes a model captures a system that is already built to some extent, while at other times a model serves as a specification that the final system must conform to. In the rest of this chapter, we consider the following tasks in the context of timed or hybrid automata models: • Modeling: We discuss timed and hybrid automata in Section 13.2. Mod- eling is of course a task by itself, and probably the most crucial one, since it is a creative and to a large extent nonautomatable task. • Exhaustive verification: We use the term exhaustive verification to denote the task of proving that a given model of a system satisfies a given property (also expressed in some modeling language). This task is exhaustive in the sense that it is conclusive: either the proof succeeds or a counter-example is found that demonstrates that the system fails to satisfy the property. We focus on automatic (push-button) exhaustive
Modeling, Veriﬁcation, and Testing Using Timed and Hybrid Automata 385 verification, also called model checking. We discuss exhaustive verifica- tion in Section 13.3. • Partial verification: Fundamental issues such as undecidability (in the case of hybrid automata) or state-explosion (in the case of both timed and hybrid automata) place limits on exhaustive verification. In Section 13.4 we discuss an alternative, namely, partial verification, which aims to check a given model as much as possible, given time and resource constraints. This is done using mainly simulation-based methods. • Testing: It is important to test the correctness of a system even after it is built. Testing mainly serves this purpose. Since designing good and correct test cases is itself a time-consuming and error-prone process, one of the main challenges in testing is automatic test generation from a formal specification. We discuss testing in general in Section 13.5, and test generation from timed and hybrid automata models in Sec- tions 13.6 and 13.7, respectively. Obviously, the topics covered in this chapter are wide and deep, and we can only offer an overview. We attempt an intuitive presentation and omit most of the technical details. Those can be found in the referenced papers. We also restrict ourselves to the topics mentioned earlier and omit many others. For example, we do not discuss discrete-time/state models, theorem prov- ing, controller synthesis, implementability and code generation, as well as other interesting topics. Finally, excellent surveys exist for some of the topics covered in this chapter (e.g., see Alur’s survey on timed automata [3] and an overview of hybrid systems in the book [107]), thus we prefer to devote more of our discussion to topics that are more recent and perhaps have been less widely exposed such as testing and partial verification. 13.2 Modeling with Timed and Hybrid Automata Timed and hybrid automata models are extensions of finite automata with variables that evolve continuously in time. Timed automata are a subclass (i.e., special case) of hybrid automata. In timed automata all variables evolve with rate 1: that is, these variables measure time itself. Hybrid automata are more general, with variables that can in principle obey any type of continu- ous dynamics, usually expressed by some type of differential equations. These models were introduced in order to meet the desire to blend the “discrete” world of computers with the “continuous” physical world. Classi- cal models from computer science (e.g., finite-state automata) provide means for reasoning about discrete systems only. Classical models from engineer- ing (e.g., differential equations) provide means for reasoning mostly about