Verifying Fixed-Point Digital Filters using SMT- Based Bounded Model Checking

Renato B. Abreu, Lucas Cordeiro, Eddie B. L. Filho

DOI: 10.14209/sbrt.2013.178

Keywords: fixed-point filters formal methods bounded model checking.

Abstract

The implementation of digital filters in processors based on fixed-point arithmetic can lead to problems related to the finite word-length. In particular, the processing of signals in such filters can produce overflows and unwanted noise caused by quantization and round off effect during the accumulative addition and multiplication operations. In this paper, we describe a new approach to verify digital filters using an off-the-shelf bounded model checker called ESBMC, which supports full C/C++ and is based on satisfiability modulo theories solvers. In particular, we are able to verify the occurrence of overflows, limit cycles, and time constraints based on a discrete-time model implemented in C. The experiments show that the proposed approach can be used to verify potential problems in fixed-point implementation of digital filters and it can thus be effective in finding realistic design errors.

Download

Estudo da Interferência entre Sistemas de Comunicações Baseados em C-OFDM e W-CDMA

Pedro A.M. Fonini, Markus V.S. Lima, Paulo S.R. Diniz

DOI: 10.14209/sbrt.2013.125

Keywords: C-OFDM W-CDMA interferência rádios cognitivos LTE

Abstract

O objetivo deste trabalho é estudar os efeitos da co-existência de dois sistemas de transmissão que empregam técnicas utilizadas nos sistemas de comunicações modernos. Os sistemas considerados são o wideband code-division multiple access (W-CDMA) e o orthogonal frequency-division multiplexing com codificação de canal (C-OFDM). A principal motivação desse estudo é a ideia central de rádios cognitivos: a de que usuários não licenciados possam usar faixas de frequências subutilizadas pelo usuário licenciado. Consequentemente, nesse contexto, in- terferência entre diferentes sistemas devem ocorrer com mais frequência.

Download

PROPOSTA DE ARQUITETURA OTN SWITCH SEGUNDO AS RECOMENDAÇÕES ITU-T

Matheus Brunoro Dilem, Rafael Campanharo Favoreto, Rodrigo Stange Tessinari, Luiz Guilherme Bergamaschi Bueloni, Anilton Salles Garcia

DOI: 10.14209/sbrt.2013.179

Keywords: OTN Switch OTN ROADM Multiplexing OMNeT++

Abstract

This paper presents an architecture proposal for OTN Switch equipment, focusing on functionality provided by ITU-T Recommendations, especially the ITU-T G.798. It explores the main features of OTN Switch: multiplexing and switching of signals in optical and electrical domains. These features make the OTN more flexible and dynamic, approaching it to the next generation transport networks. It is presented a preliminary simulation of the proposed architecture using a simulation framework for OTN networks developed using the OMNeT++ simulator.

Download

Complexity Reduction of Turbo Decoding Based on Decision Thresholds

Luís O. Mataveli, Celso de Almeida

DOI: 10.14209/sbrt.2013.130

Keywords: Turbo decoding complexity reduction decision thresholds.

Abstract

In this paper we propose a method for reducing turbo decoding complexity. Based on decision thresholds, some calculations are previously considered negligible, and it is pos- sible to reduce the number of calculations required to perform turbo decoding. Simulations show that almost 40% of the state metrics (α and β) and 25% of the LLRs (Log-Likelihood Ratios) calculations can be eliminated. With the same idea, decision thresholds can be used to take decisions on the information bits based on the LLRs, achieving good decoding complexity reduction, especially for high SNR (Signal to Noise Ratio).

Download

Complexity Reduction of the Viterbi Algorithm Based on Samples Reliability

Luís O. Mataveli, Celso de Almeida

DOI: 10.14209/sbrt.2013.180

Keywords: Viterbi algorithm complexity reduction relia- bility threshold.

Abstract

The Viterbi algorithm is a maximum likelihood algorithm that is used for decoding convolutional codes. In order to determine the survivor path in a trellis, it is necessary to calculate the metrics of each branch. In this paper, we propose a method that reduces the number of branches in the trellis and consequently its complexity, based on the reliability of the received signal samples. The complexity of the proposed algorithm is reduced with the number of reliable samples. The proposed algorithm achieves a performance close to the Viterbi algorithm, but with lesser complexity, depending on the reliability threshold. The performance is evaluated in terms of bit error probability and complexity, obtained by simulation, for different signal to noise ratio and reliability threshold values. The results are obtained for different convolutional encoders by considering a Rayleigh fading channel.

Download

Filtro Adaptativo de Rank Reduzido para Receptor UWB em Sistemas PLC

Marlon L. G. Salmento, Cristiano A. G. Marques, Weiler A. Finamore, Moises V. Ribeiro

DOI: 10.14209/sbrt.2013.181

Keywords: Ultra Wide Band Power line communication Adaptive Filters

Abstract

This work analyzes the usability of reduced rank adaptive filter with time varying decimation for the reception of impulsive ultra wide band symbols in power line communication systems. The performance analysis of such adaptive filter was carried out when the PLC channel is indoor, linear and time invariant under the presence of additive white gaussian noise (AWGN) ou additive impulsive gaussian noise (AIGN). Computational results shows that this kind of adaptive filter can be very useful for low cost and low bit-rate PLC systems.

Download

Efeito da Modelagem probabilı́stica dos ganhos nos lóbulos laterais das antenas das estações terrenas no cálculo de interferências entre sistemas via satélite

Alfredo Córdova, Jose Mauro P. Fortes.

DOI: 10.14209/sbrt.2013.245

