• 喀什12个贫困村实现生活垃圾集中处置 2019-06-30
  • 起底特大网络盗刷案:数亿人的秘密因一习惯被盗卖 2019-06-30
  • 黄淳的专栏作者中国国家地理网 2019-06-12
  • 坚守传统手工包粽 探访沪上老字号粽子生产车间 2019-06-10
  • 满满的都是屏 OPPO妹子最爱手机曝光 2019-06-10
  • 北京进入旅游旺季 警察提示游客需防揽客者连环设套忽悠购物 2019-06-08
  • 我写文章不是为了别人的赞许,是为了讨论问题,让人有思考的价值,就像你网名一样,探寻真理。我并非就全盘赞成市场经济,只是在讨论它的合理性,在文中也提问,“既然我们 2019-06-08
  • 山东假存单揽储1.6亿难追回,该省另一相似案件银行被判赔 2019-05-31
  • 天上不会掉馅饼,想要富起来,就要把别人的据为己有,能把别人的据为己有的问世间能有谁,能有几人,所谓的专家明白了吗。 2019-05-31
  • 乌鲁木齐市中级人民法院庭审在线直播 2019-05-21
  • 第530期:为何吃新鲜蔬果能抗肿瘤、强免疫……?因为有“它”! 2019-05-19
  • 世界杯大中华区官方票代谈假票门黄牛倒票行为 2019-05-19
  • 英媒:漫步北京上海,仿佛踏入未来 2019-05-17
  • 2017年各地领导干部给网友书写23万封回信 2019-05-17
  • 回到1396年的波斯街头文章中国国家地理网 2019-04-23
  • 江苏七位体彩开奖结果
    学霸学习网 这下你爽了
    相关文章
    当前位置:江苏七位体彩开奖结果 >> >>

    体彩江苏7位数开奖:FORMAL VERIFICATION OF DISTRIBUTED MUTUAL-EXCLUSION CIRCUITS_图文

    江苏七位体彩开奖结果 www.jwbw.net FORMAL VERIFICATION OF DISTRIBUTED MUTUAL-EXCLUSION CIRCUITS
    Robert Meolic, Tatjana Kapus, Bogdan Dugonik, Zmago Brezoˇ nik c Faculty of Electrical Engineering and Computer Science, University of Maribor, Smetanova ulica 17, SI-2000 Maribor, Slovenia
    Keywords: Asynchronous circuit, Fundamental mode, Process algebra, Model checking, ACTL Abstract: Distributed mutual-exclusion (DME) circuits are an interesting example of asynchronous circuits. They are composed of identical DME cells connected in a ring of arbitrary size. Each DME cell provides a connection point for one user, and all users compete for exclusive access to a shared resource. This paper reports about formal veri?cation of two well-known DME circuit implementations. External behaviour of the circuits is described with a simple process, whereas the required properties are expressed with temporal logic ACTL. We were able to detect hazards and verify correctness of external behaviour of the circuits under the fundamental mode of operation.

    Formalna veri?kacija vezij za porazdeljeno medsebojno izkljuˇ evanje c
    Kljuˇ ne besede: Asinhrono vezje, Fundamentalni naˇ in, Procesna algebra, Preverjanje modelov, ACTL c c Povzetek: Vezja za porazdeljeno medsebojno izkljuˇ evanje (DME) so zanimiv primer asinhronih vezij. Sestavljena so iz c enakih celic DME, povezanih v obroˇ poljubne velikosti. Vsaka od celic DME ponuja prikljuˇ no toˇ ko za enega uporabnika in c c c ˇ vsi uporabniki med seboj tekmujejo za izkljuˇ en dostop do skupnega vira. V clanku obravnavamo formalno veri?kacijo dveh c znanih izvedb vezja DME. Obnaˇanje vezij opiˇemo s preprostim procesom, zahtevane lastnosti pa s temporalno logiko ACTL. s s Na ta naˇ in smo lahko odkrili hazarde ter veri?cirali pravilnost obnaˇanja vezij v fundamentalnem naˇ inu delovanja. c s c

    1 Introduction
    Asynchronous circuits have been built and used for decades, and nowadays, large and ef?cient circuits can be constructed [5, 7, 17, 19, 20]. Techniques and methodologies for designing asynchronous circuits differ from those used with the synchronous approach. An important issue in asynchronous design is hazard removal. Because synchronization is performed without a global clock, unwanted signal changes can kill the circuit. Well known techniques for hazard-free synthesis, decomposition and veri?cation of asynchronous circuits are based on modelling with ?ow tables [4], asynchronous ?nite state machines (AFSM), burstmode state machines (BM), signal transition graphs (STG), state graphs (SG) [17], and also process algebrae. Some of algebraic approaches to veri?cation of asynchronous circuits are Circal agents [2], CCS-like burst-mode speci?cation [20], and DILL speci?cation based on LOTOS [8]. An overview of the state-of-the-art in tools for asynchronous design can be found in [1]. This paper describes an algebraic approach to detecting hazards and verifying correctness of asynchronous circuits. Muller’s model is used for modelling, and funda1

    mental mode of operation is assumed. Section 2 gives an overview of asynchronous design and introduces Muller’s model and hazards. Section 3 describes a simple process algebra and shows how it can be used for modelling individual gates. Section 4 describes the procedure for veri?cation of asynchronous circuits. Section 5 introduces ACTL model checking. Section 6 presents two well-known implementations of DME circuits and reports about the results of their veri?cation. In the conclusion we evaluate our work.

    2 Asynchronous design
    Circuits are composed of gates and wires. In this paper, the term gate refers to simple or complex elements for which only external behaviour is considered, and the term wire refers to connections between gates carrying binary signals. Regarding their operation, circuits can be classi?ed into combinational and sequential. In a combinational circuit, output values of all gates are logic functions of current circuit input values. In a sequential circuit, some gate outputs depend also on a history of circuit input values. The memory effect is achieved with feedback loops.

    Fundamental to an asynchronous design are assumptions about gate and wire delays. If delays are overestimated, the resulting circuit is likely to be inef?cient and expensive. If they are underestimated, the design may not guarantee correct circuit operation. Delays can be bounded or unbounded. For bounded delay the upper bound is given, while the magnitude of unbounded delay is only known to be positive and ?nite. The delays can also be pure or inertial. In the latter case, short pulses are ?ltered out. With regard to assumptions about delays, there are two widely used models for designing asynchronous circuits. Huffman’s model supposes that gate and wire delays are bounded and known. Circuits designed with this model are called Huffman circuits. On the other hand, Muller’s model supposes that wires have negligible delays in comparison to gates, which have inertial unbounded delays. Muller’s model is typically used to design speed-independent circuits. Because of negligible wire delays, all forks in Muller’s model are isochronic. This means that if a signal splits, all instances of this signal have equal delays. Thus, an output signal produced by a gate is equally delayed for all gates which consume it. By explicitly adding nonisochronic FORK elements, Muller’s model can be extended to produce self-timed, delay-insensitive, and quasi-delayinsensitive circuits, where wire delays are important. Note that there are also other design methodologies for asynchronous circuits not based on the mentioned models (e.g. self-clocked circuits and micropipelines) A simple Muller’s model is presented in Figure 1. It represents the C-element, a standard building block used in many asynchronous systems, which was also introduced by Muller. The C-element changes its output only if both inputs are changed to 0 or 1. In the ?gure, the small boxes labeled with d1 , d2 , d3 , and d4 are delay elements attached to the gate outputs, which are the only components in the circuit delaying signals. The ?gure clearly shows that in the Muller’s model an output signal produced by a gate is equally delayed for all gates which consume it.

    environment can change values of input signals at any time. A third type of circuit’s mode of operation is generalized fundamental mode or burst mode. There, signal changes are segregated in time forming input bursts (intervals where input signal values change) and output bursts (intervals where output signal values change). An output burst can be empty, whereas an input burst must contain at least one signal. Input and output bursts must alternate. Within a burst, the ordering of signal changes is not determined. There are some anomalous types of asynchronous circuit behaviour, which the designers try to avoid. An example of a usually unwanted behaviour is a possibility that the circuit enters a closed loop of transitions without becoming stable. This can result in the circuit with oscilating outputs. A simple example of such a circuit and its simulation run are presented in Figure 2.

    Figure 2: A circuit with oscilating output If due to internal delays, a circuit can make an unwanted pulse called a glitch or can become stable with an unwanted combination of values on internal or output lines, we have a hazard. Hazards re?ecting in glitches are classi?ed with regard to their shape into static and dynamic hazards. Static hazard occurs when the signal is momentarily changed although it should remain the same. Dynamic hazard occurs if the signal oscillates before changing its value. A circuit which operates without hazards in the fundamental mode is called a fundamental-mode circuit. For each hazard, there is a reason for its existence. In combinational circuits, three types of hazards are distinguished. Logic hazards are a property of particular implementation. A logic hazard exists in the circuit because for the same signal, two or more parallel paths through the circuit exist, which then reconverge. Functional hazards are a property of the logic functions which do not change monotonically during a sequence of particular input changes. The hazard arises when such inputs change simultaneously. Logic and functional hazards can both be either static or dynamic. A much different type of hazard is delay hazard. It occurs because a new input signal is applied before the circuit becomes stable. Logic hazards can always be avoided by redesigning the circuit. Functional and delay hazards can be removed only by engineering delays. Under fundamental and burst mode of operation, functional and delay hazards do not have an impact. In combinational circuits, hazardous behaviour is a transitory phenomenon, and if no new inputs are applied until the circuit stabilizes, then the correct outputs will be produced. 2

    Figure 1: A gate-level implementation of the C-element An important concept related to delays is circuit’s mode of operation, which characterizes the interaction between a circuit and its environment. Fundamental mode of operation assumes that the environment will change the value of only one input signal at once and then wait until the circuit becomes stable. An asynchronous circuit is stable if no internal or output signal value can be changed without changing some input signal value. The opposite of fundamental mode is input/output mode of operation. In this mode, the

    (a)

    (b)

    (c)

    (d)

    Figure 3: Simple circuits containing (a) static hazard, (b) dynamic hazard, (c) transient hazard, and (d) steady-state hazard. In sequential circuits, additional sequential hazards can exist as a consequence of the order in which input signals and feedback signals are considered. Sequential hazard which results in a glitch is transient hazard. On the other hand, if due to delays the circuit can become stable with incorrect values of internal or even output signals, we have steady-state hazard. Both types of sequential hazards are an inherent property of sequential functions and not of the particular circuit implementation. Sequential hazards appear despite of fundamental and burst mode constraints. Figure 3 shows circuits containing different types of hazards and their simulation runs. Signals f , y 1, and y 2 represent the behaviour of output signals without delays in the circuit, while signals fd, y 1d, and y 2d represent their behaviour after introducing signi?cant delays. Figures 3(a) and 3(b) show logic hazards. The static hazard in Figure 3(a) is obtained by using delayed inverters. The dynamic hazard in Figure 3(b) appears when the left AND gate is delayed and the top inventer is even more delayed. Figure 3(c) represents a transient hazard which appears if the AND gate gets the new value from the feedback line earlier than the new input value. The circuit in Figure 3(d) has steady-state hazard because after changing input x, the circuit without delays produces outputs y 1 = 0, y 2 = 1, whereas using a delayed inverter, it produces outputs y 1d = 1, y 2d = 1. 3

    3 Representing circuits with processes
    Process algebrae are widely used formalisms for modelling and veri?cation of concurrent systems, e.g. communication protocols. In a process algebra, a system is described as a set of communicating processes. Among others, well known process algebrae are CCS (Calculus of Communicating Systems) introduced by R. Milner in 1980 and CSP (Communicating Sequential Processes) introduced by C. A. R. Hoare in 1985. We will use an algebraic approach which is similar to CCS and has some notation from CSP. In our approach, processes are labelled directed graphs. Graph nodes are called states. An edge from state p to state q labelled with action is called an -transition or shortly a transition from state p to state q . If there exists an transition from a given state, we say that in this state the process can perform -transition or that it can perform action . The set of all actions which a process can perform is called the alphabet of the process. A sequence of transitions in the process is called a path. The alphabet of a process always includes a special action , which is used to model internal communications, not visible to an external observer. A transition with action is called silent transition. All actions others than are called visible actions. Visible actions are divided into input and output actions. The name of an output

    action always terminates by ’!’, e.g. a!; b!; ::: The name of an input action always terminates by ’?’, e.g. a?; b?; ::: Two actions whose names differ only in the last sign, e.g. a? and a!, are called complementary actions. An action complementary to the given action is denoted by . A sequence of visible actions is called a trace. Two states p and q have equivalent traces if from them the same traces can be performed. Processes are trace-equivalent if their initial states have equivalent traces. A state without outgoing transitions is a deadlock state. If there exists a sequence of transitions from the initial state of a process to a state p, then state p is reachable in this process. Otherwise, the state is unreachable in this process. Other important concepts in process algebrae are strong equivalence, observational equivalence, and determinacy of processes [16]. Processes are used to represent external behaviour of circuits. Each transition in the process represents a change of a signal value and we do not distinguish whether the value changes from 0 to 1 or vice versa. A transition with an input action represents change of an input signal value, caused by the environment. A transition with an output action represents change of an output signal value, caused by the circuit. We will use interleaving semantics, i.e. a simultaneous occurence of two or more signal changes will be modeled by including multiple sequences of transitions, one for each permutation of changing signals. The process represents an external behaviour of the circuit if each of its traces starting in the initial state of the process corresponds to a possible sequence of changes of input and output signal values during the operation of the circuit in the given environment considering given initial values of all input and output signals. We are not interested in exact timing when the value of signals changes. If two circuits have the same possible sequences of changes, they have the same external behaviour, although one of them is much faster than other. Therefore, two processes represent equal external behaviour iff they are trace-equivalent. However, delays are important because different sequences of changes can be possible in the same asynchronous circuit if the delay of gates changes. Some traces in the process may correspond to sequences of changes possible only with particular arrangements of gate delays and not all of them. Note that we do not require ?xed delays. Gate delays can change during the operation of the circuit. Because each action represents just a change of signal value, we cannot uniformly associate a circuit to the given process without knowing the initial value of all input and output signals. Namely, to determine whether performing a particular transition represents a rising or falling edge, one must know the initial value of that signal and follow its changes. With regard to the level of abstraction, the process can represent more or less details on the circuit’s internal behaviour and its connections with the enviroment. For the purpose of ?nding hazards and veri?cation of asynchronous circuits under the fundamental mode of operation, we introduce a special form of processes called circuit models. A circuit model is determinate process without unreachable states and without silent transitions. All circuit models representing external behaviour of the same circuit in the same 4

    environment and with the same initial values of input and output signals are strongly equivalent. Among them, the one with minimal number of states will be identi?ed and used for veri?cation. Circuit models in Figure 4 represent external behaviour of an AND gate, the C element, and the FORK element, respectively. Further, they will be used to build DME cells. The AND gate and the C element have two input signals (actions a? and b?) and one output signal (action c!). The FORK element is a frequently used gate in asynchronous circuits. It has one input signal (action a?) and two output signals (actions b! and c!). The value of both outputs changes simultaneously after the change of the input value. Simultaneous change of two outputs is modelled by the ability of performing corresponding output actions in both orders. The presented circuit models describe external behaviour of gates under the fundamental mode of operation with all input and output signals initially set to 0.

    c! b?

    a?

    a? c!

    b? b? c! a? a?

    b?

    (a)

    a? a? b? c!

    b?

    b?

    a?

    (b)

    c! b! a? c! b!
    (c)

    Figure 4: Circuit model of (a) two-input AND gate, (b) the C-element, and (c) the FORK element

    q! s? qn!

    qn! q!
    g2! g1! r1? g1! r2? r1? r2? r1?

    r?

    r?

    s? qn! q!

    STOP q!

    r?

    s?

    s?

    r2? g2!

    r2?

    r? qn!

    r1?

    r1? r2?

    g2!

    g1!

    (a)

    (b)

    g2! z? g2! r2? r2? r2? r2? g2! r1? r1? g2! z? z? z? z? r2? g2! r1? r1? r2? g2! g1! r2? r1? z? z? z? g1! g1! z? r1? r1? r1? r2? r2? r1?

    g1!

    g1!

    r1? r1? r2? r2? z? r1? g1! r2? r2? r1? z? z? z?

    (c)

    Figure 5: Circuit model of (a) RS ?ip-?op, (b) ME element, and (c) ME element with inhibit signal. DME circuits contain some more complex gates, too. The circuit model in Figure 5(a) describes external behaviour of RS ?ip-?op with two inputs denoted by s (set) and r (reset) and two outputs denoted by q and qn, where qn is inverted q. Initially, s, r, and q are equal to 0. When input signal s is set to 1, output q becomes 1. When input signal r is set to 1, then output q becomes 0. Inputs r and s must never be set to 1 at the same time. The circuit model contains a deadlock state, which is not reached if the RS ?ip-?op is properly driven by its environment. Mutual exclusion (ME) element is a non-deterministic element used in asynchronous circuits as an arbiter. Two different versions of ME elements appear in DME circuits. In the ?rst one, the ME element has two inputs denoted by r1 and r2 and two outputs denoted by g 1 and g 2. If input signal r1 is set to 1 and output g 2 is not set to 1, then output g1 becomes 1. When input signal r2 is set to 1 and output g 1 is not set to 1, then output g 2 becomes 1. If inputs r1 and r2 are simultaneously set to 1, then the ME element non-deterministically chooses one output and sets it to 1. In another version, the ME element has an additional input z 5 intended for an inhibit signal, which prevents the grant to new requests until the request that caused the previous grant is removed. The circuit models we used to describe external behaviour of the ME element without and with inhibit signal, where all input and output signals are initially equal to 0, are presented in Figures 5(b) and 5(c), respectively.

    4 Veri?cation of asynchronous circuits
    The veri?cation of an asynchronous circuit starts by representing all necessary gates with circuit models. Then, they are composed together using parallel composition with multi-way synchronisation [8, 20]. The compound process represents external behaviour of the circuit. The behaviour of gates in the circuit is asynchronous, but they are not completely independent. Complementary actions in different circuit models must be performed simultaneously as the value of a signal cannot change only in one part of a wire. Simultaneous performance of complementary actions is called synchronisation between circuit models. During

    the composition, two types of transitions with visible actions are distinguished. The transitions used for synchronisation with the system’s environment are external transitions, whereas the transitions serving for synchronisation between processes in the system are internal transitions. The parallel composition of circuit models will not return a meaningful result if: signals do not have unique names, the outputs of two or more gates are connected together, there exists a gate directly driving itself, an output signal observable by the environment is used as a feedback signal into the circuit. The ?rst two situations are straighforward. A gate is not allowed to drive itself because it is expected that at least two different circuit models cooperate in synchronisation. An output signal observable from the environment is not allowed to be a feedback signal into the circuit because the same visible action cannot be used in internal and external transitions. The last two requirements have an impact on the preciseness of the veri?cation. For example, circuits in Fig. 3(c) and Fig. 3(d) cannot be veri?ed in their original form without adding FORK elements after the OR gates which produce signals y 1 and y 2. The next veri?cation step is a transformation of the obtained compound process into a circuit model which represents the external behaviour of the assembled circuit under the fundamental mode of operation. This transformation consists of two steps, removal of redundant traces and determinization of the process. We call the ?rst operation fundamental-mode reduction and it removes: all transitions with an input action from states where a silent transition can be performed, all transitions with an input action from states where a transition with an output action can be performed. all silent transitions from states where a transition with an output action can be performed. An example of the circuit model obtained by composing circuit models of individual gates is presented in Figure 6. It is a circuit model which represents the external behaviour of the circuit with oscilating output under the fundamental mode of operation. In the initial state, it can perform input action x?. After changing input x, output f begins to oscilate. Afterwards, the circuit cannot change the value of input signal again because it never becomes stable. One of the goals of our approach was hazard detection. It can be done by ?nding particular patterns in the circuit models which represent unwanted external behaviour. This patterns are simpler for the circuits containing only one output signal. Therefore, in the case of a circuit with many outputs we made the veri?cation separately for each output. A hazard resulting in a glitch is present in the circuit if in its circuit model, after performing an output action, the same output action can be performed again before any input action is performed. Hence, most hazards can be easily detected by looking for such sequences of transitions, although in this 6

    x?

    f!

    Figure 6: Circuit model of the circuit with oscilat. output way they cannot be classi?ed into logic, functional and transient hazards. However, static and dynamic hazards can be distinguished, as a static hazard results in an output action successively repeated an even number of times, whereas in the case of a dynamic hazard, the output action is repeated an odd number of times. It is more complicated to detect steady-state hazards. A steady-state hazard is present in the circuit if after a particular sequence of input signals with some arrangements of delays an output signal appears, but with other arrangements of delays it does not. This always results in a state in the circuit model where both input and output actions can be performed. However, not all such states are a consequence of steady-state hazards: it can also indicate a glitch which appears with some arrangements of delays, but not with all of them, if some actions representing output signals have been abstracted from the model, then it can also indicate a non-deterministic behaviour of the circuit, which in particular situations produces the retained output signal and sometimes the abstracted one. Glitches which appear only with some arrangements of delays and not with all of them are avoidable by engineering delays. We will call them avoidable hazards. Not all hazards are avoidable (i.e. they are unavoidable) because delays can be set only to gates and not to wires. An example of avoidable and unavoidable static logic hazard is shown in Figure 7. An example of a circuit with non-deterministic behaviour is the ME element with inhibit signal in Figure 5(c). Circuit models in Figure 8 represent the external behaviour of circuits with hazards. They were obtained by composing circuits in Figure 3. The circuit model in Figure 8(a) shows that in the circuit in Figure 3(a), if the value of a and b is initially assumed to be 0, after changing any of them, output f may change two times consecutively. This represents a static hazard. Afterwards, if the same input is changed again, another static hazard may appear. All hazards in this circuit are avoidable. The circuit model in Figure 8(b) shows that in the circuit in Figure 3(b), if a and b have initial value 0 and the value of a changes, no hazards will occur. However, the situation is quite different after b is changed to 1. Then, each change of a may be followed by three consecutive changes of output f , which is a dynamic hazard. This hazard is avoidable, too. The circuit model in Figure 8(c) indicates a transient hazard in the circuit in Figure 3(c). If x is initially assumed to be 0 and then changes to 1, a static hazard may appear on ouput y 1. The hazard is avoidable and it is possible only after the ?rst change of x. The circuit models in Figure 8(d), 8(e), and 8(f) represent the behaviour of the circuit in Figure 3(d). The initial value of all signals is assumed to be 0. After x changes to 1, the

    a? f! f!

    a?

    a? f! f!

    a?

    (a)

    (b)

    Figure 7: A circuit with (a) avoidable and (b) unavoidable static logic hazard
    a? a? f! a? f! b? b? b? b? f! f! a? a? a? b? b? a? f! b? f!

    (a)

    f! a?
    x?

    b?

    b? a?

    b? f! a? f! f!
    y1! x?
    (b) (c)

    x?

    y1!

    x? x? x? y2! y1! y1! x? x?

    x?

    x? y2! x?

    (d)

    (e)

    (f)

    Figure 8: External behaviour of the circuits in Figure 3

    7

    value of y 1 with some arrangements of delays changes and with some arrangements it does not. In both cases, further changes of x do not affect y 1 anymore. There are no hazards on line y 2. Figure 8(d) shows the circuit model containing both output signals, while in the other two circuit models one output signal is abstracted away.

    are valid only if the state is a '-state. Formulae EX f g ', AX f g ', EF f g ', AF f g ', E ' f g U f 0 g '0 ], and A ' f g U f 0 g '0 ] are invalid in all deadlock states. We will take that an ACTL formula is valid in process P iff it is valid in its initial state. In ACTL formulae, the constant true can be omitted in many cases, for example: E true f g U f 0 g '0 ] A ' ftrueg U ftrueg '0 ]
    = =

    5 ACTL model checking
    In Section 4 we detected hazards in asynchronous circuits by looking for particular patterns in the circuit models. This step of veri?cation can be effectively done by model checking, which is a powerful technique for checking properties of processes. It is also used for veri?cation of liveness and safety properties of asynchronous circuits. We will specify circuit properties with action computation tree logic (ACTL), which is a propositional branching time temporal logic [6, 14]. The syntax of ACTL formulae includes constants true and false, standard Boolean operators NOT; AND; OR, path quanti?ers E (“there exists a path”) and A (“for all paths”), and temporal operators U (“until”), W (“unless”), X (“for the next transition”), F (“for some transition in the future”), and G (“for all transitions in the future”). ACTL formulae are state formulae. A state where ACTL formula ' is valid will be called '-state. ACTL formulae are constructed from action and path formulae. An action for which action formula is valid will be called -action. A transition from state p to state q where action formula is valid for the action executed during this transition and ACTL formula ' is valid in state q will be called ( ; ')-transition. In a process, path formulae are evaluated as follows: Path formula Xf g ' is valid on path iff the ?rst transition on this path is a ( ; ')-transition. Path formula Ff g ' is valid on path a ( ; ')-transition on this path. iff there exists

    E f g U f 0 g '0 ] A ' U '0 ]

    There are also two widely accepted abbreviations of ACTL operators:

    < >' ]'

    = =

    EXf g ' :EXf g :'

    ACTL formula < > ' is valid in the given state iff there exists a transition with action from that state to a state where ACTL formula ' is valid. ACTL formula ]' is valid in the given state iff all transitions with action from that state lead to a state where ACTL formula ' is valid. Suppose that the alphabet of the process contains actions a?, b?, and f !. Here are some ACTL formulae which can be used for checking properties of this process: There is no deadlock state: AG AF ftrueg At any moment, ouput action the future: AG AF ff !g

    f ! will be performed in f!
    can be per-

    There is no state where output action formed succesively two times: NOT EF ff !g <f ! > true

    There is no state where output action f ! and also input action a? or b? can be performed: NOT EF ((<f ! > true) AND (<a? OR b? > true))

    Path formula G 'f g is valid on path iff ACTL formula ' is valid in the ?rst state of this path and all transitions on the path are ( ; ')-transitions. Path formula ' f g U f 0 g '0 ] is valid on path iff ACTL formula ' is valid in the ?rst state of this path and the path begins with a ?nite sequence of ( ; ')transitions followed by a ( 0 ; '0 )-transition. Path formula ' f g W f 0 g '0 ] is valid on path iff formula 'f gUf 0 g'0 ] is valid on this path or formula G 'f g is valid on this path. The given rules are used for ?nite and in?nite paths. In ACTL, each path formula is always immediately preceded by a path quanti?er. Path quanti?er E requires that the property expressed by the path formula is valid for at least one path starting in the given state. On the other hand, path quanti?er A requires that the property expressed by the path formula is valid for all paths starting in the given state. In a deadlock state, formulae EG 'f g, AG 'f g, E ' f g W f 0 g '0 ], and A ' f g W f 0 g '0 ] 8

    6 Results from veri?cation of DME circuits
    We veri?ed distributed mutual-exclusion (DME) circuits. They are composed of DME cells connected in a ring. DME cells work by passing a token around the ring. The ownership of the token is determined by output signal q of the RS ?ip-?op. The token is exchanged via the request and acknowledge signals with the left cell (LR and LA) and with the right cell (RR and RA). The users gain exclusive access to the resource via the request and acknowledge signals UR and UA. The DME circuit was originally proposed by Martin in 1985 [11]. Martin’s design does not work correctly under the input/output mode of operation [10]. In 1988, Burns gave a simpler design of the DME cell [3]. It was later slightly modi?ed by McMillan and became a standard benchmark for asynchronous design veri?cation tools [12, 13, 18]. The DME cells from Martin and McMillan are presented in Figure 9. In Martin’s design, the token indicates which user has last accessed the shared resource. If a DME cell receives a request but does not have the token, it notices this to its right

    UA
    I8 I3

    I7

    C

    S S Q R QN QN I1 I4 Q

    Y1

    UR
    INH

    R1

    G1

    U QI L I6 QO

    RR

    z

    ME

    LR

    R2

    G2

    RA
    R

    I2

    I5 I10 I9

    LA

    C

    (a)

    UA
    P E

    R

    S Q M

    R QN N

    Q

    C UR
    R1 A K C H G D I H J

    RR

    G1

    ME LR
    R2 G2 B

    C
    L

    RA C

    LA

    O

    F

    (b)

    Figure 9: A cell of the DME circuit (a) as proposed by Martin [11], and (b) as proposed by McMillan [12] neighbour via the RR signal. When a DME cell gets a request, either from the user via the UR signal or from its left neighbour via the LR signal, the DME cell attempts to satisfy the demand. If a DME cell has the token and no granted request is outstanding, then it sends an acknowledgement, either via the UA or LA signal, as appropriate. When a DME cell establishes it can approve user access, it immediately sends the UA signal to the user. If this DME cell does not have the token, then the token is transferred to it after the user removes the request. In McMillan’s design, a user request is never acknowledged by a DME cell which does not possess the token. The token is transferred ?rst, which makes the response to a user request slower. Moreover, McMillan’s design has slower response times regardless of the token position because there the request signal has a longer path through the decision logic. 9 The veri?cation was done with Ef?cient Symbolic Tools (EST), our BDD-based tool for symbolic veri?cation of concurrent systems [15]. We started by modelling all necessary gates and composing them in DME cells. Afterwards, possible hazards in each DME cell were examined. Finally, we composed DME cells into rings of different sizes and checked correctness of external behaviour of the obtained circuits. To con?rm the results of formal veri?cation we also implemented the circuits on the prototype board (Figure 10) and tested their behaviour by measurements with HP 1652B Logic Analyzer. In Figure 10(b), the reader may notice that some logic for initialisation of the RS ?ip-?ops was added for testing. The test runs obtained for the ring composed of two DME cells are given in Figure 11. Signals UR, UA, Q, RR, LA, Z, S, R, G1, and G2 belong to the ?rst DME cell, while others belong to the second one.

    (a)

    (b)

    Figure 10: The ring of two Martin’s DME cells: (a) implementation with gates and wires, (b) LED indicators for testing

    (a)

    (b)

    Figure 11: Test run of the ring composed of (a) two Martin’s DME cells, (b) two McMillan’s DME cells 10

    In the circuit model of DME cell, input signal changes were represented with actions ur?, lr?, and ra?, and output signal changes were represented with actions ua!, la!, and rr!. We created 3 different circuit models for each DME cell. Each circuit model represents the behaviour of one output signal, whereas the other two are abstracted away. This makes the veri?cation simpler. To ?nd hazards, we used the following ACTL formulae, which are for simplicity here presented using macros, although EST does not support them yet:
    \define IN (ur? OR lr? OR ra?) \define OUT (ua! OR la! OR rr!) # Static hazards NOT EF {IN} <OUT> <OUT> <IN> true # Dynamic hazards NOT EF {IN} <OUT> <OUT> <OUT> <IN> true # Steady-state hazards NOT EF {IN} ((<IN> true) AND (<OUT> <IN> true))

    In McMillan’s DME cell, which initially does not possess the token, we found only static hazards on output signal RR:
    1. 2. 3. 4. ra?,ur?,rr!,rr! ra?,lr?,rr!,rr! ur?,rr!,lr?,ur?,rr!,rr! lr?,rr!,ur?,lr?,rr!,rr!

    Due to the separate veri?cation for each output signal, counterexamples do not describe the behaviour of all output signals, which can be a drawback. A test run corresponding to the hazard no. 3 in McMillan’s DME cell is given in Figure 12. Initially, all input and ouput signals are set to 0 and the DME cell does not possess the token. When the DME cell gets a user request, it immediately sends signal RR to its right neighbour. Afterwards, if LR and UR change before other signals, we get static hazard on signal RR.

    For any formula which is invalid for a given model, EST shows a counterexample. To ?nd all hazards on the particular output signal effectively, model checker should ?nd all counterexamples (e.g. tree-like counterexamples [9]). Unfortunately, EST is not capable of that, and therefore we helped us with an iteration method. For each hazard found, we deleted outgoing transitions from the state where the hazard began and then checked the same ACTL formula again. We repeated this until the formula became valid. With the presented formulae only hazards containing two or three successive changes of an output signal can be detected, but we also veri?ed that the model contains no other hazards. In Martin’s DME cell, which initially does not possess the token, we found static hazards on output signals UA (1-4) and RR (5-8) and steady-state hazards on output signals UA (9), LA (10-11), and RR (12-20):
    1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13. 14. 15. 16. 17. 18. 19. 20. ra?,ur?,ua!,ra?,ua!,ua! ra?,ur?,ua!,lr?,ra?,ua!,ua! ra?,ur?,ua!,ur?,ur?,ra?,ua!,ua! ra?,ur?,ua!,ur?,ur?,lr?,ra?,ua!,ua! ur?,rr!,lr?,ur?,rr!,rr! lr?,rr!,ur?,lr?,rr!,rr! ra?,lr?,rr!,ur?,lr?,rr!,lr?,ra?,rr!,ur?,rr!,rr! ra?,lr?,rr!,ur?,lr?,rr!,lr?,ra?,rr!,lr?,rr!,rr! ra?,lr?,ur?,lr?,lr?,ra?,ra?,[ua!] ra?,ur?,ur?,ur?,lr?,ra?,[la!] ra?,lr?,la!,ur?,lr?,lr?,ra?,la!,ra?,[la!] ra?,ur?,rr!,ur?,rr!,ur?,lr?,ra?,lr?,[rr!] ra?,lr?,rr!,ur?,lr?,rr!,lr?,ra?,rr!,ra?,ra?,[rr!] ra?,lr?,rr!,ur?,lr?,rr!,lr?,ra?,rr!,ra?,ur?,[rr!] ra?,lr?,rr!,ur?,lr?,rr!,lr?,ra?,rr!,ra?,lr?,[rr!] ra?,ur?,rr!,ur?,rr!,ur?,lr?,ra?,ra?,lr?,lr?,ra?,[rr!] ra?,ur?,rr!,ur?,rr!,ur?,lr?,ra?,ra?,ur?,lr?,ra?,lr?,[r r!] ra?,ur?,rr!,ur?,rr!,ur?,lr?,ra?,ra?,ur?,ur?,lr?,lr?,ra? ,[rr!] ra?,ur?,rr!,ur?,rr!,ur?,lr?,ra?,ra?,ur?,lr?,ra?,ra?,ur? ,[rr!] ra?,ur?,rr!,ur?,rr!,ur?,lr?,ra?,ra?,ur?,lr?,ra?,ra?,lr ?,[rr!]

    Figure 12: Hazard on signal RR in McMillan’s DME cell The results of the veri?cation show that both designs of DME cell contain hazards even under the fundamental mode of operation. However, McMillan’s design is much cleaner. Table 1 gives the number of hazards found. Note that we distinguish two hazards only if they occur in different situation in the circuit. A DME cell can ?rst acquire the token and then deliver it forward, and afterwards it is found in the same situation as in the beginning. Moreover, static hazard in Martin’s DME cell described with the sequence ur?,ra?,ua!,ra?,ua!,ua! is treated to be the same as the ?rst one in the given list because the situation in the circuit is the same regardless of the order in which the value of input signals ur? and ra? changes. Table 1: Hazards in DME cells Martin [11]
    UA LA RR

    McMillan [12]
    UA LA RR

    Static hazards Dynamic hazards Steady-state hazards

    4 0 1

    0 0 2

    4 0 9

    0 0 0

    0 0 0

    4 0 0

    11

    In the next step of the veri?cation we checked, whether the DME circuits of different sizes satisfy safety and liveness properties proposed in [13]: 1. An acknowledgement is not given without a request. 2. An acknowledgement is not removed while a request persists. 3. All requests are eventually acknowledged. 4. No two users are acknowledged simultaneously. After composing DME cells, only signals UR and UA from and, respectively, to different users remain in the model. They were represented with actions ur1?, ua1!, ur2?, ua2!, etc. Because in a circuit model the same action represents either the change of signal value from 0 to 1 or vice versa, the ?rst two properties can be veri?ed with the same ACTL formulae. On the other hand, the last and the most important property cannot be directly expressed with one ACTL formula. We can only express mutual exclusion after a user gets the acknowledgement for a given number of times. Here are the formulae used for veri?cation of the DME circuit composed of two DME cells:
    # After an acknowledgement is sent # (removed), it will not be removed # (sent) before the user requests this. AG [ua1!] A[{NOT ua1!} UU {ur1?}] AG [ua2!] A[{NOT ua2!} UU {ur2?}] # All requests will be acknowledged.

    The size of circuit models used during the veri?cation is given in Table 2. The most complex task during the veri?cation was the composition of processes. Table 3 and Table 4 give some statistics about the complexity of parallel composition obtained on a system composed of 800 MHz Athlon processor, 512 MB RAM and Linux OS. The size of DME cells in Table 2 refers to the circuit model describing external behaviour of DME cells which initially do not possess the token. The sizes reported in the last two tables refer to the circuit model describing external behaviour of rings where internal behaviour of DME cells is abstracted away. We were not able to compose more than 4 Martin’s and 5 McMillan’s DME cells although the resulting process is supposed not to be enormous. Hence, an “on the ?y” model checker would be of great interest here. Table 2: The size of circuit models
    Circuit Inputs / Outputs States / Transitions BDD nodes

    C element RS ?ip-?op ME element [11] ME element [12] DME cell [11] DME cell [12]

    2/1 2/2 3/2 2/2 3/3 3/3

    4/7 11/16 24/51 11/16 72/148 48/104

    32 75 164 73 474 304

    AG [ur1?] AF {ua1!} AG [ur2?] AF {ua2!}

    Table 3: Parallel composition of Martin’s DME cells
    # # # # # After a user gets the acknowledgement for the first time (second time etc.), other users will not get an acknowledgement until his acknowledgement is removed. Circuit States / Transitions BDD nodes Time for composition

    2 DME cells 3 DME cells 4 DME cells

    11/16 57/117 236/632

    62 365 1752

    0.1s 2.4s 100.2s

    \define UA1 {NOT ua1!} UU {ua1!} \define UA2 {NOT ua2!} UU {ua2!} A[UA1 A[{NOT ua2!} UU {ua1!}]] A[UA2 A[{NOT ua1!} UU {ua2!}]] A[UA1 A[UA1 A[UA1 A[{NOT ua2!} UU {ua1!}]]]] A[UA2 A[UA2 A[UA2 A[{NOT ua1!} UU {ua2!}]]]]

    Table 4: Parallel composition of McMillan’s DME cells
    Circuit States / Transitions BDD nodes Time for composition

    All listed formulae were valid for the circuit composed of two Martin’s DME cell and also for the circuit composed of two McMillan’s DME cell. Afterwards, we veri?ed DME circuits composed of three and more DME cells, too. To do this, ACTL formulae must have been adequately adapted. Because no incorrect behaviour was detected, we may conclude that both designs of DME cell operate correctly under the fundamental mode of operation. Evidently, with the presented approach, we were not able to detect malfunction of DME circuits composed of Martin’s cells because it is the result of delay hazards. 12

    2 DME cells 3 DME cells 4 DME cells 5 DME cells

    11/16 40/72 145/316 596/1545

    66 251 974 4444

    0.1s 0.8s 12.9s 1299.1s

    7 Conclusion
    Asychronous circuits are an important class of digital circuits used as autonomous devices or just a part of otherwise synchronous circuits. They have many nice properties, but they are also dif?cult to design and verify, especially in an ad hoc fashion. Emerging tools for formal veri?cation promise a solution for many problems in this area. This paper introduces a method for formal veri?cation of asychronous circuits modelled with Muller’s model under the fundamental mode of operation. It is suitable for detecting hazards in the given circuit and for veri?cation of safety and liveness properties. The method is based on the representation of external behaviour of the circuit with processes. A special form of processes called circuit models is used to describe gates. A parallel composition with the ability of multi-way synchronisation and an operation called fundamental-mode reduction serve for construction of circuits from single gates. Determinization of processes assures a canonical form of speci?cations. The properties of circuits can be checked by ACTL model checking. The results obtained by veri?cation and measurements on real circuits convince us about the correctness of our approach. We used presented method for the veri?cation of DME circuits. We were able to verify the external behaviour of DME circuits composed of up to 5 DME cells. For larger circuits, BDD-based tool EST exceeded memory limits of 512 MB during the parallel composition of circuit models. Maybe, the impact of state explosion could be moderated by using “on the ?y” model checking. Alternatively, parallel composition and fundamental-mode reduction could be united in a more ef?cient operation. There are many topics for further research. The ability of model checking to ?nd tree-like counterexamples was mentioned in the paper. We are also interested in experiments with input-quasi-receptive circuit models, which describe the behaviour of the circuit under input/output mode of operation. They enable checking semi-modularity. Input-quasireceptive models accept input signals in all states and this leads to more complex speci?cations. It is a challenge how to apply such an approach to larger asynchronous circuits.

    [5] A. Davis and S. M. Nowick. An Introduction to Asynchronous Circuit Design. Technical Report UUCS-97013, University of Utah, September 1997. [6] A. Fantechi, S. Gnesi, F. Mazzanti, R. Pugliese, and E. Tronci. A Symbolic Model Checker for ACTL. In Proceedings of FM-Trends’98, volume 1641 of LNCS, pages 228–242. Springer-Verlag, October 1998. [7] S. Hauck. Asynchronous Design Methodologies: An Overview. Proceedings of the IEEE, 83(1):69–93, January 1995. [8] J. He. Formal Speci?cation and Analysis of Digital Hardware Circuits in LOTOS, August 2000. Technical Report CSM-158. University of Stirling. [9] Y. Lu. Automatic Abstraction in Model Checking. PhD thesis, Department of Electrical and Computer Engineering, Carnegie Mellon University, 2000. [10] A. R. Martello. Temporal Analysis for Time-Bounded Causal Digital Systems. PhD thesis, University of Pittsburgh, April 1993. [11] A. J. Martin. The Design of a Self-timed Circuit for Distributed Mutual Exclusion. In Proceedings of the 1985 Chapel Hill Conference on VLSI, pages 245–260, 1985. [12] K. L. McMillan. Symbolic Model Checking. PhD thesis, Carnegie Mellon University, May 1992. Technical report CMU-CS-92-131. [13] K. L. McMillan. The SMV system, November 2000. //www-2.cs.cmu.edu/ modelcheck/smv.html. [14] R. Meolic. Checking correctness of concurrent systems behaviour. Master’s thesis, University of Maribor, 1999. In Slovene. [15] R. Meolic, T. Kapus, and Z. Brezoˇ nik. The Ef?cient c Symbolic Tools Package. In Proceedings of the SoftCOM 2000, volume I, pages 147–156, Split, Croatia, October 2000. //www.el.feri.uni-mb.si/est/. [16] R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice Hall, 1989. [17] C. Myers. Asynchronous Circuit Design. John Wiley & Sons, 2001. [18] O. Roig, J. Cortadella, and E. Pastor. Conservative Symbolic Model-Checking of Petri Nets for Speedindependent Circuit Veri?cation, 1994. DAC/UPC Technical Report No. RR-94. [19] M. Shams, J. C. Ebergen, and M. I. Elmasry. Asynchronous Circuits. John Wiley’s Encyclopedia of Electrical Engineering. [20] K. S. Stevens. Practical Veri?cation and Synthesis of Low Latency Asynchronous Systems. PhD thesis, Dept. of Computer Science, University of Calgary, Canada, September 1994.

    References
    [1] ACiD-WG. Report on Design, Automation and Test for Asynchronous Circuits and Systems, January 2002. [2] A. Bailey. Automatic Veri?cation of Speed-Independent Circuit Designs Using the Circal System. In Correct Hardware Design and Veri?cation Methods (CHARME ’93), volume 683 of LNCS, pages 167–178. Springer-Verlag, May 1993. [3] S. M. Burns. Automated Compilation of Concurrent Programs into Self-timed Circuits. Master’s thesis, California Institute of Technology, 1988. [4] F.-C. Cheng. Exact Essential-Hazard-Free State Minimization of Incompletely Speci?ed Asynchronous Sequential Machines. Technical report CUCS-033-94. 13


    推荐相关:

    ...VERIFICATION OF DISTRIBUTED MUTUAL-EXCLUSION CIR....pdf

    FORMAL VERIFICATION OF DISTRIBUTED MUTUAL-EXCLUSION CIRCUITS_专业资料。Abstract: Distributed mutual-exclusion (DME) circuits are an interesting example of ...

    一个分布式K互斥算法的概率模型检测.pdf

    ofthedistributedK-mutualexclu-sionalgorithms.Thispaperresolvedtheproblem,andgavemorestudy.ItproposedaformalverificationandanalysismethodfordistributedK-mutualexclusion...

    A distributed K-mutual exclusion algorithm_图文.pdf

    A Distributed K-Mutual Exclusion Algorithm Shailaja Bulgannawar Nitin H. Vaidya Department of Computer Science Texas A&M University College Station, TX ...

    ...Protocols for Distributed (k + 1)-Exclusion_图文.pdf

    Here also, instead of the traditional database system that uses distributed mutual exclusion to ensure one update to the replicated data at any time, ...

    A Survey of Mutual-Exclusion Algorithms for Multipr....pdf

    A Survey of Mutual-Exclusion Algorithms for ...1 When discussing distributed and concurrent ...Only through formal proof techniques can we be ...

    Towards formal verification of UML diagrams based o....pdf

    Towards formal verification of UML diagrams based on graph transformation_专业...in particular when they are used to describe complex, distributed systems. ...

    ...a formal verification of a secure distributed sy....pdf

    TOWARDS A FORMAL VERIFICATION OF A SECURE AND DISTRIBUTED SYSTEM AND ITS APPLICATIONS1 Cui Zhang, Rob Shaw, Mark R. Heckman, Gregory D. Benson, Myla ...

    Taxonomy of Distributed Mutual Exclusion Algorithms.pdf

    Taxonomy of Distributed Mutual Exclusion Algorithms_专业资料。Mobile computing ...FORMAL VERIFICATION... 暂无评价 13页 免费 A taxonomy and survey ... ...

    Formal verification of programs that use MPI one-si....pdf

    an existing distributed byte-range locking protocol [12] and its formal ...of even simple concurrent protocols such as Peterson’s mutual exclusion. The...

    ...of Quorum-Based Protocols for Distributed (k + 1....pdf

    Abbadi, “Analysis of Quorum-Based Protocols for Distributed (k + 1)-...The majority quorum algorithm 20, 7] for distributed mutual exclusion has ...

    Extending Distributed Mutual Exclusion Algorithms t....pdf

    We are interested in the class of token-based distributed mutual exclusion algorithms. We selected ?ve algorithms from this class, sharing the following ...

    Verification of Peterson's Algorithm for Leader Ele....pdf

    Keywords: SMV, Formal Verification, Model Checking, Distributed Systems, ...formal verification of the mutual exclusion algorithms [10], [16], [17]....

    ...Diagrams for Verification of Large Circuits.pdf

    Distributed Binary Decision Diagrams for Verification of Large Circuits_专业资料...Formal Techniques for Veri cation of Synchronous Sequential Circuits. PhD ...

    ...evaluation of distributed mutual exclusion algor....pdf

    Empirical evaluation of distributed mutual exclusion algorithms_专业资料。In this paper, we evaluated various distributed mutual exclusion algorithms on the IBM ...

    A distributed K-mutual exclusion algorithm.pdf

    This structure is used to forward token requests. The algorithm is designed to minimize the number of messages and a A Distributed K -Mutual Exclusion ...

    ...Friedrich von Henke. Formal verification of the ....pdf

    Formal verification of a... 暂无评价 15页 免费...In ACM Symposium on Principles of Distributed ...A fast mutual exclusion algorithm. ACM Transactions...

    Formal specification using agents conceptualization.pdf

    Mathematically, it allows formal verification of safety (what a program is ...of distributed systems: safety (for example deadlock or mutual exclusion), ...

    Formal Verification of E-Services and Workflows.pdf

    Formal Verification of E-Services and Workflows_...ers, e.g., pc p mutual exclusion property are...Journal of Circuits, systems and computers, 8(1...

    Formal verification of programs that use MPI one-si....pdf

    an existing distributed byte-range locking algorithm [17] and its formal ...of even simple concurrent protocols such as Peterson’s mutual exclusion. The...

    ...algorithm for distributed mutual exclusion.pdf

    A Centralized Token-Based Algorithm for Distributed Mutual Exclusion Edward W. Felten Michael Rabinovich Department of Computer Science and Engineering University...

    江苏七位体彩开奖结果 | 江苏七位体彩开奖结果
    All rights reserved Powered by 江苏七位体彩开奖结果 江苏七位体彩开奖结果 www.jwbw.net
    copyright ©right 2010-2021。
    文档资料库内容来自网络,如有侵犯请联系客服。[email protected]
  • 喀什12个贫困村实现生活垃圾集中处置 2019-06-30
  • 起底特大网络盗刷案:数亿人的秘密因一习惯被盗卖 2019-06-30
  • 黄淳的专栏作者中国国家地理网 2019-06-12
  • 坚守传统手工包粽 探访沪上老字号粽子生产车间 2019-06-10
  • 满满的都是屏 OPPO妹子最爱手机曝光 2019-06-10
  • 北京进入旅游旺季 警察提示游客需防揽客者连环设套忽悠购物 2019-06-08
  • 我写文章不是为了别人的赞许,是为了讨论问题,让人有思考的价值,就像你网名一样,探寻真理。我并非就全盘赞成市场经济,只是在讨论它的合理性,在文中也提问,“既然我们 2019-06-08
  • 山东假存单揽储1.6亿难追回,该省另一相似案件银行被判赔 2019-05-31
  • 天上不会掉馅饼,想要富起来,就要把别人的据为己有,能把别人的据为己有的问世间能有谁,能有几人,所谓的专家明白了吗。 2019-05-31
  • 乌鲁木齐市中级人民法院庭审在线直播 2019-05-21
  • 第530期:为何吃新鲜蔬果能抗肿瘤、强免疫……?因为有“它”! 2019-05-19
  • 世界杯大中华区官方票代谈假票门黄牛倒票行为 2019-05-19
  • 英媒:漫步北京上海,仿佛踏入未来 2019-05-17
  • 2017年各地领导干部给网友书写23万封回信 2019-05-17
  • 回到1396年的波斯街头文章中国国家地理网 2019-04-23
  • 黑龙江6十开奖结果 浙江11选5任选5秘诀 红蓝球霸手机版 博彩通评级机构 t香港六合彩开奖结果 快乐十分现场摇奖 足彩胜负彩18119期推荐 哪里看天津时时彩直播开奖 利用遗漏模式选号 精准一尾中特百分百 黑龙江快乐十分前三直 赛马会官方网一波中特 排列五走势图最近1000期 彩票代理点如何赚钱 海南私彩有漏洞吗