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.

<p>In design verication, although simulation is still a widely used verication</p> <p>technique in FPGA design, formal verication is obtaining greater acceptance</p> <p>as the complexity of designs increases. In the simulation method, for a circuit</p> <p>with n inputs and m registers an exhaustive test vector will have as many as</p> <p>2^(m+n) elements making it impractical for many modern circuits. Therefore</p> <p>this method is incomplete, i.e., it may fail to catch some design errors due to</p> <p>the lack of complete test coverage. Formal verication can be introduced as a</p> <p>complement to traditional verication techniques.</p> <p>The primary objectives of this thesis are determining: (i) how to for-</p> <p>malize FPGA implementations at dierent levels of abstraction, and (ii) how</p> <p>to prove their functional correctness. This thesis explores two variations of a</p> <p>formal verication framework by proving the functional correctness of several</p> <p>FPGA implementations of commonly used safety subsystem components us-</p> <p>ing the theorem prover PVS. We formalize components at the netlist level and</p> <p>the Verilog Register Transfer HDL level, preserving their functional semantics.</p> <p>Based on these formal models, we prove correctness conditions for the com-</p> <p>ponents using PVS. Finally, we present some techniques which can facilitate</p> <p>the proving process and describe some general strategies which can be used to</p> <p>prove properties of a synchronous circuit design.</p> / Master of Applied Science (MASc)

La synthèse d'images, qui consiste à développer des algorithmes pour générer des images à l'aide d'un ordinateur, est devenue incontournable dans de nombreuses disciplines. Les méthodes d'affichage interactives permettent à l'utilisateur d'explorer des environnements virtuels en réalisant l'affichage des images à une cadence suffisamment élevée pour donner une impression de continuité et d'immersion. Malgré les progrès réalisés par le matériel, de nouveaux besoins supplantent toujours les capacités de traitement, et des techniques d'accélération sont nécessaires pour parvenir à maintenir une cadence d'affichage suffisante. Ce travail s'inscrit précisemment dans ce cadre. Il est consacré à la problématique de l'élimination efficace des objets masqués, en vue d'accélérer l'affichage de scènes complexes. Nous nous sommes plus particulièrement intéressé aux méthodes de précalcul, qui effectuent les calculs coûteux de visibilité durant une phase de prétraitement et les réutilisent lors de la phase de navigation interactive. Les méthodes permettant un précalcul complet et exact sont encore hors de portée à l'heure actuelle, c'est pourquoi des techniques approchées leur sont préférée en pratique. Nous proposons trois méthodes de ce type. La première, présentée dans le chapitre 4, est un algorithme permettant de déterminer de manière exacte si deux polygones convexes sont mutuellement visibles, lorsque des écrans sont placés entre eux. Nos contributions principales ont été de simplifier cette requête, tant du point de vue théorique que du point de vue de l'implémentation, ainsi que d'accélérer son temps moyen d'exécution à l'aide d'un ensemble de techniques d'optimisation. Il en résulte un algorithme considérablement plus simple à mettre en oeuvre que les algorithmes exacts existant dans la littérature. Nous montrons qu'il est également beaucoup plus efficace que ces derniers en termes de temps de calcul. La seconde méthode, présentée dans le chapitre 5, est une approche originale pour encoder l'information de visibilité, qui consiste à stocker l'ombre que générerait chaque objet de la scène s'il était remplacé par une source lumineuse. Nous présentons une analyse des avantages et des inconvénients de cette nouvelle représentation. Finalement, nous proposons dans le chapitre 6 une méthode de calcul de visibilité adaptée aux scènes d'intérieur. Dans ce type d'environnements, les graphes cellules-portails sont très répandus pour l'élimination des objets masqués, en raison de leur faible coût mémoire et de leur grande efficacité. Nous reformulons le problème de la génération de ces graphes en termes de segmentation d'images, et adaptons un algorithme classique, appelé «watershed», pour les obtenir de manière automatique. Nous montrons que la décomposition calculée de la sorte est proche de la décomposition classique, et qu'elle peut être utilisée pour l'élimination des objets masqués.

