Recommending content to users involves understanding a) what to present and b) how to present them, so as to increase quality of experience (QoE) and thereby, content consumption. This work attempts to address the question of how to present contents in a way so that the user finds it easy to get to desired content. While the process of User Interface (UI) design is dependent on several human factors, there are basic design components and their combination that have to be common to any recommender system user interface. Personalization of the UI design process involves picking the right components and their combination, and presenting a UI to suit the usage behavior of an individual user, so as to enhance the QoE. This work proposes a system that learns from a user's content consumption patterns and makes some recommendations regarding how to present the content for the user (in the context of Video-On-Demand/Live-TV services on Computer displays), so as to enhance the QoE of the recommender system.

In modern day digital design flow, high-level models written in C and C++ serve multiple purposes, one of which is to aid verification of register-transfer level (RTL) hardware models. These high-level models, also called system-level models (SLMs), act as reference models for hardware designs created at the RTL level. They define the correct behavior for the RTL hardware design under verification. Written in a programming language (or similar) and therefore executable, they are used extensively in both simulation-based verification and formal equivalence checking. This paper presents how SLMs fit into the different RTL verification schemes and the challenges involved in the various verification flows. Input stimulus generation based on formal verification technology is introduced as a new way to improve simulation coverage. This paper also covers other techniques engineers use to meet various challenges encountered in RTL verification.

Formal and dynamic (simulation, emulation, etc.) verification techniques are both needed to deal with the overall challenge of verification. Ideally, the same specification/testbench would work with both formal and dynamic techniques, with the same semantics in both. Unfortunately, this is typically not the case. In particular, generalized symbolic trajectory evaluation (GSTE) is a powerful formal verification technique developed by Intel and successfully used on next-generation microprocessor designs, but the specification formalism for GSTE relies on "symbolic constants", which intrinsically exploit the underlying formal verification engine and cannot be reasonably handled via non-symbolic means. In this paper, we propose a modified version of GSTE specifications, and we present efficient, automatic constructions to convert from the new simulation-friendly GSTE specifications into the conventional GSTE specifications (to access the formal verification tool flow) as well as into completely non-symbolic monitor circuits suitable for the conventional dynamic verification. We demonstrate empirically that our simulation-friendly specification style is expressive enough for almost all real GSTE specifications, that our monitor construction is linear-size, and that our monitor construction imposes minimal overhead over a previously published monitor construction that was not fully non-symbolic.

We describe a complete method for the latch mapping problem that is based on the efficient integration of previously proposed tech-niques for latch mapping as well as novel optimizations for further improvement. The highlights of the proposed approach include a new method of integrating complete methods and incomplete meth-ods for latch mapping, the use of incremental reasoning to optimize the overall algorithm and the use of a conventional combinational equivalence checking tool as the core engine. Experiments con-firm that the proposed method retains much of the efficiency and capacity of incomplete methods while providing the completeness of complete methods and derives significant performance improve-ments from the proposed optimizations.