Encoding RTL Constructs for MathSAT: a Preliminary Report

Formal checking at Register-Transfer Level (RTL) is currently a fundamental step in the design of hardware circuits. Most tools for formal checking, however, work at the boolean level, which is not expressive enough to capture the abstract, high level (e.g., structural, word level) information of RTL designs. Tools for formal checking are thus confronted with problems which are “flattened” down to boolean level, so that a predominant part of their computational effort is wasted in performing useless boolean search on the bitwise encoding of integer data and arithmetical operations. In this paper we present a way of encoding RTL constructs into SMT formulas, that is, boolean combinations of boolean variables and quantifier-free constraints in Integer Linear Arithmetic. Such formulas can be handled by the MathSAT tool (and others) directly, without flattening to boolean level, so that to reduce drastically the computational effort.We propose a mixed boolean/ILP encoding, in which control variables are encoded as boolean variables, datapath variables as integer variables; control constructs are handled as boolean combination of control variables and predicates over datapath variables, and datapath constructs are encoded, as much as possible, as linear arithmetical constraints over datapath variables.     

Lethal factor active-site mutations affect catalytic activity in vitro

The lethal factor (LF) protein of Bacillus anthracis lethal toxin contains the thermolysin-like active-site and zinc-binding consensus motif HEXXH (K. R. Klimpel, N. Arora, and S. H. Leppla, Mol. Microbiol. 13:1093-1100, 1994). LF is hypothesized to act as a Zn2+ metalloprotease in the cytoplasm of macrophages, but no proteolytic activities have been previously shown on any target substrate. Here, synthetic peptides are hydrolyzed by LF in vitro. Mass spectroscopy and peptide sequencing of isolated cleavage products separated by reverse-phase high-pressure liquid chromatography indicate that LF seems to prefer proline-containing substrates. Substitution mutations within the consensus active-site residues completely abolish all in vitro catalytic functions, as does addition of 1,10-phenanthroline, EDTA, and certain amino acid hydroxamates, including the novel zinc metalloprotease inhibitor ZINCOV. In contrast, the protease inhibitors bestatin and lysine CMK, previously shown to block LF activity on macrophages, did not block LF activity in vitro. These data provide the first direct evidence that LF may act as an endopeptidase.     

Windows with rapidly decaying sidelobes and steerable sidelobe dips

A window in the form of a sum of cosine terms is considered and the temporal weights are evaluated analytically so that it can have rapidly decaying sidelobes as well as steerable sidelobe dips. An analytic expression is derived so that the window designer can exploit the trade-off between a high sidelobe falloff rate (SLFOR) and many steerable sidelobe dips (SSLD). The treatment is based on using the L degrees of freedom inherent in the L temporal weights of the L+1 term window in partially achieving the goals of a high SLFOR and many SSLD. In the extreme case where all degrees of freedom are used in achieving the maximum SLFOR a simple closed-form expression is derived for the temporal weights thus formalizing and generalizing the results of Nuttall (1981). The other extreme case where all degrees of freedom are used in creating many SSLD has been recently treated by Zhong et al. (see ibid. vol.40, no.6, p.1452-1459, 1992) combining both desired features in one unified mathematical framework is the main objective of this paper. Simulation results demonstrate the superior performance of a window having both features to that of a window having only one feature in extracting a weak sinusoidal signal dominated by a leakage from another stronger signal     

Preparation and characterization of transparent cellulose films using an improved cellulose dissolution process

Effective dissolution of cellulosic macromolecules is the first predominant step to prepare functional bio‐based materials with desirable properties. In this study, we developed an improved dissolution process using a freeze‐drying pretreatment to promote the dissolution of cellulose. Rheological measurements of cellulose solutions and physicochemical characterization of regenerated cellulose films (scanning electron microscopy, Fourier transform infrared spectroscopy, X‐ray diffraction, and thermogravimetric analysis) were performed. Cellulose solution prepared from 5% microcrystalline cellulose (w:v) in the solvent exhibits a Newtonian fluid character while cellulose solutions at higher concentrations show a pseudo‐plastic fluid behavior. Results from physicochemical characterization indicate that a freeze‐drying pretreatment step of cellulose leads to a complete dissolution at 5% concentration while only part of cellulose is dissolved at 10% and 15% concentrations. The results obtained indicated that the use of a freeze‐drying pretreatment step under mild conditions lead to a complete dissolution of cellulose at 5% concentration. The cellulose films prepared from 5% concentration exhibited desirable properties such as good optical transparency, crystallinity, and thermal stability. © 2017 Wiley Periodicals, Inc. J. Appl. Polym. Sci. 2017 , 134, 44871.     

Hot Corrosion Mechanism of Steels Exposed to Heavy Metal Chlorides and Sulphates in SO<Subscript>2</Subscript> Environment