Keywords: Sistemas via Satélite Interferência Ganhos de Antenas Modelagem Probabilı́stica

Abstract

Como alternativa ao procedimento usual de cálculo de interferências que utiliza diagramas de referência na caracterização dos ganhos das antenas, este trabalho propõe um procedimento mais próximo da realidade no qual os ganhos nos lóbulos laterais das antenas envolvidas são modelados por variáveis aleatórias. Neste caso, a razão portadora interferência resultante é também uma variável aleatória. Expressões analı́ticas para a função distribuição de probabilidade da razão são desen- volvidas para dois tipos de modelagem dos ganhos nos lóbulos laterais das antenas: como variáveis aleatórias com distribuição exponencial e como variáveis aleatórias com distribuição gama. Estas expressões são aplicadas a situações especı́ficas envolvendo multiplos satélites multifeixe e os resultados obtidos são com- parados àqueles resultantes do cálculo que utiliza um diagrama de referência na caracterização dos ganhos das antenas.

Download

Desempenho de Sistemas de Diversidade Cooperativa com Constelações θ -QAM sob Desvanecimento κ - μ

Rafael F. Lopes, Wamberto J. L. Queiroz, Marcelo S. Alencar

DOI: 10.14209/sbrt.2013.183

Keywords: Diversidade cooperativa Constelações θ-QAM Desvanecimento κ-μ

Abstract

Este artigo apresenta expressões matemáticas para a avaliação da probabilidade de erro de sı́mbolo (Symbol Error Probability – SEP) de sistemas de diversidade cooperativa, basea- dos no esquema decodifica-e-encaminha (Decode-and-Forward – DF), que utilizam constelações θ-QAM. A avaliação do sistema é realizada sob desvanecimento κ-μ, um modelo de desvanecimento generalizado para o canal de comunicações. A expressão obtida é representada como uma soma de integrais definidas da função geratriz de momentos (Moment Generating Function – MGF) da distribuição da SNR de canais com desvanecimento κ-μ e permite calcular a SEP desses sistemas considerando canais com caracterı́sticas heterogêneas. Simulações de Monte Carlo foram utilizadas para confirmar os resultados teóricos obtidos.

Download

Impact of Device-to-Device Communications on Cellular Communications in a Multi-Cell Scenario

Rodrigo L. Batista, Carlos F. M. e Silva, José M. B. da Silva, Tarcisio F. Maciel, Francisco R. P. Cavalcanti

DOI: 10.14209/sbrt.2013.184

Keywords: Multi-cell scenario device-to-device communications D2D network-assisted performance assessment

Abstract

Device-to-Device (D2D) communication, while being network-assisted, is seen as promising technology for the next generation of wireless systems as a mean to improve the utilization of cellular spectrum and to reduce the energy consumption of User Equipments (UEs). However, D2D communications can generate significant interference to the cellular network when the same Physical Resource Blocks (PRBs) are shared by both systems. The design of an efficient D2D network underlaying the cellular network with minimal impact on cellular communications is the key problem. In this paper, we provide an impact assessment of D2D communications on the performance of cellular communications in a Long Term Evolution (LTE)-like multi-cell scenario through system-level simulations. Simulation results show that the overall system capacity is always improved when D2D communications are enabled. However, the performance loss of cellular communications in Downlink (DL) is highly significant. For Uplink (UL), the impact on cellular performance is less noticed, being almost negligible for the urban-macrocell environment and acceptable for the spatial multiplexing-based multi-antenna configuration scheme.

Download

Receptor cego PARATUCK2 para Sistemas MIMO Baseados em Codificação Espaço-Temporal

Gilderlan Tavares de Araújo, André L. E de Almeida

DOI: 10.14209/sbrt.2013.187

Keywords: Codificação espaço-temporal decomposição de decodificação em sistemas MIMO-OSTBC depende PARATUCK2 estimação de canal sistema MIMO.

Abstract

Este trabalho considera um sistema MIMO baseado tus de transmissio, além do ganho de diversidade, o que em um esquema de codificação espaço-temporal modificado, o propicia um melhor desempenho em termos de taxa de erro de qual consiste na combinação de um código espaço-temporal bits. sem alterar significativamente a potência de transmissão em bloce ortogonal e um filtre formatador que mupeia o sinal codificado nas antends transmissores e em múltiplos blocos de [1].[2]. tempo. Para este sistema, é proposto um receptor tensorial para codificação e paço-temporal e uma das princip estimação conjunta de canal e detecção de simboles baseado no abordagens empregadas em sistemas MIMO. Dentre a modelo PARATUCK2. O receptor é composto de duas etapas, diversas abordagens existentes, destaca-se a classe de códigos Na primeira, o modelo tensorial PARATUCK2 é wiilizado para espaço-temporais ortogonais por bloco (do inglês, Orthogonal prover uma estimação cega do cinal MIMO atrines de um algoritmo de minimos quadrados alternadas. Na segunda etapa, Space-Time Block Codes-OSTBC), a qual compreende um decodificador linear baseado na ortogonalidade do codigo métodos eficientes de transmissão em comunicações sem fecupera o símbolos transmitido, extruindo-se iN máxime fio, è que oferecein um menor grau de complexidade de Lanhos de diversidade espacial. Resultados de simulação no decodificação no roocptor, quando comparado com outros apresentados para avaliar o desempenho do receptor proposto esquemas [3]-[41.[1]. Apesar do bom desempenho de esquemas em termos do erro médio quadratico de estimação do canal e da taxa de erre de bits. OSTBC, cu suceso está condicionado ao conhecimento do canal no receptor 3). Sabe-se que o sucesso do processo

Download