O contínuo avanço da capacidade dos circuitos integrados e a necessidade de sistemas embarcados cada vez mais complexos para lidar com os problemas atuais, com prazos cada vez mais curtos, estão direcionando o desenvolvimento de sistemas de circuitos integrados para ambientes de alto nível de abstração cada vez mais distantes dos detalhes de hardware. O uso de linguagens de alto nível para auxiliar o desenvolvimento de sistemas embarcados é uma tendência atual pois tal abordagem tende a reduzir a complexidade e o tempo de desenvolvimento. Este trabalho propõe o desenvolvimento de uma nova ferramenta para geração de arquiteturas de hardware em Bluespec em um ambiente gráfico utilizando diagramas da UML. Esta ferramenta permite que o projetista descreva o comportamento utilizando máquina de estados finita no padrão UML 2.0, onde cada estado pode conter a codificação do comportamento com as linguagens Bluespec e C. Dada uma máquina de estados, a mesma é traduzida para a linguagem Bluespec por meio de um compilador e templates. Como resultado, é apresentado a geração de duas arquiteturas de hardware a fim de demonstrar as vantagens e limitações da ferramenta desenvolvida / The continuous advancement of integrated circuits capacity and the need for embedded systems even more complex to deal with current problems, with shorter time-to-market, are driving the development of integrated circuits systems to environments with high level abstraction more and more distant from the hardware details. The use of high level languages to assist the embedded systems development is a current trend for such an approach tends to reduce the complexity and development time. This work proposes the development of a new tool in Bluespec to generate hardware architectures in a graphical environment using UML diagrams. This tool allows the designer to describe the behavior using finite state machine in UML 2.0 standard, where each state can contain the coding behavior with Bluespec and C languages. Given a state machine, it is translated to Bluespec language through a compiler and templates. As a result is presented the generation of two hardware architectures in order to demonstrate the advantages and limitations of the developed tool

Esse trabalho tem por objetivo descrever o desenvolvimento e os atuais resultados do protótipo dataflow PIFLOW, um processador baseado no modelo de dataflow dinâmico, inspirado na Maquina Dataflow de Manchester e desenvolvido no Instituto de Física de São Carlos, da Universidade de São Paulo. Esse protótipo foi capaz de oferecer speedups muito próximos do ideal, a partir de programas que possuem grande grau de paralelismo, apresentando o grande potencial deste modelo - já bastante estudado no decorrer das últimas décadas - em oferecer desempenho superior ao de processadores sequenciais comerciais modernos. / The aim of this work is to describe the development and the current results of the PIFLOW dataflow prototype, a processor based on the dynamic dataflow model of execution, inspired by the Manchester Dataflow Machine and developed in the Instituto de Física de São Carlos, Universidade de São Paulo. This prototype shows speedups very close to the ideal case, when executing programs with a high degree of parallelism, showing the dataflow model potential, which has been extensibly analysed in the last decades, to offer higher performance when compared to commercial modern sequential processors.

O contínuo avanço da capacidade dos circuitos integrados e a necessidade de sistemas embarcados cada vez mais complexos para lidar com os problemas atuais, com prazos cada vez mais curtos, estão direcionando o desenvolvimento de sistemas de circuitos integrados para ambientes de alto nível de abstração cada vez mais distantes dos detalhes de hardware. O uso de linguagens de alto nível para auxiliar o desenvolvimento de sistemas embarcados é uma tendência atual pois tal abordagem tende a reduzir a complexidade e o tempo de desenvolvimento. Este trabalho propõe o desenvolvimento de uma nova ferramenta para geração de arquiteturas de hardware em Bluespec em um ambiente gráfico utilizando diagramas da UML. Esta ferramenta permite que o projetista descreva o comportamento utilizando máquina de estados finita no padrão UML 2.0, onde cada estado pode conter a codificação do comportamento com as linguagens Bluespec e C. Dada uma máquina de estados, a mesma é traduzida para a linguagem Bluespec por meio de um compilador e templates. Como resultado, é apresentado a geração de duas arquiteturas de hardware a fim de demonstrar as vantagens e limitações da ferramenta desenvolvida / The continuous advancement of integrated circuits capacity and the need for embedded systems even more complex to deal with current problems, with shorter time-to-market, are driving the development of integrated circuits systems to environments with high level abstraction more and more distant from the hardware details. The use of high level languages to assist the embedded systems development is a current trend for such an approach tends to reduce the complexity and development time. This work proposes the development of a new tool in Bluespec to generate hardware architectures in a graphical environment using UML diagrams. This tool allows the designer to describe the behavior using finite state machine in UML 2.0 standard, where each state can contain the coding behavior with Bluespec and C languages. Given a state machine, it is translated to Bluespec language through a compiler and templates. As a result is presented the generation of two hardware architectures in order to demonstrate the advantages and limitations of the developed tool