Copper flash smelting produces flue dust containing SO₂-rich exhaust gas, causing corrosion problems in the heat recovery boiler of the gas train. In order to understand the corrosion behaviour of boiler steels, conditions of the boiler were simulated in the laboratory. Corrosion damage occurred as chlorine reacted with steel surfaces forming chlorides which deplete the steels from their alloying metals. At the scale/dust deposit interface, where the highest sulphur partial pressures prevail, a sulphate layer covered the mixed oxide and chloride scale. Molten sulphate deposit reduced the metal loss of AISI 304 steel by preventing chromium chloride diffusion away from the steel surface. The Cr₂O₃ scales were quite stable under molten sulphates. The dust deposit melted partially due to the presence of ZnCl₂ in the deposit which initiated corrosion damage by producing a molten salt layer on the steel surfaces bringing it in contact with aggressive compounds in the copper smelter flue dust.     

A kinetic model for ammonia selective catalytic reduction over Cu-ZSM-5

Kinetic modeling, in combination with flow reactor experiments, was used in this study for simulating NH₃ selective catalytic reduction (SCR) of NO_x over Cu-ZSM-5. First the mass-transfer in the wash-coat was examined experimentally, by using two monoliths: one with 11 wt.% wash-coat and the other sample with 23 wt.% wash-coat. When the ratio between the total flow rate and the wash-coat amount was kept constant similar results for NO_x conversion and NH₃ slip were obtained, indicating no significant mass-transfer limitations in the wash-coat layer. A broad range of experimental conditions was used when developing the model: ammonia temperature programmed desorption (TPD), NH₃ oxidation, NO oxidation, and NH₃ SCR experiments with different NO-to-NO₂ ratios. 5% water was used in all experiments, since water affects the amount of ammonia stored and also the activity of the catalyst. The kinetic model contains seven reaction steps including these for: ammonia adsorption and desorption, NH₃ oxidation, NO oxidation, standard SCR (NO + O₂ + NH₃), rapid SCR (NO + NO₂ + NH₃), NO₂ SCR (NO₂ + NH₃) and N₂O formation. The model describes all experiments well. The kinetic parameters and 95% linearized confidence regions are given in the paper. The model was validated with six experiments not included in the kinetic parameter estimation. The ammonia concentration was varied from 200 up to 800 ppm using NO only as a NO_x source in the first experiment and 50% NO and 50% NO₂ in the second experiment. The model was also validated with transient experiments at 175 and 350 °C where the NO and NH₃ concentrations were varied stepwise with a duration of 2 min for each step. In addition, two short transient experiments were simulated where the NO₂ and NO levels as well as NO₂-to-NO_x ratio were varied. The model could describe all validation experiments very well.     

Photodarkening rate in Yb-doped silica fibers

Yb-doped fibers are widely used in laser applications requiring high average output powers and high-peak-power pulse amplification. Photodarkening (PD) is recognized as one limiting factor in these fibers when pumped with high-intensity radiation. We describe an approach for performing quantitative PD studies of fibers, and we present measurements of the rate of PD in Yb-doped single-mode fibers with varying inversion levels. The method is applicable to large-mode-area fibers. We observed a seventh-order dependence of the PD rate on the excited-state Yb concentration for two different fibers; this result implies that PD of a Yb-doped fiber source fabricated using a particular fiber will be strongly dependent on the configuration of the device.     

Design of Foundations on Sensitive Champlain Clay Subjected to Cyclic Loading

Sensitive clay subjected to cyclic loading may experience gradual loss of its shear strength, which may lead to liquefaction. Foundations built on this clay would suffer extensive settlement and significant loss of bearing capacity or perhaps catastrophic failure. This paper presents an experimental investigation on sensitive (Champlain) clay obtained from the city of Rigaud, Quebec (Canada). Consolidation tests, static and cyclic undrained and drained triaxial tests were performed on representative samples of this clay. The objective of this investigation was to examine the influence of the physical and mechanical parameters, which govern the shear strength of sensitive clay subjected to cyclic loading. Based on the results of the present investigation and those available in the literature, it can be reported herein that the undrained response is the most critical for these foundations; furthermore, the preconsolidation pressure is considered as an important parameter in establishing the shear strength of sensitive clay. A design procedure is developed to determine the safe zone for the undrained and drained responses, within which a combination of the cyclic deviator stress and the number of cycles for a given soil/loading/site conditions can achieve a quasielastic resilient state without reaching failure. The proposed design procedure is applicable to all regions around the world, where sensitive clays can be found. Furthermore, this procedure can be adopted to examine the conditions of existing foundations built on sensitive clay at any time during its lifespan.     

情绪家具

Hanna Emelie Ernsting曾在瑞士的卢塞恩造型艺术学院学习产品设计,她一直在研究产品和使用者情绪之间的关联,最近完成的Moody系列就是这一课题的研究成果。Moody系列总共有3组,分别是Moody Couch、Moody Nest、Moody Bag,它们能够跟随使用者当时的情绪变化而变化