MOTIVATION: Three-way data structures, characterized by three entities, the units, the variables and the occasions, are frequent in biological studies. In RNA sequencing, three-way data structures are obtained when high-throughput transcriptome sequencing data are collected for n genes across p conditions at r occasions. Matrix variate distributions offer a natural way to model three-way data and mixtures of matrix variate distributions can be used to cluster three-way data. Clustering of gene expression data is carried out as means of discovering gene co-expression networks. RESULTS: In this work, a mixture of matrix variate Poisson-log normal distributions is proposed for clustering read counts from RNA sequencing. By considering the matrix variate structure, full information on the conditions and occasions of the RNA sequencing dataset is simultaneously considered, and the number of covariance parameters to be estimated is reduced. We propose three different frameworks for parameter estimation: a Markov chain Monte Carlo-based approach, a variational Gaussian approximation-based approach, and a hybrid approach. Various information criteria are used for model selection. The models are applied to both real and simulated data, and we demonstrate that the proposed approaches can recover the underlying cluster structure in both cases. In simulation studies where the true model parameters are known, our proposed approach shows good parameter recovery. AVAILABILITY AND IMPLEMENTATION: The GitHub R package for this work is available at https://github.com/anjalisilva/mixMVPLN and is released under the open source MIT license.

Computing systems utilize multicore processors with complex cache coherence protocols to meet the increasing need for performance and energy improvement. It is a major challenge to verify the correctness of a cache coherence protocol since the number of reachable states grows exponentially with the number of cores. In this paper, we propose an efficient test generation technique, which can be used to achieve full state and transition coverage in simulation-based verification for a wide variety of cache coherence protocols. Based on effective analysis of the state space structure, our method can generate more efficient test sequences (50% shorter) on-the-fly compared with tests generated by BFS. While our on-the-fly method can reduce the numbers of required tests by half, it can still be impractical to verify all possible transitions in the presence of large number of cores. We propose scalable on-the-fly test generation techniques using quotient state space. The proposed approach guarantees selection of important transitions by utilizing equivalence classes, and omits only similar transitions. Our experimental results demonstrate that our proposed approaches can efficiently tradeoff between transition coverage and validation effort.

Processors with multiple cores and complex cache coherence protocols are widely employed to improve the overall performance. It is a major challenge to verify the correctness of a cache coherence protocol since the number of reachable states grows exponentially with the number of cores. In this paper, we propose an efficient test generation technique, which can be used to achieve full state and transition coverage in simulation based verification for a wide variety of cache coherence protocols. Based on effective analysis of the state space structure, our method can generate more efficient test sequences (50% shorter) compared with tests generated by breadth first search. Moreover, our proposed approach can generate tests on-the-fly due to its space efficient design.

The ongoing scaling of semiconductor technology is causing severe increase of on-chip power density and temperature in microprocessors. This urgently requires both power and thermal management during system design. In this paper, we propose a model checking-based technique using extended timed automata to solve the processor frequency assignment problem in a temperature and energy-constrained multitasking system. We also develop a polynomial time-approximation algorithm to address the state-space explosion problem caused by symbolic model checker. Our approximation scheme is guaranteed to not generate any false-positive answer, while it may return false-negative answer in rare cases. Our method is universally applicable since it is independent of any system and task characteristics. Experimental results demonstrate the usefulness of our approach.

Functional validation is widely acknowledged as a major challenge for multicore architectures. Directed tests are promising since a significantly smaller number of directed tests can achieve the same coverage goal compared to constrained-random tests. SAT-based bounded model checking is effective for automated generation of directed tests (counterexamples). While existing approaches focus on clause forwarding between different bounds to reduce the test generation time, this article proposes a novel technique that exploits temporal, structural, and spatial symmetry in multicore designs at the same time. Our proposed technique enables the reuse of the knowledge learned from one core to the remaining cores in multicore architectures (structural symmetry), from one bound to the next for a give property (temporal symmetry), as well as from one property to other properties (spatial symmetry). The experimental results demonstrate that our approach can significantly (3--10 times) reduce overall test generation time compared to existing approaches.

Bitstream compression is important in reconfigurable system design since it reduces the bitstream size and the memory requirement. It also improves the communication bandwidth and thereby decreases the reconfiguration time. Existing research in this field has explored two directions: efficient compression with slow decompression or fast decompression at the cost of compression efficiency. This paper proposes a novel decode-aware compression technique to improve both compression and de compression efficiencies. The three major contributions of this paper are: 1) smart placement of compressed bitstreams that can significantly decrease the overhead of decompression engine; 2) selection of profitable parameters for bitstream compression; and 3) efficient combination of bitmask-based compression and run length encoding of repetitive patterns. Our proposed technique outperforms the existing compression approaches by 15%, while our decompression hardware for variable-length coding is capable of operating at the speed closest to the best known field-programmable gate array-based decoder for fixed-length coding.

Model checking techniques are promising for automated generation of directed tests. However, due to the prohibitively large time and resource requirements, conventional model checking techniques do not scale well when checking complex designs. In SAT-based BMC, many variable ordering heuristics have been investigated to improve counterexample (test) generation involving only one property. This paper presents efficient decision ordering techniques that can improve the overall test generation time of a cluster of similar properties. Our method exploits the assignments of previously generated tests and incorporates it in the decision ordering heuristic for current test generation. Our experimental results using both software and hardware benchmarks demonstrate that our approach can drastically reduce the overall test generation time.

The ongoing scaling of semiconductor technology is causing severe increase of on-chip power density and temperature in microprocessors. This has raised urgent requirement for both power and thermal management during each level of system design. In this paper, we propose a formal technique based on model checking using extended timed automata to solve the processor frequency assignment problem in a temperature- and energy- constrained multitasking system. The state space explosion problem is alleviated by transforming and solving a Pseudo-Boolean satisfiability problem. Our approach is capable of finding efficient solutions under various constraints and applicable to other problem variants as well. Our method is independent of any system and task characteristics. Experimental results demonstrate the usefulness of our approach.

Instruction compression is important in embedded system design since it reduces the code size (memory requirement) and thereby improves the overall area, power, and performance. Existing research in this field has explored two directions: efficient compression with slow decompression, or fast decompression at the cost of compression efficiency. This paper combines the advantages of both approaches by introducing a novel bitstream placement method. Our contribution in this paper is a novel compressed bitstream placement technique to support parallel decompression without sacrificing the compression efficiency. The proposed technique enables splitting a single bitstream (instruction binary) fetched from memory into multiple bitstreams, which are then fed into different decoders. As a result, multiple slow decoders can simultaneously work to produce the effect of high decode bandwidth. We prove that our approach is a close approximation of the optimal placement scheme. Our experimental results demonstrate that our approach can improve the decode bandwidth up to four times with minor impact (less than 3%) on the compression efficiency.

Among various algorithms for vision-based traffic monitoring, spatio-temporal (ST) slice analysis is attractive by computing over a larger temporal scale. However, it is unsuitable for further pattern recognition, since the conventional ST slice cannot preserve the spatial relationship of the original object image. In this paper, we propose a novel algorithm for accurate traffic object extraction. Compared with previous ST algorithms depending on one line per frame, we assemble the object based on foreground strips obtained from each frame and carefully designed motion estimation. Thus, both the spatial and temporal information is used more effectively. Applications in real canal traffic scenes show the advantages of our algorithm.