Esse trabalho tem por objetivo descrever o desenvolvimento e os atuais resultados do protótipo dataflow PIFLOW, um processador baseado no modelo de dataflow dinâmico, inspirado na Maquina Dataflow de Manchester e desenvolvido no Instituto de Física de São Carlos, da Universidade de São Paulo. Esse protótipo foi capaz de oferecer speedups muito próximos do ideal, a partir de programas que possuem grande grau de paralelismo, apresentando o grande potencial deste modelo - já bastante estudado no decorrer das últimas décadas - em oferecer desempenho superior ao de processadores sequenciais comerciais modernos. / The aim of this work is to describe the development and the current results of the PIFLOW dataflow prototype, a processor based on the dynamic dataflow model of execution, inspired by the Manchester Dataflow Machine and developed in the Instituto de Física de São Carlos, Universidade de São Paulo. This prototype shows speedups very close to the ideal case, when executing programs with a high degree of parallelism, showing the dataflow model potential, which has been extensibly analysed in the last decades, to offer higher performance when compared to commercial modern sequential processors.

Este trabalho apresenta o desenvolvimento de um processador open source baseado no processador Nios II da Altera. O processador desenvolvido permite a customização de instruções, a inclusão de componentes que possibilitem um estudo detalhado da memória cache, tal como um monitor de cache, definir o tamanho da cache, dentre outras características. Além disso, o processador é baseado na arquitetura do Nios II e implementa 90% do ISA do Nios II, o mesmo está integrado aos ambientes Qsys e SOPC Builder da ferramenta Quartus II da Altera, sendo possível utilizar todo o conjunto de IP (Propriedade Intelectual) e ferramentas disponíveis pela Altera. Assim, este trabalho tem como propósito colaborar com o desenvolvimento de arquiteturas de hardware com uma unidade de processamento configurável e customizável facilmente pelo usuário, uma vez que o seu código fonte em Bluespec SystemVerilog está aberto a todos os usuários, diferente do Nios II da Altera, que tem o código encriptado, inviabilizando fornecer qualquer mudança no processador a nível RTL (Register Transfer Level ). Para o desenvolvimento do processador foi utilizada a Linguagem de Descrição de Hardware Bluespec SystemVerilog, pelo fato de ser uma ESL (Electronic System Level ) que acelera o processo de desenvolvimento de hardware / This work presents the development of an open source based Nios II processor from Altera. The developed processor allows custom instructions, use of components that allows a detailed study of the cache memory, among other features. In addition, the processor is based on the Nios II architecture, which can be integrated into the Qsys and SOPC Builder of the Altera Quartus II environment tool as well as use the entire set of IP (Intellectual Property) and tools available from Altera. This work contributes to the development of hardware architectures with a processing unit configurable and easily customizable by the user, since its source code in Bluespec SystemVerilog is open to all users, other than the Nios II from Altera which has encrypted code, making it impossible to do any changes in the processor at RTL (Register Transfer level) level. For the development of the processor hardware the description language Bluespec SystemVerilog was used, which is an ESL (Electronic System Level) that speeds up the development of the hardware

Este trabalho apresenta o desenvolvimento de um processador open source baseado no processador Nios II da Altera. O processador desenvolvido permite a customização de instruções, a inclusão de componentes que possibilitem um estudo detalhado da memória cache, tal como um monitor de cache, definir o tamanho da cache, dentre outras características. Além disso, o processador é baseado na arquitetura do Nios II e implementa 90% do ISA do Nios II, o mesmo está integrado aos ambientes Qsys e SOPC Builder da ferramenta Quartus II da Altera, sendo possível utilizar todo o conjunto de IP (Propriedade Intelectual) e ferramentas disponíveis pela Altera. Assim, este trabalho tem como propósito colaborar com o desenvolvimento de arquiteturas de hardware com uma unidade de processamento configurável e customizável facilmente pelo usuário, uma vez que o seu código fonte em Bluespec SystemVerilog está aberto a todos os usuários, diferente do Nios II da Altera, que tem o código encriptado, inviabilizando fornecer qualquer mudança no processador a nível RTL (Register Transfer Level ). Para o desenvolvimento do processador foi utilizada a Linguagem de Descrição de Hardware Bluespec SystemVerilog, pelo fato de ser uma ESL (Electronic System Level ) que acelera o processo de desenvolvimento de hardware / This work presents the development of an open source based Nios II processor from Altera. The developed processor allows custom instructions, use of components that allows a detailed study of the cache memory, among other features. In addition, the processor is based on the Nios II architecture, which can be integrated into the Qsys and SOPC Builder of the Altera Quartus II environment tool as well as use the entire set of IP (Intellectual Property) and tools available from Altera. This work contributes to the development of hardware architectures with a processing unit configurable and easily customizable by the user, since its source code in Bluespec SystemVerilog is open to all users, other than the Nios II from Altera which has encrypted code, making it impossible to do any changes in the processor at RTL (Register Transfer level) level. For the development of the processor hardware the description language Bluespec SystemVerilog was used, which is an ESL (Electronic System Level) that speeds up the development of the hardware