De plus en plus de calculs de surveillance, contrôle etc. sont effectués de façon logicielle. Notre objectif est de prouver formellement des calculs numériques qui offrent déjà un premier niveau de garantie sur leurs résultats, comme des calculs par intervalles, et en particulier des calculs avec des modèles de Taylor.<br /><br />Cette thèse présente la construction d'une bibliothèque de modèles de Taylor pour l'assistant de preuves PVS. Nous avons développé les modèles de Taylor pour les opérations d'addition, soustraction, multiplication par un scalaire, multiplication, élévation au carré, puissance et racine carrée. Nous avons également développé les modèles de Taylor pour l'exponentielle, le sinus, l'arctangente et les sinus et cosinus hyperboliques. Nous avons démontré dans PVS que les opérations et fonctions définies dans notre bibliothèque préservent la propriété d'inclusion, travail de preuve qui n'avait pas été fait auparavant dans les implantations des modèles de Taylor.<br /><br />Nous avons développé une stratégie PVS pour certifier des inégalités ou bornes d'expressions. Quand on utilise un assistant de preuves pour démontrer une inégalité, il peut être nécessaire de guider l'assistant pas à pas dans la démonstration. Pour cette raison, les utilisateurs effectuent rarement la démonstration. Par conséquent, simplifier la façon de prouver les inégalités et bornes d'expressions facilite l'utilisation de PVS.<br /><br />Notre bibliothèque peut être utilisée pour construire des modèles de Taylor pour des expressions données, pour dériver des bornes plus ou moins précises pour des expressions arithmétiques et également pour certifier des inégalités ou bornes d'expressions. Disposer d'une méthode pour vérifier des expressions dans un assistant de preuves permet de vérifier certaines expressions qui apparaissent dans des logiciels de missions critiques.<br /><br />Pour résumer, nous avons développé une bibliothèque de modèles de Taylor en PVS qui comprend les opérations arithmétiques et certaines fonctions élémentaires. Nous avons démontré la propriété d'inclusion pour les opérations et fonctions développées. Nous avons développé une stratégie appelée containment pour démontrer la propriété d'inclusion des modèles de Taylor construits à partir des opérations et fonctions précédemment définies. Nous avons développé une stratégie appelée taylors pour prouver des inégalités en utilisant les modèles de Taylor. Nous avons illustré sur deux applications l'intérêt de ces développements.

Demonstration videos can be found on fr.linkedin.com/in/doriangomez/ / Cette thèse porte sur la modélisation procédurale de mondes virtuels étendus dans le domaine de l’informatique graphique. Nous proposons d’exploiter les propriétés de visibilité entre régions élémentaires de la scène, que nous appelons tuiles, pour contrôler sa construction par pavage rectangulaire. Deux objectifs distincts sont visés par nos travaux : (1) fournir aux infographistes un moyen efficace pour générer du contenu 3D pour ces scènes virtuelles de très grande taille, et (2) garantir, dès la création du monde, des performances de rendu et de visualisation efficace. Pour cela, nous proposons plusieurs méthodes de détermination de la visibilité en 2D et en 3D. Ces méthodes permettent l’évaluation d’ensembles potentiellement visibles (PVS) en temps interactif ou en temps réel. Elles sont basées sur les calculs de lignes séparatrices et de lignes de support des objets, mais aussi sur l’organisation hiérarchique des objets associés aux tuiles. La première technique (2D) garantit l’occultation complète du champ visuel à partir d’une distance fixe, spécifiée par le concepteur de la scène, depuis n’importe quel endroit sur le pavage. La seconde permet d’estimer et de localiser les tuiles où se propage la visibilité, et de construire le monde en conséquence. Afin de pouvoir générer des mondes variés, nous présentons ensuite l’extension de cette dernière méthode à la 3D. Enfin, nous proposons deux méthodes d’optimisation du placement des objets sur les tuiles permettant d’améliorer leurs propriétés d’occultation et leurs impacts sur les performances de rendu tout en conservant l’atmosphère créée par l’infographiste par ses choix de placement initiaux. / This thesis deals with procedural modeling applied to extended worlds for computer graphics.We study visibility applied to tiling patterns, aiming at two distinct objectives : (1) providing artists with efficient tools to generate 3D content for very extended virtual scenes, and (2) guaranteeing that this content improves performance of subsequent renderings, during its construction. We propose several methods for 2D and 3D visibility determination, in order to achieve interactive or real-time evaluation of potentially visible sets (PVS). They are based on the concepts of separating and supporting lines/planes, as well as objects hierarchies over tiles. Our first 2D method guarantees full occlusion of the visual field (view frustum) beyond a fixed distance, regardless of the observer’s location on a tiling. The second method enables fast estimation and localization of visible tiles, and builds up a virtual world accordingly. We also extend this method to 3D. Finally, we present two methods to optimize objects locations on tiles, and show how to improve rendering performance for scenes generated on the fly.

