China
Africa
Explore chapters and articles related to this topic
Low-Power RF Digital PLLs with Direct Carrier Modulation
Published in Christopher Siu, Krzysztof Iniewski, IoT and Low-Power Wireless, 2018
Salvatore Levantino, Carlo Samori
As a final point, it should be noted that the gain of the BB-TDC depends on its input jitter, which in turn depends on the noise transfer function of the PLL, that depends again on the BB-TDC gain. Even if this vicious circle appears as a peculiar issue of the BB-TDC approach, it is only one particular version of a very general and standard problem of PLLs. As a matter of fact, the noise transfer function of any PLL depends on analog parameters (e.g. the TDC time resolution when a multi-bit TDC is employed in a DPLL) that are difficult to control with the required accuracy. This issue is solved by adopting the automatic loop-gain control scheme disclosed in ref. [38]. This automatic calibration normalises the loop gain so that the whole frequency response and the bandwidth of the PLL are repeatable regardless of the spread of the analog parameters, including TDC gain. This solution makes the phase noise profile and the integrated phase noise (or jitter) independent of PLL parameters such as TDC gain, but dependent on digital coefficients. This property will also be useful in the following, when the PLL is used as direct-FM modulator with pre-emphasis filter.
A novel structure-exploiting encoding for SAT-based diagnosis
Published in Journal of Experimental & Theoretical Artificial Intelligence, 2022
SAT solving is a decision procedure based on the classical DPLL procedure (Davis & Putnam, 1960; Davis et al., 1962). A circuit SAT solver keeps assigning values to circuit variables until all gates are satisfied in that every gate gets consistent values at its input(s) and output without any conflict. During SAT solving, assignments made by choice are called decisions and those by Boolean propagation are called implications. For example, if the input of an gate is assigned a value by decision then its output is also assigned by implication through Boolean propagation. Each decision and implication assignment is associated with a number called decision level. At the start the decision level is initialised to . Later the decision level is incremented at each decision assignment and decremented as a decision is rolled back. Values assigned at decision level are permanent assignments that cannot be rolled back. Permanent assignments are those that are known a priori such as the abnormal observation of a circuit (as in Figure 1).
Combining bounded solving and controllable randomization for approximate model counting
Published in Journal of Experimental & Theoretical Artificial Intelligence, 2022
Shuai Lü, Tongbo Zhang, Yue Xu, Wenbo Zhou, Yong Lai
The earliest approaches for model counting are mainly based on an extension of DPLL-based SAT solvers and provide exact counts, such as Relsat (Bayardo & Pehoushek, 2000), Cachet (Sang et al., 2005a) and sharpSAT (Thurley, 2006). The #SAT solver Cachet was built on the SAT solver zChaff and uses component caching and clause learning. It greatly simplifies the solving process by recording conflicts and the models of sub-formulas. Also, Cachet is one of the most widely used solvers in the field of model counting. Thurley proposed sharpSAT by introducing Boolean constraint propagator and new cache management strategies. Compared with Cachet, sharpSAT further improves the solving efficiency. Unfortunately, the DPLL-based solvers have difficulty in scaling up to larger problem sizes.