Cyber-Physical Systems theory is a new concept that is about to revolutionize the way computers interact with the physical world by integrating physical knowledge into the computing systems and tailoring such computing systems in a way that is more compatible with the way processes happen in the physical world. In this master’s thesis, Field Programmable Gate Arrays (FPGA) are studied as a potential technological asset that may contribute to the enablement of the Cyber-Physical paradigm. As an example application that may benefit from cyber-physical system support, the Electro-Slag Remelting process - a process for remelting metals into better alloys - has been chosen due to the maturity of its related physical models and controller designs. In particular, the Particle Filter that estimates the state of the process is studied as a candidate for FPGA-based computing enhancements. In comparison with CPUs, through the designs and experiments carried in relationship with this study, the FPGA reveals itself as a serious contender in the arsenal of v computing means for Cyber-Physical Systems, due to its capacity to mimic the ubiquitous parallelism of physical processes. / text

This work presents optimizations for modern capability machines and specifically for the CHERI architecture, a 64-bit MIPS instruction set extension for security, supporting fine-grained memory protection through hardware-enforced capabilities. The original CHERI model uses 256-bit capabilities to carry information required for various checks helping to enforce memory safety, leading to increased memory bandwidth requirements and cache pressure when using CHERI capabilities in place of conventional 64-bit pointers. In order to mitigate this cost, I present two new 128-bit CHERI capability formats, using different compression techniques, while preserving C-language compatibility lacking in previous pointer compression schemes. I explore the trade-offs introduced by these new formats over the 256-bit format. I produce an implementation in the L3 ISA modeling language, collaborate on the hardware implementation, and provide an evaluation of the mechanism. Another cost related to CHERI capabilities is the memory traffic increase due to capability-validity tags: to provide unforgeable capabilities, CHERI uses a tagged memory that preserves validity tags for every 256-bit memory word in a shadowspace inaccessible to software. The CHERI hardware implementation of this shadowspace uses a capability-validity-tag table in memory and caches it at the end of the cache hierarchy. To efficiently implement such a shadowspace and improve on CHERI’s current approach, I use sparse data structures in a hierarchical tag-cache that filters unnecessary memory accesses. I present an in-depth study of this technique through a Python implementation of the hierarchical tag-cache, and also provide a hardware implementation and evaluation. I find that validity-tag traffic is reduced for all applications and scales with tag use. For legacy applications that do not use tags, there is near zero overhead. Removing these costs through the use of the proposed optimizations makes the CHERI architecture more affordable and appealing for industrial adoption.

Formal methods play a significant and increasing role in hardware verification, but their effectiveness can be impaired by the ac hoc nature of mainstream hardware languages such as VHDL, Verilog and SystemC, which have convoluted semantics that often necessitate contrived proof techniques. This dissertation investigates the application of formal reasoning to hardware architectures expressed in an alternative class of semantically elegant languages, which support efficient design, whilst also having been developed with proof techniques in mind. A network-on-chip architecture belonging to the SpiNNaker many-core processor is specified in Concurrent Haskell, and a hand proof is presented which verifies a novel routing mechanism by mathematical induction. A subset of Bluespec SystemVerilog (BSV) is embedded in the higher order logic of the PVS theorem prover. Owing to the clean semantics of BSV, application of monadic techniques leads to a surprisingly elegant embedding, in which hardware designs are translated into logic almost verbatim, preserving types and language constructs. Proof strategies are written in the PVS strategy language; these automatically verify temporal logic theorems concerning the resulting monadic expressions, by employing a combination of model checking and deductive reasoning. The subset of BSV which is embedded includes module definition and instantiation, methods, implicit conditions, scheduling attributes, and rule composition using methods from instantiated modules. The aforementioned subset of BSV is also embedded in the specification language of the SAL model checker, and a verification strategy is presented which combines the specialised model checking capabilities of SAL with the diverse proof strategies of PVS.

The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library. / Thesis / Doctor of Philosophy (PhD) / The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library.