La vérification à base de propriétés (PBV) est devenue un élément essentiel des flots de conception pour supporter la vérification de circuits complexes. Pour de tels composants où les techniques de vérification formelle ne peuvent s'appliquer, la vérification dynamique à base de propriétés connecte au circuit des moniteurs et des générateurs de test synthétisés à partir de propriétés pour construire de manière simple un environnement de test. Durant cette thèse une partie des travaux à consisté à développer une approche de synthèse de propriétés pour la génération de vecteurs de test. Dans ce contexte, les propriétés décrivent l'environnement du circuit sous test. Elles sont synthétisées en générateurs produisant des séquences de test respectant la propriété correspondante. Il est alors possible de spécifier et d'obtenir un modèle pour tout l'environnement du circuit. Alors que notre approche est modulaire, une méthode à base d'automates a été développée en collaboration avec l'université de McGill. La contribution la plus intéressante de cette thèse tiens dans la méthode qui a été mise en place pour synthétiser une spécification temporelle en un circuit correct par construction. Alors que les approches de l'état de l'art ont une complexité polynomiale, la nôtre est linéaire en la spécification. L'outil SyntHorus a été développé pour supporter cette méthode et synthétise en quelques secondes un circuit correct par construction à partir d'une spécification de plusieurs centaines de propriétés. La correction des générateurs et de la méthode de synthèse a été effectuée à l'aide du prouveur de théorème PVS. Les méthodes et outils développés durant cette thèse ont été validés, renforcés et transférés dans l'industrie grâce à plusieurs coopérations (Thalès Group, Dolphin Integration et ST-Microelectronics) et au projet ANR SFINCS.

Questo studio tratta dei rapporti della cooperazione internazionale per lo sviluppo che favorisce lo scambio tra culture. Si tratta di una ricerca socio-antropologica sull’orientamento cognitivo di entrambi gli attori della cooperazione: chi fornisce e chi riceve l’aiuto. Lo studio è realizzato su due fronti: in Mozambico, in un progetto di cooperazione, e in Italia con membri delle ONG. La tesi sostiene che la cooperazione non solo propone progetti atti a modificare una situazione nei PVS, ma unisce culture favorendo lo scambio di contenuti, opinioni divergenti, abitudini, ecc., trasformandoli in un continuo processo di ‘miscegenation’. La maggior parte delle ONG implementa progetti sul principio della sussidiarietà affrontando difficoltà per stimolare l’‘azione’ per apportare cambiamenti dal basso. La cooperazione è anche fautrice della fusione di culture che genera nuove correnti di pensiero, creando opinioni critiche nei confronti delle idee prevalenti, e provvede voce a movimenti sociali dal basso. In una macro-prospettiva, la globalizzazione continua ad avere un ruolo preponderante nei PVS: il Mozambico non è ancora decolonizzato. Il termine ‘sviluppo’ mantiene tuttora un pregiudizio evolutivo Eurocentrico, e non dovrebbe essere più associato alla crescita economica, e per ottenere un mondo equo non basta ‘empower’ i poveri, è necessario ‘disempower’ i ricchi. / This study addresses the relationships on international cooperation for development that put cultures into motion. This is a socio-anthropological research that outlines the cognitive orientation of both sides in the international cooperation: who provides and who receives Aid. The locus of the investigation is an international cooperation project in Mozambique, along with interviews with Italian NGOs practitioners. The thesis argues that international cooperation not only provides projects apt to change situation in developing countries, but unites cultures that mutually exchange meanings, disagreements, habits, etc., in a continuous process of cultural ‘miscegenation’. Although most NGOs propose bottom-up approach to development, usually projects start from the top, and they face difficulties to stimulate the agency to change from below. International cooperation also generates new lines of though, and usually gives voice to counter-current social movements. In a macro perspective, globalization continues to play a dominant role in the poorest countries, and Mozambique has not been fully decolonized yet. The meaning of the term Development still maintains an Eurocentric and evolutionary bias. However, development should not be anymore associated to economic growth and if we really want to achieve an equal world, there is also the need to ‘disempower’ the rich.

The subject of this thesis is a suggestion on mechanism for automatic interfacing of boring and facing heads with CNC U-axis on horizontal machining centres made in Tajmac-ZPS company. The thesis is terminated in modal analysis which is done in the point of view of the constructed boring head´s behaviour.

As the demand for imported electricity from the grid continues to increase in Södermanland county, achieving a smoother load profile for the overall imports becomes very critical. The utilization of batteries in every type of a company’s infrastructure aims to provide a backup solution when the electric network’s capabilities are unable to support demand for high imported capacities. The current degree project aims to analyse the impact of a New Market Logic, which encourages the prospective stakeholders of a future industrial park to invest in upgrades of their energy infrastructures. Interviews with company employees and literature reviews were used to analyse the conventional energy system according to its power-generating entities, distribution operators, and market norms of electricity. Microsoft Excel was used to simulate a model that aligns with the research goal specifications. Sensitivity analysis was also carried out to provide a better understanding of how different aspects impact the economics and the energy flows. Inventory management theory principles were applied to the design of an integrated battery charging algorithm with the goal of achieving a smother load profile while keeping a low battery capacity. The results indicated a smoother load profile of the companies, followed by a lower intensity in fluctuations during hourly peaks. Further, the author observed a positive economic impact on the yearly cash flows of the companies accompanied with a sustainable investment cost. This was particularly evident when the charges were adjusted according to the norms introduced by the New Market Logic. / <p>This thesis is a part of the integrated Master's studies program at the Department of Mechanical Engineering at the Aristotle University of Thessaloniki. The author had the privilege of completing it in Sweden through the Erasmus+ Exchange program. </p>

No description available.